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:
hab.eq,

Goal state after:
G : Type u_1
inst✝ : DivisionMonoid G
a b : G
hab : Commute a b
⊢ (b * a)⁻¹ = a⁻¹ * b⁻¹
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRecAuto k m = npowBinRecAuto k m

Tactic:
npowBinRecAuto,

Goal state after:
M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRecAuto k m = npowBinRec k m
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst✝ : Nonempty γ
h : ∃ e, g = e ∘ f
x✝¹ x✝ : α
hf : f x✝¹ = f x✝
⊢ g x✝¹ = g x✝

Tactic:
rw [Classical.choose_spec h, comp_apply, comp_apply, hf]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
a b c : α
hab : r a b
⊢ ReflTransGen r a b

Tactic:
exact refl.tail hab

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (p on f)
a i✝ b✝ c✝ : α
a✝ : TransGen r a b✝
hcd : r b✝ c✝
hac : (TransGen p on f) a b✝
⊢ (TransGen p on f) a c✝

Tactic:
exact TransGen.tail hac (h _ _ hcd)

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (p on f)
a i✝ : α
hab : TransGen r a i✝
⊢ (TransGen p on f) a i✝

Tactic:
induction hab with
  | single hac => exact TransGen.single (h a _ hac)
  | tail _ hcd hac => exact TransGen.tail hac (h _ _ hcd)

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
⊢ EqvGen r a b → r a b

Tactic:
intro h
      induction h with
      | rel => assumption
      | refl => exact h.1 _
      | symm => apply h.symm; assumption
      | trans _ _ _ _ _ hab hbc => exact h.trans hab hbc

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
H : Function.Injective f
a : α
o : Option α
⊢ f a ∈ Option.map f o ↔ a ∈ o

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha : a ∈ x
⊢ f a ⋯ ∈ pmap f x h

Tactic:
mem_def

Goal state after:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha✝ : a ∈ x
ha : x = some a
⊢ pmap f x h = some (f a ⋯)
Module: Mathlib.Order.Defs.LinearOrder

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

Tactic:
obtain h | h | h := lt_trichotomy a b <;> simp [le_of_lt, not_le_of_gt, h, max_def]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
by_cases h₁ : y.1 ≤ x.1
    · exact Or.inr ⟨h.1.1, LE.le.lt_of_not_ge h.1.2 fun h₂ ↦ h.2 ⟨h₁, h₂⟩⟩
    · exact Or.inl ⟨LE.le.lt_of_not_ge h.1.1 h₁, h.1.2⟩

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → γ
s : Set α
t : Set β
⊢ (f '' s) ×ˢ t = (fun x ↦ (f x.fst, x.snd)) '' s ×ˢ t

Tactic:
aesop

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → γ
s : Set α
t : Set β
⊢ t ×ˢ (f '' s) = (fun x ↦ (x.fst, f x.snd)) '' t ×ˢ s

Tactic:
aesop

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

Goal state before:
pp: case ind
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
⊢ ¬P x

Tactic:
by_cases hx : x = ⊤
    · exact hx ▸ hexists
    · intro hx'
      obtain ⟨M, hM, hM'⟩ := hind x hx hx'
      exact IH _ hM hM'

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

Goal state before:
pp: α : Type u
s : Set α
p : α → Prop
⊢ (∀ (x : α), x ∈ s ∧ p x ↔ x ∈ s) ↔ ∀ (x : α), x ∈ s → p x

Tactic:
and_iff_left_iff_imp

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

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ s = ∅ ∧ s ≠ {x} ↔ s = ∅

Tactic:
and_iff_left_iff_imp

Goal state after:
α : Type u_1
s : Set α
x : α
⊢ s = ∅ → s ≠ {x}
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
x y z w : α
⊢ ((x = z ∨ x = w) ∧ (y = z ∨ y = w)) ∧ (z = x ∨ z = y) ∧ (w = x ∨ w = y) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
⊢ (y ⊔ x) ⊓ (y ⊔ z) = y ⊔ x ⊓ z

Tactic:
by rw [← sup_inf_left]

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

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

Tactic:
aesop

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : ¬b ≤ c
⊢ a ≤ c ↔ a ≤ c ∨ b ≤ c

Tactic:
or_iff_left h

Goal state after:
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : ¬b ≤ c
⊢ a ≤ c ↔ a ≤ c
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ insert a (s \ (t ∪ {a})) = insert a (s \ t)

Tactic:
← sdiff_sdiff,

Goal state after:
α : Type u_1
s t : Set α
a : α
⊢ insert a ((s \ t) \ {a}) = insert a (s \ t)
Module: Mathlib.Order.BooleanAlgebra.Set

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

Tactic:
simp [*, Set.ite, or_iff_left_of_imp (@h x)]

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

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

Tactic:
simp [*, Set.ite, or_iff_left_of_imp (@h x)]

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⇨ y = ⊤ ∧ x = ⊤ ↔ x = ⊤ ∧ y = ⊤

Tactic:
aesop

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a b x : α
h : x ≠ a ∧ x ≠ b
⊢ (swap a b) x = x

Tactic:
exact swap_apply_of_ne_of_ne h.1 h.2

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c = a ∆ (b ∆ c)

Tactic:
symmDiff_symmDiff_right

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
⊢ (swap i j).sumCongr (Equiv.refl β) = swap (Sum.inl i) (Sum.inl j)

Tactic:
aesop

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

Goal state before:
pp: α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : β
⊢ sumCongr (Equiv.refl α) (swap i j) = swap (Sum.inr i) (Sum.inr j)

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d)

Tactic:
by
  simp_rw [bihimp_assoc, bihimp_left_comm]

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

Goal state before:
pp: case mp
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
x_in_u : ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u
⊢ ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ

Tactic:
x_in_v

