mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Commute.Defs

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b : G
hab : Commute a b
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
by rw [hab.eq, mul_inv_rev]

Goal state after:
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b c : M
hba : b * a = 1
hac : a * c = 1
⊢ b = b * 1

Tactic:
mul_one b

Goal state after:
M : Type u_2
inst✝ : Monoid M
a b c : M
hba : b * a = 1
hac : a * c = 1
⊢ b = b
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝ : Nontrivial α
b : β
⊢ ¬Injective fun x ↦ b

Tactic:
rw [not_injective_iff]
  obtain ⟨a₁, a₂, h⟩ := exists_pair_ne α
  exact ⟨a₁, a₂, rfl, h⟩

Goal state after:
Module: Mathlib.Logic.Function.Conjugate

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
f' : β → α
h : Semiconj f ga gb
hf₁ : LeftInverse f' f
hf₂ : RightInverse f' f
x : β
⊢ f' (gb x) = ga (f' x)

Tactic:
rw [← hf₁.injective.eq_iff, h, hf₂, hf₂]

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
⊢ f^[n.succ] = f ∘ f^[n]

Tactic:
rw [iterate_succ, (Commute.self_iterate f n).comp_eq]

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f^[n.pred] ∘ f = f^[n]

Tactic:
← iterate_succ,

Goal state after:
α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f^[n.pred.succ] = f^[n]
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (∃ fab, p fab) ↔ ∃ fa fb, p fun t ↦ rec fa fb t

Tactic:
rw [← not_forall_not, forall_sum]
  simp

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → CommMagma (f i)
x✝² x✝¹ : (i : I) → f i
x✝ : I
⊢ (x✝² * x✝¹) x✝ = (x✝¹ * x✝²) x✝

Tactic:
apply mul_comm

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ (if a ≤ a then a else a) = a

Tactic:
ite_id

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ a = a
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b

pp: case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b

pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b

Tactic:
· exact compare_lt_iff_lt

Goal state after:
case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b

case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a b : α
⊢ ¬a < b ↔ ¬a ≤ b ∨ b ≤ a

Tactic:
by
  rw [lt_iff_le_not_ge, Classical.not_and_iff_not_or_not, Classical.not_not]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
⊢ o.Compares a b ↔ o.Compares a' b'

Tactic:
by
  refine ⟨h, fun ho => ?_⟩
  rcases lt_trichotomy a b with hab | hab | hab
  · have hab : Compares Ordering.lt a b := hab
    rwa [ho.inj (h hab)]
  · have hab : Compares Ordering.eq a b := hab
    rwa [ho.inj (h hab)]
  · have hab : Compares Ordering.gt a b := hab
    rwa [ho.inj (h hab)]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x < y ↔ x' < y'

Tactic:
by
  rw [← cmp_eq_lt_iff, ← cmp_eq_lt_iff, h]

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
by
  simp_rw [not_monotone_not_antitone_iff_exists_le_le, ← and_assoc]
  refine exists₃_congr (fun a b c ↦ and_congr_left <|
    fun h ↦ (Ne.le_iff_lt ?_).and <| Ne.le_iff_lt ?_) <;>
  (rintro rfl; simp at h)

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
g : α → α
hg : ∀ (x : α), x < g x
⊢ ∃ f, StrictMono f ∧ f 0 = a

Tactic:
exact ⟨fun n ↦ Nat.recOn n a fun _ ↦ g, strictMono_nat_of_lt_succ fun n ↦ hg _, rfl⟩

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n : ℤ
x : α
h1 : f (n + 1) < x
h2 : x < f n
a : ℤ
⊢ f a ≠ x

Tactic:
rintro rfl
  exact (hf.reflect_lt h2).not_ge (Int.le_of_lt_add_one <| hf.reflect_lt h1)

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case mpr
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ (∃ c, b = a ⊔ c) → a ≤ b

Tactic:
rintro ⟨c, rfl : _ = _ ⊔ _⟩
    exact le_sup_left

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case min
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e (x✝ ⊓ y✝) = Min.min (e x✝) (e y✝)

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case max
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e (x✝ ⊔ y✝) = Max.max (e x✝) (e y✝)

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case compare
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ Ord.compare (e x✝) (e y✝) = Ord.compare x✝ y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e y✝ ≤ e x✝ ↔ y✝ ≤ x✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e y✝ < e x✝ ↔ y✝ < x✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
⊢ DistribLattice α

Tactic:
by
  let lattice := e.lattice
  apply e.injective.distribLattice <;> intros <;> first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
b : { y // y ≠ x }
⊢ (fun a ↦ ⟨↑e (some a), ⋯⟩) ((fun b ↦ ((↑e).symm ↑b).get ⋯) b) = b

Tactic:
ext
        simp

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
x : α
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂

Tactic:
by_cases hx : x ∈ t <;> simp [*, Set.ite, or_iff_left_of_imp (@h x)]

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ e ⊤ = ⊤

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_himp
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ e ⊥ = ⊥

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_sdiff
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y ⊓ x = y ⊓ z
⊢ y \ x = y \ z

Tactic:
rw [← sdiff_inf_self_right, ← sdiff_inf_self_right z y, inf_comm, h, inf_comm]

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ e ⊤ = ⊤

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ e ⊥ = ⊥

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_compl
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_himp
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
y✝ x✝ : α
⊢ e y✝ ≤ e x✝ ↔ y✝ ≤ x✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
y✝ x✝ : α
⊢ e y✝ < e x✝ ↔ y✝ < x✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := ⋯
top : Top α := ⋯
hnot : HNot α := ⋯
⊢ e ⊤ = ⊤

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := ⋯
top : Top α := ⋯
hnot : HNot α := ⋯
⊢ e ⊥ = ⊥

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_hnot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a✝ : α
⊢ e (￢a✝) = ￢e a✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_sdiff
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
b✝ a✝ : α
⊢ e (b✝ \ a✝) = e b✝ \ e a✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ e ⊤ = ⊤

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ e ⊥ = ⊥

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after: