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

Goal state before:
pp: M : Type u_2
inst✝ : CancelCommMonoid M
a x y : M
h : x = y
⊢ SemiconjBy a x y

Tactic:
by rw [h, SemiconjBy, mul_comm]

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
n : ℕ
⊢ 1 ^ n * 1 = 1

Tactic:
one_pow,

Goal state after:
M : Type u_2
inst✝ : Monoid M
n : ℕ
⊢ 1 * 1 = 1
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Bijective f
g : α → γ
⊢ (fun g ↦ g ∘ f) (g ∘ surjInv ⋯) = g

Tactic:
simp only [comp_assoc g _ f, (leftInverse_surjInv hf).comp_eq_id, comp_id]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.inl.inr
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
e : α
be : r b✝ e
ec : ReflTransGen r e c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
· cases U bd be
        exact Or.inl ec

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
f : α ≃ β
g : α → γ
e' : β → γ
b : β
⊢ extend (⇑f) g e' b = g (f.symm b)

Tactic:
by
  rw [← f.apply_symm_apply b, f.injective.extend_apply, apply_symm_apply]

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

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g⁻¹ • a = b
⊢ a = g • b

Tactic:
← h,

Goal state after:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g⁻¹ • a = b
⊢ a = g • g⁻¹ • a
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g • a = b
⊢ a = g⁻¹ • b

Tactic:
← h,

Goal state after:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g • a = b
⊢ a = g⁻¹ • g • a
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
h : ∀ (x : M) (y : N), x • 1 * y = x • y
x : M
y z : N
⊢ (x • y) • z = x • y • z

Tactic:
← h,

Goal state after:
M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
h : ∀ (x : M) (y : N), x • 1 * y = x • y
x : M
y z : N
⊢ (x • 1 * y) • z = x • y • z
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Sort u_1
p : α → Prop
⊢ IsEmpty (Subtype p) ↔ ∀ (x : α), ¬p x

Tactic:
simp only [← not_nonempty_iff, nonempty_subtype, not_exists]

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) → DivInvMonoid (f i)
⊢ ∀ (a : (i : I) → f i), a ^ 0 = 1

Tactic:
intros; ext; exact DivInvMonoid.zpow_zero' _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
x : β
⊢ extend f (g₁ * g₂) (e₁ * e₂) x = (extend f g₁ e₁ * extend f g₂ e₂) x

Tactic:
simp [Function.extend_def, apply_dite₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
x : β
⊢ extend f (g₁ / g₂) (e₁ / e₂) x = (extend f g₁ e₁ / extend f g₂ e₂) x

Tactic:
simp [Function.extend_def, apply_dite₂]

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case mp
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
⊢ x ≤ ⊥

Tactic:
exact (update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => bot_le⟩)
      (update_le_iff.mpr ⟨hg, fun _ _ => bot_le⟩)).1

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

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

Tactic:
by
  rw [strictAntiOn_toDual_comp_iff, strictMonoOn_comp_ofDual_iff]

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

Goal state before:
pp: case refine_2
α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
h : MonotoneOn f {x | k ≤ x}
x y : ℕ
hle : x ≤ y
⊢ (fun n ↦ f (n + k)) x ≤ (fun n ↦ f (n + k)) y

Tactic:
← Nat.add_le_add_iff_right

Goal state after:
case refine_2
α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
h : MonotoneOn f {x | k ≤ x}
x y : ℕ
hle✝ : x ≤ y
hle : x + ?m.52 ≤ y + ?m.52
⊢ (fun n ↦ f (n + k)) x ≤ (fun n ↦ f (n + k)) y

α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
h : MonotoneOn f {x | k ≤ x}
x y : ℕ
hle : x ≤ y
⊢ ℕ
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : 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)
sup_idem : ∀ (a : α), a ⊔ a = a
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : a ⊔ b = b
⊢ b ⊓ a = a

Tactic:
← h,

Goal state after:
α : 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)
sup_idem : ∀ (a : α), a ⊔ a = a
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : a ⊔ b = b
⊢ (a ⊔ b) ⊓ a = a
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : 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)
sup_idem : ∀ (a : α), a ⊔ a = a
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : b ⊓ a = a
⊢ a ⊔ b = b

Tactic:
← h,

Goal state after:
α : 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)
sup_idem : ∀ (a : α), a ⊔ a = a
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : b ⊓ a = a
⊢ b ⊓ a ⊔ b = b
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
b : α
⊢ b ⊔ b = b ⊔ b ⊓ (b ⊔ b)

Tactic:
rw [inf_sup_self]

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
b : α
⊢ b ⊓ (b ⊔ b ⊓ b) = b

Tactic:
rw [inf_sup_self]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ a ⊓ (b ⊔ c) = a ⊓ (a ⊔ c) ⊓ (b ⊔ c)

Tactic:
rw [inf_sup_self]

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

Goal state before:
pp: α : Type u
s : Set α
x : α
hs : s.Nontrivial
H : s = {x}
⊢ False

Tactic:
rw [H] at hs

Goal state after:
α : Type u
s : Set α
x : α
hs : {x}.Nontrivial
H : s = {x}
⊢ False
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
by
  apply le_antisymm
  · rw [le_himp_iff, ← compl_compl_inf_distrib]
    exact compl_anti (compl_anti himp_inf_le)
  · refine le_compl_comm.1 ((compl_anti compl_sup_le_himp).trans ?_)
    rw [compl_sup_distrib, le_compl_iff_disjoint_right, disjoint_right_comm, ←
      le_compl_iff_disjoint_right]
    exact inf_himp_le

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

Goal state before:
pp: α : Type u_1
t s₁ s₂ s : Set α
h : s₁ ∩ s = s₂ ∩ s
⊢ t.ite (s₁ ∩ s) (s₂ ∩ s) = s₁ ∩ s

Tactic:
← h,

Goal state after:
α : Type u_1
t s₁ s₂ s : Set α
h : s₁ ∩ s = s₂ ∩ s
⊢ t.ite (s₁ ∩ s) (s₁ ∩ s) = s₁ ∩ s
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
← sdiff_inf_self_right z y,

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x ⊓ y = ⊥
⊢ y = ⊥

Tactic:
← h,

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x ⊓ y = ⊥
⊢ y = x ⊓ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
← h,

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

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

Tactic:
by rw [inf_assoc, ← inf_sup_left, sup_inf_sdiff]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ a \ b ⊔ b \ a = a ⊔ b

Tactic:
h.sdiff_eq_left,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ a ⊔ b \ a = a ⊔ b
Module: Mathlib.Order.SymmDiff

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

Tactic:
rw [symmDiff_comm, symmDiff_symmDiff_inf]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
rw [symmDiff_symmDiff_left, symmDiff_symmDiff_right]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint b c
⊢ a ≤ b ∆ a ⊔ c ∆ a

Tactic:
exact h.le_symmDiff_sup_symmDiff_left

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f '' Subtype.val '' Subtype.val ⁻¹' s = (fun a ↦ ↑a) '' Subtype.val ⁻¹' f '' s

Tactic:
Subtype.image_preimage_coe,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f '' (f ⁻¹' t ∩ s) = (fun a ↦ ↑a) '' Subtype.val ⁻¹' f '' s
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f '' (f ⁻¹' t ∩ s) = (fun a ↦ ↑a) '' Subtype.val ⁻¹' f '' s

Tactic:
Subtype.image_preimage_coe,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f '' (f ⁻¹' t ∩ s) = t ∩ f '' s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.snd '' s ×ˢ t ⊆ Prod.snd '' s₁ ×ˢ t₁
⊢ t ⊆ t₁

Tactic:
snd_image_prod st.1,

Goal state after:
case inr.refine_2
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : t ⊆ Prod.snd '' s₁ ×ˢ t₁
⊢ t ⊆ t₁
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ 𝒫 insert a s = 𝒫 s ∪ insert a '' 𝒫 s

Tactic:
ext t
  constructor
  · intro h
    by_cases hs : a ∈ t
    · right
      refine ⟨t \ {a}, by grind⟩
    · grind
  · grind

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
h : ∀ (x : α), (∃ y, f y = x) ↔ x = y
x✝ : ι
⊢ f x✝ = y

Tactic:
← h,

Goal state after:
α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
h : ∀ (x : α), (∃ y, f y = x) ↔ x = y
x✝ : ι
⊢ ∃ y, f y = f x✝
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp.h₁
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ s ⊆ t

Tactic:
rw [← preimage_subset_preimage_iff hs, h]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ Function.diag '' s = diagonal α ∩ s ×ˢ s

Tactic:
← range_diag,

Goal state after:
α : Type u_1
s : Set α
⊢ Function.diag '' s = range Function.diag ∩ s ×ˢ s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
s : Set α
⊢ Function.diag '' s = diagonal α ∩ s ×ˢ s

Tactic:
rw [← range_diag, ← image_preimage_eq_range_inter, diag_preimage_prod_self]

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂

Tactic:
constructor <;>
      · rintro i ⟨his, hpi⟩
        simpa [*] using h i

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 \ {i}).pi fun j ↦ t j (update f i a j)

Tactic:
union_sdiff_self,

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)) = ({i} ∪ s).pi fun j ↦ t j (update f i a j)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c
⊢ f '' s ⊓ g '' t ⊆ ⊥

Tactic:
by rintro a ⟨⟨b, hb, eq⟩, c, hc, rfl⟩; exact h b hb c hc eq

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
⊢ SurjOn f ∅ t ↔ t = ∅

Tactic:
by
  simp [SurjOn, subset_empty_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
⊢ invFun f ⁻¹' s = f '' s

Tactic:
ext x
  rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)
  · rw [mem_preimage, leftInverse_invFun hf, hf.mem_set_image]
  · have : x ∉ f '' s := fun h' => hx (image_subset_range _ _ h')
    simp only [mem_preimage, invFun_neg hx, h, this]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
n : ℕ
⊢ (1 ^ (n + 1))⁻¹ = 1

Tactic:
one_pow,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
n : ℕ
⊢ 1⁻¹ = 1
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
← h,

Goal state after:
G : Type u_3
inst✝ : Group G
a b c : G
h : a * c = b
⊢ a = a * c * c⁻¹
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
← h,

Goal state after:
G : Type u_3
inst✝ : Group G
a b c : G
h : b * a = c
⊢ a = b⁻¹ * (b * a)
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
← h,

Goal state after:
G : Type u_3
inst✝ : Group G
a b c : G
h : a⁻¹ * b = c
⊢ b = a * (a⁻¹ * b)
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
← h,

Goal state after:
G : Type u_3
inst✝ : Group G
a b c : G
h : a * b⁻¹ = c
⊢ a = a * b⁻¹ * b
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u = a
⊢ ↑u⁻¹ * a = 1

Tactic:
← h,

Goal state after:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u = a
⊢ ↑u⁻¹ * ↑u = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u = a
⊢ a * ↑u⁻¹ = 1

Tactic:
← h,

Goal state after:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u = a
⊢ ↑u * ↑u⁻¹ = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : αˣ
b c : α
h : ↑a⁻¹ * b = c
⊢ b = ↑a * c

Tactic:
← h,

Goal state after:
α : Type u
inst✝ : Monoid α
a : αˣ
b c : α
h : ↑a⁻¹ * b = c
⊢ b = ↑a * (↑a⁻¹ * b)
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
c : αˣ
a b : α
h : a * ↑c = b
⊢ a = b * ↑c⁻¹

Tactic:
← h,

Goal state after:
α : Type u
inst✝ : Monoid α
c : αˣ
a b : α
h : a * ↑c = b
⊢ a = a * ↑c * ↑c⁻¹
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : ↑b * a = c
⊢ a = ↑b⁻¹ * c

Tactic:
← h,

Goal state after:
α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : ↑b * a = c
⊢ a = ↑b⁻¹ * (↑b * a)
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : a * ↑b⁻¹ = c
⊢ a = c * ↑b

Tactic:
← h,

Goal state after:
α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : a * ↑b⁻¹ = c
⊢ a = a * ↑b⁻¹ * ↑b
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : a * ↑u = 1
⊢ 1 * ↑u⁻¹ = a

Tactic:
← h,

Goal state after:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : a * ↑u = 1
⊢ a * ↑u * ↑u⁻¹ = a
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u * a = 1
⊢ ↑u⁻¹ * 1 = a

Tactic:
← h,

Goal state after:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u * a = 1
⊢ ↑u⁻¹ * (↑u * a) = a
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
ha : a ≠ 0
⊢ a * b = 0 ↔ b = 0

Tactic:
by simp [ha]

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
ha : a ≠ 0
⊢ a * b ≠ 0 ↔ b ≠ 0

Tactic:
by simp [ha]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroOneClass M₀
h : 0 = 1
a : M₀
⊢ a * 1 = 0

Tactic:
← h,

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroOneClass M₀
h : 0 = 1
a : M₀
⊢ a * 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: R : Type u_3
inst✝ : MonoidWithZero R
x : R
m : ℕ
h✝ : IsNilpotent (x ^ m)
n : ℕ
h : (x ^ m) ^ n = 0
⊢ x ^ (m * n) = 0

Tactic:
← h,

Goal state after:
R : Type u_3
inst✝ : MonoidWithZero R
x : R
m : ℕ
h✝ : IsNilpotent (x ^ m)
n : ℕ
h : (x ^ m) ^ n = 0
⊢ x ^ (m * n) = (x ^ m) ^ n
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : FunLike F α β
inst✝¹ : ZeroHomClass F α β
a : α
f : F
hf : Injective ⇑f
inst✝ : NeZero a
⊢ f a ≠ 0

Tactic:
← ZeroHomClass.map_zero f

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : FunLike F α β
inst✝¹ : ZeroHomClass F α β
a : α
f : F
hf : Injective ⇑f
inst✝ : NeZero a
⊢ f a ≠ f 0
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
by simp [ha]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b : G₀
⊢ a ^ 2 * b / a = a * b

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
b : G₀
⊢ 0 ^ 2 * b / 0 = 0 * b

case inr
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : a ≠ 0
⊢ a ^ 2 * b / a = a * b
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
n : ℕ
h : ↑0 = ↑n
⊢ ↑n = 0

Tactic:
← h,

Goal state after:
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
n : ℕ
h : ↑0 = ↑n
⊢ ↑0 = 0
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
n : ℕ
h : ↑0 = ↑n
⊢ 0 = n

Tactic:
rw [H n]; rw [← h, Nat.cast_zero]

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

Goal state before:
pp: M : Type u_3
inst✝² : AddCommMonoid M
R : Type u_5
inst✝¹ : Ring R
inst✝ : Module R M
r : R
m : M
⊢ r • m + (1 - r) • m = m

Tactic:
by rw [← add_smul, add_sub_cancel, one_smul]

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

Goal state before:
pp: case refine_1
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝¹ : n ≥ m
hn : m ≤ n
x✝ : ∀ (k : ℤ), k < m → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x ↦ Int.strongRec lt ge k_1
l : ℤ
hl : l < m
⊢ Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) m m lt
      (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) (fun n x hn l x_1 ↦ hn l ⋯) l hl =
    Int.strongRec lt ge l

Tactic:
inductionOn'_self,

Goal state after:
case refine_1
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝¹ : n ≥ m
hn : m ≤ n
x✝ : ∀ (k : ℤ), k < m → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x ↦ Int.strongRec lt ge k_1
l : ℤ
hl : l < m
⊢ lt l hl = Int.strongRec lt ge l
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m✝ n✝ m n : ℕ
h : Even m
⊢ ¬Even (n + 3) ↔ Even (m ^ 2 + m + n)

Tactic:
simp [*, parity_simps]

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

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
mM : MulOneClass M
mN : MulOneClass N
mP : CommMonoid P
f : M →* N →* P
y : N
⊢ (f 1) y = 1

Tactic:
by simp [f.map_one, one_apply]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
n : ℕ
a : M
ha : a ^ n = 1
hn : n ≠ 0
⊢ ↑(ofPowEqOne a n ha hn ^ n) = ↑1

Tactic:
by simp [ha]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
h : n < m
⊢ 0 ^ (m - n) = 0 ^ m * (0 ^ n)⁻¹

case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
ha : a ≠ 0
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ a⁻¹ʳ = a⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
⊢ 0⁻¹ʳ = 0⁻¹

case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ a⁻¹ʳ = a⁻¹
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
⊢ (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2

Tactic:
by
  rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
⊢ CharZero R

Tactic:
refine ⟨fun m n h => @Nat.cast_injective M _ _ _ _ ?_⟩

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
m n : ℕ
h : ↑m = ↑n
⊢ ↑m = ↑n