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)
b : Bool
n : Nat
ih : motive n
h : ¬(n = 0 → b = true)
⊢ Nat.bit b n = 0

Tactic:
rw [bit_eq_zero_iff]

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)
b : Bool
n : Nat
ih : motive n
h : ¬(n = 0 → b = true)
⊢ n = 0 ∧ b = false
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : b = a ∨ TransGen r a b
⊢ ReflTransGen r a b

Tactic:
· rcases h with (rfl | h)
    · rfl
    · exact h.to_reflTransGen

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case symm
α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
i✝¹ i✝ a b : α
a✝ : EqvGen r a b
ih : EqvGen p a b
⊢ EqvGen p b a

Tactic:
| symm a b _ ih =>

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

Goal state before:
pp: α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ ⇑f = ⇑g.symm ∘ id ↔ f = g.symm

Tactic:
comp_id,

Goal state after:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ ⇑f = ⇑g.symm ↔ f = g.symm
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
⊢ f^[n * m] = f^[m * n]

Tactic:
Nat.mul_comm

Goal state after:
α : Type u
f : α → α
m n : ℕ
⊢ f^[m * n] = f^[m * n]
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α✝ : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
M : Type u_9
α : Type u_10
inst✝¹ : CommMonoid M
inst✝ : MulAction M α
a a' : M
b : α
⊢ a • a' • b = a' • a • b

Tactic:
rw [← mul_smul, mul_comm, mul_smul]

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

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
H : ∀ (x : M) (y : N), y * x • 1 = x • y
x : M
y z : N
⊢ x • y • z = y • x • z

Tactic:
rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]

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) → DivInvMonoid (f i)
⊢ ∀ (a : (i : I) → f i), a ^ 0 = 1

Tactic:
by intros; ext; exact DivInvMonoid.zpow_zero' _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : Option α
f : α → β
⊢ Option.map f x = none ↔ x = none

Tactic:
map_eq_none_iff

Goal state after:
α : Type u_1
β : Type u_2
x : Option α
f : α → β
⊢ x = none ↔ x = none
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder β
x✝ : α × β
a : α
b : β
⊢ ∃ b_1, b_1 < (a, b)

Tactic:
obtain ⟨c, h⟩ := exists_lt b
    exact ⟨(a, c), Prod.mk_lt_mk_iff_right.2 h⟩

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 ∧ i ≤ j

Tactic:
h j,

Goal state after:
α : Type u_3
inst✝ : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j ≤ i ∧ True
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : ¬(x = y ∨ y = z ∨ x = z)
⊢ False

Tactic:
simp only [not_or, ← Ne.eq_def] at hne

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
⊢ False
Module: Mathlib.Data.Bool.Basic

Goal state before:
pp: b : Bool
⊢ ofNat b.toNat = b

Tactic:
grind [cases Bool]

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

Goal state before:
pp: α : Sort u_1
f : Bool → α
H : f false ≠ f true
x y : Bool
⊢ f x = f y → x = y

Tactic:
grind [cases Bool]

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

Goal state before:
pp: case false.false
f : Bool → Bool
x : Bool
h₁ : f true = false
h₂ : f false = false
⊢ f (f (f x)) = f x

Tactic:
grind [cases Bool]

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

Goal state before:
pp: case false.true
f : Bool → Bool
x : Bool
h₁ : f true = false
h₂ : f false = true
⊢ f (f (f x)) = f x

Tactic:
grind [cases Bool]

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

Goal state before:
pp: case true.false
f : Bool → Bool
x : Bool
h₁ : f true = true
h₂ : f false = false
⊢ f (f (f x)) = f x

Tactic:
grind [cases Bool]

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

Goal state before:
pp: case true.true
f : Bool → Bool
x : Bool
h₁ : f true = true
h₂ : f false = true
⊢ f (f (f x)) = f x

Tactic:
grind [cases Bool]

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

Goal state before:
pp: a b : ℤ
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
← not_iff_not,

Goal state after:
a b : ℤ
⊢ ¬a * b ≤ 0 ↔ ¬(0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b)
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
← not_iff_not,

Goal state after:
a b : ℤ
⊢ ¬a * b < 0 ↔ ¬(0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b)
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case succ.inl
b : ℕ
ha : 0 ≠ 1
⊢ 0 * (b + 1) ≤ 0 ^ (b + 1)

Tactic:
Nat.zero_mul

Goal state after:
case succ.inl
b : ℕ
ha : 0 ≠ 1
⊢ 0 ≤ 0 ^ (b + 1)
Module: Mathlib.Order.Compare

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (cmp a b).Compares a b

Tactic:
simp [cmp, cmpUsing, h, h.not_gt]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ (cmp a b).Compares a b

Tactic:
simp [cmp, cmpUsing, h, h.not_gt]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b < a
⊢ (cmp a b).Compares a b

Tactic:
simp [cmp, cmpUsing, h, h.not_gt]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictAntiOn (f ∘ ⇑ofDual) s ↔ StrictMonoOn f s

Tactic:
strictAntiOn_comp_ofDual_iff

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

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁

Tactic:
rw [h_fa]; exact h_mon h₂

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : Subsingleton α
⊢ s.Nonempty → s = univ

Tactic:
rintro ⟨x, hx⟩

Goal state after:
α : Type u
s : Set α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
⊢ s = univ
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ Codisjoint ↑a ↑b ↔ Codisjoint a b

Tactic:
rw [codisjoint_iff, codisjoint_iff, ← coe_sup, ← coe_top, coe_inj]

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

Goal state before:
pp: α : Type u_1
s✝ t u : Set α
p : α → Prop
s : { s // ∀ (a : α), a ∈ s → p a }
x✝ : α
⊢ x✝ ∈ ↑((fun s ↦ ⟨{a | ∃ h, ⟨a, h⟩ ∈ s}, ⋯⟩) ((fun s ↦ {a | ↑a ∈ ↑s}) s)) ↔ x✝ ∈ ↑s

Tactic:
exact ⟨fun h ↦ h.2, fun h ↦ ⟨s.property _ h, h⟩⟩

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

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

Tactic:
specialize hc n

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

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
⊢ Lattice α

Tactic:
let semilatticeInf := e.semilatticeInf

Goal state after:
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
⊢ Lattice α
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ b ⊔ c \ a = c

Tactic:
by
  rw [sup_sdiff_eq_sup hab, sup_of_le_right hbc]

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
hac : c ≤ a
hbc : c ≤ b
h : a \ c = b \ c
⊢ a = b

Tactic:
by rw [← sdiff_sup_cancel hac, h, sdiff_sup_cancel hbc]

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

Goal state before:
pp: α : Type u_1
t s s' : Set α
⊢ t.ite s s' ∩ t = s ∩ t

Tactic:
by
  rw [Set.ite, union_inter_distrib_right, sdiff_inter_self, inter_assoc, inter_self, union_empty]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ (￢a) ∆ a = ⊤

Tactic:
by
  rw [eq_top_iff, symmDiff, hnot_sdiff, sup_sdiff_self]
  exact Codisjoint.top_le codisjoint_hnot_left

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : a ∆ b = a ⊔ b
⊢ Disjoint a b

Tactic:
rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq_self_iff_disjoint] at h

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : Disjoint (a ⊓ b) (a ⊔ b)
⊢ Disjoint a b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ b ⇔ a ⇔ a = b

Tactic:
simp [bihimp_assoc]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s₁ = ∅ ∨ t₁ = ∅

Tactic:
prod_eq_empty_iff.mp h,

Goal state after:
case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ True ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s₁ = ∅ ∨ t₁ = ∅
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
hs : s.Nontrivial
hf : Surjective f
⊢ (f ⁻¹' s).Nontrivial

Tactic:
rcases hs with ⟨fx, hx, fy, hy, hxy⟩
  rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
  exact ⟨x, hx, y, hy, mt (congr_arg f) hxy⟩

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

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

Tactic:
ext f
  refine ⟨fun h => ?_, ?_⟩
  · constructor <;>
      · rintro i ⟨his, hpi⟩
        simpa [*] using h i
  · rintro ⟨ht₁, ht₂⟩ i his
    by_cases p i <;> simp_all

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : ¬i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
j : ι
hj : j ∈ s
⊢ t j (update f i a j) = t j (f j)

Tactic:
rw [update_of_ne]
    exact fun h => hi (h ▸ hj)

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

Goal state before:
pp: case mpr
ι : 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 : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case mpr
ι : 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
hx : ∀ (i : ι), i ∈ s → x i ∈ t i
⊢ ∃ x, (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a b : α
⊢ InjOn f {a, b} ↔ f a = f b → a = b

Tactic:
unfold InjOn; aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
f : α → β
g : β → γ
⊢ graphOn (g ∘ f) s = (fun x ↦ (x.1, g x.2)) '' graphOn f s

Tactic:
by
  simpa using! image_comp (fun x ↦ (x.1, g x.2)) (fun x ↦ (x, f x)) _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set β
t : Set γ
hf : Surjective f
hg : SurjOn g s t
⊢ t ⊆ g '' f '' f ⁻¹' s

Tactic:
image_preimage_eq _ hf

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set β
t : Set γ
hf : Surjective f
hg : SurjOn g s t
⊢ t ⊆ g '' s
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ (-Int.negSucc n) = (a ^ Int.negSucc n)⁻¹

Tactic:
by
    rw [zpow_negSucc, inv_inv, ← zpow_natCast]
    rfl

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
⊢ f (x / y) = f (x * y⁻¹)

Tactic:
div,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
⊢ f x / f y = f (x * y⁻¹)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
⊢ a * b = 1 ↔ b = a⁻¹

Tactic:
by
  rw [mul_eq_one_iff_inv_eq, eq_comm]

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₂
inst✝¹ : One M₂
inst✝ : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ 1 * f x = f x

Tactic:
by rw [← one, ← mul, one_mul]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a * c⁻¹ = b * c⁻¹ ↔ a = b

Tactic:
exact Units.mul_left_inj h.inv.unit'

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬f 0 = f 1

Tactic:
rw [zero, one]
    exact zero_ne_one

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
a_eq_0 : a⁻¹ = 0
⊢ False

Tactic:
by
  simpa [a_eq_0] using mul_inv_cancel₀ h

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

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁶ : MonoidWithZero M₀
inst✝⁵ : MonoidWithZero M₀'
inst✝⁴ : Zero A
inst✝³ : MulActionWithZero M₀ A
inst✝² : Zero A'
inst✝¹ : SMul M₀ A'
p : Prop
inst✝ : Decidable p
f : M₀' →*₀ M₀
r s : M₀'
m : A
⊢ (r * s) • m = r • s • m

Tactic:
by change f (r * s) • m = f r • f s • m; simp [mul_smul]

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

Goal state before:
pp: α : Type u_3
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
⊢ ∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c

Tactic:
have : c = x * (b - x) := (eq_neg_of_add_eq_zero_right h).trans (by simp [mul_sub, mul_comm])

Goal state after:
α : Type u_3
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ ∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
⊢ (-1)⁻¹ = -1

Tactic:
rw [← neg_inv, inv_one]

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

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

Tactic:
div_div_div_eq,

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
c a b : G₀
hc : c ≠ 0
⊢ c * b / (a * c) = b / a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: N : Type u_2
r : N → N → Prop
inst✝ : Group N
⊢ Covariant N N (swap fun x1 x2 ↦ x1 * x2) r ↔ Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r

Tactic:
refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
  · rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a]
    exact h a⁻¹ bc
  · rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a] at bc
    exact h a⁻¹ bc

Goal state after:
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 - (c + d) ≤ a - c + (b - d)

Tactic:
rw [add_comm c, tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]
  refine (tsub_le_tsub_right add_tsub_le_assoc c).trans ?_
  rw [add_comm a, add_comm (a - c)]
  exact add_tsub_le_assoc

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

Goal state before:
pp: α : Type u
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : Monoid α
inst✝¹ : ExistsMulOfLE α
inst✝ : MulLeftReflectLT α
a b : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
x : α
hxb : b < x
⊢ a ≤ x

Tactic:
obtain ⟨ε, rfl⟩ := exists_mul_of_le hxb.le
    exact h _ (one_lt_of_lt_mul_right hxb)

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬c * a = b * a

Tactic:
exact mul_lt_mul_left (h.lt_of_ne h') a |>.ne

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

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a * a ≤ b * b ↔ a ≤ b

Tactic:
exact
    ⟨fun h => not_lt.mp fun k => not_lt.mpr h (mul_lt_mul_of_lt_of_lt k k), fun h =>
      mul_le_mul' h h⟩

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

Goal state before:
pp: case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : 1 ≤ a
⊢ 1 * 1 ≤ a

Tactic:
rwa [mul_one]

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

Goal state before:
pp: α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : Nontrivial α
⊢ ∃ a, 1 < a

Tactic:
obtain ⟨y, hy⟩ := Decidable.exists_ne (1 : α)
  obtain h | h := hy.lt_or_gt
  · exact ⟨y⁻¹, one_lt_inv'.mpr h⟩
  · exact ⟨y, h⟩

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : Preorder R
a b : R
inst✝² : ZeroLEOneClass R
inst✝¹ : MulPosMono R
inst✝ : AddLeftMono R
a2 : 2 ≤ a
b0 : 0 ≤ b
⊢ a + (a + a * b) ≤ a * (2 + b)

Tactic:
by rw [mul_add, mul_two, add_assoc]

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 b : G₀
inst✝ : ZeroLEOneClass G₀
h : a ≤ b
hb : 0 ≤ b
⊢ a ≤ b * 1

Tactic:
rwa [mul_one]

Goal state after:
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:
by
  rw [le_div_iff₀ ha, le_div_iff₀' hc]

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

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

Tactic:
by
  rw [mul_neg_iff, sub_pos, sub_pos, sub_neg, sub_neg, or_iff_left_iff_imp, and_comm]
  exact And.imp h.trans_lt h.trans_lt'

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

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

Tactic:
simpa only [mul_comm, and_comm] using mabs_mul_eq_mul_mabs_le ab

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

Goal state before:
pp: a b : ℤ
H : b ≠ 0
⊢ a % b < |b|

Tactic:
by
  rw [← emod_abs]; exact emod_lt_of_pos _ (abs_pos.2 H)

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

Goal state before:
pp: this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / ↑n| ≤ |a|

Tactic:
apply this

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 1 ≤ ↑n + 1

Tactic:
convert! (@mono_cast α _).imp (?_ : 1 ≤ n + 1)
  <;> simp

Goal state after:
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 ^ ↑(m.gcd n)

Tactic:
Nat.gcd_eq_gcd_ab

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 * m.gcdA n + ↑n * m.gcdB 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 ^ ↑(m.gcd n)

Tactic:
Nat.gcd_eq_gcd_ab

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 * m.gcdA n + ↑n * m.gcdB n)
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

Tactic:
← not_iff_not,

Goal state after:
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ ¬a + b = ⊤ ↔ ¬(a = ⊤ ∨ b = ⊤)
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case inl
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
hxa : log 0 ≤ a
⊢ 0 ≤ exp a

Tactic:
simp [← log_le_iff_le_exp, *]

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

Goal state before:
pp: case inr
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log ≤ a
hx : x ≠ 0
⊢ x ≤ exp a

Tactic:
simp [← log_le_iff_le_exp, *]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
y : WithZero α
a b : α
hy : ↑b ≤ y
⊢ b ≤ unzeroD a y

Tactic:
by
  have hne : y ≠ 0 := ne_bot_of_le_ne_bot WithZero.coe_ne_zero hy
  rwa [le_unzeroD_iff hne]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
⊢ ⌈a⌉₊ ≤ ⌊a⌋₊ + 1

Tactic:
rw [ceil_le, Nat.cast_add, Nat.cast_one]
  exact (lt_floor_add_one a).le

Goal state after:
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
⊢ ↑n + ↑d ≤ a + ↑n ↔ d + n ≤ ⌊a⌋₊ + n

Tactic:
add_comm (n : R),

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 + ↑n ≤ a + ↑n ↔ d + n ≤ ⌊a⌋₊ + n