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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n = 0 → b = true
ih : motive n
h' : n = 0
⊢ Nat.bit b 0 = Nat.bit true 0

Tactic:
h h'

Goal state after:
motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n = 0 → b = true
ih : motive n
h' : n = 0
⊢ Nat.bit true 0 = Nat.bit true 0
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < 1 → npowRec' (2 * m_1) m = npowRec' m_1 (m * m)
⊢ npowRec' (2 * 1) m = npowRec' 1 (m * m)

Tactic:
simp [npowRec']

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < 1 → m_1 ≠ 0 → m * npowRec' m_1 m = npowRec' m_1 m * m
k0 : 1 ≠ 0
⊢ m * npowRec' 1 m = npowRec' 1 m * m

Tactic:
simp [npowRec']

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

Goal state before:
pp: case one
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
hk : 1 ≠ 0
⊢ Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y) (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) 1
      m n =
    m * npowRec' 1 n

Tactic:
simp [npowRec']

Goal state after:
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 * a

Tactic:
← pow_add,

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

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

Tactic:
← pow_add,

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

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

Tactic:
← pow_add,

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ = g₁ ∘ f ∘ g₂

Tactic:
rw [h₂.comp_eq_id, comp_id]

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

Goal state before:
pp: p : Prop
α : Sort u_1
inst✝ : Nonempty α
P : α → Prop
f : p → α
a : p
h : P (f a)
⊢ P (sometimes f)

Tactic:
by
  rwa [sometimes_eq]

Goal state after:
Module: Mathlib.Data.FunLike.Equiv

Goal state before:
pp: case mp
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst✝ : EquivLike E α β
e : E
b : β
a : α
⊢ inv e b = a → b = e a

Tactic:
rintro ⟨_, rfl⟩

Goal state after:
case mp
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst✝ : EquivLike E α β
e : E
b : β
⊢ b = e (inv e b)
Module: Mathlib.Data.FunLike.Equiv

Goal state before:
pp: case mpr
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst✝ : EquivLike E α β
e : E
b : β
a : α
⊢ b = e a → inv e b = a

Tactic:
rintro ⟨_, rfl⟩

Goal state after:
case mpr
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst✝ : EquivLike E α β
e : E
a : α
⊢ inv e (e a) = a
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : Std.Refl r
f : α → β
hf : Surjective f
x : β
⊢ Relation.Map r f f x x

Tactic:
obtain ⟨y, rfl⟩ := hf x
    exact ⟨y, y, refl y, rfl, rfl⟩

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
| @tail d e _ hde ih =>

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

Goal state before:
pp: α : Type u_3
β : Type u_4
b : β
f : α → β
a : Option α
⊢ Option.elim' b f a = a.elim b f

Tactic:
cases a <;> rfl

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) → Monoid (f i)
⊢ ∀ (n : ℕ) (x : (i : I) → f i), x ^ (n + 1) = x ^ n * x

Tactic:
by intros; ext; exact Monoid.npow_succ _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
f : α → β
a : Option α
⊢ a.casesOn' b f = a.elim b f

Tactic:
cases a <;> rfl

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

Goal state before:
pp: f : Bool → Bool
x : Bool
⊢ f (f (f x)) = f x

Tactic:
by
  cases h₁ : f true <;> cases h₂ : f false <;> grind [cases Bool]

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

Goal state before:
pp: case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} ↦ next)
⊢ Surjective (leRecOn ⋯ fun {k} ↦ next)

Tactic:
intro x
    obtain ⟨w, rfl⟩ := Hnext _ x
    obtain ⟨x, rfl⟩ := ih w
    refine ⟨x, ?_⟩
    rw [leRecOn_succ]

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

Goal state before:
pp: case inr
k : ℕ
hk : k > 0
⊢ 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)

Tactic:
· have hk0 : 0 < 2 * k ^ 2 := Nat.mul_pos Nat.two_pos (Nat.pow_pos hk)
    calc 2 * k ^ 2
      _ < 2 * k ^ 2 + 2 * k ^ 2 := Nat.lt_add_of_pos_left hk0
      _ = (2 * k) ^ 2 := by rw [Nat.mul_pow, ← Nat.add_mul]
      _ ≤ (2 ^ k) ^ 2 := Nat.pow_le_pow_left (Nat.mul_le_pow (by decide : 2 ≠ 1) _) 2
      _ = 2 ^ (2 * k) := (Nat.pow_mul' _ _ _).symm

Goal state after:
Module: Mathlib.Tactic.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst✝¹ : CanLift α β coeβα condβα
inst✝ : CanLift γ δ coeδγ condδγ
⊢ ∀ (x : α × γ), condβα x.fst ∧ condδγ x.snd → ∃ y, map coeβα coeδγ y = x

Tactic:
by
    rintro ⟨x, y⟩ ⟨hx, hy⟩
    rcases CanLift.prf (β := β) x hx with ⟨x, rfl⟩
    rcases CanLift.prf (β := δ) y hy with ⟨y, rfl⟩
    exact ⟨(x, y), by simp⟩

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

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

Tactic:
← Nat.sub_add_cancel hx,

Goal state after:
case refine_1
α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
h : Monotone fun n ↦ f (n + k)
x : ℕ
hx : x ∈ {x | k ≤ x}
y : ℕ
hy : y ∈ {x | k ≤ x}
hle : x ≤ y
⊢ f (x - k + k) ≤ f y
Module: Mathlib.Order.Lattice

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

Tactic:
sup_eq_right.2 hxy

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊔ y) = f x ⊔ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ f y = f y
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ≤ aᶜ ↔ a = ⊥

Tactic:
le_compl_iff_disjoint_left,

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ Disjoint a a ↔ a = ⊥
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case none.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNoneAux x)) = none
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
rw [removeNoneAux_some _ ⟨_, h2⟩] at h1

Goal state after:
case none.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (e (some x)) = none
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
h1 : some x = e.symm (some a)
⊢ False ↔ e.symm none = some x

Tactic:
simp [h1]

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
a : α
⊢ (fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩)) ((fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e)) (some a)) =
    some a

Tactic:
| some a =>

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

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.17
β : Type ?u.16
inst✝ : IsEmpty β
s : α ⊕ β
⊢ inl (Sum.elim id (fun a ↦ isEmptyElim a) s) = s

Tactic:
rcases s with (_ | x)
    · rfl
    · exact isEmptyElim x

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

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.12
β : Option α → Type u_9
f : (a : Option α) → β a
a : Option α
⊢ (fun x a ↦ Option.casesOn a x.fst x.snd) ((fun f ↦ (f none, fun a ↦ f (some a))) f) a = f a

Tactic:
cases a <;> rfl

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
r a : α
⊢ swapCore a a r = r

Tactic:
unfold swapCore
  split_ifs <;> simp [*]

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

Goal state before:
pp: case mpr.inr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
hai : ¬a ∈ {i}
has : a ∈ s
⊢ a ∈ Set.image (⇑(swap i j)) s

Tactic:
exact ⟨a, has, swap_apply_of_ne_of_ne hai (ne_of_mem_of_not_mem has hj)⟩

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)

Tactic:
← symmDiff_assoc,

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b ∆ c = b ∆ a ∆ c
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ (⟨x, hx⟩, ⟨y, hy⟩) ∈ (Prod.map (fun x ↦ ↑x) fun x ↦ ↑x) ⁻¹' diagonal α ↔ (⟨x, hx⟩, ⟨y, hy⟩) ∈ diagonal ↑s

Tactic:
simp [Set.diagonal]

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

Goal state before:
pp: case mp
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
⊢ x ∈ toPullbackDiag f '' s → x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

Tactic:
rintro ⟨x, hx, rfl⟩

Goal state after:
case mp
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : X
hx : x ∈ s
⊢ toPullbackDiag f x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Unique ι
t : (i : ι) → Set (α i)
⊢ uniqueElim ⁻¹' univ.pi t = t default

Tactic:
by ext; simp [Unique.forall_iff]

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

Goal state before:
pp: case mpr
α : Type u_1
s t u : Set α
h : s ∩ t ⊆ s ∩ u
x : ↑s
a : x ∈ val ⁻¹' t
⊢ x ∈ val ⁻¹' u

Tactic:
exact (h ⟨x.2, a⟩).2

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Injective (image f) ↔ Injective f

Tactic:
refine ⟨fun h x x' hx => ?_, Injective.image_injective⟩
  rw [← singleton_eq_singleton_iff]; apply h
  rw [image_singleton, image_singleton, hx]

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

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
⊢ (∃ x, (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) → ∃ x, ∀ (i : ι), i ∈ s → x i ∈ t i

Tactic:
rintro ⟨x, hx, rfl⟩

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
x : (x : ι) → α x
hx : ∀ (i : ι), i ∈ s → x i ∈ t i
⊢ ∃ x, ∀ (i : ι), i ∈ s → x i ∈ t i
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : Injective (imageFactorization f s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
x✝ : f x = f y
⊢ imageFactorization f s ⟨x, hx⟩ = imageFactorization f s ⟨y, hy⟩

Tactic:
simpa [imageFactorization]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
⊢ ∃ e, range f = graphOn (⇑e) univ

Tactic:
obtain ⟨e₂, he₂⟩ := exists_range_eq_graphOn_univ (f := Equiv.prodComm _ _ ∘ f) (by simpa) <|
    by simp [hf]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(Equiv.prodComm β γ) ∘ f) = graphOn e₂ univ
⊢ ∃ e, range f = graphOn (⇑e) univ
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
m n : ℕ
a : M
h : m ≤ n
⊢ a ^ m * a ^ (n - m) = a ^ n

Tactic:
← pow_add,

Goal state after:
M : Type u_4
inst✝ : Monoid M
m n : ℕ
a : M
h : m ≤ n
⊢ a ^ (m + (n - m)) = a ^ n
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
m n : ℕ
a : M
h : m ≤ n
⊢ a ^ (n - m) * a ^ m = a ^ n

Tactic:
← pow_add,

Goal state after:
M : Type u_4
inst✝ : Monoid M
m n : ℕ
a : M
h : m ≤ n
⊢ a ^ (n - m + m) = a ^ n
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
mul_div_cancel_right

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
m n : ℕ
h : n ≤ m
⊢ a ^ (m - n) * a ^ n = a ^ m

Tactic:
← pow_add,

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
m n : ℕ
h : n ≤ m
⊢ a ^ (m - n + n) = a ^ m
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
Int.neg_add_cancel_right

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (-↑(n + 1)) = (a ^ (n + 1))⁻¹
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
y : M
⊢ (fun x ↦ a * x) (↑h.unit⁻¹ * y) = y

Tactic:
simp [← mul_assoc]

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ swap i j * (swap i j * σ) = σ

Tactic:
simp [← mul_assoc]

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:
by
  rw [div_div_eq_mul_div]
  exact mul_self_div_self a

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

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

Tactic:
by
  by_cases hm : m = 0
  · simp [hm]
  by_cases hn : n = 0
  · simp [hn]
  by_cases ha : a = 0
  · subst a
    simp only [false_or, not_true, Ne, hm, hn, false_and, or_false] at h
    rw [zero_zpow _ h, zero_zpow _ hm, zero_mul]
  · exact zpow_add₀ ha m n

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

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n✝ : ℕ
h : ↑(m + 1) = ↑(n✝ + 1)
⊢ m + 1 = n✝ + 1

Tactic:
simp only [Nat.cast_succ, add_right_cancel_iff] at h; rwa [ih]

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑n = -↑(m + 1) + ↑n + ↑m.succ

Tactic:
add_assoc,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑n = -↑(m + 1) + (↑n + ↑m.succ)
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
⊢ a ^ 2 + 2 * a * b + b ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b

Tactic:
add_assoc,

Goal state after:
α : Type u
inst✝ : CommSemiring α
a b : α
⊢ a ^ 2 + (2 * a * b + b ^ 2) = a ^ 2 + b ^ 2 + 2 * a * b
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: m✝ n m : ℤ
⊢ IsSquare m ↔ sqrt m * sqrt m = m

Tactic:
simp_rw [← exists_mul_self m, IsSquare, eq_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
a b : α
x✝ : MulOpposite.op a ∣ MulOpposite.op b
c : αᵐᵒᵖ
hc : MulOpposite.op b = MulOpposite.op a * c
⊢ b = MulOpposite.unop c * a

Tactic:
by simpa using congrArg MulOpposite.unop hc

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
m n : ℕ
a : α
h : m ≤ n
⊢ a ^ n = a ^ m * a ^ (n - m)

Tactic:
← pow_add,

Goal state after:
α : Type u_1
inst✝ : Monoid α
m n : ℕ
a : α
h : m ≤ n
⊢ a ^ n = a ^ (m + (n - m))
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: case cons
c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ IsChain (fun x1 x2 ↦ x1 → x2) (b :: l) → (l.getLastD b → a) → (a ↔ b) ∧ (b :: l).TFAE
h_chain : (a → b) ∧ (b → c) ∧ IsChain (fun x1 x2 ↦ x1 → x2) (c :: l)
h_last : l.getLastD c → a
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE

Tactic:
rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩

Goal state after:
case cons
c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ IsChain (fun x1 x2 ↦ x1 → x2) (b :: l) → (l.getLastD b → a) → (a ↔ b) ∧ (b :: l).TFAE
h_last : l.getLastD c → a
ab : a → b
bc : b → c
ch : IsChain (fun x1 x2 ↦ x1 → x2) (c :: l)
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) * a ^ n = a ^ m

Tactic:
← pow_add,

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n + n) = a ^ m
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: A : Type u_5
inst✝ : AddGroupWithOne A
f : ℤ →+ A
h1 : f 1 = 1
⊢ f 1 = (castAddHom A) 1

Tactic:
simp [h1]

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
⊢ Even a ↔ 2 ∣ a

Tactic:
by simp [Even, Dvd.dvd, two_mul]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 =
    a ^ (2 * k + 1) * a ^ 2 + b ^ (2 * k + 1) * a ^ 2 + b ^ (2 * k + 3)

Tactic:
← pow_add,

Goal state after:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 =
    a ^ (2 * k + 1 + 2) + b ^ (2 * k + 1) * a ^ 2 + b ^ (2 * k + 3)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case h
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ -a = -(2 * k) + -(2 * 1) + 1

Tactic:
add_assoc,

Goal state after:
case h
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ -a = -(2 * k) + (-(2 * 1) + 1)
Module: Mathlib.Algebra.Order.Sub.Defs

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

Tactic:
add_assoc,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a + (c + (b - c))
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ a + b ≤ d + c + (a - c + (b - d))

Tactic:
add_assoc,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ a + b ≤ d + (c + (a - c + (b - d)))
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b ≤ a + c + (b - a - c)

Tactic:
add_assoc,

Goal state after:
case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b ≤ a + (c + (b - a - c))
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : IsMulCommutative α
inst✝ : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : (fun x ↦ x * a) b = (fun x ↦ x * a) c
⊢ a * b = a * c

Tactic:
rwa [mul_comm' a, mul_comm' a]

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

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b

Tactic:
simpa only [mul_zero] using mul_le_mul_of_nonneg_left hb ha

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

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b ≤ 0

Tactic:
simpa only [mul_zero] using mul_le_mul_of_nonneg_left hb ha

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + b + b * c ≤ c
⊢ 1 + a + (b + b * c) ≤ 1 + c

Tactic:
add_assoc,

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + b + b * c ≤ c
⊢ 1 + (a + (b + b * c)) ≤ 1 + c
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + c + b * c ≤ b
⊢ 1 + a + (c + b * c) ≤ 1 + b

Tactic:
add_assoc,

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + c + b * c ≤ b
⊢ 1 + (a + (c + b * c)) ≤ 1 + b
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : b + b * c ≤ a + c
⊢ 1 + (b + b * c) ≤ 1 + c + a

Tactic:
add_assoc,

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : b + b * c ≤ a + c
⊢ 1 + (b + b * c) ≤ 1 + (c + a)
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : c + b * c ≤ a + b
⊢ 1 + (c + b * c) ≤ 1 + b + a

Tactic:
add_assoc,

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : c + b * c ≤ a + b
⊢ 1 + (c + b * c) ≤ 1 + (b + a)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
⊢ a ≤ b / c ↔ c ≤ b / a

Tactic:
le_div_iff₀ ha,

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
⊢ a ≤ b / c ↔ c * a ≤ b