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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ n) (y ^ n)

Tactic:
induction n with

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
inst✝¹ : Std.Symm r
inst✝ : IsTrans α r
a b c d : α
h₁ : r a b
h₂ : r c d
⊢ r a c ↔ r b d

Tactic:
by
  rw [rel_congr_left h₁, rel_congr_right h₂]

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

Goal state before:
pp: case succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
hn : n + 1 ≠ 0
⊢ npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a

Tactic:
induction n with

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b : M
n : ℕ
⊢ (a * b) ^ n * a = a * (b * a) ^ n

Tactic:
induction n with

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
r p q : α → Prop
⊢ (∃ x x_1, r x) ↔ (∃ x x_1, r x) ∨ ∃ x x_1, r x

Tactic:
simp only [exists_prop]
  exact Iff.trans (exists_congr fun x ↦ or_and_right) exists_or

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

Goal state before:
pp: case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b

Tactic:
by_cases h₂ : ∃ c, f₁₂ c = b

Goal state after:
case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ∃ c, f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b

case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ab : ReflTransGen r a b
ac : ReflTransGen r a c
⊢ ReflTransGen r b c ∨ ReflTransGen r c b

Tactic:
induction ab with
  | refl => exact Or.inl ac
  | tail _ bd IH =>
    rcases IH with (IH | IH)
    · rcases cases_head IH with (rfl | ⟨e, be, ec⟩)
      · exact Or.inr (single bd)
      · cases U bd be
        exact Or.inl ec
    · exact Or.inr (IH.tail bd)

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

Goal state before:
pp: α : Type u
f g : α → α
h : Commute f g
n : ℕ
⊢ (f ∘ g)^[n] = f^[n] ∘ g^[n]

Tactic:
induction n with

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

Goal state before:
pp: α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f.trans g = Equiv.refl α ↔ f = g.symm

Tactic:
rw [← Equiv.coe_inj, coe_trans, coe_refl, ← eq_symm_comp, comp_id, Equiv.coe_inj]

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

Goal state before:
pp: α : Type u_5
β γ : Type u_6
p : α → Prop
f : (a : α) → p a → β
x : Option α
g : β → Option γ
H : ∀ (a : α), x = some a → p a
⊢ pmap f x H >>= g = x.pbind fun a h ↦ g (f a ⋯)

Tactic:
by
  grind [cases Option, pmap]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), A_le a a
le_trans✝¹ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge✝¹ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
le_antisymm✝¹ : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), A_le a a
le_trans✝ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm✝ : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total✝ : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge✝ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
B_max_def : ∀ (a b : α), B_max a b = if A_le a b then b else a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
a b : α
⊢ A_max a b = B_max a b

Tactic:
exact (A_max_def _ _).trans (B_max_def _ _).symm

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: m n : ℕ
⊢ ¬2 * n % 2 = (2 * m + 1) % 2

Tactic:
rw [Nat.add_comm, add_mul_mod_self_left, mul_mod_right, mod_eq_of_lt]

Goal state after:
m n : ℕ
⊢ ¬0 = 1

m n : ℕ
⊢ 1 < 2
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case step
m n k : ℕ
hmn : m ≤ n
m✝ : ℕ
hnk : n.le m✝
ih :
  ∀ {motive : (m : ℕ) → m ≤ m✝ → Sort u_1} (of_succ : (k : ℕ) → (h : k < m✝) → motive (k + 1) h → motive k ⋯)
    (self : motive m✝ ⋯),
    decreasingInduction of_succ self ⋯ =
      decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m✝.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m✝.succ) → motive (k + 1) h → motive k ⋯
self : motive m✝.succ ⋯
⊢ decreasingInduction of_succ self ⋯ =
    decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self ⋯) hmn

Tactic:
| step hnk ih =>

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case pos
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : x ≤ y
yx : y ≤ x
⊢ cmpLE x y = cmp x y

Tactic:
simp [cmpLE, lt_iff_le_not_ge, *, cmp, cmpUsing]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : x ≤ y
yx : ¬y ≤ x
⊢ cmpLE x y = cmp x y

Tactic:
simp [cmpLE, lt_iff_le_not_ge, *, cmp, cmpUsing]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case pos
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : ¬x ≤ y
yx : y ≤ x
⊢ cmpLE x y = cmp x y

Tactic:
simp [cmpLE, lt_iff_le_not_ge, *, cmp, cmpUsing]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ cmpLE x y = cmp x y

Tactic:
simp [cmpLE, lt_iff_le_not_ge, *, cmp, cmpUsing]

Goal state after:
case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : γ → α
g : γ → β
⊢ (∀ ⦃a b : γ⦄, a ≤ b → f a ≤ f b ∧ g a ≤ g b) ↔ (∀ ⦃a b : γ⦄, a ≤ b → f a ≤ f b) ∧ ∀ ⦃a b : γ⦄, a ≤ b → g a ≤ g b

Tactic:
forall_and

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
⊢ ((∀ (i : ι), Disjoint (f i) (g i)) ∧ ∀ (i : ι), Codisjoint (f i) (g i)) ↔
    ∀ (i : ι), Disjoint (f i) (g i) ∧ Codisjoint (f i) (g i)

Tactic:
forall_and

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ c

Tactic:
sup_inf_right

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ⊓ (b ⊔ c) ≤ (a ⊔ c) ⊓ (b ⊔ c)
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y : α
h : IsCompl x y
hle : a ≤ b ⊔ y
⊢ b ⊓ x ⊔ y ⊓ x = b ⊓ x

Tactic:
by rw [h.symm.inf_eq_bot, sup_bot_eq]

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

Goal state before:
pp: β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
⊢ r (f a) (f (a + ↑n.succ))

Tactic:
induction n with

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ (s ∩ t).Nonempty ↔ ∃ x, x ∈ t ∧ x ∈ s

Tactic:
simp_rw [inter_nonempty, and_comm]

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

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z → ∀ (x : α), x ≤ z ↔ l x ≤ y

pp: case mpr
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ (∀ (x : α), x ≤ z ↔ l x ≤ y) → u y = z

Tactic:
· rintro rfl x
    exact (gc x y).symm

Goal state after:
case mpr
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ (∀ (x : α), x ≤ z ↔ l x ≤ y) → u y = z
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c

Tactic:
by
    simp_rw [inf_comm a, ← le_himp_iff, sup_le_iff, le_himp_iff, ← sup_le_iff]; rfl

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

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

Tactic:
← disjoint_assoc,

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

Goal state before:
pp: α : Type u_1
a b : α
hab : a ≠ b
⊢ {a, b} \ {a} = {b}

Tactic:
insert_sdiff_of_mem _ (mem_singleton a),

Goal state after:
α : Type u_1
a b : α
hab : a ≠ b
⊢ {b} \ {a} = {b}
Module: Mathlib.Order.BooleanAlgebra.Set

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

Tactic:
← ite_compl,

Goal state after:
α : Type u_1
t s s' : Set α
⊢ tᶜ.ite s' s ∩ tᶜ = s' ∩ tᶜ
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
sup_inf_right

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y)) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y))
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
n : ℕ
⊢ Sum.elim succ (fun x ↦ 0) ((fun n ↦ Nat.casesOn n (inr PUnit.unit) inl) n) = n

Tactic:
by cases n <;> rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
sup_eq_bot_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ b = ⊥ ∧ 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:
by rw [sup_comm, symmDiff_sup_inf]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a ∆ b ⊔ b

Tactic:
convert! symmDiff_triangle a b ⊥

Goal state after:
case e'_3
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a = a ∆ ⊥

