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 * x) (y ^ n * y)

Tactic:
exact ih.mul_right h

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a✝ b✝ a b c : G
h : (fun x ↦ a * x) b = (fun x ↦ a * x) c
⊢ b = c

Tactic:
rw [← inv_mul_cancel_left a b, show a * b = a * c from h, inv_mul_cancel_left]

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

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

Tactic:
exact nontrivial_of_ne _ _ h

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

Goal state before:
pp: case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f x = g y
z : α
⊢ f z = g z

pp: case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f = g
⊢ f x = g y

Tactic:
· rwa [Subsingleton.elim x z, Subsingleton.elim y z] at h

Goal state after:
case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f = g
⊢ f x = g y
Module: Mathlib.Logic.Function.Basic

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

Tactic:
by
  ext a
  by_cases h₃ : ∃ b, f₂₃ b = a
  · obtain ⟨b, rfl⟩ := h₃
    rw [Injective.extend_apply h₂₃]
    by_cases h₂ : ∃ c, f₁₂ c = b
    · obtain ⟨c, rfl⟩ := h₂
      rw [h₁₂.extend_apply]
      exact (h₂₃.comp h₁₂).extend_apply _ _ _
    · rw [extend_apply' _ _ _ h₂, extend_apply', comp_apply]
      exact fun h ↦ h₂ (Exists.casesOn h fun c hc ↦ Exists.intro c (h₂₃ hc))
  · rw [extend_apply' _ _ _ h₃, extend_apply']
    exact fun h ↦ h₃ (Exists.casesOn h fun c hc ↦ Exists.intro (f₁₂ c) (hc))

Goal state after:
Module: Mathlib.Lean.Meta.CongrTheorems

Goal state before:
pp: α β : Sort u
inst✝ : FastSubsingleton α
h₂ : α = β
a : α
b : β
⊢ a ≍ b

Tactic:
have : Subsingleton α := FastSubsingleton.inst

Goal state after:
α β : Sort u
inst✝ : FastSubsingleton α
h₂ : α = β
a : α
b : β
this : Subsingleton α
⊢ a ≍ b
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 - k + k) ≤ f (y - k + k)

Tactic:
← Nat.sub_le_sub_iff_right hy

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 - k ≤ y - k
⊢ f (x - k + k) ≤ f (y - k + k)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case neg
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
hlt : f 1 < f 0
⊢ ∃ n_1, n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1

Tactic:
let g (i : ℕ) := f (i + 1)

Goal state after:
case neg
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
hlt : f 1 < f 0
g : ℕ → ℕ := fun i ↦ f (i + 1)
⊢ ∃ n_1, n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ s ⊂ {x} ↔ s = ∅

Tactic:
rw [ssubset_iff_subset_ne, subset_singleton_iff_eq, or_and_right, and_not_self_iff, or_false,
    and_iff_left_iff_imp]
  exact fun h => h ▸ empty_ne_singleton _

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

Goal state before:
pp: f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
hc : ∀ (n : ℕ), f n ≤ c
⊢ ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
induction c with
  | zero => use 0, 0, fun n _ ↦ Nat.eq_zero_of_le_zero (hc n)
  | succ c ih =>
    by_cases! h : ∀ n, f n ≤ c
    · exact ih h
    · obtain ⟨N, hN⟩ := h
      replace hN : f N = c + 1 := by specialize hc N; lia
      use c + 1, N; intro n hn
      specialize mono_f hn; specialize hc n; lia

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : Max α
inst✝³ : Min α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : DistribLattice β
f : α → β
hf_inj : 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
a b c : α
⊢ f (a ⊔ b) ⊓ f (a ⊔ c) ≤ f (a ⊔ b ⊓ c)

Tactic:
map_sup,

Goal state after:
α : Type u
β : Type v
inst✝⁴ : Max α
inst✝³ : Min α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : DistribLattice β
f : α → β
hf_inj : 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
a b c : α
⊢ (f a ⊔ f b) ⊓ f (a ⊔ c) ≤ f (a ⊔ b ⊓ c)
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : Max α
inst✝³ : Min α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : DistribLattice β
f : α → β
hf_inj : 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
a b c : α
⊢ (f a ⊔ f b) ⊓ f (a ⊔ c) ≤ f (a ⊔ b ⊓ c)

Tactic:
map_sup,

Goal state after:
α : Type u
β : Type v
inst✝⁴ : Max α
inst✝³ : Min α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : DistribLattice β
f : α → β
hf_inj : 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
a b c : α
⊢ (f a ⊔ f b) ⊓ (f a ⊔ f c) ≤ f (a ⊔ b ⊓ c)
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : Max α
inst✝³ : Min α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : DistribLattice β
f : α → β
hf_inj : 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
a b c : α
⊢ (f a ⊔ f b) ⊓ (f a ⊔ f c) ≤ f (a ⊔ b ⊓ c)

Tactic:
map_sup,

Goal state after:
α : Type u
β : Type v
inst✝⁴ : Max α
inst✝³ : Min α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : DistribLattice β
f : α → β
hf_inj : 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
a b c : α
⊢ (f a ⊔ f b) ⊓ (f a ⊔ f c) ≤ f a ⊔ f (b ⊓ c)
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⇨ b ⇨ c ↔ d ≤ a ⊓ b ⇨ c

Tactic:
by simp_rw [le_himp_iff, inf_assoc]

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

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

Tactic:
le_bot_iff

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a = ⊥ ↔ a = ⊥
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
refine ((compl_anti compl_sup_compl_le).trans (compl_sup_distrib _ _).le).antisymm ?_
  rw [le_compl_iff_disjoint_right, disjoint_assoc, disjoint_compl_compl_left_iff,
    disjoint_left_comm, disjoint_compl_compl_left_iff, ← disjoint_assoc, inf_comm]
  exact disjoint_compl_right

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedCoheytingAlgebra β
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 c : α
⊢ f a \ f b ≤ f c ↔ f a ≤ f (b ⊔ c)

Tactic:
map_sup,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedCoheytingAlgebra β
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 c : α
⊢ f a \ f b ≤ f c ↔ f a ≤ f b ⊔ f c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
⊢ CoheytingAlgebra α

Tactic:
by
  let generalizedCoheytingAlgebra := e.generalizedCoheytingAlgebra
  let top := e.top
  let hnot := e.hnot
  apply e.injective.coheytingAlgebra <;> intros <;> first | rfl | exact e.apply_symm_apply _

Goal state after:
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 ⊓ b ⊔ a \ b) = f a

Tactic:
map_sup,

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 ⊓ b) ⊔ f (a \ b) = f a
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✝⁵ : Top α
inst✝⁴ : Bot α
inst✝³ : Compl α
inst✝² : SDiff α
inst✝¹ : HImp α
inst✝ : BooleanAlgebra β
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_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b : α
⊢ f b ⊔ (f a)ᶜ = f (b ⊔ aᶜ)

Tactic:
map_sup,

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝⁹ : Max α
inst✝⁸ : Min α
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Top α
inst✝⁴ : Bot α
inst✝³ : Compl α
inst✝² : SDiff α
inst✝¹ : HImp α
inst✝ : BooleanAlgebra β
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_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b : α
⊢ f b ⊔ (f a)ᶜ = f b ⊔ f aᶜ
Module: Mathlib.Data.Set.Image

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

Tactic:
simp_rw [Set.ext_iff, Set.mem_range, Set.mem_singleton_iff]

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

Goal state before:
pp: X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' {p | p.fst = p.snd} ↔ fst ⟨(p₁, p₂), he⟩ = snd ⟨(p₁, p₂), he⟩

Tactic:
Subtype.ext_iff,

Goal state after:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' {p | p.fst = p.snd} ↔ ↑(fst ⟨(p₁, p₂), he⟩) = ↑(snd ⟨(p₁, p₂), he⟩)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ StrictMono (rangeSplitting f)

Tactic:
refine fun x y h ↦ hf.reflect_lt ?_
  simpa [apply_rangeSplitting f]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ univ.pi t = {a} ↔ ∀ (i : ι), t i = {a i}

Tactic:
classical
  simp only [eq_singleton_iff_unique_mem]
  refine ⟨fun ⟨h₁, h₂⟩ i => ⟨by grind, fun x hx => ?_⟩, by grind⟩
  rw [← h₂ _ fun j _ => (update_mem_pi_iff_of_mem h₁).mpr (fun _ => hx) j trivial, update_self]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
t : (i : ι) → Set (α i)
⊢ ⇑(piCongrLeft α f) ⁻¹' univ.pi t = univ.pi fun i ↦ t (f i)

Tactic:
simpa [f.surjective.range_eq] using piCongrLeft_preimage_pi f univ t

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst✝³ : EquivLike F α β
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
h1 : M ≃* N
h2 : N ≃* P
x y : M
⊢ h2 (h1 x * h1 y) = h2 (h1 x) * h2 (h1 y)

Tactic:
map_mul

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst✝³ : EquivLike F α β
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
h1 : M ≃* N
h2 : N ≃* P
x y : M
⊢ h2 (h1 x) * h2 (h1 y) = h2 (h1 x) * h2 (h1 y)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : MapsTo (⇑g) s t
⊢ MapsTo (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)

Tactic:
rintro _ ⟨a, ha, rfl⟩; exact ⟨_, h ha, by simp_rw [Function.comp_apply, extendDomain_apply_image]⟩

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

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

Tactic:
by rw [← zpow_add_one, Int.sub_add_cancel]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
by
  rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm,
    hd.div_mul_cancel]

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
this : Decidable (a = 0)
ha : ¬a = 0
⊢ a * 0 = 0

Tactic:
mul_zero

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : ¬a = 0
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
mul_zero

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

Goal state before:
pp: n : ℕ
S : Type u_5
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
N : ℕ
hN : x ^ N = 0
⊢ x ^ (n * N) * 0 = 0

Tactic:
mul_zero

Goal state after:
n : ℕ
S : Type u_5
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
N : ℕ
hN : x ^ N = 0
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
mul_zero

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

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

Tactic:
by
  rw [mul_eq_right, swap_eq_one_iff]

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

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

Tactic:
mul_zero

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

Goal state before:
pp: case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a = 0
⊢ 0 * 0 * 0 = 0

Tactic:
mul_zero

Goal state after:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
R : Type v
inst✝¹ : MulZeroClass α
inst✝ : HasDistribNeg α
⊢ 0 = 0 * 0

Tactic:
mul_zero

Goal state after:
α : Type u
R : Type v
inst✝¹ : MulZeroClass α
inst✝ : HasDistribNeg α
⊢ 0 = 0
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ a * 0 = 0

Tactic:
mul_zero

Goal state after:
α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ 0 = 0
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : IsLeftRegular r
r' : R
eq : r * r' = 0
⊢ 0 = r * 0

Tactic:
mul_zero

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
r₁ r₂ : R
eq : (fun x ↦ x * r) r₁ = (fun x ↦ x * r) r₂
⊢ (r₁ - r₂) * r = 0

Tactic:
simp_rw [sub_mul, eq, sub_self]

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

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

Tactic:
mul_zero

Goal state after:
case zero
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
⊢ 0 = 0
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
h : f 1 = 0
x : α
⊢ f x * 0 = 0

Tactic:
mul_zero

Goal state after:
α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
h : f 1 = 0
x : α
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Commute

Goal state before:
pp: case neg.inl
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
ha : ¬IsUnit a
⊢ 0 = b⁻¹ʳ * 0

Tactic:
mul_zero

Goal state after:
case neg.inl
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
ha : ¬IsUnit a
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b✝ c : G₀
m n : ℕ
a b : G₀
h : a ≠ 0 ∧ b ≠ 0
⊢ a * b ≠ 0

Tactic:
exact (Units.mk0 a h.1 * Units.mk0 b h.2).ne_zero

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

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝⁴ : Add S
inst✝³ : Mul S
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : RightDistribClass R
add : ∀ (x y : R), f (x + y) = f x + f y
mul : ∀ (x y : R), f (x * y) = f x * f y
x y z : R
⊢ (f x + f y) * f z = f x * f z + f y * f z

Tactic:
by simp only [← add, ← mul, right_distrib]

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
⊢ a * 0 = 0

Tactic:
mul_zero

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
⊢ 0 = 0
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a + b ≤ c
⊢ b + a ≤ c

Tactic:
by rwa [add_comm]

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

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
h : a + c < b
⊢ c + a < b

Tactic:
by rwa [add_comm]

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

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a⁻¹ < b / c ↔ c < a * b

Tactic:
rw [div_eq_mul_inv, lt_mul_inv_iff_mul_lt, inv_mul_lt_iff_lt_mul]

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ b < c / a ↔ a * b < c

Tactic:
lt_div_iff_mul_lt,

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ b * a < c ↔ a * b < c
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
add_le_add_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
toIsOrderedAddMonoid : IsOrderedAddMonoid α := { add_le_add_left := add_le_add_left }
le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
a b c : α
h : b + a ≤ c + a
⊢ b ≤ c

Tactic:
rw [add_comm _ a, add_comm _ a] at h; exact le_of_add_le_add_left a b c h

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

Goal state before:
pp: M₀ : Type u_2
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : PartialOrder M₀
a b c d : M₀
inst✝³ : PosMulMono M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : MulPosStrictMono M₀
inst✝ : DecidableLE M₀
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ a * 0 < c * d

Tactic:
mul_zero

Goal state after:
M₀ : Type u_2
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : PartialOrder M₀
a b c d : M₀
inst✝³ : PosMulMono M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : MulPosStrictMono M₀
inst✝ : DecidableLE M₀
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ 0 < c * d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosMono G₀
n : ℕ
hn : 0 < ↑n
⊢ StrictMonoOn (fun a ↦ a ^ ↑n) {a | 0 ≤ a}

Tactic:
simpa using pow_left_strictMonoOn₀ (by lia)

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

Goal state before:
pp: case mp
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
h : 0 < 0 * 0
⊢ False

Tactic:
mul_zero

Goal state after:
case mp
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
h : 0 < 0
⊢ False
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₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ 0 < b⁻¹

Tactic:
exact inv_pos.2 (hd.trans_le hdb)

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

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
b : β
a : α
H : ∀ (y : β), s y (f a) → Acc s y
IH : ∀ (y : β), s y (f a) → ∀ (a : α), f a = y → Acc r a
⊢ Acc r a

Tactic:
exact ⟨_, fun a' h => IH (f a') (map_rel f h) _ rfl⟩

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) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
rw [← mul_le_mul_iff_left (x ⊓ (y ⊓ z)), inf_mul_sup x (y ⊓ z), ← inv_mul_le_iff_le_mul,
      le_inf_iff]

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