feat(tactic/simps): use new options in library (#7095)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/data/equiv/local_equiv.lean

@@ -87,6 +87,9 @@ not_false_iff and_imp set.prod_inter_prod set.univ_prod_univ true_or or_true pro
 set.preimage_inter heq_iff_eq equiv.sigma_equiv_prod_apply equiv.sigma_equiv_prod_symm_apply
 subtype.coe_mk equiv.to_fun_as_coe equiv.inv_fun_as_coe
 
+/-- Common `@[simps]` configuration options used for manifold-related declarations. -/
+def mfld_cfg : simps_cfg := {attrs := [`simp, `mfld_simps], fully_applied := ff}
+
 namespace tactic.interactive
 
 /-- A very basic tactic to show that sets showing up in manifolds coincide or are included in
@@ -129,9 +132,9 @@ structure local_equiv (α : Type*) (β : Type*) :=
 (right_inv'  : ∀{x}, x ∈ target → to_fun (inv_fun x) = x)
 
 /-- Associating a local_equiv to an equiv-/
-def equiv.to_local_equiv (e : equiv α β) : local_equiv α β :=
-{ to_fun      := e.to_fun,
-  inv_fun     := e.inv_fun,
+def equiv.to_local_equiv (e : α ≃ β) : local_equiv α β :=
+{ to_fun      := e,
+  inv_fun     := e.symm,
   source      := univ,
   target      := univ,
   map_source' := λx hx, mem_univ _,

src/geometry/manifold/charted_space.lean

@@ -861,17 +861,17 @@ namespace open_embedding
 variable [nonempty α]
 
 /-- An open embedding of `α` into `H` induces an `H`-charted space structure on `α`.
-See `ocal_homeomorph.singleton_charted_space` -/
+See `local_homeomorph.singleton_charted_space` -/
 def singleton_charted_space {f : α → H} (h : open_embedding f) :
-  charted_space H α := (h.to_local_homeomorph f).singleton_charted_space (h.source f)
+  charted_space H α := (h.to_local_homeomorph f).singleton_charted_space (by simp)
 
 lemma singleton_charted_space_chart_at_eq {f : α → H} (h : open_embedding f) {x : α} :
   ⇑(@chart_at H _ α _ (h.singleton_charted_space) x) = f := rfl
 
 lemma singleton_has_groupoid {f : α → H} (h : open_embedding f)
   (G : structure_groupoid H) [closed_under_restriction G] :
   @has_groupoid _ _ _ _ h.singleton_charted_space G :=
-(h.to_local_homeomorph f).singleton_has_groupoid (h.source f) G
+(h.to_local_homeomorph f).singleton_has_groupoid (by simp) G
 
 end open_embedding
 

src/geometry/manifold/smooth_manifold_with_corners.lean

@@ -649,7 +649,7 @@ lemma open_embedding.singleton_smooth_manifold_with_corners
   {M : Type*} [topological_space M]
   [nonempty M] {f : M → H} (h : open_embedding f) :
   @smooth_manifold_with_corners 𝕜 _ E _ _ H _ I M _ h.singleton_charted_space :=
-(h.to_local_homeomorph f).singleton_smooth_manifold_with_corners I (h.source f)
+(h.to_local_homeomorph f).singleton_smooth_manifold_with_corners I (by simp)
 
 namespace topological_space.opens
 

src/order/order_iso_nat.lean

@@ -90,7 +90,7 @@ begin
     simp },
   { refine ⟨(nat.subtype.order_iso_of_nat s).symm ⟨x, h⟩, _⟩,
     simp only [rel_embedding.coe_trans, rel_embedding.order_embedding_of_lt_embedding_apply,
-      rel_embedding.nat_lt_apply, function.comp_app, order_embedding.coe_subtype],
+      rel_embedding.nat_lt_apply, function.comp_app, order_embedding.subtype_apply],
     rw [← subtype.order_iso_of_nat_apply, order_iso.apply_symm_apply, subtype.coe_mk] }
 end
 

src/order/rel_iso.lean

@@ -26,6 +26,8 @@ namespace rel_hom
 
 instance : has_coe_to_fun (r →r s) := ⟨λ _, α → β, λ o, o.to_fun⟩
 
+initialize_simps_projections rel_hom (to_fun → apply)
+
 theorem map_rel (f : r →r s) : ∀ {a b}, r a b → s (f a) (f b) := f.map_rel'
 
 @[simp] theorem coe_fn_mk (f : α → β) (o) :
@@ -45,16 +47,12 @@ theorem ext_iff {f g : r →r s} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ h x, h ▸ rfl, λ h, ext h⟩
 
 /-- Identity map is a relation homomorphism. -/
-@[refl] protected def id (r : α → α → Prop) : r →r r :=
-⟨id, λ a b, id⟩
+@[refl, simps] protected def id (r : α → α → Prop) : r →r r :=
+⟨λ x, x, λ a b x, x⟩
 
 /-- Composition of two relation homomorphisms is a relation homomorphism. -/
-@[trans] protected def comp (g : s →r t) (f : r →r s) : r →r t :=
-⟨g.1 ∘ f.1, λ a b h, g.2 (f.2 h)⟩
-
-@[simp] theorem id_apply (x : α) : rel_hom.id r x = x := rfl
-
-@[simp] theorem comp_apply (g : s →r t) (f : r →r s) (a : α) : (g.comp f) a = g (f a) := rfl
+@[trans, simps] protected def comp (g : s →r t) (f : r →r s) : r →r t :=
+⟨λ x, g (f x), λ a b h, g.2 (f.2 h)⟩
 
 /-- A relation homomorphism is also a relation homomorphism between dual relations. -/
 protected def swap (f : r →r s) : swap r →r swap s :=
@@ -157,6 +155,12 @@ instance : has_coe (r ↪r s) (r →r s) := ⟨to_rel_hom⟩
 -- see Note [function coercion]
 instance : has_coe_to_fun (r ↪r s) := ⟨λ _, α → β, λ o, o.to_embedding⟩
 
+/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
+  because it is a composition of multiple projections. -/
+def simps.apply (h : r ↪r s) : α → β := h
+
+initialize_simps_projections rel_embedding (to_embedding_to_fun → apply, -to_embedding)
+
 @[simp] lemma to_rel_hom_eq_coe (f : r ↪r s) : f.to_rel_hom = f := rfl
 
 @[simp] lemma coe_coe_fn (f : r ↪r s) : ((f : r →r s) : α → β) = f := rfl
@@ -182,7 +186,7 @@ theorem ext_iff {f g : r ↪r s} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ h x, h ▸ rfl, λ h, ext h⟩
 
 /-- Identity map is a relation embedding. -/
-@[refl] protected def refl (r : α → α → Prop) : r ↪r r :=
+@[refl, simps] protected def refl (r : α → α → Prop) : r ↪r r :=
 ⟨embedding.refl _, λ a b, iff.rfl⟩
 
 /-- Composition of two relation embeddings is a relation embedding. -/
@@ -191,11 +195,9 @@ theorem ext_iff {f g : r ↪r s} : f = g ↔ ∀ x, f x = g x :=
 
 instance (r : α → α → Prop) : inhabited (r ↪r r) := ⟨rel_embedding.refl _⟩
 
-@[simp] theorem refl_apply (x : α) : rel_embedding.refl r x = x := rfl
-
 theorem trans_apply (f : r ↪r s) (g : s ↪r t) (a : α) : (f.trans g) a = g (f a) := rfl
 
-@[simp] theorem coe_trans (f : r ↪r s) (g : s ↪r t)  : ⇑(f.trans g) = g ∘ f := rfl
+@[simp] theorem coe_trans (f : r ↪r s) (g : s ↪r t) : ⇑(f.trans g) = g ∘ f := rfl
 
 /-- A relation embedding is also a relation embedding between dual relations. -/
 protected def swap (f : r ↪r s) : swap r ↪r swap s :=
@@ -362,11 +364,9 @@ of_map_rel_iff f (λ _ _, h.le_iff_le)
   (h : strict_mono f) : ⇑(of_strict_mono f h) = f := rfl
 
 /-- Embedding of a subtype into the ambient type as an `order_embedding`. -/
-def subtype (p : α → Prop) : subtype p ↪o α :=
+@[simps {fully_applied := ff}] def subtype (p : α → Prop) : subtype p ↪o α :=
 ⟨embedding.subtype p, λ x y, iff.rfl⟩
 
-@[simp] lemma coe_subtype (p : α → Prop) : ⇑(subtype p) = coe := rfl
-
 end order_embedding
 
 /-- A relation isomorphism is an equivalence that is also a relation embedding. -/
@@ -418,16 +418,25 @@ coe_fn_injective (funext h)
 theorem ext_iff {f g : r ≃r s} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ h x, h ▸ rfl, λ h, ext h⟩
 
-/-- Identity map is a relation isomorphism. -/
-@[refl] protected def refl (r : α → α → Prop) : r ≃r r :=
-⟨equiv.refl _, λ a b, iff.rfl⟩
-
 /-- Inverse map of a relation isomorphism is a relation isomorphism. -/
 @[symm] protected def symm (f : r ≃r s) : s ≃r r :=
 ⟨f.to_equiv.symm, λ a b, by erw [← f.map_rel_iff, f.1.apply_symm_apply, f.1.apply_symm_apply]⟩
 
+/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
+  because it is a composition of multiple projections. -/
+def simps.apply (h : r ≃r s) : α → β := h
+/-- See Note [custom simps projection]. -/
+def simps.symm_apply (h : r ≃r s) : β → α := h.symm
+
+initialize_simps_projections rel_iso
+  (to_equiv_to_fun → apply, to_equiv_inv_fun → symm_apply, -to_equiv)
+
+/-- Identity map is a relation isomorphism. -/
+@[refl, simps apply] protected def refl (r : α → α → Prop) : r ≃r r :=
+⟨equiv.refl _, λ a b, iff.rfl⟩
+
 /-- Composition of two relation isomorphisms is a relation isomorphism. -/
-@[trans] protected def trans (f₁ : r ≃r s) (f₂ : s ≃r t) : r ≃r t :=
+@[trans, simps apply] protected def trans (f₁ : r ≃r s) (f₂ : s ≃r t) : r ≃r t :=
 ⟨f₁.to_equiv.trans f₂.to_equiv, λ a b, f₂.map_rel_iff.trans f₁.map_rel_iff⟩
 
 instance (r : α → α → Prop) : inhabited (r ≃r r) := ⟨rel_iso.refl _⟩
@@ -441,11 +450,6 @@ protected def swap (f : r ≃r s) : (swap r) ≃r (swap s) :=
 @[simp] theorem coe_fn_symm_mk (f o) : ((@rel_iso.mk _ _ r s f o).symm : β → α) = f.symm :=
 rfl
 
-@[simp] theorem refl_apply (x : α) : rel_iso.refl r x = x := rfl
-
-@[simp] theorem trans_apply (f : r ≃r s) (g : s ≃r t) (a : α) : (f.trans g) a = g (f a) :=
-rfl
-
 @[simp] theorem apply_symm_apply  (e : r ≃r s) (x : β) : e (e.symm x) = x :=
 e.to_equiv.apply_symm_apply x
 
@@ -471,12 +475,10 @@ f.injective.eq_iff
 protected def preimage (f : α ≃ β) (s : β → β → Prop) : f ⁻¹'o s ≃r s := ⟨f, λ a b, iff.rfl⟩
 
 /-- A surjective relation embedding is a relation isomorphism. -/
+@[simps apply]
 noncomputable def of_surjective (f : r ↪r s) (H : surjective f) : r ≃r s :=
 ⟨equiv.of_bijective f ⟨f.injective, H⟩, λ a b, f.map_rel_iff⟩
 
-@[simp] theorem of_surjective_coe (f : r ↪r s) (H) : (of_surjective f H : α → β) = f :=
-rfl
-
 /--
 Given relation isomorphisms `r₁ ≃r r₂` and `s₁ ≃r s₂`, construct a relation isomorphism for the
 lexicographic orders on the sum.

src/topology/homeomorph.lean

@@ -30,32 +30,40 @@ rfl
 
 @[simp] lemma coe_to_equiv (h : α ≃ₜ β) : ⇑h.to_equiv = h := rfl
 
+/-- Inverse of a homeomorphism. -/
+protected def symm (h : α ≃ₜ β) : β ≃ₜ α :=
+{ continuous_to_fun  := h.continuous_inv_fun,
+  continuous_inv_fun := h.continuous_to_fun,
+  to_equiv := h.to_equiv.symm }
+
+/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
+  because it is a composition of multiple projections. -/
+def simps.apply (h : α ≃ₜ β) : α → β := h
+/-- See Note [custom simps projection] -/
+def simps.symm_apply (h : α ≃ₜ β) : β → α := h.symm
+
+initialize_simps_projections homeomorph
+  (to_equiv_to_fun → apply, to_equiv_inv_fun → symm_apply, -to_equiv)
+
 lemma to_equiv_injective : function.injective (to_equiv : α ≃ₜ β → α ≃ β)
 | ⟨e, h₁, h₂⟩ ⟨e', h₁', h₂'⟩ rfl := rfl
 
 @[ext] lemma ext {h h' : α ≃ₜ β} (H : ∀ x, h x = h' x) : h = h' :=
 to_equiv_injective $ equiv.ext H
 
 /-- Identity map as a homeomorphism. -/
+@[simps apply {fully_applied := ff}]
 protected def refl (α : Type*) [topological_space α] : α ≃ₜ α :=
 { continuous_to_fun := continuous_id,
   continuous_inv_fun := continuous_id,
   to_equiv := equiv.refl α }
 
-@[simp] lemma coe_refl : ⇑(homeomorph.refl α) = id := rfl
-
 /-- Composition of two homeomorphisms. -/
 protected def trans (h₁ : α ≃ₜ β) (h₂ : β ≃ₜ γ) : α ≃ₜ γ :=
 { continuous_to_fun  := h₂.continuous_to_fun.comp h₁.continuous_to_fun,
   continuous_inv_fun := h₁.continuous_inv_fun.comp h₂.continuous_inv_fun,
   to_equiv := equiv.trans h₁.to_equiv h₂.to_equiv }
 
-/-- Inverse of a homeomorphism. -/
-protected def symm (h : α ≃ₜ β) : β ≃ₜ α :=
-{ continuous_to_fun  := h.continuous_inv_fun,
-  continuous_inv_fun := h.continuous_to_fun,
-  to_equiv := h.to_equiv.symm }
-
 @[simp] lemma homeomorph_mk_coe_symm (a : equiv α β) (b c) :
   ((homeomorph.mk a b c).symm : β → α) = a.symm :=
 rfl
@@ -259,13 +267,12 @@ def prod_assoc : (α × β) × γ ≃ₜ α × (β × γ) :=
   to_equiv := equiv.prod_assoc α β γ }
 
 /-- `α × {*}` is homeomorphic to `α`. -/
+@[simps apply {fully_applied := ff}]
 def prod_punit : α × punit ≃ₜ α :=
 { to_equiv := equiv.prod_punit α,
   continuous_to_fun := continuous_fst,
   continuous_inv_fun := continuous_id.prod_mk continuous_const }
 
-@[simp] lemma coe_prod_punit : ⇑(prod_punit α) = prod.fst := rfl
-
 /-- `{*} × α` is homeomorphic to `α`. -/
 def punit_prod : punit × α ≃ₜ α :=
 (prod_comm _ _).trans (prod_punit _)