mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.AdaptationNote

Goal state before:
pp: ⊢ True

Tactic:
#adaptation_note /-- This is a test -/

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, z * x = 1
x y : M
h : x * y = 1
z : M
hz : z * x = 1
⊢ y * x = 1

Tactic:
show y = z by simpa [mul_assoc, h] using congr_arg (· * y) hz.symm

Goal state after:
M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, z * x = 1
x y : M
h : x * y = 1
z : M
hz : z * x = 1
⊢ z * x = 1
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a✝ b✝ a b : G
⊢ a * b * (b⁻¹ * a⁻¹) = 1

Tactic:
rw [mul_assoc, mul_inv_cancel_left, mul_inv_cancel]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
x y : γ
h : f (g x) = f (g y)
⊢ g x = g y

Tactic:
exact congr_arg g (I h)

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

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

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

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

Goal state after:
case refine_2
α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b) → ∀ (a : α), ∃! b, r a b
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a c : α
h : TransGen r a c
⊢ ∃ b, ReflTransGen r a b ∧ r b c

Tactic:
cases h with
  | single hac => exact ⟨_, by rfl, hac⟩
  | tail hab hbc => exact ⟨_, hab.to_reflTransGen, hbc⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
⊢ ReflTransGen r = ReflGen r

Tactic:
by
  rw [← reflGen_transGen, transGen_eq_self]

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

Goal state before:
pp: α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
⊢ foldr (fun x ↦ f) b (a :: l) = f^[l.length + 1] b

Tactic:
foldr,

Goal state after:
α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
⊢ f (foldr (fun x ↦ f) b l) = f^[l.length + 1] b
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α : Type u_1
inst✝ : LT α
T : Std.Trichotomous LT.lt
a b : αᵒᵈ
⊢ ¬a < b → ¬b < a → a = b

Tactic:
rw [eq_comm]; exact T.trichotomous b a

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Subsingleton α
⊢ ∀ (a b : α), r a b = emptyRelation a b

Tactic:
simpa using not_rel_of_subsingleton r

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

Goal state before:
pp: case ind
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
⊢ ∃ n_1, n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1

Tactic:
by_cases heq : f 0 = f 1

Goal state after:
case pos
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
⊢ ∃ n_1, n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1

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
⊢ ∃ n_1, n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ c ⊔ (b ⊔ d)

Tactic:
sup_left_comm b,

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ⊔ (c ⊔ (b ⊔ d)) = a ⊔ c ⊔ (b ⊔ d)
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
x y z w : α
⊢ {x, y} = {z, w} ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
simp [subset_antisymm_iff, insert_subset_iff]; aesop

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

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
hs : s.Nonempty
⊢ s ⊆ {a, b} ↔ s = {a} ∨ s = {b} ∨ s = {a, b}

Tactic:
Set.subset_pair_iff_eq,

Goal state after:
α : Type u_1
s : Set α
a b : α
hs : s.Nonempty
⊢ s = ∅ ∨ s = {a} ∨ s = {b} ∨ s = {a, b} ↔ s = {a} ∨ s = {b} ∨ s = {a, b}
Module: Mathlib.Order.Lattice

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

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

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

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

Tactic:
exact himp_inf_le.trans le_himp_himp

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

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ x \ y = x ⊓ yᶜ

Tactic:
ext <;> simp [sdiff_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ Injective (preimage f) ↔ Surjective f

Tactic:
← Injective.of_comp_iff Set.mem_injective,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ Injective (Membership.mem ∘ preimage f) ↔ Surjective f
Module: Mathlib.Data.Set.Image

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

pp: case mp.h₂
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ t ⊆ s

Tactic:
· rw [← preimage_subset_preimage_iff hs, h]

Goal state after:
case mp.h₂
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ t ⊆ s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
h : x ∈ update f i ⁻¹' s.pi t
⊢ x ∈ t i

Tactic:
convert! h i hi
    simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f '' s = t ↔ SurjOn f s t ∧ MapsTo f s t

Tactic:
by
  refine ⟨?_, fun h => h.1.image_eq_of_mapsTo h.2⟩
  rintro rfl
  exact ⟨s.surjOn_image f, s.mapsTo_image f⟩

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

Goal state before:
pp: ι : 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
F : Type u_9
inst✝ : MulOne M
n : ℕ
f : Monoid.End M
⊢ (⇑f)^[n] = ⇑(npowRec n f)

Tactic:
induction n <;> simp [npowRec, *] <;> rfl

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
n : ℕ
a : M
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1

Tactic:
by
  rw [← pow_left_inj (a := a) hn, one_pow]

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

Goal state before:
pp: a b c d : ℤ
hb : b ≠ 0
hbc : b ∣ c
h : b * a = c * d
⊢ a = c / b * d

Tactic:
obtain ⟨k, rfl⟩ := hbc

Goal state after:
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = b * k / b * d
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : DivInvMonoid G
a b : G
⊢ a * b⁻¹ = a * (1 / b)

Tactic:
one_div

Goal state after:
G : Type u_3
inst✝ : DivInvMonoid G
a b : G
⊢ a * b⁻¹ = a * b⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : b * a = 1
⊢ a⁻¹ = 1 / a

Tactic:
one_div

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : b * a = 1
⊢ a⁻¹ = a⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ a⁻¹ = 1 / a

Tactic:
one_div

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ a⁻¹ = a⁻¹
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✝ : DivisionMonoid 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 (y⁻¹ * x⁻¹)

Tactic:
rw [inv, mul, mul_inv_rev, mul, inv, inv]

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

Goal state before:
pp: case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n - 1))

Tactic:
rw [zpow_sub_one]
    exact h_inv _ ih

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b : α
h : IsUnit b
⊢ a⁻¹ = 1 / a

Tactic:
one_div

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a b : α
h : IsUnit b
⊢ a⁻¹ = a⁻¹
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y : α
⊢ swap (f x) (f y) = f * swap x y * f⁻¹

Tactic:
mul_swap_eq_swap_mul,

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y : α
⊢ swap (f x) (f y) = swap (f x) (f y) * f * f⁻¹
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddMonoidWithOne M
inst✝ : CharZero M
⊢ 1 ≠ 0

Tactic:
by
    rw [← Nat.cast_one, Nat.cast_ne_zero]
    trivial

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(↑m + -[n+1]) = ↑↑m + ↑-[n+1]

Tactic:
rw [Int.ofNat_add_negSucc, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_add_neg]

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

Goal state before:
pp: case refine_1
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝¹ : n ≥ m
hn : m ≤ n
x✝ : ∀ (k : ℤ), k < m → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x ↦ Int.strongRec lt ge k_1
l : ℤ
hl : l < m
⊢ Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) m m lt
      (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) (fun n x hn l x_1 ↦ hn l ⋯) l hl =
    Int.strongRec lt ge l

Tactic:
rw [inductionOn'_self, strongRec_of_lt hl]

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

Goal state before:
pp: m✝ n m : ℕ
⊢ IsSquare m ↔ m.sqrt * m.sqrt = m

Tactic:
by
    simp_rw [← Nat.exists_mul_self m, IsSquare, eq_comm]

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: n : ℕ
⊢ Even ↑n ↔ Even n

Tactic:
rw_mod_cast [even_iff, Nat.even_iff]

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: l : List Prop
⊢ (map Not l).TFAE ↔ l.TFAE

Tactic:
by
  classical
  simp only [TFAE, mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
    Decidable.not_iff_not]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a) x y
⊢ ↑a⁻¹ * (y * ↑a * ↑a⁻¹) = x * ↑a⁻¹

Tactic:
by rw [← h.eq, ← mul_assoc, Units.inv_mul_cancel_left]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
n : ℕ
⊢ SemiconjBy a ↑(x ^ -[n+1]) ↑(y ^ -[n+1])

Tactic:
simp only [zpow_negSucc, Units.val_pow_eq_pow_val, units_inv_right, h, pow_right]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
n : ℕ
a✝ b✝ : M
u✝ u₁ u₂ u : Mˣ
a b : M
hu : a * b = ↑u
hc : Commute a b
this : Commute a ↑u
⊢ b * ↑u⁻¹ * a = 1

Tactic:
rw [← this.units_inv_right.right_comm, ← hc.eq, hu, u.mul_inv]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : a ≠ 0
⊢ b⁻¹ = 1 / b

Tactic:
one_div

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : a ≠ 0
⊢ b⁻¹ = b⁻¹
Module: Mathlib.Algebra.Ring.Parity

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

Tactic:
add_comm_sub,

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

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

Tactic:
rw [lt_iff_le_and_ne, ← tsub_le_iff_left]
  refine ⟨h.le, ?_⟩
  rintro rfl
  simp [hb] at h

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

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

Tactic:
by
  rw [← mul_le_mul_iff_left b, mul_inv_cancel_left]

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

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

Tactic:
rw [← mul_le_mul_iff_right a]
  simp

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

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

Tactic:
rw [← mul_le_mul_iff_right a]
  simp

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
mul_le_mul_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b
toIsOrderedMonoid : IsOrderedMonoid α := { mul_le_mul_left := mul_le_mul_left }
le_of_mul_le_mul_left : ∀ (a b c : α), a * b ≤ a * c → b ≤ c
a b c : α
h : b * a ≤ c * a
⊢ b ≤ c

Tactic:
mul_comm _ a,

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
mul_le_mul_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b
toIsOrderedMonoid : IsOrderedMonoid α := { mul_le_mul_left := mul_le_mul_left }
le_of_mul_le_mul_left : ∀ (a b c : α), a * b ≤ a * c → b ≤ c
a b c : α
h : a * b ≤ c * a
⊢ b ≤ c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
⊢ a * c = b * d ↔ a = b ∧ c = d

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
  simp only [eq_iff_le_not_lt, hab, hcd, true_and]
  refine ⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩
  · exact (mul_lt_mul_of_pos_right hab c0).trans_le (mul_le_mul_of_nonneg_left hcd b0.le)
  · exact (mul_le_mul_of_nonneg_right hab c0.le).trans_lt (mul_lt_mul_of_pos_left hcd b0)

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

Goal state before:
pp: R : Type u
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : ZeroLEOneClass R
mul_nonneg : ∀ (a b : R), 0 ≤ a → 0 ≤ b → 0 ≤ a * b
a : R
ha : 0 ≤ a
b c : R
hbc : b ≤ c
⊢ b * a ≤ c * a

Tactic:
by
    simpa only [sub_mul, sub_nonneg] using mul_nonneg _ _ (sub_nonneg.2 hbc) ha

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hba : b ≤ a
hdc : d ≤ c
⊢ b * c + a * d ≤ a * c + b * d

Tactic:
add_comm (a * c)

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hba : b ≤ a
hdc : d ≤ c
⊢ b * c + a * d ≤ b * d + a * c
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₀
ha : 0 < a
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a

Tactic:
simpa using inv_mul_le_one₀ ha (b := 1)

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : AddLeftReflectLT R
inst✝² : ExistsAddOfLE R
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftStrictMono R
hba : b < a
hdc : d < c
⊢ b * c + a * d < a * c + b * d

Tactic:
add_comm (a * c)

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : AddLeftReflectLT R
inst✝² : ExistsAddOfLE R
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftStrictMono R
hba : b < a
hdc : d < c
⊢ b * c + a * d < b * d + a * c
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₀
ha : 0 < a
⊢ 1 < a⁻¹ ↔ a < 1

Tactic:
by simpa using one_lt_inv_mul₀ ha (b := 1)

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₀
hc : 0 < c
⊢ b / c < a ↔ b < a * c

Tactic:
rw [div_eq_mul_inv, mul_inv_lt_iff₀ hc]

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₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c⁻¹
⊢ a * c ≤ b

Tactic:
by
  obtain rfl | hc := hc.eq_or_lt
  · simpa using hb
  · rwa [le_mul_inv_iff₀ hc] at h

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 : β
⊢ f (EquivLike.inv f b) < f a ↔ b < f a

Tactic:
simp only [EquivLike.apply_inv_apply]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : ComplementedLattice α
f : α ≃o β
x : β
⊢ ∃ b, IsCompl x b

Tactic:
by
    obtain ⟨y, hy⟩ := exists_isCompl (f.symm x)
    rw [← f.symm_apply_apply y] at hy
    exact ⟨f y, f.symm.isCompl_iff.2 hy⟩

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

Goal state before:
pp: m x : ℤ
h1 : m ∣ x
h2 : |x| < m
⊢ x = 0

Tactic:
by_contra h

Goal state after:
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
h : ¬x = 0
⊢ False
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑n ≤ 0 ↔ n = 0

Tactic:
norm_cast; lia

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

Goal state before:
pp: x y : ℤ
hc : x = 0 ∧ y = 0
⊢ x.gcd y = 0

Tactic:
rw [hc.left, hc.right, gcd_zero_right, natAbs_zero]

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

Goal state before:
pp: M : Type u_1
inst✝ : Group M
a : M
m n : ℤ
⊢ a ^ m.gcd n = 1 ↔ a ^ m = 1 ∧ a ^ n = 1

Tactic:
obtain m | m := m <;> obtain n | n := n <;> simp

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

Goal state before:

Tactic:
n = a * p.succ + b * q.succ := this.symm
       _ ≤ q * p.succ + -1 * q.succ := by gcongr <;> lia
       _ = p * q - 1 := by simp_rw [Nat.cast_succ, mul_add, mul_comm]; lia
       _ ≤ n - 1 := by rwa [sub_le_sub_iff_right, ← Nat.cast_mul, Nat.cast_le]
       _ < n := by lia

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : EquivLike F α β
inst✝² : MulZeroClass α
inst✝¹ : MulZeroClass β
inst✝ : MulEquivClass F α β
f : F
⊢ f 0 = f 0 * f (EquivLike.inv f 0)

Tactic:
by rw [← map_mul, zero_mul]

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 : b ≤ a
hcb : c ≤ b
⊢ a - b = a - c - (b - c)

Tactic:
rw [tsub_tsub, add_tsub_cancel_of_le hcb]

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b✝ : α
n : ℕ
a b : α
hab✝ : a ≤ b
c : α
hc : c ≠ 0
hab : a < b
⊢ a * c ≤ b * c

Tactic:
exact (mul_lt_mul_of_pos_right hab hc.pos).le

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: case inr.inl
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
⊢ ∃ z ∈ insert y s, r x z ∧ r y z

Tactic:
obtain ⟨w, hws, hwr⟩ := ha x hx

Goal state after:
case inr.inl
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
w : α
hws : w ∈ s
hwr : r y w ∧ r x w
⊢ ∃ z ∈ insert y s, r x z ∧ r y z
Module: Mathlib.Algebra.Group.Invertible.Defs

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

Tactic:
← mul_right_inj_of_invertible (c := c),

Goal state after:
α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ c * (⅟c * a) = c * b ↔ a = c * b
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
hf : ∃ x, f x ≠ 1
a : G₀
h : IsUnit (f a)
⊢ IsUnit a

Tactic:
rcases eq_or_ne a 0 with (rfl | h)

Goal state after:
case inl
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
hf : ∃ x, f x ≠ 1
h : IsUnit (f 0)
⊢ IsUnit 0

case inr
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
hf : ∃ x, f x ≠ 1
a : G₀
h✝ : IsUnit (f a)
h : a ≠ 0
⊢ IsUnit a
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:

Tactic:
_ ≤ (2 * (a ^ 2 + b ^ 2)) ^ n := pow_le_pow_left₀ (sq_nonneg _) add_sq_le _
    _ = 2 ^ n * (a ^ 2 + b ^ 2) ^ n := by -- TODO: Should be `Nat.cast_commute`
        rw [Commute.mul_pow]; simp [Commute, SemiconjBy, two_mul, mul_two]
    _ ≤ 2 ^ n * (2 ^ (n - 1) * ((a ^ 2) ^ n + (b ^ 2) ^ n)) := mul_le_mul_of_nonneg_left
          (add_pow_le (sq_nonneg _) (sq_nonneg _) _) <| pow_nonneg (zero_le_two (α := R)) _
    _ = _ := by
      simp only [← mul_assoc, ← pow_add, ← pow_mul]
      cases n
      · rfl
      · simp [Nat.two_mul]

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

Goal state before:
pp: case inr
v : ℤ
h : -1 * v = -1
⊢ -1 = 1 ∧ v = -1 ∨ -1 = -1 ∧ v = 1

Tactic:
· simpa [Int.neg_mul] using h

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

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

Tactic:
by
  induction n with | zero => simp [geomSum] | succ n ih => ?_
  rw [geomSum, mul_add, mul_comm a, ← mul_assoc, ← ih,
    sub_mul, sub_mul, ← pow_succ, ← pow_succ', mul_comm, sub_add_sub_cancel]

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: case inr
α : Type u_1
a b c : α
inst✝ : Preorder α
h₂ : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) b c
h : b ≤ a
⊢ SymmGen (fun x1 x2 ↦ x1 ≤ x2) a c

Tactic:
· exact (h₂.ge.trans h).symmGen_symm

Goal state after: