awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.PositiveLinearMap (goal)
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
toLinearMap : E₁ →ₗ[R] E₂
monotone' : Monotone toLinearMap.toFun
toLinearMap_1 : E₁ →ₗ[R] E₂
monotone'_1 : Monotone toLinearMap_1.toFun
h :
  Eq (α := (a : E₁) → E₂) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap, monotone' := monotone' })
    ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap_1, monotone' := monotone'_1 })
⊢ toLinearMap = toLinearMap_1
have mk : Eq (α := (a : E₁) → E₂) (⇑toLinearMap : (a : E₁) → E₂) (⇑toLinearMap_1 : (a : E₁) → E₂)
Tactic: apply DFunLike.coe_injective'
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.PositiveLinearMap (goal)
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
x x_1 : E₁ →ₚ[R] E₂
h : x.toLinearMap = x_1.toLinearMap
⊢ x = x_1
have h₁ : ∀ (x_2 : E₁), Eq.{u_3 + 1} (α := E₂) ((x : (a : E₁) → E₂) x_2 : E₂) ((x_1 : (a : E₁) → E₂) x_2 : E₂)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.PositiveLinearMap (goal)
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
inst_7 : IsOrderedAddMonoid E₂
n : ℕ
f : E₁ →ₚ[R] E₂
x y : E₁
h : x ≤ y
⊢ (n • f.toLinearMap).toFun x ≤ (n • f.toLinearMap).toFun y
have zero : (HSMul.hSMul (α := ℕ) 0 f.toLinearMap).toFun x ≤ (HSMul.hSMul (α := ℕ) 0 f.toLinearMap).toFun y
Tactic: induction n with
    | zero => simp
    | succ n ih => simpa [add_nsmul] using add_le_add ih (OrderHomClass.mono f h)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.PositiveLinearMap (goal)
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
inst_7 : IsOrderedAddMonoid E₂
n : ℕ
f : E₁ →ₚ[R] E₂
x y : E₁
h : x ≤ y
zero : (HSMul.hSMul (α := ℕ) 0 f.toLinearMap).toFun x ≤ (HSMul.hSMul (α := ℕ) 0 f.toLinearMap).toFun y
⊢ (n • f.toLinearMap).toFun x ≤ (n • f.toLinearMap).toFun y
have succ : ∀ (n : ℕ) (ih : (n • f.toLinearMap).toFun x ≤ (n • f.toLinearMap).toFun y),
  ((n + 1) • f.toLinearMap).toFun x ≤ ((n + 1) • f.toLinearMap).toFun y
Tactic: induction n with
    | zero => simp
    | succ n ih => simpa [add_nsmul] using add_le_add ih (OrderHomClass.mono f h)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.PositiveLinearMap (goal)
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommGroup E₁
inst_2 : PartialOrder E₁
inst_3 : IsOrderedAddMonoid E₁
inst_4 : AddCommGroup E₂
inst_5 : PartialOrder E₂
inst_6 : IsOrderedAddMonoid E₂
inst_7 : Module R E₁
inst_8 : Module R E₂
f : E₁ →ₗ[R] E₂
hf : ∀ (x : E₁), 0 ≤ x → LE.le.{u_3} (α := E₂) (0 : E₂) ((f : (a : E₁) → E₂) x : E₂)
a b : E₁
hab : a ≤ b
⊢ f.toFun a ≤ f.toFun b
have rw : ∀ (hab : 0 ≤ b - a), 0 ≤ f.toFun b - f.toFun a
Tactic: rw [← sub_nonneg] at hab ⊢
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.PositiveLinearMap (hypothesis)
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommGroup E₁
inst_2 : PartialOrder E₁
inst_3 : IsOrderedAddMonoid E₁
inst_4 : AddCommGroup E₂
inst_5 : PartialOrder E₂
inst_6 : IsOrderedAddMonoid E₂
inst_7 : Module R E₁
inst_8 : Module R E₂
f : E₁ →ₗ[R] E₂
hf : ∀ (x : E₁), 0 ≤ x → LE.le.{u_3} (α := E₂) (0 : E₂) ((f : (a : E₁) → E₂) x : E₂)
a b : E₁
hab : 0 ≤ b - a
⊢ 0 ≤ f.toFun b - f.toFun a
have this : LE.le.{u_3} (α := E₂) (0 : E₂) ((f : (a : E₁) → E₂) (b - a) : E₂)
Tactic: have : 0 ≤ f (b - a) := hf _ hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
⊢ MulLeftMono R
have refine : ∀ (a b c : R) (h : b ≤ c), a * b ≤ a * c
Tactic: refine ⟨fun a b c h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
a b c : R
h : b ≤ c
⊢ a * b ≤ a * c
have rcases : ∀ (c : R) (h : b ≤ b + c), a * b ≤ a * (b + c)
Tactic: rcases exists_add_of_le h with ⟨c, rfl⟩
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ a * b ≤ a * (b + c)
have rw : a * b ≤ a * b + a * c
Tactic: rw [mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
⊢ MulRightMono R
have refine : ∀ (a b c : R) (h : b ≤ c),
  LE.le (α := R) (swap (φ := fun (a a_1 : R) ↦ R) (fun (x1 x2 : R) ↦ x1 * x2) a b : R)
    (swap (φ := fun (a a_1 : R) ↦ R) (fun (x1 x2 : R) ↦ x1 * x2) a c : R)
Tactic: refine ⟨fun a b c h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
a b c : R
h : b ≤ c
⊢ LE.le (α := R) (swap (φ := fun (a a_1 : R) ↦ R) (fun (x1 x2 : R) ↦ x1 * x2) a b : R)
    (swap (φ := fun (a a_1 : R) ↦ R) (fun (x1 x2 : R) ↦ x1 * x2) a c : R)
have dsimp : b * a ≤ c * a
Tactic: dsimp [swap]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
a b c : R
h : b ≤ c
⊢ b * a ≤ c * a
have rcases : ∀ (c : R) (h : b ≤ b + c), b * a ≤ (b + c) * a
Tactic: rcases exists_add_of_le h with ⟨c, rfl⟩
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ b * a ≤ (b + c) * a
have rw : b * a ≤ b * a + c * a
Tactic: rw [add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : PosMulStrictMono R
a b c d : R
hab : a < b
hcd : c < d
⊢ a * c < b * d
have this : MulPosStrictMono R
Tactic: have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : PosMulStrictMono R
a b c d : R
hab : a < b
hcd : c < d
this : MulPosStrictMono R
⊢ a * c < b * d
have inl : ∀ (hcd : 0 < d), a * 0 < b * d
Tactic: obtain rfl | hc := eq_zero_or_pos c
Cleared hypotheses: c, hcd
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : PosMulStrictMono R
a b c d : R
hab : a < b
hcd : c < d
this : MulPosStrictMono R
inl : ∀ (hcd : 0 < d), a * 0 < b * d
⊢ a * c < b * d
have inr : ∀ (hc : 0 < c), a * c < b * d
Tactic: obtain rfl | hc := eq_zero_or_pos c
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : PosMulStrictMono R
a b d : R
hab : a < b
this : MulPosStrictMono R
hcd : 0 < d
⊢ a * 0 < b * d
have inl : 0 < b * d
Tactic: rw [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
⊢ a * (b - c) = a * b - a * c
have inl : ∀ (hbc : b ≤ c), a * (b - c) = a * b - a * c
Tactic: obtain (hbc | hcb) := total_of (· ≤ ·) b c
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
inl : ∀ (hbc : b ≤ c), a * (b - c) = a * b - a * c
⊢ a * (b - c) = a * b - a * c
have inr : ∀ (hcb : c ≤ b), a * (b - c) = a * b - a * c
Tactic: obtain (hbc | hcb) := total_of (· ≤ ·) b c
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hbc : b ≤ c
⊢ a * (b - c) = a * b - a * c
have inl : a * 0 = a * b - a * c
Tactic: rw [tsub_eq_zero_iff_le.2 hbc, mul_zero, tsub_eq_zero_iff_le.2 (mul_le_mul_right hbc a)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hbc : b ≤ c
inl : a * 0 = a * b - a * c
⊢ a * (b - c) = a * b - a * c
have inl₁ : 0 = a * b - a * c
Tactic: rw [tsub_eq_zero_iff_le.2 hbc, mul_zero, tsub_eq_zero_iff_le.2 (mul_le_mul_right hbc a)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hbc : b ≤ c
inl : a * 0 = a * b - a * c
inl₁ : 0 = a * b - a * c
⊢ a * (b - c) = a * b - a * c
have inl₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [tsub_eq_zero_iff_le.2 hbc, mul_zero, tsub_eq_zero_iff_le.2 (mul_le_mul_right hbc a)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) = a * b - a * c
have inr : a * (b - c) + a * c = a * b
Tactic: apply h.eq_tsub_of_add_eq
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) + a * c = a * b
have inr : a * (b - c + c) = a * b
Tactic: rw [← mul_add, tsub_add_cancel_of_le hcb]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hcb : c ≤ b
inr : a * (b - c + c) = a * b
⊢ a * (b - c) + a * c = a * b
have inr₁ : a * b = a * b
Tactic: rw [← mul_add, tsub_add_cancel_of_le hcb]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
⊢ (a - b) * c = a * c - b * c
have inl : ∀ (hab : a ≤ b), (a - b) * c = a * c - b * c
Tactic: obtain (hab | hba) := total_of (· ≤ ·) a b
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
inl : ∀ (hab : a ≤ b), (a - b) * c = a * c - b * c
⊢ (a - b) * c = a * c - b * c
have inr : ∀ (hba : b ≤ a), (a - b) * c = a * c - b * c
Tactic: obtain (hab | hba) := total_of (· ≤ ·) a b
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c
have inl : 0 * c = a * c - b * c
Tactic: rw [tsub_eq_zero_iff_le.2 hab, zero_mul, tsub_eq_zero_iff_le.2 (mul_le_mul_left hab c)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hab : a ≤ b
inl : 0 * c = a * c - b * c
⊢ (a - b) * c = a * c - b * c
have inl₁ : 0 = a * c - b * c
Tactic: rw [tsub_eq_zero_iff_le.2 hab, zero_mul, tsub_eq_zero_iff_le.2 (mul_le_mul_left hab c)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hab : a ≤ b
inl : 0 * c = a * c - b * c
inl₁ : 0 = a * c - b * c
⊢ (a - b) * c = a * c - b * c
have inl₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [tsub_eq_zero_iff_le.2 hab, zero_mul, tsub_eq_zero_iff_le.2 (mul_le_mul_left hab c)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b) * c = a * c - b * c
have inr : (a - b) * c + b * c = a * c
Tactic: apply h.eq_tsub_of_add_eq
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b) * c + b * c = a * c
have inr : (a - b + b) * c = a * c
Tactic: rw [← add_mul, tsub_add_cancel_of_le hba]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
inr : (a - b + b) * c = a * c
⊢ (a - b) * c + b * c = a * c
have inr₁ : a * c = a * c
Tactic: rw [← add_mul, tsub_add_cancel_of_le hba]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a b : R
⊢ a * (b - 1) = a * b - a
have rw : a * b - a * 1 = a * b - a
Tactic: rw [mul_tsub, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a b : R
rw : a * b - a * 1 = a * b - a
⊢ a * (b - 1) = a * b - a
have rw₁ : a * b - a = a * b - a
Tactic: rw [mul_tsub, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : MulRightMono R
inst_7 : AddLeftReflectLE R
a b : R
⊢ (a - 1) * b = a * b - b
have rw : a * b - 1 * b = a * b - b
Tactic: rw [tsub_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : NonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : MulRightMono R
inst_7 : AddLeftReflectLE R
a b : R
rw : a * b - 1 * b = a * b - b
⊢ (a - 1) * b = a * b - b
have rw₁ : a * b - b = a * b - b
Tactic: rw [tsub_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a b : R
⊢ a * a - b * b = (a + b) * (a - b)
have rw : a * a - b * b = (a + b) * a - (a + b) * b
Tactic: rw [mul_tsub, add_mul, add_mul, tsub_add_eq_tsub_tsub, mul_comm b a, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a b : R
rw : a * a - b * b = (a + b) * a - (a + b) * b
⊢ a * a - b * b = (a + b) * (a - b)
have rw₁ : a * a - b * b = a * a + b * a - (a + b) * b
Tactic: rw [mul_tsub, add_mul, add_mul, tsub_add_eq_tsub_tsub, mul_comm b a, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a b : R
rw : a * a - b * b = (a + b) * a - (a + b) * b
rw₁ : a * a - b * b = a * a + b * a - (a + b) * b
⊢ a * a - b * b = (a + b) * (a - b)
have rw₂ : a * a - b * b = a * a + b * a - (a * b + b * b)
Tactic: rw [mul_tsub, add_mul, add_mul, tsub_add_eq_tsub_tsub, mul_comm b a, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a b : R
rw : a * a - b * b = (a + b) * a - (a + b) * b
rw₁ : a * a - b * b = a * a + b * a - (a + b) * b
rw₂ : a * a - b * b = a * a + b * a - (a * b + b * b)
⊢ a * a - b * b = (a + b) * (a - b)
have rw₃ : a * a - b * b = a * a + b * a - a * b - b * b
Tactic: rw [mul_tsub, add_mul, add_mul, tsub_add_eq_tsub_tsub, mul_comm b a, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a b : R
rw : a * a - b * b = (a + b) * a - (a + b) * b
rw₁ : a * a - b * b = a * a + b * a - (a + b) * b
rw₂ : a * a - b * b = a * a + b * a - (a * b + b * b)
rw₃ : a * a - b * b = a * a + b * a - a * b - b * b
⊢ a * a - b * b = (a + b) * (a - b)
have rw₄ : a * a - b * b = a * a + a * b - a * b - b * b
Tactic: rw [mul_tsub, add_mul, add_mul, tsub_add_eq_tsub_tsub, mul_comm b a, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a b : R
rw : a * a - b * b = (a + b) * a - (a + b) * b
rw₁ : a * a - b * b = a * a + b * a - (a + b) * b
rw₂ : a * a - b * b = a * a + b * a - (a * b + b * b)
rw₃ : a * a - b * b = a * a + b * a - a * b - b * b
rw₄ : a * a - b * b = a * a + a * b - a * b - b * b
⊢ a * a - b * b = (a + b) * (a - b)
have rw₅ : a * a - b * b = a * a - b * b
Tactic: rw [mul_tsub, add_mul, add_mul, tsub_add_eq_tsub_tsub, mul_comm b a, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a b : R
⊢ HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)
have rw : a * a - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)
Tactic: rw [sq, sq, mul_self_tsub_mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a b : R
rw : a * a - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)
⊢ HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)
have rw₁ : a * a - b * b = (a + b) * (a - b)
Tactic: rw [sq, sq, mul_self_tsub_mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a b : R
rw : a * a - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)
rw₁ : a * a - b * b = (a + b) * (a - b)
⊢ HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)
have rw₂ : (a + b) * (a - b) = (a + b) * (a - b)
Tactic: rw [sq, sq, mul_self_tsub_mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a : R
⊢ a * a - 1 = (a + 1) * (a - 1)
have rw : a * a - 1 = a * a - HMul.hMul (α := R) 1 1
Tactic: rw [← mul_self_tsub_mul_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Canonical (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a : R
rw : a * a - 1 = a * a - HMul.hMul (α := R) 1 1
⊢ a * a - 1 = (a + 1) * (a - 1)
have rw₁ : a * a - 1 = a * a - 1
Tactic: rw [← mul_self_tsub_mul_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Algebra (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p : R[X]
n : ℕ
ih : eval₂ (algebraMap R S) x (p ^ n) = eval₂ (algebraMap R S) x p ^ n
⊢ eval₂ (algebraMap R S) x (p ^ (n + 1)) = eval₂ (algebraMap R S) x p ^ (n + 1)
have succ : eval₂ (algebraMap R S) x (p ^ n * p) = eval₂ (algebraMap R S) x p ^ (n + 1)
Tactic: rw [pow_succ, pow_succ, eval₂_mul', ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Algebra (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p : R[X]
n : ℕ
ih : eval₂ (algebraMap R S) x (p ^ n) = eval₂ (algebraMap R S) x p ^ n
succ : eval₂ (algebraMap R S) x (p ^ n * p) = eval₂ (algebraMap R S) x p ^ (n + 1)
⊢ eval₂ (algebraMap R S) x (p ^ (n + 1)) = eval₂ (algebraMap R S) x p ^ (n + 1)
have succ₁ : eval₂ (algebraMap R S) x (p ^ n * p) = eval₂ (algebraMap R S) x p ^ n * eval₂ (algebraMap R S) x p
Tactic: rw [pow_succ, pow_succ, eval₂_mul', ih]