mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: n : Nat
hn : n >>> 1 ≠ 0
⊢ n ≠ 0

Tactic:
by rintro rfl; exact hn rfl

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a * b * a⁻¹ = b

Tactic:
h.mul_inv_cancel

Goal state after:
G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ b = b
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, y * z = 1
x y : M
h : x * y = 1
⊢ y * x = 1

Tactic:
by
    have ⟨z, hz⟩ := ex x y h
    rwa [show x = z by simpa [← mul_assoc, h] using congr_arg (x * ·) hz.symm]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β : Sort u_2
γ : Sort u_3
f : α → γ
g : β → γ
x : α
y : β
h₁ : f ≍ g
h₂ : x ≍ y
⊢ f x = g y

Tactic:
cases h₂

Goal state after:
case refl
α : Sort u_2
γ : Sort u_3
f : α → γ
x : α
g : α → γ
h₁ : f ≍ g
⊢ f x = g x
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
⊢ ¬Injective f ↔ ∃ a b, f a = f b ∧ a ≠ b

Tactic:
simp only [Injective, not_forall, exists_prop]

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

Goal state before:
pp: case refine_1
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
⊢ update (Pi.map f default) i (f i x) = update (Pi.map f default) i (f i y)

Tactic:
hxy

Goal state after:
case refine_1
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
⊢ update (Pi.map f default) i (f i y) = update (Pi.map f default) i (f i y)
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : IsTrans α r
f : α → β
hf : ∀ (x y : α), f x = f y → r x y
⊢ IsTrans β (Relation.Map r f f)

Tactic:
refine ⟨fun _ _ _ ⟨x, y, hxy, hx, hy⟩ ⟨y', z, hyz, hy', hz⟩ ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : IsTrans α r
f : α → β
hf : ∀ (x y : α), f x = f y → r x y
x✝⁴ x✝³ x✝² : β
x✝¹ : Relation.Map r f f x✝⁴ x✝³
x✝ : Relation.Map r f f x✝³ x✝²
x y : α
hxy : r x y
hx : f x = x✝⁴
hy : f y = x✝³
y' z : α
hyz : r y' z
hy' : f y' = x✝³
hz : f z = x✝²
⊢ Relation.Map r f f x✝⁴ x✝²
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Function.swap (TransGen r) ≤ TransGen (Function.swap r)

Tactic:
intro _ _ h
  induction h with
  | single h => exact TransGen.single h
  | tail _ hbc ih => exact ih.head hbc

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
a b c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
ih : Join (ReflTransGen r) d c
⊢ Join (ReflTransGen r) e c

Tactic:
rcases ih with ⟨b, hdb, hcb⟩
    have : ∃ a, ReflTransGen r e a ∧ ReflGen r b a := by
      clear hcb
      induction hdb with
      | refl => exact ⟨e, refl, ReflGen.single hde⟩
      | @tail f b _ hfb ih =>
        rcases ih with ⟨a, hea, hfa⟩
        cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩
    rcases this with ⟨a, hea, hba⟩
    cases hba with
    | refl => exact ⟨b, hea, hcb⟩
    | single hba => exact ⟨a, hea, hcb.tail hba⟩

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)
⊢ RightInverse (Quot.map ⇑e.symm ⋯) (Quot.map ⇑e ⋯)

Tactic:
by rintro ⟨a⟩; simp only [Quot.map, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
c : γ
⊢ ∃ a, f a = c

Tactic:
by
        obtain ⟨a | b, h⟩ := h (inl c)
        · exact ⟨a, inl_injective h⟩
        · cases h

Goal state after:
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Sort u_4
β : Sort u_5
⊢ IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β

Tactic:
by
  simp only [← not_nonempty_iff, nonempty_psum, not_or]

Goal state after:
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: α : Type u_1
d x✝ : α
⊢ ((fun x ↦ x.getD d) ∘ some) x✝ = id x✝

Tactic:
simp only [Function.comp_apply, getD_some, id_eq]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PartialOrder α
⊢ ∀ (a b : OrderBot α), a = b

Tactic:
rintro @⟨⟨a⟩, ha⟩ @⟨⟨b⟩, hb⟩

Goal state after:
α : Type u
β : Type v
inst✝ : PartialOrder α
a : α
ha : ∀ (a_1 : α), ⊥ ≤ a_1
b : α
hb : ∀ (a : α), ⊥ ≤ a
⊢ { bot := a, bot_le := ha } = { bot := b, bot_le := hb }
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (cmp a b).Compares a b

Tactic:
by
  obtain h | h | h := lt_trichotomy a b <;> simp [cmp, cmpUsing, h, h.not_gt]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ MonotoneOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ MonotoneOn f s

Tactic:
by
  rw [monotoneOn_toDual_comp_iff, antitoneOn_comp_ofDual_iff]

Goal state after:
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ ¬s.Nonempty ↔ s = ∅

Tactic:
by
  simp only [Set.Nonempty, not_exists, eq_empty_iff_forall_notMem]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : semilatt_sup_inst.toPartialOrder = semilatt_inf_inst.toPartialOrder
a b : α
⊢ SemilatticeInf.inf a b ≤ a

Tactic:
by
      rw [partial_order_eq]
      apply inf_le_left

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
x y : α
⊢ x ≤ y → f x ≤ f y

Tactic:
hxy

Goal state after:
α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
x y : α
hxy : x ≤ y
⊢ f x ≤ f y
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊔ y) = f x ⊔ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ f x ⊔ f y = f y

Tactic:
rw [← h _ hx _ hy, sup_eq_right.2 hxy]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
this : f x ≤ f y
⊢ f (max x y) = f x ⊔ f y

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ x ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ y ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inr.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
this : f y ≤ f x
⊢ f (max x y) = f x ⊔ f y

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inr.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ y ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inr.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ x ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right]

Goal state after:
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: α : Type u
h : univ = {∅}
⊢ IsEmpty α

Tactic:
suffices @univ α ∈ univ by aesop

Goal state after:
α : Type u
h : univ = {∅}
⊢ univ ∈ univ
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a \ b) \ c ≤ d ↔ a \ (b ⊔ c) ≤ d

Tactic:
simp_rw [sdiff_le_iff, sup_assoc]

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

Goal state before:
pp: case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (a ⇨ b)ᶜᶜ ≤ aᶜᶜ ⇨ bᶜᶜ

pp: case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⇨ bᶜᶜ ≤ (a ⇨ b)ᶜᶜ

Tactic:
· rw [le_himp_iff, ← compl_compl_inf_distrib]
    exact compl_anti (compl_anti himp_inf_le)

Goal state after:
case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⇨ bᶜᶜ ≤ (a ⇨ b)ᶜᶜ
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s.ite s t = s ∪ t

Tactic:
simp [Set.ite]

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s.ite t s = t ∩ s

Tactic:
simp [Set.ite]

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

Goal state before:
pp: α : Type u_1
s s' : Set α
⊢ ∅.ite s s' = s'

Tactic:
simp [Set.ite]

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

Goal state before:
pp: α : Type u_1
s s' : Set α
⊢ univ.ite s s' = s

Tactic:
simp [Set.ite]

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

Goal state before:
pp: α : Type u_1
t s : Set α
⊢ t.ite ∅ s = s \ t

Tactic:
simp [Set.ite]

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

Goal state before:
pp: α : Type u_1
t s : Set α
⊢ t.ite s ∅ = s ∩ t

Tactic:
simp [Set.ite]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
⊢ GeneralizedHeytingAlgebra α

Tactic:
let himp := e.himp

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
⊢ GeneralizedHeytingAlgebra α
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
hba : b ≠ a
⊢ (optionSubtypeNe a).symm b = some ⟨b, hba⟩

Tactic:
by
  simp [hba]

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
⊢ z \ x ≤ z \ y ↔ y ≤ x

Tactic:
refine ⟨fun h ↦ ?_, sdiff_le_sdiff_left⟩
  rw [← sdiff_sdiff_eq_self hx, ← sdiff_sdiff_eq_self hy]
  exact sdiff_le_sdiff_left h

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

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

Tactic:
sup_sdiff_self_right,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊓ y ⊔ x \ z) ⊓ (z ⊔ x) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ (x \ y)ᶜ = x ⇨ y

Tactic:
by
  rw [sdiff_eq, himp_eq, compl_inf, compl_compl, sup_comm]

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

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ LeftInverse (Sum.elim Int.ofNat Int.negSucc) fun z ↦ Int.casesOn z inl inr

Tactic:
rintro (m | n) <;> rfl

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

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ RightInverse (Sum.elim Int.ofNat Int.negSucc) fun z ↦ Int.casesOn z inl inr

Tactic:
rintro (m | n) <;> rfl

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
⊢ BooleanAlgebra α

Tactic:
let himp := e.himp

Goal state after:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
⊢ BooleanAlgebra α
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
⊢ BooleanAlgebra α

Tactic:
apply e.injective.booleanAlgebra <;> intros

Goal state after:
case le
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

case map_inf
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

case map_top
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ e ⊤ = ⊤

case map_bot
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ e ⊥ = ⊥

case map_compl
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

case map_sdiff
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝

case map_himp
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c ≤ c \ (a ⊓ b)

pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c \ (a ⊓ b) ≤ a ∆ c ⊔ b ∆ c

Tactic:
· rw [h.eq_bot, sdiff_bot]

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c \ (a ⊓ b) ≤ a ∆ c ⊔ b ∆ c
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Tactic:
rcases (s ×ˢ t).eq_empty_or_nonempty with h | h
  · simp [h, prod_eq_empty_iff.1 h]
  have st : s.Nonempty ∧ t.Nonempty := by rwa [prod_nonempty_iff] at h
  refine ⟨fun H => Or.inl ⟨?_, ?_⟩, ?_⟩
  · have := image_mono (f := Prod.fst) H
    rwa [fst_image_prod _ st.2, fst_image_prod _ (h.mono H).snd] at this
  · have := image_mono (f := Prod.snd) H
    rwa [snd_image_prod st.1, snd_image_prod (h.mono H).fst] at this
  · intro H
    simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H
    exact prod_mono H.1 H.2

Goal state after:
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₂
⊢ f x ≠ f y

Tactic:
hxy

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₂
hxy : f x = f y
⊢ False
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : One M
inst✝ : One N
g : OneHom M N
toFun✝ : M → N
map_one'✝ : toFun✝ 1 = 1
h : { toFun := toFun✝, map_one' := map_one'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_one' := map_one'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : One M
inst✝ : One N
toFun✝¹ : M → N
map_one'✝¹ : toFun✝¹ 1 = 1
toFun✝ : M → N
map_one'✝ : toFun✝ 1 = 1
h : { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun = { toFun := toFun✝, map_one' := map_one'✝ }.toFun
⊢ { toFun := toFun✝¹, map_one' := map_one'✝¹ } = { toFun := toFun✝, map_one' := map_one'✝ }
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : Mul M
inst✝ : Mul N
g : M →ₙ* N
toFun✝ : M → N
map_mul'✝ : ∀ (x y : M), toFun✝ (x * y) = toFun✝ x * toFun✝ y
h : { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_mul' := map_mul'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : Mul M
inst✝ : Mul N
toFun✝¹ : M → N
map_mul'✝¹ : ∀ (x y : M), toFun✝¹ (x * y) = toFun✝¹ x * toFun✝¹ y
toFun✝ : M → N
map_mul'✝ : ∀ (x y : M), toFun✝ (x * y) = toFun✝ x * toFun✝ y
h : { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun = { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun
⊢ { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } = { toFun := toFun✝, map_mul' := map_mul'✝ }
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : MulOne M
inst✝ : MulOne N
g : M →* N
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), toOneHom✝.toFun (x * y) = toOneHom✝.toFun x * toOneHom✝.toFun y
h : (fun f ↦ f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ } = (fun f ↦ f.toFun) g
⊢ { toOneHom := toOneHom✝, map_mul' := map_mul'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : MulOne M
inst✝ : MulOne N
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), toOneHom✝¹.toFun (x * y) = toOneHom✝¹.toFun x * toOneHom✝¹.toFun y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), toOneHom✝.toFun (x * y) = toOneHom✝.toFun x * toOneHom✝.toFun y
h :
  (fun f ↦ f.toFun) { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }
⊢ { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } = { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }
Module: Mathlib.Algebra.Group.Equiv.Defs

Goal state before:
pp: case mk
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst✝³ : EquivLike F α β
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
g : M ≃* N
toEquiv✝ : M ≃ N
map_mul'✝ : ∀ (x y : M), toEquiv✝.toFun (x * y) = toEquiv✝.toFun x * toEquiv✝.toFun y
h₁ : { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }.toFun = g.toFun
h₂ : { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }.invFun = g.invFun
⊢ { toEquiv := toEquiv✝, map_mul' := map_mul'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst✝³ : EquivLike F α β
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
toEquiv✝¹ : M ≃ N
map_mul'✝¹ : ∀ (x y : M), toEquiv✝¹.toFun (x * y) = toEquiv✝¹.toFun x * toEquiv✝¹.toFun y
toEquiv✝ : M ≃ N
map_mul'✝ : ∀ (x y : M), toEquiv✝.toFun (x * y) = toEquiv✝.toFun x * toEquiv✝.toFun y
h₁ : { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ }.toFun = { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }.toFun
h₂ : { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ }.invFun = { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }.invFun
⊢ { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ } = { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MulHomClass F G H
f : F
hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹
g h : ι → G
⊢ ⇑f ∘ (g / h) = ⇑f ∘ g / ⇑f ∘ h

Tactic:
by
  ext; simp [map_div' f hf]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
g : N → M
h₁ : LeftInverse g ⇑f
⊢ g 1 = 1

Tactic:
← f.map_one,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
g : N → M
h₁ : LeftInverse g ⇑f
⊢ g (f 1) = 1
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
x' : α
hx' : x' ∈ s
he : invFunOn f s (f x) = invFunOn f s (f x')
⊢ f x = f x'

Tactic:
← invFunOn_apply_eq (f := f) hx,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
x' : α
hx' : x' ∈ s
he : invFunOn f s (f x) = invFunOn f s (f x')
⊢ f (invFunOn f s (f x)) = f x'
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : Group M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
⊢ f (x⁻¹ * x) = f 1

Tactic:
rw [mul, inv, inv_mul_cancel, one]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a * (c * (b / c)) = a * b

Tactic:
mul_div_cancel

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a * b = a * b