Goal state after:
case mp
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
x_in_u : ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u
x_in_v : ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' v
⊢ False
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
⊢ f '' s = g '' s

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
a : Set α
⊢ f ∘ g '' a = f '' g '' a

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ (∃ x, x ∈ range f ∩ s' ∧ ¬x ∈ range f ∩ s) ↔ ∃ x, x ∈ f ⁻¹' s' ∧ ¬x ∈ f ⁻¹' s

Tactic:
aesop

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
x : α
r : range f ∩ s ⊆ s'
hx : f x ∈ s
⊢ f x ∈ s'

Tactic:
aesop

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : f ⁻¹' s ⊆ f ⁻¹' s'
x : β
hx : (∃ y, f y = x) ∧ x ∈ s
⊢ x ∈ s'

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
⊢ (s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t

Tactic:
ext ⟨x, y⟩
  simp only [← and_and_right, mem_inter_iff, mem_prod]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
s : Set α
t : Set γ
x✝ : β × δ
⊢ x✝ ∈ Prod.map f g '' s ×ˢ t ↔ x✝ ∈ (f '' s) ×ˢ (g '' t)

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ Disjoint t (f '' s) ↔ Disjoint (f ⁻¹' t) s

Tactic:
by
  rw [disjoint_comm, disjoint_comm (b := s), disjoint_image_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α × β)
x✝¹ : α × β
p₁ : α
p₂ : β
x✝ : (p₁, p₂) ∈ s
⊢ (p₁, p₂) ∈ (Prod.fst '' s) ×ˢ (Prod.snd '' s)

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
g : α → β
f : ι → α
⊢ range (g ∘ f) = g '' range f

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
s : Set α
f : ↑(insert x s) → β
⊢ range f = insert (f ⟨x, ⋯⟩) (range fun y ↦ f ⟨↑y, ⋯⟩)

Tactic:
aesop

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

Goal state before:
pp: ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
⊢ extend f (r • g) (r • e) x = (r • extend f g e) x

Tactic:
classical
  simp only [extend_def, Pi.smul_apply]
  split_ifs <;> rfl

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (s.pi fun j ↦ t j (update f i a j)) = ({i} ∪ s).pi fun j ↦ t j (update f i a j)

Tactic:
union_eq_self_of_subset_left (singleton_subset_iff.2 hi)

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (s.pi fun j ↦ t j (update f i a j)) = s.pi fun j ↦ t j (update f i a j)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a b : α
⊢ (∀ ⦃x₁ : α⦄, x₁ ∈ {a, b} → ∀ ⦃x₂ : α⦄, x₂ ∈ {a, b} → f x₁ = f x₂ → x₁ = x₂) ↔ f a = f b → a = b

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set β
h✝ : InjOn g s
hs : range f ⊆ s
h : Injective f
x✝ : α
⊢ ∀ ⦃a₂ : α⦄, (g ∘ f) x✝ = (g ∘ f) a₂ → x✝ = a₂

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → γ
g : β → δ
⊢ graphOn f s ×ˢ graphOn g t = ⇑(Equiv.prodProdProdComm α γ β δ) ⁻¹' graphOn (Prod.map f g) (s ×ˢ t)

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → γ
g : β → δ
⊢ graphOn (Prod.map f g) (s ×ˢ t) = ⇑(Equiv.prodProdProdComm α β γ δ) ⁻¹' graphOn f s ×ˢ graphOn g t

Tactic:
aesop

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

Goal state before:
pp: 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✝

Tactic:
apply Equiv.coe_fn_injective h₁

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

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
e : M ≃* N
f : P →* M
⊢ (↑e.symm).comp ((↑e).comp f) = f

Tactic:
by simp [← MonoidHom.comp_assoc]

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

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f '' (s₁ ∩ s) ⊆ f' ⁻¹' s₁ ∩ f '' s

pp: case h₂
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s ⊆ f '' (s₁ ∩ s)

Tactic:
· rintro _ ⟨x, ⟨h₁, h⟩, rfl⟩
    exact ⟨by rwa [mem_preimage, hf h], mem_image_of_mem _ h⟩

Goal state after:
case h₂
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s ⊆ f '' (s₁ ∩ s)
Module: Mathlib.Algebra.Group.Torsion

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℤ
a : G
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1

Tactic:
← zpow_left_inj (a := a) hn,

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℤ
a : G
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a ^ n = 1 ^ n
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x : ⦃a : β⦄ → a ∈ t → α
hmem : ∀ ⦃a : β⦄ (a_1 : a ∈ t), x a_1 ∈ s
heq : ∀ ⦃a : β⦄ (a_1 : a ∈ t), f (x a_1) = a
⊢ (f '' range fun a ↦ x ⋯) = t

Tactic:
aesop

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
this : SurjOn Prod.fst (t₁ ×ˢ t₂) t₁ ∧ t₁.Nonempty ∧ t₂ = ∅
⊢ False

Tactic:
aesop

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
this : SurjOn Prod.snd (t₁ ×ˢ t₂) t₂ ∧ t₁ = ∅ ∧ t₂.Nonempty
⊢ False

Tactic:
aesop

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
⊢ IsAddRegular (ofMul a) ↔ IsRegular a

Tactic:
by
  simp [isAddRegular_iff, isRegular_iff]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : Additive α
⊢ IsRegular (toMul a) ↔ IsAddRegular a

Tactic:
by
  simp [isAddRegular_iff, isRegular_iff]

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

Goal state before:
pp: α : Type u
inst✝ : AddMonoid α
a : α
⊢ IsRegular (ofAdd a) ↔ IsAddRegular a

Tactic:
by
  simp [isAddRegular_iff, isRegular_iff]

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

Goal state before:
pp: α : Type u
inst✝ : AddMonoid α
a : Multiplicative α
⊢ IsAddRegular (toAdd a) ↔ IsRegular a

Tactic:
by
  simp [isAddRegular_iff, isRegular_iff]

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

Goal state before:
pp: case inl
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → AddMonoid (M i)
j : ι
a : M j
⊢ mulSingle j (ofAdd a) j = ofAdd (single j a j)

pp: case inr
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → AddMonoid (M i)
i : ι
a : M i
j : ι
h : j ≠ i
⊢ mulSingle i (ofAdd a) j = ofAdd (single i a j)

Tactic:
· simp only [mulSingle_eq_same, single_eq_same]

Goal state after:
case inr
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → AddMonoid (M i)
i : ι
a : M i
j : ι
h : j ≠ i
⊢ mulSingle i (ofAdd a) j = ofAdd (single i a j)
Module: Mathlib.Algebra.Group.TypeTags.Basic

Goal state before:
pp: case inl
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
a : M j
⊢ single j (ofMul a) j = ofMul (mulSingle j a j)

pp: case inr
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
a : M i
j : ι
h : j ≠ i
⊢ single i (ofMul a) j = ofMul (mulSingle i a j)

Tactic:
· simp only [mulSingle_eq_same, single_eq_same]

Goal state after:
case inr
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
a : M i
j : ι
h : j ≠ i
⊢ single i (ofMul a) j = ofMul (mulSingle i a j)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CancelCommMonoid α
a b c d : α
h : a * b = c * d
⊢ a = c ↔ b = d

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : CancelCommMonoid α
a b c d : α
h : a * b = c * d
⊢ a ≠ c ↔ b ≠ d

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a / b = 1
⊢ a * b⁻¹ = 1

Tactic:
by rwa [← div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (-↑(m * n.succ)) = (a ^ (m * (n + 1)))⁻¹

Tactic:
zpow_neg,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ (a ^ ↑(m * n.succ))⁻¹ = (a ^ (m * (n + 1)))⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (-↑(m.succ * n)) = a⁻¹ ^ ((m + 1) * n)

Tactic:
zpow_neg,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ (a ^ ↑(m.succ * n))⁻¹ = a⁻¹ ^ ((m + 1) * n)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
⊢ a * b * (b⁻¹ * c) = a * c

Tactic:
by
  rw [mul_assoc, ← mul_assoc b, mul_inv_cancel, one_mul]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ n.natAbs = 1 ↔ a ^ n = 1

Tactic:
by cases n <;> simp

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ (n - 1 + 1) * a⁻¹ = a ^ n * a⁻¹

Tactic:
Int.sub_add_cancel

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ n * a⁻¹ = a ^ n * a⁻¹
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ b / (a * b) = a⁻¹

Tactic:
by
  rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left]

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

Goal state before:
pp: M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
u : Mˣ
⊢ f ↑u * f u.inv = 1

Tactic:
by simp [← map_mul]

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

Goal state before:
pp: M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
u : Mˣ
⊢ f u.inv * f ↑u = 1

Tactic:
by simp [← map_mul]

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

Goal state before:
pp: F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : FunLike F M N
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass F M N
f : F
x : M
h : IsUnit x
⊢ f ↑h.unit⁻¹ * ↑⋯.unit = 1

Tactic:
by simp [← map_mul]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton M
a : M
⊢ a * a = 1

Tactic:
by subsingleton

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

Goal state before:
pp: α : Type u
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton M
x✝ : Mˣ
⊢ ↑x✝ = 1

Tactic:
by subsingleton

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ : ℕ
x✝ : G × H
⊢ x✝ ^ ↑x✝¹.succ = x✝ ^ ↑x✝¹ * x✝

Tactic:
ext <;> exact DivInvMonoid.zpow_succ' ..

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (-(↑(n + 1) + 1) + 1) = a ^ (-(↑(n + 1) + 1)) * a

Tactic:
zpow_neg,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (-(↑(n + 1) + 1) + 1) = (a ^ (↑(n + 1) + 1))⁻¹ * a
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (-↑(n + 1)) = (a ^ (↑(n + 1) + 1))⁻¹ * a

Tactic:
zpow_neg,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ (a ^ ↑(n + 1))⁻¹ = (a ^ (↑(n + 1) + 1))⁻¹ * a
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1 + 1) * a⁻¹ = a ^ n * a⁻¹

Tactic:
Int.sub_add_cancel

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ n * a⁻¹ = a ^ n * a⁻¹
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction α β
a : α
x : β
h : a • x = 0
⊢ x = 0

Tactic:
rw [← inv_smul_smul a x, h, smul_zero]

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

Goal state before:
pp: case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : ¬m + n = 0
⊢ 0 = 0 ^ m * 0 ^ n

Tactic:
zero_zpow _ hm,

Goal state after:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : ¬m + n = 0
⊢ 0 = 0 * 0 ^ n
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
n : ℤ
⊢ n • 1 = ↑n

Tactic:
by cases n <;> simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
G : Type u_4
inst✝ : CommGroup G
a b c d e : G
ha : IsSquare a
n : ℕ
k : ℤ
hk : Even k
⊢ IsSquare (a * (b * b) / c ^ 2 * d ^ k * e ^ (n + n))

Tactic:
aesop

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
G : Type u_4
inst✝ : AddCommGroup G
a b c d e : G
ha : Even a
n : ℕ
k : ℤ
hk : Even k
⊢ Even (a + (b + b) - 2 • c + k • d + (n + n) • e)

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
⊢ (map (fun p ↦ ∀ (a : α), p a) l).TFAE

Tactic:
simp only [TFAE, List.forall_mem_map]

Goal state after:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
⊢ ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∀ (a : α), j a) ↔ ∀ (a : α), j_1 a)
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
⊢ (map (fun p ↦ ∃ a, p a) l).TFAE

Tactic:
simp only [TFAE, List.forall_mem_map]

Goal state after:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
⊢ ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∃ a, j a) ↔ ∃ a, j_1 a)
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : NonAssocRing α
inst✝ : Nontrivial α
a : α
h : a - 1 = a
⊢ a + -1 = a + -0

Tactic:
simp [← sub_eq_add_neg, h]

Goal state after: