awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Star.Basic
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)
a₁ : ∀ (p : R), unop y = unop x + p ↔ y = x + 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

Tactic:
congr! with p
-- Module: Mathlib.Algebra.Order.Star.Basic
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 ↔
    Membership.mem (γ := AddSubmonoid Rᵐᵒᵖ) (AddSubmonoid.closure (range fun (s : Rᵐᵒᵖ) ↦ star s * s)) (op p)

Tactic:
simp [AddMonoidHom.map_mclosure, ← range_comp', Function.comp_def,
        ← (star_involutive.surjective.comp op_surjective).range_comp]

Premises used: InvolutiveStar.star_involutive, AddMonoidHom.map_mclosure, Function.Involutive.surjective, Function.Surjective.range_comp, Function.comp_def, Function.Surjective.comp, MulOpposite.op_surjective, Set.range_comp'
-- Module: Mathlib.Algebra.Order.Star.Basic
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
⊢ unop y = unop x + p ↔ y = x + op p

Tactic:
simp [← op_inj (α := R)]

Premises used: MulOpposite.op_inj
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
⊢ r • a ≤ r • b

Tactic:
rw [StarOrderedRing.nonneg_iff] at hr

Premises used: StarOrderedRing.nonneg_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
⊢ r • a ≤ r • b

Tactic:
rw [StarOrderedRing.le_iff] at hab ⊢

Premises used: StarOrderedRing.le_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
⊢ ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ r • b = r • a + p

Tactic:
obtain ⟨a, ha, rfl⟩ := hab

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Star.Basic
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_1 a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
⊢ ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧
      r • (a_1 + a) = r • a_1 + p

Tactic:
⟨r • a, smul_mem_closure_star_mul hr ha, smul_add ..⟩

Premises used: smul_mem_closure_star_mul, And.intro, Exists.intro, HSMul.hSMul, smul_add
-- Module: Mathlib.Algebra.Order.Star.Basic
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_1 a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
⊢ ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧
      r • (a_1 + a) = r • a_1 + p

Tactic:
exact ⟨r • a, smul_mem_closure_star_mul hr ha, smul_add ..⟩
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
⊢ r • a ≤ s • a

Tactic:
rw [StarOrderedRing.nonneg_iff] at ha

Premises used: StarOrderedRing.nonneg_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
⊢ r • a ≤ s • a

Tactic:
rw [StarOrderedRing.le_iff] at hrs ⊢

Premises used: StarOrderedRing.le_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
⊢ ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ s • a = r • a + p

Tactic:
obtain ⟨r, hr, rfl⟩ := hrs

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Star.Basic
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_1 r : R
hr : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r
⊢ ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧
      (r_1 + r) • a = r_1 • a + p

Tactic:
⟨r • a, smul_mem_closure_star_mul hr ha, add_smul ..⟩

Premises used: smul_mem_closure_star_mul, add_smul, And.intro, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Algebra.Order.Star.Basic
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_1 r : R
hr : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r
⊢ ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧
      (r_1 + r) • a = r_1 • a + p

Tactic:
exact ⟨r • a, smul_mem_closure_star_mul hr ha, add_smul ..⟩
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
⊢ r • a < r • b

Tactic:
rw [StarOrderedRing.pos_iff] at hr

Premises used: StarOrderedRing.pos_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
⊢ r • a < r • b

Tactic:
rw [StarOrderedRing.lt_iff] at hab ⊢

Premises used: StarOrderedRing.lt_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
⊢ ∃ (p : A),
    p ≠ 0 ∧
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ r • b = r • a + p

Tactic:
obtain ⟨a, ha₀, ha, rfl⟩ := hab

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Star.Basic
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
⊢ r ≠ 0

Tactic:
obtain ⟨hr₀, hr⟩ := hr
-- Module: Mathlib.Algebra.Order.Star.Basic
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
⊢ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r

Tactic:
obtain ⟨hr₀, hr⟩ := hr
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
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 • (a_1 + a) = r • a_1 + p

Tactic:
⟨r • a, smul_ne_zero hr₀ ha₀, smul_mem_closure_star_mul hr ha, smul_add ..⟩

Premises used: smul_mem_closure_star_mul, smul_ne_zero, And.intro, Exists.intro, HSMul.hSMul, smul_add
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
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 • (a_1 + a) = r • a_1 + p

Tactic:
exact ⟨r • a, smul_ne_zero hr₀ ha₀, smul_mem_closure_star_mul hr ha, smul_add ..⟩
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
⊢ r • a < s • a

Tactic:
rw [StarOrderedRing.pos_iff] at ha

Premises used: StarOrderedRing.pos_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
⊢ r • a < s • a

Tactic:
rw [StarOrderedRing.lt_iff] at hrs ⊢

Premises used: StarOrderedRing.lt_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
⊢ ∃ (p : A),
    p ≠ 0 ∧
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) p ∧ s • a = r • a + p

Tactic:
obtain ⟨r, hr₀, hr, rfl⟩ := hrs

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Star.Basic
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
⊢ a ≠ 0

Tactic:
obtain ⟨ha₀, ha⟩ := ha
-- Module: Mathlib.Algebra.Order.Star.Basic
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
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a

Tactic:
obtain ⟨ha₀, ha⟩ := ha
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
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_1 + r) • a = r_1 • a + p

Tactic:
⟨r • a, smul_ne_zero hr₀ ha₀, smul_mem_closure_star_mul hr ha, add_smul ..⟩

Premises used: smul_mem_closure_star_mul, smul_ne_zero, add_smul, And.intro, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
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_1 + r) • a = r_1 • a + p

Tactic:
exact ⟨r • a, smul_ne_zero hr₀ ha₀, smul_mem_closure_star_mul hr ha, add_smul ..⟩