refactor(*): move all mk_simp_attribute commands to 1 file (#19223)

src/algebra/group/defs.lean

@@ -87,10 +87,6 @@ variables {G : Type*}
    to the additive one.
 -/
 
-mk_simp_attribute field_simps "The simpset `field_simps` is used by the tactic `field_simp` to
-reduce an expression in a field to an expression of the form `n / d` where `n` and `d` are
-division-free."
-
 section has_mul
 variables [has_mul G]
 

src/control/basic.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl
 
 Extends the theory on functors, applicatives and monads.
 -/
+import tactic.mk_simp_attribute
 
 universes u v w
 variables {α β γ : Type u}
@@ -14,9 +15,6 @@ notation a ` $< `:1 f:1 := f a
 section functor
 variables {f : Type u → Type v} [functor f] [is_lawful_functor f]
 
-run_cmd mk_simp_attr `functor_norm
-run_cmd tactic.add_doc_string `simp_attr.functor_norm "Simp set for functor_norm"
-
 @[functor_norm] theorem functor.map_map (m : α → β) (g : β → γ) (x : f α) :
   g <$> (m <$> x) = (g ∘ m) <$> x :=
 (comp_map _ _ _).symm
@@ -85,6 +83,7 @@ lemma seq_bind_eq (x : m α) {g : β → m γ} {f : α → β} : (f <$> x) >>= g
 show bind (f <$> x) g = bind x (g ∘ f),
 by rw [← bind_pure_comp_eq_map, bind_assoc]; simp [pure_bind]
 
+@[monad_norm]
 lemma seq_eq_bind_map {x : m α} {f : m (α → β)} : f <*> x = (f >>= (<$> x)) :=
 (bind_map_eq_seq f x).symm
 

src/control/monad/basic.lean

@@ -38,11 +38,7 @@ functor, applicative, monad, simp
 
 -/
 
-mk_simp_attribute monad_norm none with functor_norm
-
 attribute [ext] reader_t.ext state_t.ext except_t.ext option_t.ext
-attribute [functor_norm]   bind_assoc pure_bind bind_pure
-attribute [monad_norm] seq_eq_bind_map
 universes u v
 
 @[monad_norm]

src/data/is_R_or_C/basic.lean

@@ -70,8 +70,6 @@ class is_R_or_C (K : Type*)
 
 end
 
-mk_simp_attribute is_R_or_C_simps "Simp attribute for lemmas about `is_R_or_C`"
-
 variables {K E : Type*} [is_R_or_C K]
 
 namespace is_R_or_C

src/data/nat/parity.lean

@@ -91,8 +91,6 @@ mod_two_add_add_odd_mod_two m odd_one
 @[simp] theorem succ_mod_two_add_mod_two (m : ℕ) : (m + 1) % 2 + m % 2 = 1 :=
 by rw [add_comm, mod_two_add_succ_mod_two]
 
-mk_simp_attribute parity_simps "Simp attribute for lemmas about `even`"
-
 @[simp] theorem not_even_one : ¬ even 1 :=
 by rw even_iff; norm_num
 

src/data/prod/basic.lean

@@ -37,7 +37,9 @@ prod.exists
 
 @[simp] lemma fst_comp_mk (x : α) : prod.fst ∘ (prod.mk x : β → α × β) = function.const β x := rfl
 
-@[simp] lemma map_mk (f : α → γ) (g : β → δ) (a : α) (b : β) : map f g (a, b) = (f a, g b) := rfl
+@[simp, mfld_simps] lemma map_mk (f : α → γ) (g : β → δ) (a : α) (b : β) :
+  map f g (a, b) = (f a, g b) :=
+rfl
 
 lemma map_fst (f : α → γ) (g : β → δ) (p : α × β) : (map f g p).1 = f (p.1) := rfl
 

src/data/set/basic.lean

@@ -409,7 +409,7 @@ Mathematically it is the same as `α` but it has a different type.
 
 @[simp] theorem set_of_true : {x : α | true} = univ := rfl
 
-@[simp] theorem mem_univ (x : α) : x ∈ @univ α := trivial
+@[simp, mfld_simps] theorem mem_univ (x : α) : x ∈ @univ α := trivial
 
 @[simp] lemma univ_eq_empty_iff : (univ : set α) = ∅ ↔ is_empty α :=
 eq_empty_iff_forall_not_mem.trans ⟨λ H, ⟨λ x, H x trivial⟩, λ H x _, @is_empty.false α H x⟩
@@ -541,7 +541,8 @@ by simp only [← subset_empty_iff]; exact union_subset_iff
 
 theorem inter_def {s₁ s₂ : set α} : s₁ ∩ s₂ = {a | a ∈ s₁ ∧ a ∈ s₂} := rfl
 
-@[simp] theorem mem_inter_iff (x : α) (a b : set α) : x ∈ a ∩ b ↔ (x ∈ a ∧ x ∈ b) := iff.rfl
+@[simp, mfld_simps]
+theorem mem_inter_iff (x : α) (a b : set α) : x ∈ a ∩ b ↔ (x ∈ a ∧ x ∈ b) := iff.rfl
 
 theorem mem_inter {x : α} {a b : set α} (ha : x ∈ a) (hb : x ∈ b) : x ∈ a ∩ b := ⟨ha, hb⟩
 
@@ -569,7 +570,7 @@ ext $ λ x, and.left_comm
 theorem inter_right_comm (s₁ s₂ s₃ : set α) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ :=
 ext $ λ x, and.right_comm
 
-@[simp] theorem inter_subset_left (s t : set α) : s ∩ t ⊆ s := λ x, and.left
+@[simp, mfld_simps] theorem inter_subset_left (s t : set α) : s ∩ t ⊆ s := λ x, and.left
 
 @[simp] theorem inter_subset_right (s t : set α) : s ∩ t ⊆ t := λ x, and.right
 
@@ -596,9 +597,9 @@ lemma inter_congr_right (hs : t ∩ u ⊆ s) (ht : s ∩ u ⊆ t) : s ∩ u = t
 lemma inter_eq_inter_iff_left : s ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u := inf_eq_inf_iff_left
 lemma inter_eq_inter_iff_right : s ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t := inf_eq_inf_iff_right
 
-@[simp] theorem inter_univ (a : set α) : a ∩ univ = a := inf_top_eq
+@[simp, mfld_simps] theorem inter_univ (a : set α) : a ∩ univ = a := inf_top_eq
 
-@[simp] theorem univ_inter (a : set α) : univ ∩ a = a := top_inf_eq
+@[simp, mfld_simps] theorem univ_inter (a : set α) : univ ∩ a = a := top_inf_eq
 
 theorem inter_subset_inter {s₁ s₂ t₁ t₂ : set α}
   (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) : s₁ ∩ s₂ ⊆ t₁ ∩ t₂ := λ x, and.imp (@h₁ _) (@h₂ _)

src/data/set/image.lean

@@ -50,19 +50,19 @@ variables {f : α → β} {g : β → γ}
 
 @[simp] theorem preimage_empty : f ⁻¹' ∅ = ∅ := rfl
 
-@[simp] theorem mem_preimage {s : set β} {a : α} : (a ∈ f ⁻¹' s) ↔ (f a ∈ s) := iff.rfl
+@[simp, mfld_simps] theorem mem_preimage {s : set β} {a : α} : (a ∈ f ⁻¹' s) ↔ (f a ∈ s) := iff.rfl
 
 lemma preimage_congr {f g : α → β} {s : set β} (h : ∀ (x : α), f x = g x) : f ⁻¹' s = g ⁻¹' s :=
 by { congr' with x, apply_assumption }
 
 theorem preimage_mono {s t : set β} (h : s ⊆ t) : f ⁻¹' s ⊆ f ⁻¹' t :=
 assume x hx, h hx
 
-@[simp] theorem preimage_univ : f ⁻¹' univ = univ := rfl
+@[simp, mfld_simps] theorem preimage_univ : f ⁻¹' univ = univ := rfl
 
 theorem subset_preimage_univ {s : set α} : s ⊆ f ⁻¹' univ := subset_univ _
 
-@[simp] theorem preimage_inter {s t : set β} : f ⁻¹' (s ∩ t) = f ⁻¹' s ∩ f ⁻¹' t := rfl
+@[simp, mfld_simps] theorem preimage_inter {s t : set β} : f ⁻¹' (s ∩ t) = f ⁻¹' s ∩ f ⁻¹' t := rfl
 
 @[simp] theorem preimage_union {s t : set β} : f ⁻¹' (s ∪ t) = f ⁻¹' s ∪ f ⁻¹' t := rfl
 
@@ -80,7 +80,7 @@ rfl
 
 @[simp] lemma preimage_id_eq : preimage (id : α → α) = id := rfl
 
-theorem preimage_id {s : set α} : id ⁻¹' s = s := rfl
+@[mfld_simps] theorem preimage_id {s : set α} : id ⁻¹' s = s := rfl
 
 @[simp] theorem preimage_id' {s : set α} : (λ x, x) ⁻¹' s = s := rfl
 
@@ -152,6 +152,7 @@ theorem mem_image_iff_bex {f : α → β} {s : set α} {y : β} :
 
 lemma image_eta (f : α → β) : f '' s = (λ x, f x) '' s := rfl
 
+@[mfld_simps]
 theorem mem_image_of_mem (f : α → β) {x : α} {a : set α} (h : x ∈ a) : f x ∈ f '' a :=
 ⟨_, h, rfl⟩
 
@@ -252,7 +253,8 @@ by { ext, simp [image, eq_comm] }
 ext $ λ x, ⟨λ ⟨y, _, h⟩, h ▸ mem_singleton _,
   λ h, (eq_of_mem_singleton h).symm ▸ hs.imp (λ y hy, ⟨hy, rfl⟩)⟩
 
-@[simp] lemma image_eq_empty {α β} {f : α → β} {s : set α} : f '' s = ∅ ↔ s = ∅ :=
+@[simp, mfld_simps]
+lemma image_eq_empty {α β} {f : α → β} {s : set α} : f '' s = ∅ ↔ s = ∅ :=
 by { simp only [eq_empty_iff_forall_not_mem],
      exact ⟨λ H a ha, H _ ⟨_, ha, rfl⟩, λ H b ⟨_, ha, _⟩, H _ ha⟩ }
 
@@ -506,7 +508,7 @@ def range (f : ι → α) : set α := {x | ∃y, f y = x}
 
 @[simp] theorem mem_range {x : α} : x ∈ range f ↔ ∃ y, f y = x := iff.rfl
 
-@[simp] theorem mem_range_self (i : ι) : f i ∈ range f := ⟨i, rfl⟩
+@[simp, mfld_simps] theorem mem_range_self (i : ι) : f i ∈ range f := ⟨i, rfl⟩
 
 theorem forall_range_iff {p : α → Prop} : (∀ a ∈ range f, p a) ↔ (∀ i, p (f i)) :=
 by simp
@@ -649,7 +651,7 @@ theorem preimage_image_preimage {f : α → β} {s : set β} :
   f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s :=
 by rw [image_preimage_eq_inter_range, preimage_inter_range]
 
-@[simp] theorem range_id : range (@id α) = univ := range_iff_surjective.2 surjective_id
+@[simp, mfld_simps] theorem range_id : range (@id α) = univ := range_iff_surjective.2 surjective_id
 
 @[simp] theorem range_id' : range (λ (x : α), x) = univ := range_id
 

src/data/set/prod.lean

@@ -42,9 +42,9 @@ lemma prod_eq (s : set α) (t : set β) : s ×ˢ t = prod.fst ⁻¹' s ∩ prod.
 
 lemma mem_prod_eq {p : α × β} : p ∈ s ×ˢ t = (p.1 ∈ s ∧ p.2 ∈ t) := rfl
 
-@[simp] lemma mem_prod {p : α × β} : p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t := iff.rfl
+@[simp, mfld_simps] lemma mem_prod {p : α × β} : p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t := iff.rfl
 
-@[simp] lemma prod_mk_mem_set_prod_eq : (a, b) ∈ s ×ˢ t = (a ∈ s ∧ b ∈ t) := rfl
+@[simp, mfld_simps] lemma prod_mk_mem_set_prod_eq : (a, b) ∈ s ×ˢ t = (a ∈ s ∧ b ∈ t) := rfl
 
 lemma mk_mem_prod (ha : a ∈ s) (hb : b ∈ t) : (a, b) ∈ s ×ˢ t := ⟨ha, hb⟩
 
@@ -77,7 +77,7 @@ by simp [and_assoc]
 
 @[simp] lemma empty_prod : (∅ : set α) ×ˢ t = ∅ := by { ext, exact false_and _ }
 
-@[simp] lemma univ_prod_univ : @univ α ×ˢ @univ β = univ := by { ext, exact true_and _ }
+@[simp, mfld_simps] lemma univ_prod_univ : @univ α ×ˢ @univ β = univ := by { ext, exact true_and _ }
 
 lemma univ_prod {t : set β} : (univ : set α) ×ˢ t = prod.snd ⁻¹' t := by simp [prod_eq]
 
@@ -103,6 +103,7 @@ by { ext ⟨x, y⟩, simp only [←and_and_distrib_right, mem_inter_iff, mem_pro
 lemma prod_inter : s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂ :=
 by { ext ⟨x, y⟩, simp only [←and_and_distrib_left, mem_inter_iff, mem_prod] }
 
+@[mfld_simps]
 lemma prod_inter_prod : s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) :=
 by { ext ⟨x, y⟩, simp [and_assoc, and.left_comm] }
 
@@ -186,7 +187,7 @@ lemma prod_range_range_eq {m₁ : α → γ} {m₂ : β → δ} :
   (range m₁) ×ˢ (range m₂) = range (λ p : α × β, (m₁ p.1, m₂ p.2)) :=
 ext $ by simp [range]
 
-@[simp] lemma range_prod_map {m₁ : α → γ} {m₂ : β → δ} :
+@[simp, mfld_simps] lemma range_prod_map {m₁ : α → γ} {m₂ : β → δ} :
   range (prod.map m₁ m₂) = (range m₁) ×ˢ (range m₂) :=
 prod_range_range_eq.symm
 
@@ -219,7 +220,6 @@ lemma prod_sub_preimage_iff {W : set γ} {f : α × β → γ} :
   s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ a b, a ∈ s → b ∈ t → f (a, b) ∈ W :=
 by simp [subset_def]
 
-
 lemma image_prod_mk_subset_prod {f : α → β} {g : α → γ} {s : set α} :
   (λ x, (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s) :=
 by { rintros _ ⟨x, hx, rfl⟩, exact mk_mem_prod (mem_image_of_mem f hx) (mem_image_of_mem g hx) }

src/data/subtype.lean

@@ -84,7 +84,7 @@ ext_iff
 
 @[simp] theorem coe_eta (a : {a // p a}) (h : p a) : mk ↑a h = a := subtype.ext rfl
 
-@[simp] theorem coe_mk (a h) : (@mk α p a h : α) = a := rfl
+@[simp, mfld_simps] theorem coe_mk (a h) : (@mk α p a h : α) = a := rfl
 
 @[simp, nolint simp_nf] -- built-in reduction doesn't always work
 theorem mk_eq_mk {a h a' h'} : @mk α p a h = @mk α p a' h' ↔ a = a' :=

src/data/typevec.lean

@@ -235,11 +235,6 @@ eq_of_drop_last_eq rfl rfl
 instance subsingleton0 : subsingleton (typevec 0) :=
 ⟨ λ a b, funext $ λ a, fin2.elim0 a  ⟩
 
-run_cmd do
-  mk_simp_attr `typevec,
-  tactic.add_doc_string `simp_attr.typevec
-"simp set for the manipulation of typevec and arrow expressions"
-
 local prefix `♯`:0 := cast (by try { simp }; congr' 1; try { simp })
 
 /-- cases distinction for 0-length type vector -/

src/logic/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 -/
-import tactic.doc_commands
+import tactic.mk_simp_attribute
 import tactic.reserved_notation
 
 /-!
@@ -63,7 +63,7 @@ instance psum.inhabited_right {α β} [inhabited β] : inhabited (psum α β) :=
   {α} [subsingleton α] : decidable_eq α
 | a b := is_true (subsingleton.elim a b)
 
-@[simp] lemma eq_iff_true_of_subsingleton {α : Sort*} [subsingleton α] (x y : α) :
+@[simp, nontriviality] lemma eq_iff_true_of_subsingleton {α : Sort*} [subsingleton α] (x y : α) :
   x = y ↔ true :=
 by cc
 
@@ -274,7 +274,7 @@ theorem imp_and_distrib {α} : (α → b ∧ c) ↔ (α → b) ∧ (α → c) :=
 ⟨λ h, ⟨λ ha, (h ha).left, λ ha, (h ha).right⟩,
  λ h ha, ⟨h.left ha, h.right ha⟩⟩
 
-@[simp] theorem and_imp : (a ∧ b → c) ↔ (a → b → c) :=
+@[simp, mfld_simps] theorem and_imp : (a ∧ b → c) ↔ (a → b → c) :=
 iff.intro (λ h ha hb, h ⟨ha, hb⟩) (λ h ⟨ha, hb⟩, h ha hb)
 
 theorem iff_def : (a ↔ b) ↔ (a → b) ∧ (b → a) :=
@@ -842,7 +842,7 @@ end mem
 section equality
 variables {α : Sort*} {a b : α}
 
-@[simp] theorem heq_iff_eq : a == b ↔ a = b :=
+@[simp, mfld_simps] theorem heq_iff_eq : a == b ↔ a = b :=
 ⟨eq_of_heq, heq_of_eq⟩
 
 theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : hp == hq :=
@@ -865,12 +865,12 @@ theorem eq_equivalence : equivalence (@eq α) :=
 ⟨eq.refl, @eq.symm _, @eq.trans _⟩
 
 /-- Transport through trivial families is the identity. -/
-@[simp]
+@[simp, transport_simps]
 lemma eq_rec_constant {α : Sort*} {a a' : α} {β : Sort*} (y : β) (h : a = a') :
   (@eq.rec α a (λ a, β) y a' h) = y :=
 by { cases h, refl, }
 
-@[simp]
+@[simp, transport_simps]
 lemma eq_mp_eq_cast {α β : Sort*} (h : α = β) : eq.mp h = cast h := rfl
 
 @[simp]
@@ -1096,6 +1096,7 @@ let ⟨a⟩ := ha in
   (λ hb, hb $ h $ λ x, (not_imp.1 (h' x)).1), λ ⟨x, hx⟩ h, hx (h x)⟩
 
 -- TODO: duplicate of a lemma in core
+@[mfld_simps]
 theorem forall_true_iff : (α → true) ↔ true :=
 implies_true_iff α
 
@@ -1118,7 +1119,7 @@ exists.elim h (λ x hx, ⟨x, and.left hx⟩)
   (∃! x, p x) ↔ ∃ x, p x :=
 ⟨λ h, h.exists, Exists.imp $ λ x hx, ⟨hx, λ y _, subsingleton.elim y x⟩⟩
 
-@[simp] theorem forall_const (α : Sort*) [i : nonempty α] : (α → b) ↔ b :=
+@[simp, mfld_simps] theorem forall_const (α : Sort*) [i : nonempty α] : (α → b) ↔ b :=
 ⟨i.elim, λ hb x, hb⟩
 
 /-- For some reason simp doesn't use `forall_const` to simplify in this case. -/

src/logic/equiv/defs.lean

@@ -120,10 +120,10 @@ initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply)
 @[trans] protected def trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
 ⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm, e₂.left_inv.comp e₁.left_inv, e₂.right_inv.comp e₁.right_inv⟩
 
-@[simp]
+@[simp, transport_simps, mfld_simps]
 lemma to_fun_as_coe (e : α ≃ β) : e.to_fun = e := rfl
 
-@[simp]
+@[simp, mfld_simps]
 lemma inv_fun_as_coe (e : α ≃ β) : e.inv_fun = e.symm := rfl
 
 protected theorem injective (e : α ≃ β) : injective e := equiv_like.injective e
@@ -189,10 +189,11 @@ theorem refl_apply (x : α) : equiv.refl α x = x := rfl
 
 theorem trans_apply (f : α ≃ β) (g : β ≃ γ) (a : α) : (f.trans g) a = g (f a) := rfl
 
-@[simp] theorem apply_symm_apply  (e : α ≃ β) (x : β) : e (e.symm x) = x :=
+@[simp, equiv_rw_simp] theorem apply_symm_apply  (e : α ≃ β) (x : β) : e (e.symm x) = x :=
 e.right_inv x
 
-@[simp] theorem symm_apply_apply (e : α ≃ β) (x : α) : e.symm (e x) = x :=
+@[simp, equiv_rw_simp, transport_simps]
+theorem symm_apply_apply (e : α ≃ β) (x : α) : e.symm (e x) = x :=
 e.left_inv x
 
 @[simp] theorem symm_comp_self (e : α ≃ β) : e.symm ∘ e = id := funext e.symm_apply_apply
@@ -208,6 +209,7 @@ e.left_inv x
 
 theorem apply_eq_iff_eq (f : α ≃ β) {x y : α} : f x = f y ↔ x = y := equiv_like.apply_eq_iff_eq f
 
+@[transport_simps]
 theorem apply_eq_iff_eq_symm_apply {α β : Sort*} (f : α ≃ β) {x : α} {y : β} :
   f x = y ↔ x = f.symm y :=
 begin
@@ -234,7 +236,7 @@ lemma symm_apply_eq {α β} (e : α ≃ β) {x y} : e.symm x = y ↔ x = e y :=
 lemma eq_symm_apply {α β} (e : α ≃ β) {x y} : y = e.symm x ↔ e y = x :=
 (eq_comm.trans e.symm_apply_eq).trans eq_comm
 
-@[simp] theorem symm_symm (e : α ≃ β) : e.symm.symm = e := by { cases e, refl }
+@[simp, equiv_rw_simp] theorem symm_symm (e : α ≃ β) : e.symm.symm = e := by { cases e, refl }
 
 @[simp] theorem trans_refl (e : α ≃ β) : e.trans (equiv.refl β) = e := by { cases e, refl }
 
@@ -411,7 +413,7 @@ A version of `equiv.arrow_congr` in `Type`, rather than `Sort`.
 The `equiv_rw` tactic is not able to use the default `Sort` level `equiv.arrow_congr`,
 because Lean's universe rules will not unify `?l_1` with `imax (1 ?m_1)`.
 -/
-@[congr, simps apply]
+@[congr, simps apply { attrs := [`simp, `transport_simps] }]
 def arrow_congr' {α₁ β₁ α₂ β₂ : Type*} (hα : α₁ ≃ α₂) (hβ : β₁ ≃ β₂) : (α₁ → β₁) ≃ (α₂ → β₂) :=
 equiv.arrow_congr hα hβ
 
@@ -638,7 +640,8 @@ def sigma_congr {α₁ α₂} {β₁ : α₁ → Sort*} {β₂ : α₂ → Sort*
 (sigma_congr_right F).trans (sigma_congr_left f)
 
 /-- `sigma` type with a constant fiber is equivalent to the product. -/
-@[simps apply symm_apply] def sigma_equiv_prod (α β : Type*) : (Σ_:α, β) ≃ α × β :=
+@[simps apply symm_apply { attrs := [`simp, `mfld_simps] }]
+def sigma_equiv_prod (α β : Type*) : (Σ_:α, β) ≃ α × β :=
 ⟨λ a, ⟨a.1, a.2⟩, λ a, ⟨a.1, a.2⟩, λ ⟨a, b⟩, rfl, λ ⟨a, b⟩, rfl⟩
 
 /-- If each fiber of a `sigma` type is equivalent to a fixed type, then the sigma type