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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
⊢ binaryRec' zero bit 0 = zero

Tactic:
rw [binaryRec', binaryRec_zero]

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
w : α
hp : p w
hq : q w hp
H : ∀ (y : α) (hy : p y), q y hy → y = w
⊢ ∃! x, ∃! hx, q x hx

Tactic:
simp only [existsUnique_iff_exists]
  exact ExistsUnique.intro w ⟨hp, hq⟩ fun y ⟨hyp, hyq⟩ ↦ H y hyp hyq

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a : G
⊢ a ^ 1 = a

Tactic:
by rw [zpow_ofNat, pow_one]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Nontrivial (α → β)
f g : α → β
h : f ≠ g
⊢ Nontrivial β

Tactic:
ne_eq,

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Nontrivial (α → β)
f g : α → β
h : ¬f = g
⊢ Nontrivial β
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β γ : Sort u_1
e : α = β
a : α
c : γ
⊢ cast e a ≍ c ↔ a ≍ c

Tactic:
subst e

Goal state after:
α γ : Sort u_1
a : α
c : γ
⊢ cast ⋯ a ≍ c ↔ a ≍ c
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β γ : Sort u_1
e : β = γ
a : α
b : β
⊢ a ≍ cast e b ↔ a ≍ b

Tactic:
subst e

Goal state after:
α β : Sort u_1
a : α
b : β
⊢ a ≍ cast ⋯ b ↔ a ≍ b
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α β : Sort u_1
h : α = β
a : α
b : β
⊢ (Equiv.cast h) a = b ↔ a ≍ b

Tactic:
by
  subst h; simp

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

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

Tactic:
rw [mem_def] at ha ⊢

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

Goal state before:
pp: case refl
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
⊢ leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) ⋯

Tactic:
rw [leRec_self]

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

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
⊢ leRec (motive := fun {n_1} mn ↦
      {motive : (m : ℕ) → m ≤ n_1 → Sort u_1} →
        ((k : ℕ) → (h : k < n_1) → motive (k + 1) h → motive k ⋯) → motive n_1 ⋯ → motive n mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) ⋯ of_succ self =
    self

Tactic:
rw [leRec_self]

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

Goal state before:
pp: ι : Sort u_2
α : Type u_3
f : ι → α
a : ι
b : ↑(range f)
⊢ rangeFactorization f a = b ↔ f a = ↑b

Tactic:
by
  rw [Set.rangeFactorization, ← b.coe_eta b.2, Subtype.ext_iff]

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: α : Type u_2
inst✝ : Subsingleton α
r : α → α → Prop
x✝ : Std.Refl r
⊢ ∀ (a b : α), r a b = ⊤ a b

Tactic:
by simp [rel_of_subsingleton]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ Monotone (f ∘ ⇑ofDual) ↔ Antitone f

Tactic:
monotone_comp_ofDual_iff

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ Antitone f ↔ Antitone f
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: P : ℕ → Prop
h : ∀ (N : ℕ), ∃ n, n > N ∧ P n
this : NoMaxOrder { n // P n }
f : ℕ → { n // P n }
hf : StrictMono f
right✝ : f 0 = ⟨⋯.choose, ⋯⟩
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
exact Exists.intro (fun n ↦ (f n).1) ⟨hf, fun n ↦ (f n).2⟩

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

Goal state before:
pp: case neg
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
h : ∃ n, c < f n
⊢ ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
obtain ⟨N, hN⟩ := h

Goal state after:
case neg
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : c < f N
⊢ ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
Module: Mathlib.Order.Lattice

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Lattice α
a b c : α
h : a ⊓ b = c ∧ a ⊔ b = c
⊢ a = c ∧ b = c

pp: case refine_2
α : Type u
inst✝ : Lattice α
a b c : α
⊢ a = c ∧ b = c → a ⊓ b = c ∧ a ⊔ b = c

Tactic:
· obtain rfl := sup_eq_inf.1 (h.2.trans h.1.symm)
    simpa using h

Goal state after:
case refine_2
α : Type u
inst✝ : Lattice α
a b c : α
⊢ a = c ∧ b = c → a ⊓ b = c ∧ a ⊔ b = c
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
simp_rw [← himp_bot, sup_himp_distrib]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
b : { y // y ≠ x }
⊢ some (((optionSubtype x) e).symm b) = (↑e).symm ↑b

Tactic:
dsimp only [optionSubtype]
  simp

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

Goal state before:
pp: α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ Surjective (Sigma.map f₁ f₂)

Tactic:
simp only [Surjective, Sigma.forall, h₁.forall]

Goal state after:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ ∀ (x : α₁) (b : β₂ (f₁ x)), ∃ a, Sigma.map f₁ f₂ a = ⟨f₁ x, b⟩
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
by rw [sup_inf_inf_sdiff, sup_comm, inf_comm]

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

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

Tactic:
sdiff_sdiff_left,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ (y ⊔ z) = x \ y ⊓ x \ z
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.15
s : (b : Bool) × bif b then β else α
⊢ (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s)
      ((fun s ↦
          match s with
          | ⟨false, a⟩ => inl a
          | ⟨true, b⟩ => inr b)
        s) =
    s

Tactic:
rcases s with ⟨_ | _, _⟩ <;> rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
sdiff_sdiff_left,

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

Goal state before:
pp: case e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ

pp: case e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ c ⊓ bᶜ ⊓ aᶜ = aᶜ ⊓ bᶜ ⊓ c

Tactic:
· congr 1
        rw [inf_comm, inf_assoc]

Goal state after:
case e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ c ⊓ bᶜ ⊓ aᶜ = aᶜ ⊓ bᶜ ⊓ c
Module: Mathlib.Order.SymmDiff

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

Tactic:
· rw [sdiff_inf]
    exact sup_le_sup le_sup_right le_sup_right

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

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

Tactic:
disjoint_comm (b := s),

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

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

Tactic:
intro h
    apply Subset.antisymm
    · rw [← preimage_subset_preimage_iff hs, h]
    · rw [← preimage_subset_preimage_iff ht, h]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.offDiag = ∅ ↔ s.Subsingleton

Tactic:
by
  rw [← not_nonempty_iff_eq_empty, ← not_nontrivial_iff, offDiag_nonempty.not]

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

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

Tactic:
rintro ⟨ht₁, ht₂⟩ i his

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ {i | i ∈ s ∧ p i}.pi t₁
ht₂ : f ∈ {i | i ∈ s ∧ ¬p i}.pi t₂
i : ι
his : i ∈ s
⊢ f i ∈ (fun i ↦ if p i then t₁ i else t₂ i) i
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
⊢ {x | x i ∈ s} = eval i ⁻¹' s

Tactic:
preimage

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
⊢ {x | x i ∈ s} = {x | eval i x ∈ s}
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
hx₂ : x₁ ∈ s₂
heq : f x₁ = f x₁
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)

Tactic:
exact mem_image_of_mem f ⟨hx₁, hx₂⟩

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

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n : ℤ
hnm : n ≤ m
⊢ Int.inductionOn' (motive := fun x ↦ (hnm : x ≤ m) → motive x hnm) (n - 1) m (fun x ↦ base)
      (fun x x_1 x_2 x_3 ↦ ⋯.elim) (fun k hle ih x ↦ pred k hle (ih hle)) ⋯ =
    pred n hnm (Int.leInductionDown base pred n hnm)

Tactic:
inductionOn'_sub_one hnm

Goal state after:
m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n : ℤ
hnm : n ≤ m
⊢ pred n hnm
      (Int.inductionOn' (motive := fun x ↦ (hnm : x ≤ m) → motive x hnm) n m (fun x ↦ base) (fun x x_1 x_2 x_3 ↦ ⋯.elim)
        (fun k hle ih x ↦ pred k hle (ih hle)) hnm) =
    pred n hnm (Int.leInductionDown base pred n hnm)
Module: Mathlib.Algebra.Group.Torsion

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

Tactic:
rw [← zpow_left_inj (a := a) hn, one_zpow]

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
a : G
⊢ a = a⁻¹ ↔ a = 1

Tactic:
← sq_eq_one,

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
a : G
⊢ a = a⁻¹ ↔ a ^ 2 = 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : DivInvOneMonoid G
a : G
⊢ a / 1 = a

Tactic:
by simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
x y : α
⊢ op (x / y) = (op y)⁻¹ * op x

Tactic:
by simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
⊢ ∀ (u₁ u₂ : αˣ), ↑(u₁ / u₂) = ↑u₁ / ↑u₂

Tactic:
by simp [div_eq_mul_inv]

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

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

Tactic:
by
  rw [mul_comm, h.div_mul_left]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst✝ : Group G
a b : G
⊢ (fun b ↦ b⁻¹ * a) ((fun b ↦ a / b) b) = b

Tactic:
by simp [div_eq_mul_inv]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst✝ : Group G
a b : G
⊢ (fun b ↦ a / b) ((fun b ↦ b⁻¹ * a) b) = b

Tactic:
by simp [div_eq_mul_inv]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst✝ : Group G
a b : G
⊢ (fun b ↦ b * a) ((fun b ↦ b / a) b) = b

Tactic:
by simp [div_eq_mul_inv]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst✝ : Group G
a b : G
⊢ (fun b ↦ b / a) ((fun b ↦ b * a) b) = b

Tactic:
by simp [div_eq_mul_inv]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
⊢ a * b = 0

Tactic:
have : Decidable (a = 0) := Classical.propDecidable (a = 0)

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
⊢ a * b = 0
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1) = 2

Tactic:
apply congrArg

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 = 2
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1 + 1) = 3

Tactic:
apply congrArg

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 + 1 = 3
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
⊢ (if x * y = 0 then 0 else 1) = (if x = 0 then 0 else 1) * if y = 0 then 0 else 1

Tactic:
by split_ifs <;> simp_all

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1 + 1 + 1) = 4

Tactic:
apply congrArg

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 + 1 + 1 = 4
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑n + 1 - 1

Tactic:
add_sub_cancel_right,

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Ring R
n : ℤ
⊢ ↑(n ^ 0) = ↑n ^ 0

Tactic:
simp [_root_.pow_succ, *]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Ring R
n : ℤ
n✝ : ℕ
a✝ : ↑(n ^ n✝) = ↑n ^ n✝
⊢ ↑(n ^ (n✝ + 1)) = ↑n ^ (n✝ + 1)

Tactic:
simp [_root_.pow_succ, *]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b : α
⊢ (∃ c, b = c * a) → a ∣ b

Tactic:
rintro ⟨c, rfl⟩

Goal state after:
α : Type u_1
inst✝ : CommSemigroup α
a c : α
⊢ a ∣ c * a
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_3
inst✝ : Ring α
⊢ IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α

Tactic:
isCancelMulZero_iff_isDomain_or_subsingleton

Goal state after:
α : Type u_3
inst✝ : Ring α
⊢ IsDomain α ∨ Subsingleton α ↔ IsDomain α ∨ Subsingleton α
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
⊢ a / b = 0 ↔ a = 0 ∨ b = 0

Tactic:
by simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + b * ↑u₂⁻¹ = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₁ * b * (↑u₂⁻¹ * ↑u₁⁻¹)

Tactic:
rw [mul_comm (↑u₁ * b), mul_comm b]

Goal state after:
α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℤ
b : M
⊢ ↑n • b = n • b

Tactic:
cases n with
  | ofNat => simp [Nat.cast_smul_eq_nsmul]
  | negSucc => simp [add_smul, Nat.cast_smul_eq_nsmul]

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

Goal state before:
pp: α : Type u
inst✝⁴ : MulOneClass α
inst✝³ : Preorder α
inst✝² : ExistsMulOfLE α
a b : α
inst✝¹ : MulLeftMono α
inst✝ : MulLeftReflectLE α
⊢ (∃ c, 1 ≤ c ∧ a * c = b) → a ≤ b

Tactic:
rintro ⟨c, hc, rfl⟩

Goal state after:
α : Type u
inst✝⁴ : MulOneClass α
inst✝³ : Preorder α
inst✝² : ExistsMulOfLE α
a : α
inst✝¹ : MulLeftMono α
inst✝ : MulLeftReflectLE α
c : α
hc : 1 ≤ c
⊢ a ≤ a * c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE

Goal state before:
pp: α : Type u
inst✝⁴ : MulOneClass α
inst✝³ : Preorder α
inst✝² : ExistsMulOfLE α
a b : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulLeftReflectLT α
⊢ (∃ c, 1 < c ∧ a * c = b) → a < b

Tactic:
rintro ⟨c, hc, rfl⟩

Goal state after:
α : Type u
inst✝⁴ : MulOneClass α
inst✝³ : Preorder α
inst✝² : ExistsMulOfLE α
a : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulLeftReflectLT α
c : α
hc : 1 < c
⊢ a < a * c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ 1 < a / b ↔ b < a

Tactic:
rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ a / b < 1 ↔ a < b

Tactic:
rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

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

Goal state before:
pp: α : Type u_1
s : Grind.CommRing α
n : ℕ
⊢ ↑(Int.negSucc n) = -↑(n + 1)

Tactic:
by
      rw [Int.negSucc_eq, Grind.Ring.intCast_neg,
        Grind.Ring.intCast_natCast_add_one, Grind.Semiring.natCast_succ]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ (y ⊓ z)) * (x ⊔ y ⊓ z)

Tactic:
inf_mul_sup x (y ⊓ z),

Goal state after:
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ x * (y ⊓ z)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone fun a ↦ f a ^ (n + 1)

Tactic:
simp_rw [pow_succ]

Goal state after:
β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone fun a ↦ f a ^ n * f a
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: m x : ℤ
h1 : m ∣ x
h2 : |x| < m
h : ¬x = 0
this : m.natAbs ≤ x.natAbs
⊢ False

Tactic:
rw [Int.abs_eq_natAbs] at h2

Goal state after:
m x : ℤ
h1 : m ∣ x
h2 : ↑x.natAbs < m
h : ¬x = 0
this : m.natAbs ≤ x.natAbs
⊢ False
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : Mul α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b : α
⊢ (∃ c, b = a * c) → a ≤ b

Tactic:
rintro ⟨c, rfl⟩

Goal state after:
α : Type u
inst✝² : Mul α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a c : α
⊢ a ≤ a * c
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
| a ^ ↑1

Tactic:
← hmn,

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
| a ^ ↑(m.gcd n)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
| b ^ ↑1

Tactic:
← hmn,

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
| b ^ ↑(m.gcd n)
Module: Mathlib.Algebra.Group.WithOne.Defs

Goal state before:
pp: α : Type u
inst✝ : Semigroup α
a b c : α
⊢ ↑a * ↑b * ↑c = ↑a * (↑b * ↑c)

Tactic:
← coe_mul,

Goal state after:
α : Type u
inst✝ : Semigroup α
a b c : α
⊢ ↑(a * b * c) = ↑(a * (b * c))
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝¹ + ↑a✝

Tactic:
rw [← WithBot.coe_add, WithBot.coe_le_coe]
    exact le_add_self

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

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x : M
⊢ exp x = 1 ↔ x = 0

Tactic:
by
  rw [← exp_zero, exp_inj]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : b ≤ a
⊢ a + a - (b + b) = a - b + (a - b)

Tactic:
· exact (tsub_add_tsub_comm h h).symm

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

Goal state before:
pp: α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
⊢ AddLECancellable ↑a

Tactic:
rintro (_ | b) (_ | c)
  · simp [none_eq_bot]
  · simp [none_eq_bot]
  · simp [some_eq_coe, ← coe_add, none_eq_bot]
  · simpa [none_eq_bot, some_eq_coe, ← coe_add] using fun a ↦ ha a

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

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑a✝¹ * ↑a✝ ≤ ↑(a✝¹ * c)

Tactic:
← coe_mul,

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑(a✝¹ * a✝) ≤ ↑(a✝¹ * c)
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ Multiplicative.toAdd (unzero hx) < a ↔ x < exp a

Tactic:
← lt_ofAdd_iff hx,

Goal state after:
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ x < ↑(Multiplicative.ofAdd a) ↔ x < exp a
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑d ≤ a ↔ d ≤ ⌊a⌋₊

Tactic:
le_floor_iff ha

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑d ≤ a ↔ ↑d ≤ a