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
      (fun b n ih ↦
        if h : n = 0 → b = true then bit b n h ih
        else
          have this := ⋯;
          ⋯ ▸ zero)
      0 =
    zero

Tactic:
binaryRec_zero

Goal state after:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
⊢ zero = zero
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ x = y

Tactic:
h x,

Goal state after:
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ default = y
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
⊢ (Surjective fun g ↦ g ∘ f) ↔ Injective f

Tactic:
by
  classical
  refine ⟨not_imp_not.mp fun not_inj surj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.surjective_comp_right)⟩
  simp only [Injective, not_forall] at not_inj
  have ⟨a₁, a₂, eq, ne⟩ := not_inj
  have ⟨f, hf⟩ := surj (if · = a₂ then c else c')
  have h₁ := congr_fun hf a₁
  have h₂ := congr_fun hf a₂
  simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂
  rw [← h₁, eq, h₂]

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

Goal state before:
pp: case succ
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + 1 + k))

Tactic:
Nat.add_right_comm,

Goal state after:
case succ
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + k + 1))
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: case refine_1
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : FaithfulSMul G α
a : G
ha : ∀ (a_1 : α), a • a_1 = a_1
⊢ ∀ (a_1 : α), a • a_1 = 1 • a_1

pp: case refine_2
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ a₁ = a₂

Tactic:
· simpa only [one_smul]

Goal state after:
case refine_2
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ a₁ = a₂
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) → MulOneClass (f i)
a✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * 1) x✝ = a✝ x✝

Tactic:
exact mul_one _

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
o : Ordering
⊢ compare a b = o ↔ o.Compares a b

Tactic:
by
  cases o <;> simp only [Ordering.Compares]
  · exact compare_lt_iff_lt
  · exact compare_eq_iff_eq
  · exact compare_gt_iff_gt

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 ↦ x1 < x2) a b
h2 : ¬(fun x1 x2 ↦ x1 < x2) b a
⊢ Ordering.eq.Compares a b

Tactic:
exact le_antisymm (not_lt.1 h2) (not_lt.1 h1)

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j ≤ i ∧ True

Tactic:
and_true

Goal state after:
α : Type u_3
inst✝ : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j ≤ i
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: α : Sort u_1
x y : α
p : x ≍ y → Prop
h : ∀ (he : x = y), p ⋯
he : x ≍ y
⊢ p he

Tactic:
by
  cases he
  exact h rfl

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

Goal state before:
pp: α : Type u
p : α → Prop
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : OrderBot (Subtype p)
hbot : p ⊥
x : { x // p x }
⊢ ↑x = ⊥ ↔ x = ⊥

Tactic:
by
  rw [← coe_bot hbot, Subtype.ext_iff]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp y x = cmp y' x'
⊢ cmp x y = cmp x' y'

Tactic:
rwa [← cmp_swap y', ← cmp_swap, swap_inj]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x y ↔ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

Tactic:
by
  constructor
  · intro h
    refine ⟨fun a hx hy ↦ (@h (a, ⊥) ⟨hx, ?_⟩ ⟨hy, ?_⟩).1,
      fun b hx hy ↦ (@h (⊥, b) ⟨?_, hx⟩ ⟨?_, hy⟩).2⟩
    all_goals exact bot_le
  · rintro ⟨ha, hb⟩ z hza hzb
    exact ⟨ha hza.1 hzb.1, hb hza.2 hzb.2⟩

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

Goal state before:
pp: f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
⊢ f n = f b

Tactic:
obtain ⟨m, hmb, hm⟩ : ∃ m ≤ b, f m = f (m + 1) := by
    contrapose! hfb
    let rec strictMono : ∀ m ≤ b + 1, m ≤ f m
    | 0, _ => Nat.zero_le _
    | m + 1, hmb => (strictMono _ <| m.le_succ.trans hmb).trans_lt <| (hfmono m.le_succ).lt_of_ne <|
        hfb _ <| Nat.le_of_succ_le_succ hmb
    exact ⟨b + 1, strictMono _ le_rfl⟩

Goal state after:
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
m : ℕ
hmb : m ≤ b
hm : f m = f (m + 1)
⊢ f n = f b
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ ¬univ ⊆ s ↔ ∃ a, ¬a ∈ s

Tactic:
by
  simp [not_subset]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s ≠ univ ↔ ∃ a, ¬a ∈ s

Tactic:
← not_forall,

Goal state after:
α : Type u_1
s : Set α
⊢ s ≠ univ ↔ ¬∀ (x : α), x ∈ s
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
l : List α
H : l.Nodup
a : α
⊢ {x | x ∈ l} = {a} ↔ l = [a]

Tactic:
by
  constructor
  · rw [ofPred_mem_list_eq_replicate]
    rintro ⟨n, hn, rfl⟩
    simp only [List.nodup_replicate] at H
    simp [show n = 1 by lia]
  · rintro rfl
    simp

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

Goal state before:
pp: α : Type u
s : Set α
⊢ (∃ a, s = {a}) ↔ s.Nonempty ∧ s.Subsingleton

Tactic:
by
  refine ⟨?_, fun h => ?_⟩
  · rintro ⟨a, rfl⟩
    exact ⟨singleton_nonempty a, subsingleton_singleton⟩
  · exact h.2.eq_empty_or_singleton.resolve_left h.1.ne_empty

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : GeneralizedHeytingAlgebra α✝
a b c d : α✝
α : ι → Type u_4
inst✝ : (i : ι) → GeneralizedHeytingAlgebra (α i)
i : (i : ι) → α i
⊢ ∀ (b c : (i : ι) → α i), i ≤ b ⇨ c ↔ i ⊓ b ≤ c

Tactic:
by simp [le_def]

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : GeneralizedCoheytingAlgebra α✝
a b c d : α✝
α : ι → Type u_4
inst✝ : (i : ι) → GeneralizedCoheytingAlgebra (α i)
i : (i : ι) → α i
⊢ ∀ (b c : (i : ι) → α i), i \ b ≤ c ↔ i ≤ b ⊔ c

Tactic:
by simp [le_def]

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

Goal state before:
pp: α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
⊢ t.ite s₁ s₂ = s₁ ∩ t ∪ s₂

Tactic:
by
  ext x
  by_cases hx : x ∈ t <;> simp [*, Set.ite, or_iff_left_of_imp (@h x)]

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x y

Tactic:
by
    rw [← h]
    exact isCompl_compl

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
rw [sup_comm, symmDiff_sup_inf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
⊢ f ⁻¹' s ⊆ t

Tactic:
by
  rintro a ha
  obtain ⟨b, hb, hba⟩ := hs ha
  rwa [hf ha _ hba.symm]
  simpa [hba]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
⊢ s ×ˢ t = univ ↔ s = univ ∧ t = univ

Tactic:
simp [eq_univ_iff_forall, forall_and]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' (s ∩ t) = f '' s ∩ f '' t

Tactic:
apply Subset.antisymm (image_inter_subset _ _ _)

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' s ∩ f '' t ⊆ f '' (s ∩ t)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
hst : t ⊆ s
⊢ f '' (s \ t) = f '' s \ f '' t

Tactic:
h.image_sdiff,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
hst : t ⊆ s
⊢ f '' s \ f '' (s ∩ t) = f '' s \ f '' t
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
f : α → β
hf : s = graphOn f (Prod.fst '' s)
⊢ InjOn Prod.fst (graphOn f (Prod.fst '' s))

Tactic:
exact InjOn.image_of_comp <| injOn_id _

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ InjOn f s ∧ InjOn f r ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ r → f x ≠ f y

pp: case refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ Disjoint s r

Tactic:
and_iff_right h.injOn,

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ InjOn f r ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ r → f x ≠ f y

case refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ Disjoint s r
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s t : Set β
hb : MapsTo fb s t
x : α
hx : x ∈ f ⁻¹' s
⊢ fa x ∈ f ⁻¹' t

Tactic:
simp only [mem_preimage, h x, hb hx]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a

Tactic:
rw [zpow_negSucc, pow_succ', mul_inv_rev, inv_mul_cancel_right]
    rw [Int.negSucc_eq, Int.neg_add, Int.neg_add_cancel_right]
    exact zpow_negSucc _ _

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

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

Tactic:
rw [div_eq_iff_eq_mul', div_eq_iff_eq_mul]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
⊢ IsUnit 1

Tactic:
exact isUnit_one

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ ↑u * ↑u⁻¹ = 1

Tactic:
Units.mul_inv

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
⊢ 1 * 1 = 1

Tactic:
exact mul_one _

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

Goal state before:
pp: α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
⊢ 1 * 1 = 1

Tactic:
exact mul_one _

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

Goal state before:
pp: α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
⊢ 1 * 1 = 1

Tactic:
exact mul_one _

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

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ (x✝ * 1).1 = x✝.1

Tactic:
exact mul_one _

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

Goal state before:
pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ (x✝ * 1).2 = x✝.2

Tactic:
exact mul_one _

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommGroup G
inst✝ : CommGroup H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)

Tactic:
by rw [mk_mul_mk, mk_mul_mk, mul_comm g₁, mul_comm h₁]

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : IsLeftCancelMulZero M₀
a b c : M₀
⊢ a * b = a * c ↔ b = c ∨ a = 0

Tactic:
by_cases ha : a = 0 <;> [simp only [ha, zero_mul, or_true]; simp [mul_right_inj', ha]]

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
⊢ f 0⁻¹ = f 0

Tactic:
by rw [inv, zero, inv_zero]

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

Goal state before:
pp: case neg
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
⊢ g • x * g • x⁻¹ = 1

Tactic:
rw [← smul_mul', mul_inv_cancel₀ hx, smul_one]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
b c a : α
h : b ∣ c
⊢ a * b ∣ a * c

Tactic:
obtain ⟨d, rfl⟩ := h
  use d
  rw [mul_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
b c a : α
h : b ∣ᵣ c
⊢ b * a ∣ᵣ c * a

Tactic:
obtain ⟨d, rfl⟩ := h
  use d
  rw [mul_assoc]

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0, ∀ {a : R}, a ≠ 0 → IsRightRegular a,
      ∀ {a : R}, a ≠ 0 → IsRegular a].TFAE

Tactic:
isRightRegular_iff_left_eq_zero_of_mul,

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0, ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0,
      ∀ {a : R}, a ≠ 0 → IsRegular a].TFAE
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: A : Type u_3
F : Type u_4
inst✝² : MulZeroOneClass A
inst✝¹ : FunLike F ℕ A
inst✝ : ZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → f n = g n
⊢ f = g

Tactic:
apply DFunLike.ext
  rintro (_ | n)
  · simp
  · exact h_pos n.succ_pos

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
inhabited_h : Inhabited α
⊢ Nontrivial (Option α)

Tactic:
exact ⟨none, some default, nofun⟩

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * x) + f (y * x) + (f (x * y) + f (y * y)) = (f x + f y) * (f x + f y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
h x,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f x * f x + f (y * x) + (f (x * y) + f (y * y)) = (f x + f y) * (f x + f y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ ↑u * ↑u⁻¹ = 1

Tactic:
Units.mul_inv

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ 1 = 1
Module: Mathlib.Algebra.Ring.Semiconj

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
a b x y : R
ha : SemiconjBy a x y
hb : SemiconjBy b x y
⊢ SemiconjBy (a - b) x y

Tactic:
by
  simpa only [sub_eq_add_neg] using ha.add_left hb.neg_left

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
h : ∀ (a : α), Even a
a : α
ha : 2 * a = 1
⊢ IsUnit 2

Tactic:
exact ⟨⟨2, a, ha, .trans (Commute.ofNat_right _ _).eq ha⟩, rfl⟩

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

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

Tactic:
← mul_lt_mul_iff_right b

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b : α
inst✝ : MulRightStrictMono α
⊢ a * a⁻¹ * b < a * b⁻¹ * b ↔ b < a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
rw [← mul_le_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✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a / b ≤ 1 ↔ a ≤ b

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

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a ≤ 1
⊢ Antitone fun n ↦ a ^ n

Tactic:
refine antitone_int_of_succ_le fun n ↦ ?_

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a ≤ 1
n : ℤ
⊢ a ^ (n + 1) ≤ a ^ n
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 d : G₀
hb : 0 < b
hd : 0 < d
⊢ a ≤ c / d * b ↔ a * d ≤ c * b

Tactic:
← mul_div_right_comm,

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
⊢ a ≤ c * b / d ↔ a * d ≤ c * b
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 d : G₀
hb : 0 < b
hd : 0 < d
⊢ a < c / d * b ↔ a * d < c * b

Tactic:
← mul_div_right_comm,

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
⊢ a < c * b / d ↔ a * d < c * b
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
⊢ ∀ {a b : α × β →o γ},
    { toFun := fun f ↦ { toFun := fun x ↦ { toFun := Function.curry (⇑f) x, monotone' := ⋯ }, monotone' := ⋯ },
            invFun := fun f ↦ { toFun := Function.uncurry fun x ↦ ⇑(f x), monotone' := ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }
          a ≤
        { toFun := fun f ↦ { toFun := fun x ↦ { toFun := Function.curry (⇑f) x, monotone' := ⋯ }, monotone' := ⋯ },
            invFun := fun f ↦ { toFun := Function.uncurry fun x ↦ ⇑(f x), monotone' := ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
by simp [le_def]

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✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ b ^ n * a * a = b ^ n * a ^ 2

Tactic:
rw [mul_assoc, sq]

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

Goal state before:
pp: case inr.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

pp: case inr.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
· simp [ha.le, hb.le, mabs_of_le_one, mul_le_one', mul_comm]

Goal state after:
case inr.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c))

Tactic:
rw [div_mul_div_comm]

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

Goal state before:
pp: x y r r' : ℕ
⊢ ∀ {s t s' t' : ℤ}, x.P y (r, s, t) → x.P y (r', s', t') → x.P y (r.xgcdAux s t r' s' t')

Tactic:
induction r, r' using gcd.induction with
  | H0 => simp
  | H1 a b h IH =>
    intro s t s' t' p p'
    rw [xgcdAux_rec h]; refine IH ?_ p; dsimp [P] at *
    rw [Int.emod_def]; generalize (b / a : ℤ) = k
    rw [p, p', Int.mul_sub, sub_add_eq_add_sub, Int.mul_sub, Int.add_mul, mul_comm k t,
      mul_comm k s, ← mul_assoc, ← mul_assoc, add_comm (x * s * k), ← add_sub_assoc, sub_sub]

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

Goal state before:
pp: case top.top.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ ⊤ → (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ⊤) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ⊤)

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case top.top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ ↑a✝ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ⊤) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝)

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case top.coe.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ↑a✝ ⊤ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ⊤)

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case top.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ↑a✝¹ ↑a✝ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝¹) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝)

Tactic:
simp [← coe_add, swap]

Goal state after: