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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
⊢ CharZero R

Tactic:
refine ⟨fun m n h => @Nat.cast_injective M _ _ _ _ ?_⟩
  rw [← nsmul_one, ← nsmul_one, ← Nat.cast_smul_eq_nsmul R, ← Nat.cast_smul_eq_nsmul R, h]

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

Goal state before:
pp: α : Type u_4
inst✝ : NonAssocSemiring α
⊢ (Set.range fun x ↦ 2 * x) = {a | Even a}

Tactic:
ext x

Goal state after:
α : Type u_4
inst✝ : NonAssocSemiring α
x : α
⊢ (x ∈ Set.range fun x ↦ 2 * x) ↔ x ∈ {a | Even a}
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_4
inst✝ : Semiring α
⊢ (Set.range fun x ↦ 2 * x + 1) = {a | Odd a}

Tactic:
ext x

Goal state after:
α : Type u_4
inst✝ : Semiring α
x : α
⊢ (x ∈ Set.range fun x ↦ 2 * x + 1) ↔ x ∈ {a | Odd a}
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
⊢ r b c

Tactic:
rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a]

Goal state after:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
⊢ r (b * a * a⁻¹) (c * a * a⁻¹)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
h : IsUnit 2
a : α
⊢ Odd a

Tactic:
rw [← sub_add_cancel a 1]

Goal state after:
α : Type u_2
inst✝ : Ring α
h : IsUnit 2
a : α
⊢ Odd (a - 1 + 1)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: m n : ℕ
⊢ m / n % 2 = 0 ↔ m % (2 * n) / n = 0

Tactic:
← Nat.mod_mul_right_div_self,

Goal state after:
m n : ℕ
⊢ m % (n * 2) / n = 0 ↔ m % (2 * n) / n = 0
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftReflectLE α
h : a + d = c + b
⊢ a + d - d - b = c + b - b - d

Tactic:
by rw [h, tsub_right_comm]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
this✝ : MulLeftMono α
this : MulRightMono α
h : a₂ * b₂ ≤ a₁ * b₁
⊢ a₁ = a₂ ∧ b₁ = b₂

Tactic:
simp only [eq_iff_le_not_lt, ha, hb, true_and]

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
this✝ : MulLeftMono α
this : MulRightMono α
h : a₂ * b₂ ≤ a₁ * b₁
⊢ ¬a₁ < a₂ ∧ ¬b₁ < b₂
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a = 1 ∧ b = 1 → a * b = 1

Tactic:
by rintro ⟨rfl, rfl⟩; rw [mul_one]

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ a⁻¹ ≤ a ↔ 1 ≤ a

Tactic:
by simp [inv_le_iff_one_le_mul']

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝² : MulZeroClass α
a✝ b✝ c d : α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLE α
a : α>0
b : α
h : ↑a * b < ↑a * b
⊢ False

Tactic:
simp at h

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝² : MulZeroClass α
a✝ b✝ c d : α
inst✝¹ : PartialOrder α
inst✝ : MulPosReflectLE α
a : α>0
b : α
h : b * ↑a < b * ↑a
⊢ False

Tactic:
simp at h

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

Goal state before:
pp: case inl
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a : R
ha✝ : a ≠ 0
x✝¹ x✝ : R
h : (fun x ↦ a * x) x✝¹ = (fun x ↦ a * x) x✝
ha : a < 0
⊢ x✝¹ = x✝

pp: case inr
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a : R
ha✝ : a ≠ 0
x✝¹ x✝ : R
h : (fun x ↦ a * x) x✝¹ = (fun x ↦ a * x) x✝
ha : 0 < a
⊢ x✝¹ = x✝

Tactic:
exacts [(strictAnti_mul_left ha).injective h, (strictMono_mul_left_of_pos ha).injective h]

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

Goal state before:
pp: case inl
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a : R
ha✝ : a ≠ 0
x✝¹ x✝ : R
h : (fun x ↦ x * a) x✝¹ = (fun x ↦ x * a) x✝
ha : a < 0
⊢ x✝¹ = x✝

pp: case inr
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a : R
ha✝ : a ≠ 0
x✝¹ x✝ : R
h : (fun x ↦ x * a) x✝¹ = (fun x ↦ x * a) x✝
ha : 0 < a
⊢ x✝¹ = x✝

Tactic:
exacts [(strictAnti_mul_right ha).injective h, (strictMono_mul_right_of_pos ha).injective h]

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:
rw [div_eq_mul_inv a c, div_eq_mul_inv b c]
  gcongr; exact Right.inv_nonneg.2 hc

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b : R
⊢ a ^ 2 + b ^ 2 + 2 * a * b = a ^ 2 + 2 * a * b + b ^ 2

Tactic:
by rw [add_right_comm]

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✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLT R
inst✝ : AddLeftStrictMono R
⊢ 0 < a * -b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
mul_pos_iff (R := R),

Goal state after:
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLT R
inst✝ : AddLeftStrictMono R
⊢ 0 < a ∧ 0 < -b ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Module: Mathlib.Algebra.Order.Group.OrderIso

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a : α
⊢ (mulRight a).symm = mulRight a⁻¹

Tactic:
ext x

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a x : α
⊢ (mulRight a).symm x = (mulRight a⁻¹) x
Module: Mathlib.Algebra.Order.Group.OrderIso

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a : α
⊢ (mulLeft a).symm = mulLeft a⁻¹

Tactic:
ext x

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a x : α
⊢ (mulLeft a).symm x = (mulLeft a⁻¹) x
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
⊢ (refl α).trans e = e

Tactic:
ext x

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
x : α
⊢ ((refl α).trans e) x = e x
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
⊢ e.trans (refl β) = e

Tactic:
ext x

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
x : α
⊢ (e.trans (refl β)) x = e x
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
⊢ ↑a.natAbs ≤ a ^ 2

Tactic:
by
  rw [← Int.natAbs_sq a, sq]
  norm_cast
  apply Nat.le_mul_self

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ

Tactic:
by
  apply le_of_mul_le_of_one_le_right _ (one_le_mabs _); rw [mabs_div_sup_mul_mabs_div_inf]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemigroup R
a b : R
⊢ IsRegular (a * b) ↔ IsRegular (a * b) ∧ IsRegular (b * a)

Tactic:
exact ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩

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

Goal state before:
pp: β : Type u_2
inst✝ : MulOneClass β
⊢ ↑(map' (MonoidHom.id β)) = MonoidHom.id (WithZero β)

Tactic:
ext x

Goal state after:
β : Type u_2
inst✝ : MulOneClass β
x : WithZero β
⊢ ↑(map' (MonoidHom.id β)) x = (MonoidHom.id (WithZero β)) x
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b✝ c b : α
h : ⊤ + b = 0
⊢ False

Tactic:
simp at h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝ : WithZero α ≃* WithZero β
⊢ (fun e ↦ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
      ((fun e ↦ { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
        x✝) =
    x✝

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝ : WithZero α ≃* WithZero β
x : WithZero α
⊢ ((fun e ↦ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
        ((fun e ↦
            { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
          x✝))
      x =
    x✝ x
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 : α
hc : AddLECancellable c
h : c ≤ a
h2 : a < b
⊢ a - c < b - c

Tactic:
apply hc.lt_tsub_of_add_lt_left
  rwa [add_tsub_cancel_of_le h]

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

Goal state before:
pp: case coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
a✝ : α
⊢ map (⇑f) (↑a✝ + b) = map ⇑f ↑a✝ + map (⇑f) b

Tactic:
induction b
    · exact (add_top _).symm
    · rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
      rfl

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
⊢ (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
x : WithBot α
⊢ (e₁.trans e₂).withBotCongr x = (e₁.withBotCongr.trans e₂.withBotCongr) x
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : LE α
x : WithBot α
hx : x = ⊥ → a ≤ b
⊢ unbotD a x ≤ b ↔ x ≤ ↑b

Tactic:
by cases x <;> simp [hx]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : LT α
x : WithBot α
hx : x = ⊥ → a < b
⊢ unbotD a x < b ↔ x < ↑b

Tactic:
by cases x <;> simp [hx]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedAddCommMonoidWithTop α
a : α
ha : 0 < Multiplicative.ofAdd (OrderDual.toDual a)
b c : α
hbc : c < b
⊢ a ≠ ⊤

Tactic:
simpa using! ha.ne'

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝² : Add α
inst✝¹ : Add β
inst✝ : Add γ
e₁ : α ≃+ β
e₂ : β ≃+ γ
⊢ (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr

Tactic:
ext x

Goal state after:
α : Type u
β : Type v
γ : Type u_1
inst✝² : Add α
inst✝¹ : Add β
inst✝ : Add γ
e₁ : α ≃+ β
e₂ : β ≃+ γ
x : WithBot α
⊢ (e₁.trans e₂).withBotCongr x = (e₁.withBotCongr.trans e₂.withBotCongr) x
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
EX : ∃ n, P (b + ↑n)
n : ℕ
h : P (b + ↑n)
⊢ b + ↑(Nat.find EX) ≤ b + ↑n

Tactic:
Nat.find_min' EX h

Goal state after:
P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
EX : ∃ n, P (b + ↑n)
n : ℕ
h : P (b + ↑n)
⊢ b + ↑n ≤ b + ↑n
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
floor : α → ℤ
gc_coe_floor : GaloisConnection Int.cast floor
a : α
z : ℤ
⊢ -z ≤ floor (-a) ↔ a ≤ ↑z

Tactic:
← gc_coe_floor,

Goal state after:
F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
floor : α → ℤ
gc_coe_floor : GaloisConnection Int.cast floor
a : α
z : ℤ
⊢ ↑(-z) ≤ -a ↔ a ≤ ↑z
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ↑n ≤ ⌊a⌋ ↔ ↑n ≤ a

Tactic:
Int.le_floor,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ↑↑n ≤ a ↔ ↑n ≤ a
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ a + (↑b + ↑d) ↔ b ≤ ⌊a⌋₊ + (b + d)

Tactic:
add_left_comm _ b,

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ a + (↑b + ↑d) ↔ b ≤ b + (⌊a⌋₊ + d)
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
    exact ⟨w, Set.mem_insert_of_mem _ hws, hwr.symm⟩

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

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
n : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
hn : n ≠ 0
⊢ x ^ n + y ^ n ≤ (x + y) ^ n

Tactic:
by
  rcases Nat.exists_eq_add_one_of_ne_zero hn with ⟨k, rfl⟩
  induction k with
  | zero => simp only [zero_add, pow_one, le_refl]
  | succ k ih =>
    let n := k.succ
    have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n))
    have h2 := add_nonneg hx hy
    calc
      x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) := by
        rw [pow_succ' _ n, pow_succ' _ n]
        exact le_add_of_nonneg_right h1
      _ = (x + y) * (x ^ n + y ^ n) := by
        rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
          add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
      _ ≤ (x + y) ^ (n + 1) := by
        rw [pow_succ' _ n]
        gcongr; exact ih (Nat.succ_ne_zero k)

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

Goal state before:
pp: case hab
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ≤ a + b

Tactic:
try assumption

Goal state after:
case hab
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ≤ a + b
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case hab
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ b ≤ a + b

Tactic:
try assumption

Goal state after:
case hab
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ b ≤ a + b
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b + c / d = (a * d + b * c) / (b * d)

Tactic:
by
  rw [add_div, mul_div_mul_right _ b hd, hbc.eq, hbd.eq, mul_div_mul_right c d hb]

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

Goal state before:
pp: case ha
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ 0 ≤ |a - b|

pp: case hbc
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n

Tactic:
· exact abs_nonneg _

Goal state after:
case hbc
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
n : ℕ
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
⊢ a ^ 0 = b ^ 0 ↔ 0 = 0 ∨ a = b ∨ a = -b ∧ Even 0

case inr
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
n : ℕ
hn : n ≠ 0
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x ↦ x ∈ s
inst✝ : DecidablePred fun x ↦ x ∈ t
e₀ : ↑s ≃ ↑t
e : { e // ∀ (x : ↑s), e ↑x = ↑(e₀ x) }
⊢ (fun e₁ ↦ ⟨Trans.trans (Trans.trans (Set.sumCompl s).symm (e₀.sumCongr e₁)) (Set.sumCompl t), ⋯⟩)
      ((fun e ↦ (↑e).subtypeEquiv ⋯) e) =
    e

Tactic:
ext x

Goal state after:
α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x ↦ x ∈ s
inst✝ : DecidablePred fun x ↦ x ∈ t
e₀ : ↑s ≃ ↑t
e : { e // ∀ (x : ↑s), e ↑x = ↑(e₀ x) }
x : α
⊢ ↑((fun e₁ ↦ ⟨Trans.trans (Trans.trans (Set.sumCompl s).symm (e₀.sumCongr e₁)) (Set.sumCompl t), ⋯⟩)
          ((fun e ↦ (↑e).subtypeEquiv ⋯) e))
      x =
    ↑e x
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case inr
γ : Type u_3
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ Iio i = Iic j

Tactic:
exact Set.ext fun k => ⟨fun hk_lt => hj.1 hk_lt, fun hk_le_j => lt_of_le_of_lt hk_le_j hj_lt_i⟩

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeInf α
a b : α
⊢ Iic a ∩ Iic b = Iic (a ⊓ b)

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝ : SemilatticeInf α
a b x : α
⊢ x ∈ Iic a ∩ Iic b ↔ x ∈ Iic (a ⊓ b)
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a₁ a₂ b₁ b₂ : α
⊢ Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Tactic:
simp only [Ici_inter_Iic.symm, Ici_inter_Ici.symm, Iic_inter_Iic.symm]; ac_rfl

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: case eq
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * db + nb * da = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑db * ⅟↑da * ⅟↑db + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑da * ⅟↑db
h₂ : ↑nc * ↑(da * db) * (⅟↑da * ⅟↑db * ⅟↑dc) = ↑nc * ↑(k * dc) * (⅟↑da * ⅟↑db * ⅟↑dc)
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
simp only [H, mul_invOf_cancel_right', Nat.cast_mul, ← mul_assoc] at h₁ h₂

Goal state after:
case eq
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * db + nb * da = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑db * ⅟↑da * ⅟↑db + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑da * ⅟↑db
h₂ : ↑nc * ↑(da * db) * (⅟↑da * ⅟↑db * ⅟↑dc) = ↑nc * ↑(k * dc) * (⅟↑da * ⅟↑db * ⅟↑dc)
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
simp only [H, mul_invOf_cancel_right', Nat.cast_mul, ← mul_assoc] at h₁ h₂

Goal state after:
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
⊢ a < (a + b) / 2 ↔ a < b

Tactic:
simp [lt_div_iff₀, mul_two]

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 0 < a ^ n

Tactic:
exact pow_pos (zero_lt_one.trans_le a1) _

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 0 < a ^ m

Tactic:
exact pow_pos (zero_lt_one.trans_le a1) _

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

Goal state before:
pp: case inl
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb : 0 ≤ 0
h : ∀ (ε : α), 1 < ε → a ≤ 0
⊢ a ≤ 0

Tactic:
exact h 2 one_lt_two

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
⊢ AntitoneOn (fun x ↦ x⁻¹) (Set.Iio 0)

Tactic:
convert! sub_inv_antitoneOn_Iio (α := α)

Goal state after:
case e'_5
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
x✝ : α
⊢ x✝ = x✝ - 0
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
l₁ l₂ : List α
⊢ l₁.length ≤ (l₁ ++ l₂).length

Tactic:
by simp only [length_append, Nat.le_add_right]

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
a : α
⊢ l₁.length ≤ (l₁ ++ l₂).length

Tactic:
by simp only [length_append, Nat.le_add_right]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
h : a < b
⊢ a + -(a / 2) + b / 2 < b

Tactic:
← sub_eq_add_neg,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
h : a < b
⊢ a - a / 2 + b / 2 < b