mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
x : G
⊢ x⁻¹ = 1 / x

Tactic:
by rw [div_eq_mul_inv, one_mul]

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

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∃ x, p x (update f a b x)) ↔ p a b ∨ ∃ x, x ≠ a ∧ p x (f x)

Tactic:
← not_forall_not,

Goal state after:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (¬∀ (x : α), ¬p x (update f a b x)) ↔ p a b ∨ ∃ x, x ≠ a ∧ p x (f x)
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_2
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
h : update default i x = update default i y
⊢ x = y

pp: case refine_1
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
⊢ Pi.map f (update default i x) = Pi.map f (update default i y)

Tactic:
· simpa using congrFun h i

Goal state after:
case refine_1
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
⊢ Pi.map f (update default i x) = Pi.map f (update default i y)
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
  · refine ⟨fun a ↦ (h a).choose, fun hr ↦ ?_, fun h' ↦ h' ▸ ?_⟩
    exacts [((h _).choose_spec.2 _ hr).symm, (h _).choose_spec.1]
  · rintro ⟨f, hf⟩
    simp [hf]

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

Goal state before:
pp: α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (∃ fab, p fab) ↔ ∃ fa fb, p fun t ↦ rec fa fb t

Tactic:
← not_forall_not,

Goal state after:
α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (¬∀ (x : (ab : α ⊕ β) → γ ab), ¬p x) ↔ ∃ fa fb, p fun t ↦ rec fa fb t
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ x * r • a = r • b * x

Tactic:
mul_smul_comm,

Goal state after:
M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ r • (x * a) = r • b * x
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ r • x * a = b * r • x

Tactic:
mul_smul_comm,

Goal state after:
M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ r • x * a = r • (b * x)
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
⊢ ∀ (a : α × β), ¬Prod.Lex r s a a

Tactic:
rintro ⟨i, a⟩ (⟨_, _, h⟩ | ⟨_, h⟩) <;> exact irrefl _ h

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝ : LinearOrder α
a b : αᵒᵈ
⊢ compare a b = compareOfLessAndEq a b

Tactic:
by
    simp only [compare, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq, eq_comm]
    rfl

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a b : α
⊢ ¬(a ≤ b ∧ ¬b ≤ a) ↔ ¬a ≤ b ∨ b ≤ a

Tactic:
Classical.not_and_iff_not_or_not,

Goal state after:
α : Type u_2
inst✝ : Preorder α
a b : α
⊢ ¬a ≤ b ∨ ¬¬b ≤ a ↔ ¬a ≤ b ∨ b ≤ a
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case a.inl
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a : ℕ
h : a + 1 < a + 1 + 1
⊢ P (a + 1) (a + 1)

Tactic:
exact ha _

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝¹ x✝ : α × β
a₁ : α
a₂ : β
b₁ : α
b₂ : β
hab : ¬Prod.Lex r s (a₁, a₂) (b₁, b₂)
hba : ¬Prod.Lex r s (b₁, b₂) (a₁, a₂)
⊢ (a₁, a₂) = (b₁, b₂)

Tactic:
obtain rfl := Std.Trichotomous.trichotomous a₁ b₁
      (mt (Prod.Lex.left a₂ b₂) hab) (mt (Prod.Lex.left b₂ a₂) hba)
    obtain rfl := Std.Trichotomous.trichotomous a₂ b₂
      (mt (Prod.Lex.right a₁) hab) (mt (Prod.Lex.right a₁) hba)
    rfl

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

Goal state before:
pp: P : ℕ → Prop
h : ∀ (N : ℕ), ∃ n, n > N ∧ P n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
by
  have : NoMaxOrder {n // P n} :=
    ⟨fun n ↦ Exists.intro ⟨(h n.1).choose, (h n.1).choose_spec.2⟩ (h n.1).choose_spec.1⟩
  obtain ⟨f, hf, _⟩ := Nat.exists_strictMono' (⟨(h 0).choose, (h 0).choose_spec.2⟩ : {n // P n})
  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: 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
flat : ∀ (j : ℕ), f j = f (j + 1)
m : ℕ
x✝ : 0 ≤ m
⊢ f m = f 0

Tactic:
induction m with grind

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:
by
  rw [symmDiff_comm, symmDiff_symmDiff_inf]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by simp [symmDiff]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by simp [symmDiff]

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a : α
⊢ Injective fun x ↦ swap x a

Tactic:
simp_rw [swap_comm _ a]
  exact swap_injective_of_left a

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

Goal state before:
pp: case mp.inr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
ne : a ≠ i
⊢ a ∈ insert j s \ {i}

Tactic:
exact ⟨.inr ha, ne⟩

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

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

Tactic:
image_inter_nonempty_iff

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x✝ : ∃ g, ∀ (x : ↑s), f ↑x = ↑(g x)
x : α
hx : x ∈ s
g : ↑s → ↑t
hg : ∀ (x : ↑s), f ↑x = ↑(g x)
⊢ f x ∈ t

Tactic:
hg ⟨x, hx⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x✝ : ∃ g, ∀ (x : ↑s), f ↑x = ↑(g x)
x : α
hx : x ∈ s
g : ↑s → ↑t
hg : ∀ (x : ↑s), f ↑x = ↑(g x)
⊢ ↑(g ⟨x, hx⟩) ∈ 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
⊢ f ⁻¹' s ⊆ f ⁻¹' t → s ⊆ t

Tactic:
intro h x hx

Goal state after:
case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
x : α
hx : x ∈ s
⊢ x ∈ t
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ ⊤ ⊆ range Sum.inl ⊔ range Sum.inr

Tactic:
rintro (x | y) - <;> [left; right]

Goal state after:
case inl
α : Type u_1
β : Type u_2
x : α
⊢ Sum.inl x ∈ range Sum.inl

case inr
α : Type u_1
β : Type u_2
y : β
⊢ Sum.inr y ∈ range Sum.inr
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ Surjective (image f)

Tactic:
intro s
  use f ⁻¹' s
  rw [hf.image_preimage]

Goal state after:
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:
by
  rw [h.image_sdiff, inter_eq_self_of_subset_right hst]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
⊢ x ∈ f '' s → x ∈ g ⁻¹' s

Tactic:
rintro ⟨y, hy, rfl⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
y : α
hy : y ∈ s
⊢ f y ∈ g ⁻¹' s
Module: Mathlib.Data.Int.Init

Goal state before:
pp: case pos
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h✝ : z = b
⊢ cast ⋯
      (match -[(b - z).toNat+1] with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] =>
        match n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg b zero pred n))) =
    pred z hz
      (cast ⋯
        (match z - b with
        | ofNat n => inductionOn'.pos b zero succ n
        | -[n+1] => inductionOn'.neg b zero pred n))

Tactic:
show z - b = 0 by lia

Goal state after:
case pos
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h✝ : z = b
⊢ cast ⋯
      (match -[(b - z).toNat+1] with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] =>
        match n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg b zero pred n))) =
    pred z hz
      (cast ⋯
        (match 0 with
        | ofNat n => inductionOn'.pos b zero succ n
        | -[n+1] => inductionOn'.neg b zero pred n))
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : CommGroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
⊢ ∀ (a b : H), a * b = b * a

Tactic:
hf.forall₂,

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : CommGroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
⊢ ∀ (x₁ x₂ : G), f x₁ * f x₂ = f x₂ * f x₁
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * b * c = b * (a * c)

Tactic:
mul_comm a,

Goal state after:
G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ b * a * c = b * (a * c)
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ ↑(v * u⁻¹) = a * ↑u * ↑u⁻¹

Tactic:
rw [← hv, Units.val_mul]

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

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
⊢ ↑(u⁻¹ * v) = ↑u⁻¹ * (↑u * a)

Tactic:
rw [← hv, Units.val_mul]

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

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
x : M
⊢ f x * ↑((liftRight f g h) x)⁻¹ = 1

Tactic:
Units.mul_inv_eq_iff_eq_mul,

Goal state after:
M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
x : M
⊢ f x = 1 * ↑((liftRight f g h) x)
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
a c : α
b d : αˣ
⊢ a * ↑b⁻¹ = ↑d⁻¹ * c ↔ a * ↑d = c * ↑b

Tactic:
Units.mul_inv_eq_iff_eq_mul,

Goal state after:
α : Type u
inst✝ : CommMonoid α
a c : α
b d : αˣ
⊢ a = ↑d⁻¹ * c * ↑b ↔ a * ↑d = c * ↑b
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case inr
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : a ≠ 0
⊢ a * (a * b) / a = a * b

Tactic:
mul_div_cancel_left₀ _ ha

Goal state after:
case inr
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : a ≠ 0
⊢ a * b = a * b
Module: Mathlib.Algebra.Group.Hom.Instances

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
f : M →* N
⊢ { toFun := comp 1, map_one' := ⋯, map_mul' := ⋯ } f = 1 f

Tactic:
exact one_comp f

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u) a ↔ ↑u * a * ↑u⁻¹ = a

Tactic:
Units.mul_inv_eq_iff_eq_mul,

Goal state after:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u) a ↔ ↑u * a = a * ↑u
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
M : Type u_4
inst✝ : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
⊢ a * ↑⋯.unit⁻¹ = 1

Tactic:
Units.mul_inv_eq_iff_eq_mul,

Goal state after:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
M : Type u_4
inst✝ : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
⊢ a = 1 * ↑⋯.unit
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a : α
hp : Odd a
⊢ Odd (-a)

Tactic:
obtain ⟨k, hk⟩ := hp

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

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

Tactic:
add_comm (a - c)

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

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

Tactic:
add_comm (a - c)

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

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

Tactic:
by
  rw [← mul_le_mul_iff_left d, ← mul_le_mul_iff_right b, mul_inv_cancel_left, mul_assoc,
    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✝ : MulPosReflectLT G₀
a : G₀
⊢ 0 < a⁻¹ ↔ 0 < a

Tactic:
by
  suffices ∀ a : G₀, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩
  intro a ha
  apply lt_of_mul_lt_mul_right _ ha.le
  apply lt_of_mul_lt_mul_right _ ha.le
  simpa [ha.ne']

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ a / b < 1 ↔ a < b

Tactic:
by rw [div_lt_iff₀ hb, one_mul]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ a * c⁻¹ ≤ b / c

Tactic:
div_eq_mul_inv b c

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ a * c⁻¹ ≤ b * c⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
h : a < b
hc : 0 < c
⊢ a * c⁻¹ < b / c

Tactic:
div_eq_mul_inv b c

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
h : a < b
hc : 0 < c
⊢ a * c⁻¹ < b * c⁻¹
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 : G₀
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Tactic:
by
  rw [inv_le_iff_one_le_mul₀' ha, le_mul_inv_iff₀ hb, one_mul]

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₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ a / b < c / d

Tactic:
by
  rw [div_eq_mul_inv, div_eq_mul_inv]
  apply mul_lt_mul hac (by gcongr; assumption) _ hc
  exact inv_pos.2 (hd.trans_le hdb)

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ EquivLike.inv f b < a ↔ b < f a

Tactic:
by
  rw [← map_lt_map_iff f]
  simp only [EquivLike.apply_inv_apply]

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

Goal state before:
pp: ⊢ OrderedSub ℕ

Tactic:
by
  refine ⟨fun m n k ↦ ?_⟩
  induction n generalizing k with
  | zero => simp
  | succ n ih => simp only [sub_succ, pred_le_iff, ih, succ_add, add_succ]

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

Goal state before:
pp: m n : ℕ
⊢ ↑(-[m+1].gcd -[n+1]) = -(↑m + 1) * -m.succ.gcdA -[n+1].natAbs + -(↑n + 1) * - -[m+1].natAbs.gcdB n.succ

Tactic:
rw [Int.neg_mul_neg, Int.neg_mul_neg]
      apply Nat.gcd_eq_gcd_ab

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

Goal state before:
pp: α : Type u
d : α
x y : WithOne α
⊢ unoneD d x = unoneD d y ↔ x = y ∨ x = ↑d ∧ y = 1 ∨ x = 1 ∧ y = ↑d

Tactic:
induction y

Goal state after:
case one
α : Type u
d : α
x : WithOne α
⊢ unoneD d x = unoneD d 1 ↔ x = 1 ∨ x = ↑d ∧ 1 = 1 ∨ x = 1 ∧ 1 = ↑d

case coe
α : Type u
d : α
x : WithOne α
a✝ : α
⊢ unoneD d x = unoneD d ↑a✝ ↔ x = ↑a✝ ∨ x = ↑d ∧ ↑a✝ = 1 ∨ x = 1 ∧ ↑a✝ = ↑d
Module: Mathlib.Algebra.Order.Monoid.WithTop

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

Tactic:
induction y

Goal state after:
case coe.bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ ⊥ ≤ ⊥ + ↑a✝

case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝ + ↑a✝¹
Module: Mathlib.Algebra.Order.Monoid.WithTop

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

Tactic:
induction y

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

case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝¹ + ↑a✝
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c : α
hc : AddLECancellable c
h : c ≤ a + c
h' : a < a + c - c
⊢ False

Tactic:
exact h'.ne' hc.add_tsub_cancel_right

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ b = c

Tactic:
rw [← hab.inj]
  rw [tsub_add_cancel_of_le h₁, h₃, tsub_add_cancel_of_le h₂]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h✝ : b ≤ a
h : b ≤ b + ⋯.choose
this : a = b + ⋯.choose
⊢ ⋯.choose ≤ c ↔ ⋯.choose + b ≤ c + b

Tactic:
add_le_add_iff_right

Goal state after:
case pos
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h✝ : b ≤ a
h : b ≤ b + ⋯.choose
this : a = b + ⋯.choose
⊢ ⋯.choose ≤ c ↔ ⋯.choose ≤ c
Module: Mathlib.Data.Nat.Cast.Order.Ring

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
m n : ℕ
⊢ ↑m = -↑n ↔ m = 0 ∧ n = 0

Tactic:
by
  simp [eq_neg_iff_add_eq_zero, ← cast_add]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
d : α
x y : WithBot α
⊢ unbotD d x = unbotD d y ↔ x = y ∨ x = ↑d ∧ y = ⊥ ∨ x = ⊥ ∧ y = ↑d

Tactic:
induction y

Goal state after:
case bot
α : Type u_1
d : α
x : WithBot α
⊢ unbotD d x = unbotD d ⊥ ↔ x = ⊥ ∨ x = ↑d ∧ ⊥ = ⊥ ∨ x = ⊥ ∧ ⊥ = ↑d

case coe
α : Type u_1
d : α
x : WithBot α
a✝ : α
⊢ unbotD d x = unbotD d ↑a✝ ↔ x = ↑a✝ ∨ x = ↑d ∧ ↑a✝ = ⊥ ∨ x = ⊥ ∧ ↑a✝ = ↑d
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
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : a ≤ 0
⊢ ⌊a - ↑n⌋₊ = 0 - n

Tactic:
floor_of_nonpos (tsub_nonpos_of_le (ha.trans n.cast_nonneg)),

Goal state after:
case inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : a ≤ 0
⊢ 0 = 0 - n
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : Set β
f : β → α
⊢ DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s

Tactic:
by
  simp only [DirectedOn, Set.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, Order.Preimage]

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible a
h : ⅟a = b
⊢ ⅟a * a = 1

Tactic:
invOf_mul_self

Goal state after:
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible a
h : ⅟a = b
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝ : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = ⅟r
⊢ ⅟r * r = 1

Tactic:
invOf_mul_self

Goal state after:
α : Type u
inst✝ : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = ⅟r
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible (a * b)
⊢ ⅟(a * b) * (a * b) = 1

Tactic:
invOf_mul_self

Goal state after:
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible (a * b)
⊢ 1 = 1
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ ↑(y.mulLeft ↑(-x)) = ↑(-y.mulLeft ↑x)

Tactic:
simp [neg_mul_eq_mul_neg]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommRing α
a b : α
n✝ n : ℕ
ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * (a * geomSum a b n) + (a - b) * b ^ (n + 1)

Tactic:
mul_comm a,

Goal state after:
case succ
α : Type u_1
inst✝ : CommRing α
a b : α
n✝ n : ℕ
ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * (geomSum a b n * a) + (a - b) * b ^ (n + 1)