case e'_4
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b = b ∆ ⊥
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_4
P : Sort u_9
e : α ≃ β
⊢ (piCongrLeft' (fun x ↦ P) e).symm = piCongrLeft' (fun a ↦ P) e.symm

Tactic:
ext; simp [piCongrLeft']

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

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
α : Type u_9
β : Type u_10
γ : Type u_11
p : (α → γ) × (β → γ)
⊢ (fun f ↦ (f ∘ inl, f ∘ inr)) ((fun p ↦ Sum.elim p.fst p.snd) p) = p

Tactic:
by
    cases p
    rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ bᶜ \ aᶜ ⊔ aᶜ \ bᶜ = a ∆ b

Tactic:
simp_rw [compl_sdiff_compl, sdiff_eq, symmDiff_eq]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b ⊔ (a ⊔ b)ᶜ = ⊥ ↔ IsCompl a b

Tactic:
sup_eq_bot_iff,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b = ⊥ ∧ (a ⊔ b)ᶜ = ⊥ ↔ IsCompl a b
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
f : α → α
n : ℕ
⊢ preimage f^[n] = (preimage f)^[n]

Tactic:
induction n with

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

Goal state before:
pp: α : Type u_1
f : α → α
n : ℕ
⊢ image f^[n] = (image f)^[n]

Tactic:
induction n with

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ s.pi t = ∅ ↔ ∃ i, i ∈ s ∧ t i = ∅

Tactic:
by simp [pi_eq_empty_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ Prod.fst '' graphOn f s = s

Tactic:
by
  simp [graphOn, image_image]

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:
simp [← MonoidHom.comp_assoc]

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

Goal state before:
pp: case negSucc
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)
pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)
i n : ℕ
⊢ motive (-↑n)

Tactic:
induction n with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ SurjOn f s t ↔ ∃ s', s' ⊆ s ∧ BijOn f s' t

Tactic:
by
  constructor
  · rcases eq_empty_or_nonempty t with (rfl | ht)
    · exact fun _ => ⟨∅, empty_subset _, bijOn_empty f⟩
    · intro h
      have : Nonempty α := ⟨Classical.choose (h.comap_nonempty ht)⟩
      exact ⟨_, h.mapsTo_invFunOn.image_subset, h.bijOn_subset⟩
  · rintro ⟨s', hs', hfs'⟩
    exact hfs'.surjOn.mono hs' (Subset.refl _)

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

Goal state before:
pp: a b c : ℤ
⊢ (↑(a.gcd b)).gcd c = (↑(a.gcd c)).gcd b

Tactic:
by
  rw [gcd_assoc, gcd_assoc, gcd_comm b c]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n

Tactic:
by simp_rw [zpow_negSucc, ← inv_pow, mul_inv, mul_pow]

Goal state after:
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✝ : DivInvMonoid 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
n : ℕ
x : M₁
⊢ f (x ^ Int.negSucc n) = f (x ^ ↑n.succ)⁻¹

Tactic:
rw [zpow, zpow_negSucc, inv, zpow, zpow_natCast]

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

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

Tactic:
induction n with

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℤ
⊢ P (g ^ n)

Tactic:
induction n with

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℤ
⊢ P (g ^ n)

Tactic:
induction n with

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

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

Tactic:
mul_comm c,

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
h : IsUnit a
⊢ a / a = 1

Tactic:
by rw [div_eq_mul_inv, h.mul_inv_cancel]

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

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

Tactic:
mul_comm c,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
c : α
h : IsUnit c
a b : α
⊢ a * c / (c * b) = a / b
Module: Mathlib.Algebra.Group.Units.Defs

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

Tactic:
mul_comm c,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
c : α
h : IsUnit c
a b : α
⊢ a * c / (b * c) = a / b
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
mul_comm c,

Goal state after:
α : Type u
inst✝ : CommMonoid α
a c : α
b d : αˣ
⊢ a * ↑b⁻¹ = ↑d⁻¹ * c ↔ a * ↑d = c * ↑b
Module: Mathlib.Tactic.FunProp.Decl

Goal state before:
pp: ⊢ Name

Tactic:
exact decl_name%

Goal state after:
Module: Mathlib.Tactic.FunProp.Theorems

Goal state before:
pp: ⊢ Name

Tactic:
exact decl_name%

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
⊢ ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y

Tactic:
induction n with

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

Goal state before:
pp: α : Type u_4
p : α → Prop
f : Perm α
n : ℕ
hf : ∀ (x : α), p (f x) ↔ p x
⊢ f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯

Tactic:
induction n with

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

Goal state before:
pp: case neg
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : ¬p x
⊢ ((f.subtypePerm h₁).extendDomain (Equiv.refl { x // p x })) x = f x

Tactic:
Equiv.Perm.extendDomain_apply_not_subtype _ _ hx

Goal state after:
case neg
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : ¬p x
⊢ x = f x
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n✝ : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
n : ℕ
ha : a ^ n = 0
⊢ a = 0

Tactic:
induction n with

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
⊢ ↑(m + n) = ↑m + ↑n

Tactic:
induction n with

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

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

Tactic:
mul_self_mul_inv a

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a = a
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
induction n with

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M₂ →+ M
hf : Injective ⇑f
smul : ∀ (c : R) (x : M₂), f (c • x) = c • f x
x : M₂
⊢ f (0 • x) = f 0

Tactic:
by simp only [smul, zero_smul, f.map_zero]

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocSemiring α
n : ℕ
a : α
⊢ n • a = ↑n * a

Tactic:
induction n with

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
⊢ n ≤ n.sqrt.succ * n.sqrt + n.sqrt

Tactic:
exact le_of_lt_succ (lt_succ_sqrt n)

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

Goal state before:
pp: m n : ℕ
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0

Tactic:
induction n with

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

Goal state before:
pp: m : ℤ
n : ℕ
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0

Tactic:
induction n with

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

Goal state before:
pp: A : Type u_2
F : Type u_4
inst✝² : FunLike F ℕ A
inst✝¹ : AddZeroClass A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : f 1 = g 1
n : ℕ
⊢ f n = g n

Tactic:
induction n with

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
n : ℕ
⊢ a ^ n ∣ b ^ n

Tactic:
induction n with

Goal state after:
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
⊢ n • a = a * ↑n

Tactic:
induction n with

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ b * (1 / -a) = b * -(1 / a)

Tactic:
one_div_neg_eq_neg_one_div

Goal state after:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ b * -(1 / a) = b * -(1 / a)
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : a = 0 → b = 0
⊢ a * b / a = b

Tactic:
by
  rw [mul_comm, mul_div_cancel_of_imp h]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Commute

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
n : ℕ
x : α
⊢ Commute (↑n) x

Tactic:
induction n with

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : M
⊢ ↑n • b = n • b

Tactic:
induction n with

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : R
y : M
⊢ (n • x) • y = n • x • y

Tactic:
induction n with

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

Goal state before:
pp: M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : ℕ
a : M
⊢ f (↑x • a) = ↑x • f a

Tactic:
by
  simp only [Nat.cast_smul_eq_nsmul, map_nsmul]

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
n : ℕ
ha : Odd a
⊢ Odd (a ^ n)

Tactic:
induction n with

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
⊢ b + a - (a + c) = b - c

Tactic:
add_comm a c,

Goal state after:
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
⊢ b + a - (c + a) = b - c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ a * a⁻¹ ≤ a * b ↔ 1 ≤ a * b

Tactic:
by rw [mul_inv_cancel]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ b * a ≤ b * b⁻¹ ↔ b * a ≤ 1

Tactic:
by rw [mul_inv_cancel]

Goal state after: