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

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

Tactic:
pow_succ,

Goal state after:
case succ
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x ^ n * x) (y ^ (n + 1))
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 1 = a

Tactic:
pow_succ,

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 0 * a = a
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
pow_succ,

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
⊢ a ^ (n + 1) * a = a * (a ^ n * a)
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 2 = a * a

Tactic:
pow_succ,

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 1 * a = a * a
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 3 = a * a * a

Tactic:
pow_succ,

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 2 * a = a * a * a
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
pow_succ,

Goal state after:
M : Type u_2
inst✝ : Monoid M
n : ℕ
⊢ 1 ^ n * 1 = 1
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
pow_succ,

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m + (n + 1)) = a ^ m * (a ^ n * a)
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
pow_succ,

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m * n) * a ^ m = (a ^ m) ^ n * a ^ m
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∀ (x : α), p x (update f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)

Tactic:
← and_forall_ne a,

Goal state after:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (p a (update f a b a) ∧ ∀ (b_1 : α), b_1 ≠ a → p b_1 (update f a b b_1)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g ↦ extend f g e') g₁ = (fun g ↦ extend f g e') g₂
x : α
H : (fun g ↦ extend f g e') g₁ (f x) = (fun g ↦ extend f g e') g₂ (f x)
⊢ g₁ x = g₂ x

Tactic:
simp only [hf.extend_apply] at H

Goal state after:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g ↦ extend f g e') g₁ = (fun g ↦ extend f g e') g₂
x : α
H : g₁ x = g₂ x
⊢ g₁ x = g₂ x
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {motive : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), motive a ⋯) →
      (∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯) → motive a a✝
motive : (a : α) → TransGen r a c → Prop
single : ∀ {a : α} (h : r a c), motive a ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ motive a ⋯

Tactic:
| @tail b c _ hbc h_ih =>

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

Goal state before:
pp: α : Type u
f : α → α
x : α
h : f x = x
n✝ n : ℕ
ihn : f^[n] x = x
⊢ f^[n.succ] x = x

Tactic:
rw [iterate_succ_apply, h, ihn]

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → α
b : β
l : List β
H : ∀ (a : α), foldl (fun b x ↦ f b) a l = f^[l.length] a
a : α
⊢ foldl (fun b x ↦ f b) a (b :: l) = f^[(b :: l).length] a

Tactic:
| cons b l H =>

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)
d : δ
⊢ ∃ a, g a = d

Tactic:
obtain ⟨a | b, h⟩ := h (inr d)

Goal state after:
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
a : α
h : Sum.map f g (inl a) = inr d
⊢ ∃ a, g a = d

case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ a, g a = d
Module: Mathlib.Order.Basic

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

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

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False

Tactic:
have : ¬ f a = f b := by rename_i h; exact inj.ne h

Goal state after:
case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
this : ¬f a = f b
⊢ False
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
sup_inf_sdiff

Goal state after:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y : α
⊢ x = x
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
sup_inf_sdiff

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

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

pp: case x
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ α

pp: case y
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ α

Tactic:
sup_inf_sdiff

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ ?x✝ ⊓ ?y✝ ⊓ ?x✝ \ ?y✝ = x ⊓ y ⊓ x \ y

case x
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ α

case y
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ α
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
sup_inf_sdiff

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y \ x ≤ y

Tactic:
grw [sdiff_le]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y ≤ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
sup_inf_sdiff

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

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

Tactic:
sup_inf_sdiff

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

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

Tactic:
· calc
      x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by rw [inf_sup_left]
      _ = x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by ac_rfl
      _ = x ⊓ y \ z ⊓ x \ y := by rw [inf_sdiff_self_left, bot_inf_eq, inf_bot_eq, bot_sup_eq]
      _ = x ⊓ (y \ z ⊓ y) ⊓ x \ y := by conv_lhs => rw [← inf_sdiff_left]
      _ = x ⊓ (y \ z ⊓ (y ⊓ x \ y)) := by ac_rfl
      _ = ⊥ := by rw [inf_sdiff_self_right, inf_bot_eq, inf_bot_eq]

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

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

Tactic:
sup_inf_sdiff

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

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

Tactic:
by
          rw [sup_inf_left, sup_inf_right, sup_sdiff_self_right, inf_sup_right, inf_sdiff_sup_right]

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

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

Tactic:
sup_inf_sdiff

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b : α
⊢ f a ⊓ f b ⊔ f a \ f b = f a

Tactic:
sup_inf_sdiff

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b : α
⊢ f a = f a
Module: Mathlib.Order.SymmDiff

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

Tactic:
← symmDiff_sdiff_inf a,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a ∆ b \ (a ⊓ b)) ∆ (a ⊓ b) = a ⊔ b
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
⊢ s.piecewise f g ∈ t.pi t'

Tactic:
intro i ht
  by_cases hs : i ∈ s <;> simp [hf i ht, hg i ht, hs]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ SurjOn id s s

Tactic:
by simp [SurjOn]

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

Goal state before:
pp: G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
n : ℕ
⊢ f (a ^ (n + 1)) = f a ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
n : ℕ
⊢ f (a ^ n * a) = f a ^ (n + 1)
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
n : ℕ
⊢ f (a ^ n * a) = f a ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
n : ℕ
⊢ f (a ^ n * a) = f a ^ n * f a
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
⊢ (∃ b, b ∈ t ∧ p b) → ∃ a, a ∈ s ∧ p (f a)

Tactic:
rintro ⟨b, hb, h⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
b : β
hb : b ∈ t
h : p b
⊢ ∃ a, a ∈ s ∧ p (f a)
Module: Mathlib.Data.Set.Function

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

Tactic:
by rwa [hf hx]

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

Goal state before:
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, ne_eq, h, not_false_eq_true, Function.update_of_ne, one_apply, single,
      zero_apply, ofAdd_zero]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a b : M
n : ℕ
h : a * b = 1
⊢ a ^ n.succ * b ^ n.succ = a ^ n * a * (b * b ^ n)

Tactic:
pow_succ,

Goal state after:
M : Type u_4
inst✝ : Monoid M
a b : M
n : ℕ
h : a * b = 1
⊢ a ^ n * a * b ^ n.succ = a ^ n * a * (b * b ^ n)
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
pow_succ,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a⁻¹ * a⁻¹ ^ n = (a ^ n * a)⁻¹
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✝ : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f x ^ (n + 1) = f (x ^ n * x)

Tactic:
pow_succ,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₁
inst✝² : One M₁
inst✝¹ : Pow M₁ ℕ
inst✝ : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f x ^ n * f x = f (x ^ n * 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✝ : 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 ^ n.succ = f (x ^ ↑n) * f x

Tactic:
pow_succ,

Goal state after:
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 ^ n * f x = f (x ^ ↑n) * f x
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
⊢ b / a = c / a ↔ b = c

Tactic:
by
  rw [div_eq_mul_inv, div_eq_mul_inv]
  exact mul_left_inj _

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
x : G
m n : ℤ
h : x ^ n = 1
⊢ x ^ m = x ^ (m % n + n * (m / n))

Tactic:
Int.emod_add_mul_ediv

Goal state after:
G : Type u_3
inst✝ : Group G
x : G
m n : ℤ
h : x ^ n = 1
⊢ x ^ m = x ^ m
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✝ : Monoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ (n + 1)) = f x ^ n * f x

Tactic:
pow_succ,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₂
inst✝² : One M₂
inst✝¹ : Pow M₂ ℕ
inst✝ : Monoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ n * x) = f x ^ n * f x
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
by
  rw [← div_eq_mul_inv, mul_div_cancel a b]

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 : Surjective 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 ^ n.succ) = f (x ^ n) * f x

Tactic:
pow_succ,

Goal state after:
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 : Surjective 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 ^ n * x) = f (x ^ n) * f x
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
n : ℕ
⊢ c (f ^ (n + 1)) = (c f)^[n + 1]

Tactic:
pow_succ,

Goal state after:
M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
n : ℕ
⊢ c (f ^ n * f) = (c f)^[n + 1]
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
rw [mul_comm, h.div_mul_cancel]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 0 ^ (n + 1) = 0

Tactic:
pow_succ,

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 0 ^ n * 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a : M₀
n✝ m✝ : ℕ
hmn : n✝.le m✝
ha : a ^ n✝ = 0
⊢ a ^ m✝.succ = 0

Tactic:
pow_succ,

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a : M₀
n✝ m✝ : ℕ
hmn : n✝.le m✝
ha : a ^ n✝ = 0
⊢ a ^ m✝ * a = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case succ
M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n✝ : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
n : ℕ
ih : a ^ n = 0 → a = 0
ha : a ^ (n + 1) = 0
⊢ a = 0

Tactic:
pow_succ,

Goal state after:
case succ
M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n✝ : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
n : ℕ
ih : a ^ n = 0 → a = 0
ha : a ^ n * a = 0
⊢ a = 0
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: case zero
α : Type u
inst✝ : NonAssocSemiring α
a : α
⊢ 0 • a = ↑0 * a

Tactic:
rw [zero_nsmul, Nat.cast_zero, zero_mul]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
n✝ : ℕ
a✝ : a ^ n✝ ∣ b ^ n✝
⊢ a ^ (n✝ + 1) ∣ b ^ (n✝ + 1)

Tactic:
pow_succ,

Goal state after:
case succ
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
n✝ : ℕ
a✝ : a ^ n✝ ∣ b ^ n✝
⊢ a ^ n✝ * a ∣ b ^ (n✝ + 1)
Module: Mathlib.Algebra.GroupWithZero.Commute

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
n : ℕ
⊢ r⁻¹ʳ * r⁻¹ʳ ^ n = (r ^ (n + 1))⁻¹ʳ

Tactic:
pow_succ,

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
n : ℕ
⊢ r⁻¹ʳ * r⁻¹ʳ ^ n = (r ^ n * r)⁻¹ʳ
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hc : c ≠ 0
hd : d ≠ 0
h : a / b = c / d
⊢ b ≠ 0

Tactic:
intro hb
    rw [hb, div_zero] at h
    exact div_ne_zero hc hd h.symm

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

Goal state before:
pp: R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = -1
⊢ (-1) ^ (n + 1) = 1

Tactic:
pow_succ,

Goal state after:
R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = -1
⊢ (-1) ^ n * -1 = 1
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = 1
⊢ (-1) ^ (n + 1) = -1

Tactic:
pow_succ,

Goal state after:
R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = 1
⊢ (-1) ^ n * -1 = -1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : -1 ≠ 1
⊢ (-1) ^ n = 1 ↔ Even n

Tactic:
by simp [neg_one_pow_eq_ite, h]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.NatCast

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftStrictMono α
⊢ 1 < 2

Tactic:
by
  rw [← one_add_one_eq_two]
  exact lt_add_one _

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

Goal state before:
pp: α : Type u_1
s : Semiring α
n : ℕ
⊢ OfNat.ofNat (n + 2 + 1) = OfNat.ofNat (n + 2) + 1

Tactic:
change Nat.cast (n + 2 + 1) = Nat.cast (n + 2) + 1

Goal state after:
α : Type u_1
s : Semiring α
n : ℕ
⊢ ↑(n + 2 + 1) = ↑(n + 2) + 1
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ a / b ≤ c / d

Tactic:
by
  rw [div_eq_mul_inv, div_eq_mul_inv]
  gcongr
  exacts [inv_nonneg.2 <| hd.le.trans hdb, hc, hd]

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

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ a < x ∧ b < x ∨ x < a ∧ x < b ↔ x < a ∨ b < x

Tactic:
and_iff_right_of_imp h.trans_lt,

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ b < x ∨ x < a ∧ x < b ↔ x < a ∨ b < x
Module: Mathlib.Algebra.Order.Archimedean.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Archimedean R
x : R
n : ℤ
h : -x ≤ ↑n
⊢ ↑(-n) ≤ x

Tactic:
by simpa [neg_le] using h

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ (k + 1) ≤ b ^ (k + 1)

Tactic:
pow_succ,

Goal state after:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ k * a ≤ b ^ (k + 1)
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ a ≤ b * c ∧ b ≤ a * c ↔ a ≤ b * c ∧ b / a ≤ c

Tactic:
div_le_iff_le_mul'

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ a ≤ b * c ∧ b ≤ a * c ↔ a ≤ b * c ∧ b ≤ a * c
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case mpr
a b : ℤ
n : ℕ
⊢ (∃ x y, ↑n = a * x + b * y) → a.gcd b ∣ n

Tactic:
rintro ⟨x, y, h⟩

Goal state after:
case mpr
a b : ℤ
n : ℕ
x y : ℤ
h : ↑n = a * x + b * y
⊢ a.gcd b ∣ n