awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Nontrivial R
x : R
hx : IsRegular x
⊢ 0 < star x * x
have rw : 0 ≠ x
Tactic: rw [(star_mul_self_nonneg _).lt_iff_ne, ← mul_zero (star x), hx.star.left.ne_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
⊢ 0 ≤ u * x * star u ↔ 0 ≤ x
have refine : ∀ (h : 0 ≤ u * x * star u), 0 ≤ x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ star_right_conjugate_nonneg h _⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
⊢ 0 ≤ x
have obtain : ∀ (v : R) (hv : v * u = 1), 0 ≤ x
Tactic: obtain ⟨v, hv⟩ := hu.exists_left_inv
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
⊢ 0 ≤ x
have this : 0 ≤ v * u * x * star u * star v
Tactic: have := by simpa [← mul_assoc] using star_right_conjugate_nonneg h v
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ v * u * x * star u * star v
⊢ 0 ≤ x
have rwa : ∀ (this : 0 ≤ 1 * x * star u * star v), 0 ≤ x
Tactic: rwa [hv, one_mul, mul_assoc, ← star_mul, hv, star_one, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ v * u * x * star u * star v
rwa : ∀ (this : 0 ≤ 1 * x * star u * star v), 0 ≤ x
⊢ 0 ≤ x
have rwa₁ : ∀ (this : 0 ≤ x * star u * star v), 0 ≤ x
Tactic: rwa [hv, one_mul, mul_assoc, ← star_mul, hv, star_one, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ v * u * x * star u * star v
rwa : ∀ (this : 0 ≤ 1 * x * star u * star v), 0 ≤ x
rwa₁ : ∀ (this : 0 ≤ x * star u * star v), 0 ≤ x
⊢ 0 ≤ x
have rwa₂ : ∀ (this : 0 ≤ x * (star u * star v)), 0 ≤ x
Tactic: rwa [hv, one_mul, mul_assoc, ← star_mul, hv, star_one, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ v * u * x * star u * star v
rwa : ∀ (this : 0 ≤ 1 * x * star u * star v), 0 ≤ x
rwa₁ : ∀ (this : 0 ≤ x * star u * star v), 0 ≤ x
rwa₂ : ∀ (this : 0 ≤ x * (star u * star v)), 0 ≤ x
⊢ 0 ≤ x
have rwa₃ : ∀ (this : 0 ≤ x * star (v * u)), 0 ≤ x
Tactic: rwa [hv, one_mul, mul_assoc, ← star_mul, hv, star_one, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ v * u * x * star u * star v
rwa : ∀ (this : 0 ≤ 1 * x * star u * star v), 0 ≤ x
rwa₁ : ∀ (this : 0 ≤ x * star u * star v), 0 ≤ x
rwa₂ : ∀ (this : 0 ≤ x * (star u * star v)), 0 ≤ x
rwa₃ : ∀ (this : 0 ≤ x * star (v * u)), 0 ≤ x
⊢ 0 ≤ x
have rwa₄ : ∀ (this : 0 ≤ x * star 1), 0 ≤ x
Tactic: rwa [hv, one_mul, mul_assoc, ← star_mul, hv, star_one, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ v * u * x * star u * star v
rwa : ∀ (this : 0 ≤ 1 * x * star u * star v), 0 ≤ x
rwa₁ : ∀ (this : 0 ≤ x * star u * star v), 0 ≤ x
rwa₂ : ∀ (this : 0 ≤ x * (star u * star v)), 0 ≤ x
rwa₃ : ∀ (this : 0 ≤ x * star (v * u)), 0 ≤ x
rwa₄ : ∀ (this : 0 ≤ x * star 1), 0 ≤ x
⊢ 0 ≤ x
have rwa₅ : ∀ (this : 0 ≤ x * 1), 0 ≤ x
Tactic: rwa [hv, one_mul, mul_assoc, ← star_mul, hv, star_one, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ v * u * x * star u * star v
rwa : ∀ (this : 0 ≤ 1 * x * star u * star v), 0 ≤ x
rwa₁ : ∀ (this : 0 ≤ x * star u * star v), 0 ≤ x
rwa₂ : ∀ (this : 0 ≤ x * (star u * star v)), 0 ≤ x
rwa₃ : ∀ (this : 0 ≤ x * star (v * u)), 0 ≤ x
rwa₄ : ∀ (this : 0 ≤ x * star 1), 0 ≤ x
rwa₅ : ∀ (this : 0 ≤ x * 1), 0 ≤ x
⊢ 0 ≤ x
have rwa₆ : ∀ (this : 0 ≤ x), 0 ≤ x
Tactic: rwa [hv, one_mul, mul_assoc, ← star_mul, hv, star_one, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonUnitalSemiring R
inst_1 : StarRing R
inst_2 : PartialOrder R
inst_3 : StarOrderedRing R
x y : Rᵐᵒᵖ
⊢ x ≤ y ↔
    ∃ (p : Rᵐᵒᵖ),
      Membership.mem (γ := AddSubmonoid Rᵐᵒᵖ) (AddSubmonoid.closure (range fun (s : Rᵐᵒᵖ) ↦ star s * s)) p ∧ y = x + p
have rw : (∃ (p : R),
    Membership.mem (γ := AddSubmonoid R)
        (AddSubmonoid.comap (F := R ≃+ Rᵐᵒᵖ) opAddEquiv
          (AddSubmonoid.map (F := R ≃+ Rᵐᵒᵖ) opAddEquiv (AddSubmonoid.closure (range fun (s : R) ↦ star s * s))))
        p ∧
      unop y = unop x + p) ↔
  ∃ (x_1 : R),
    Membership.mem (γ := AddSubmonoid Rᵐᵒᵖ) (AddSubmonoid.closure (range fun (s : Rᵐᵒᵖ) ↦ star s * s)) (op x_1) ∧
      y = x + op x_1
Tactic: rw [← unop_le_unop, StarOrderedRing.le_iff, op_surjective.exists,
      ← (AddSubmonoid.closure _).comap_map_eq_of_injective opAddEquiv.injective]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonUnitalSemiring R
inst_1 : StarRing R
inst_2 : PartialOrder R
inst_3 : StarOrderedRing R
x y : Rᵐᵒᵖ
⊢ (∃ (p : R),
      Membership.mem (γ := AddSubmonoid R)
          (AddSubmonoid.comap (F := R ≃+ Rᵐᵒᵖ) opAddEquiv
            (AddSubmonoid.map (F := R ≃+ Rᵐᵒᵖ) opAddEquiv (AddSubmonoid.closure (range fun (s : R) ↦ star s * s))))
          p ∧
        unop y = unop x + p) ↔
    ∃ (x_1 : R),
      Membership.mem (γ := AddSubmonoid Rᵐᵒᵖ) (AddSubmonoid.closure (range fun (s : Rᵐᵒᵖ) ↦ star s * s)) (op x_1) ∧
        y = x + op x_1
have a : ∀ (p : R),
  Membership.mem (γ := AddSubmonoid R)
      (AddSubmonoid.comap (F := R ≃+ Rᵐᵒᵖ) opAddEquiv
        (AddSubmonoid.map (F := R ≃+ Rᵐᵒᵖ) opAddEquiv (AddSubmonoid.closure (range fun (s : R) ↦ star s * s))))
      p ↔
    Membership.mem (γ := AddSubmonoid Rᵐᵒᵖ) (AddSubmonoid.closure (range fun (s : Rᵐᵒᵖ) ↦ star s * s)) (op p)
Tactic: congr! with p
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonUnitalSemiring R
inst_1 : StarRing R
inst_2 : PartialOrder R
inst_3 : StarOrderedRing R
x y : Rᵐᵒᵖ
a :
  ∀ (p : R),
    Membership.mem (γ := AddSubmonoid R)
        (AddSubmonoid.comap (F := R ≃+ Rᵐᵒᵖ) opAddEquiv
          (AddSubmonoid.map (F := R ≃+ Rᵐᵒᵖ) opAddEquiv (AddSubmonoid.closure (range fun (s : R) ↦ star s * s))))
        p ↔
      Membership.mem (γ := AddSubmonoid Rᵐᵒᵖ) (AddSubmonoid.closure (range fun (s : Rᵐᵒᵖ) ↦ star s * s)) (op p)
⊢ (∃ (p : R),
      Membership.mem (γ := AddSubmonoid R)
          (AddSubmonoid.comap (F := R ≃+ Rᵐᵒᵖ) opAddEquiv
            (AddSubmonoid.map (F := R ≃+ Rᵐᵒᵖ) opAddEquiv (AddSubmonoid.closure (range fun (s : R) ↦ star s * s))))
          p ∧
        unop y = unop x + p) ↔
    ∃ (x_1 : R),
      Membership.mem (γ := AddSubmonoid Rᵐᵒᵖ) (AddSubmonoid.closure (range fun (s : Rᵐᵒᵖ) ↦ star s * s)) (op x_1) ∧
        y = x + op x_1
have a₁ : ∀ (p : R), unop y = unop x + p ↔ y = x + op p
Tactic: congr! with p
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
r : R
hr : 0 ≤ r
a b : A
hab : a ≤ b
⊢ r • a ≤ r • b
have rw : ∀ (hr : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r) (a b : A)
  (hab : a ≤ b), r • a ≤ r • b
Tactic: rw [StarOrderedRing.nonneg_iff] at hr
Cleared hypotheses: hr, a, b, hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
r : R
hr : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r
a b : A
hab : a ≤ b
⊢ r • a ≤ r • b
have rw : ∀
  (hab :
    ∃ (p : A),
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ b = a + p),
  ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ r • b = r • a + p
Tactic: rw [StarOrderedRing.le_iff] at hab ⊢
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
r : R
hr : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r
a b : A
hab :
  ∃ (p : A), Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ b = a + p
⊢ ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ r • b = r • a + p
have obtain : ∀ (a_1 : A) (ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a_1),
  ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧
      r • (a + a_1) = r • a + p
Tactic: obtain ⟨a, ha, rfl⟩ := hab
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
a : A
ha : 0 ≤ a
r s : R
hrs : r ≤ s
⊢ r • a ≤ s • a
have rw : ∀ (ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a) (r s : R)
  (hrs : r ≤ s), r • a ≤ s • a
Tactic: rw [StarOrderedRing.nonneg_iff] at ha
Cleared hypotheses: ha, r, s, hrs
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
r s : R
hrs : r ≤ s
⊢ r • a ≤ s • a
have rw : ∀
  (hrs :
    ∃ (p : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ s = r + p),
  ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ s • a = r • a + p
Tactic: rw [StarOrderedRing.le_iff] at hrs ⊢
Cleared hypotheses: hrs
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
r s : R
hrs :
  ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ s = r + p
⊢ ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ s • a = r • a + p
have obtain : ∀ (r_1 : R) (hr : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r_1),
  ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧
      (r + r_1) • a = r • a + p
Tactic: obtain ⟨r, hr, rfl⟩ := hrs
Cleared hypotheses: s, hrs
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : IsDomain R
inst_13 : IsCancelAdd A
inst_14 : Module.IsTorsionFree R A
r : R
hr : 0 < r
a b : A
hab : a < b
⊢ r • a < r • b
have rw : ∀ (hr : r ≠ 0 ∧ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r)
  (a b : A) (hab : a < b), r • a < r • b
Tactic: rw [StarOrderedRing.pos_iff] at hr
Cleared hypotheses: hr, a, b, hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : IsDomain R
inst_13 : IsCancelAdd A
inst_14 : Module.IsTorsionFree R A
r : R
hr : r ≠ 0 ∧ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r
a b : A
hab : a < b
⊢ r • a < r • b
have rw : ∀
  (hab :
    ∃ (p : A),
      p ≠ 0 ∧
        Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ b = a + p),
  ∃ (p : A),
    p ≠ 0 ∧
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ r • b = r • a + p
Tactic: rw [StarOrderedRing.lt_iff] at hab ⊢
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : IsDomain R
inst_13 : IsCancelAdd A
inst_14 : Module.IsTorsionFree R A
r : R
hr : r ≠ 0 ∧ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r
a b : A
hab :
  ∃ (p : A),
    p ≠ 0 ∧ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ b = a + p
⊢ ∃ (p : A),
    p ≠ 0 ∧
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ r • b = r • a + p
have obtain : ∀ (a_1 : A) (ha₀ : a_1 ≠ 0)
  (ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a_1),
  ∃ (p : A),
    p ≠ 0 ∧
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧
        r • (a + a_1) = r • a + p
Tactic: obtain ⟨a, ha₀, ha, rfl⟩ := hab
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : IsDomain R
inst_13 : IsCancelAdd A
inst_14 : Module.IsTorsionFree R A
r : R
hr : r ≠ 0 ∧ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r
a_1 a : A
ha₀ : a ≠ 0
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
⊢ ∃ (p : A),
    p ≠ 0 ∧
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧
        r • (a_1 + a) = r • a_1 + p
have hr₀ : r ≠ 0
Tactic: obtain ⟨hr₀, hr⟩ := hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : IsDomain R
inst_13 : IsCancelAdd A
inst_14 : Module.IsTorsionFree R A
r : R
hr : r ≠ 0 ∧ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r
a_1 a : A
ha₀ : a ≠ 0
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
hr₀ : r ≠ 0
⊢ ∃ (p : A),
    p ≠ 0 ∧
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧
        r • (a_1 + a) = r • a_1 + p
have hr₁ : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r
Tactic: obtain ⟨hr₀, hr⟩ := hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : IsDomain R
inst_13 : IsCancelAdd A
inst_14 : Module.IsTorsionFree R A
inst_15 : IsCancelAdd R
a : A
ha : 0 < a
r s : R
hrs : r < s
⊢ r • a < s • a
have rw : ∀ (ha : a ≠ 0 ∧ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a)
  (r s : R) (hrs : r < s), r • a < s • a
Tactic: rw [StarOrderedRing.pos_iff] at ha
Cleared hypotheses: ha, r, s, hrs
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : IsDomain R
inst_13 : IsCancelAdd A
inst_14 : Module.IsTorsionFree R A
inst_15 : IsCancelAdd R
a : A
ha : a ≠ 0 ∧ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
r s : R
hrs : r < s
⊢ r • a < s • a
have rw : ∀
  (hrs :
    ∃ (p : R),
      p ≠ 0 ∧
        Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ s = r + p),
  ∃ (p : A),
    p ≠ 0 ∧
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ s • a = r • a + p
Tactic: rw [StarOrderedRing.lt_iff] at hrs ⊢
Cleared hypotheses: hrs
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : IsDomain R
inst_13 : IsCancelAdd A
inst_14 : Module.IsTorsionFree R A
inst_15 : IsCancelAdd R
a : A
ha : a ≠ 0 ∧ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
r s : R
hrs :
  ∃ (p : R),
    p ≠ 0 ∧ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ s = r + p
⊢ ∃ (p : A),
    p ≠ 0 ∧
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ s • a = r • a + p
have obtain : ∀ (r_1 : R) (hr₀ : r_1 ≠ 0)
  (hr : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r_1),
  ∃ (p : A),
    p ≠ 0 ∧
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧
        (r + r_1) • a = r • a + p
Tactic: obtain ⟨r, hr₀, hr, rfl⟩ := hrs
Cleared hypotheses: s, hrs
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : IsDomain R
inst_13 : IsCancelAdd A
inst_14 : Module.IsTorsionFree R A
inst_15 : IsCancelAdd R
a : A
ha : a ≠ 0 ∧ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
r_1 r : R
hr₀ : r ≠ 0
hr : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r
⊢ ∃ (p : A),
    p ≠ 0 ∧
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧
        (r_1 + r) • a = r_1 • a + p
have ha₀ : a ≠ 0
Tactic: obtain ⟨ha₀, ha⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring A
inst_5 : StarRing A
inst_6 : PartialOrder A
inst_7 : StarOrderedRing A
inst_8 : Module R A
inst_9 : StarModule R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : IsDomain R
inst_13 : IsCancelAdd A
inst_14 : Module.IsTorsionFree R A
inst_15 : IsCancelAdd R
a : A
ha : a ≠ 0 ∧ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
r_1 r : R
hr₀ : r ≠ 0
hr : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r
ha₀ : a ≠ 0
⊢ ∃ (p : A),
    p ≠ 0 ∧
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧
        (r_1 + r) • a = r_1 • a + p
have ha₁ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
Tactic: obtain ⟨ha₀, ha⟩ := ha
Cleared hypotheses: ha