awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
linarith : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
linarith₁ : x - 1 / 2 < x + 1 / 2 - 1 → HMul.hMul (α := α) 1 2 = 2
linarith₂ : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
linarith₃ : x - 1 / 2 < x + 1 / 2 - 1 → HMul.hMul (α := α) 1 2 = 2
linarith₄ : x - 1 / 2 < x + 1 / 2 - 1 → GT.gt.{u_2} (α := α) 2 0
linarith₅ :
  x - 1 / 2 < x + 1 / 2 - 1 →
    2 * x - HMul.hMul (α := α) 1 1 - (2 * x + HMul.hMul (α := α) 1 1 - HMul.hMul (α := α) 2 1) = 0
linarith₆ : x + 1 / 2 - 1 < x - 1 / 2 → 2 / 2 = 1
⊢ x - 1 / 2 = x + 1 / 2 - 1
have linarith₇ : x + 1 / 2 - 1 < x - 1 / 2 → HMul.hMul (α := α) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
linarith : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
linarith₁ : x - 1 / 2 < x + 1 / 2 - 1 → HMul.hMul (α := α) 1 2 = 2
linarith₂ : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
linarith₃ : x - 1 / 2 < x + 1 / 2 - 1 → HMul.hMul (α := α) 1 2 = 2
linarith₄ : x - 1 / 2 < x + 1 / 2 - 1 → GT.gt.{u_2} (α := α) 2 0
linarith₅ :
  x - 1 / 2 < x + 1 / 2 - 1 →
    2 * x - HMul.hMul (α := α) 1 1 - (2 * x + HMul.hMul (α := α) 1 1 - HMul.hMul (α := α) 2 1) = 0
linarith₆ : x + 1 / 2 - 1 < x - 1 / 2 → 2 / 2 = 1
linarith₇ : x + 1 / 2 - 1 < x - 1 / 2 → HMul.hMul (α := α) 1 2 = 2
linarith₈ : x + 1 / 2 - 1 < x - 1 / 2 → 2 / 2 = 1
linarith₉ : x + 1 / 2 - 1 < x - 1 / 2 → HMul.hMul (α := α) 1 2 = 2
⊢ x - 1 / 2 = x + 1 / 2 - 1
have linarith₁₀ : x + 1 / 2 - 1 < x - 1 / 2 → GT.gt.{u_2} (α := α) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
linarith : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
linarith₁ : x - 1 / 2 < x + 1 / 2 - 1 → HMul.hMul (α := α) 1 2 = 2
linarith₂ : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
linarith₃ : x - 1 / 2 < x + 1 / 2 - 1 → HMul.hMul (α := α) 1 2 = 2
linarith₄ : x - 1 / 2 < x + 1 / 2 - 1 → GT.gt.{u_2} (α := α) 2 0
linarith₅ :
  x - 1 / 2 < x + 1 / 2 - 1 →
    2 * x - HMul.hMul (α := α) 1 1 - (2 * x + HMul.hMul (α := α) 1 1 - HMul.hMul (α := α) 2 1) = 0
linarith₆ : x + 1 / 2 - 1 < x - 1 / 2 → 2 / 2 = 1
linarith₇ : x + 1 / 2 - 1 < x - 1 / 2 → HMul.hMul (α := α) 1 2 = 2
linarith₈ : x + 1 / 2 - 1 < x - 1 / 2 → 2 / 2 = 1
linarith₉ : x + 1 / 2 - 1 < x - 1 / 2 → HMul.hMul (α := α) 1 2 = 2
linarith₁₀ : x + 1 / 2 - 1 < x - 1 / 2 → GT.gt.{u_2} (α := α) 2 0
⊢ x - 1 / 2 = x + 1 / 2 - 1
have linarith₁₁ : x + 1 / 2 - 1 < x - 1 / 2 →
  2 * x + HMul.hMul (α := α) 1 1 - HMul.hMul (α := α) 2 1 - (2 * x - HMul.hMul (α := α) 1 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
⊢ x - 1 / 2 < (↑(round x) : α)
have rw : x + 1 / 2 - 1 < (↑⌊x + 1 / 2⌋ : α)
Tactic: rw [round_eq x, show x - 1 / 2 = x + 1 / 2 - 1 by linarith]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
⊢ (↑(round x) : α) ≤ x + 1 / 2
have rw : (↑⌊x + 1 / 2⌋ : α) ≤ x + 1 / 2
Tactic: rw [round_eq x]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : FloorRing α
inst_7 : FloorRing β
inst_8 : FunLike F α β
inst_9 : RingHomClass F α β
f : F
hf : StrictMono.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)
a : α
⊢ round.{u_3} (α := β) ((f : (a : α) → β) a : β) = round a
have simp_rw : ⌊HAdd.hAdd (α := β) ((f : (a : α) → β) a : β) (1 / 2)⌋ = ⌊a + 1 / 2⌋
Tactic: simp_rw [round_eq, ← map_floor _ hf, map_add, one_div, map_inv₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : FloorRing α
inst_7 : FloorRing β
inst_8 : FunLike F α β
inst_9 : RingHomClass F α β
f : F
hf : StrictMono.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)
a : α
simp_rw : ⌊HAdd.hAdd (α := β) ((f : (a : α) → β) a : β) (1 / 2)⌋ = ⌊a + 1 / 2⌋
⊢ round.{u_3} (α := β) ((f : (a : α) → β) a : β) = round a
have simp_rw₁ : ⌊HAdd.hAdd (α := β) ((f : (a : α) → β) a : β) (1 / 2)⌋ = floor.{u_3} (α := β) ((f : (a : α) → β) (a + 1 / 2) : β)
Tactic: simp_rw [round_eq, ← map_floor _ hf, map_add, one_div, map_inv₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : FloorRing α
inst_7 : FloorRing β
inst_8 : FunLike F α β
inst_9 : RingHomClass F α β
f : F
hf : StrictMono.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)
a : α
simp_rw : ⌊HAdd.hAdd (α := β) ((f : (a : α) → β) a : β) (1 / 2)⌋ = ⌊a + 1 / 2⌋
simp_rw₁ :
  ⌊HAdd.hAdd (α := β) ((f : (a : α) → β) a : β) (1 / 2)⌋ = floor.{u_3} (α := β) ((f : (a : α) → β) (a + 1 / 2) : β)
⊢ round.{u_3} (α := β) ((f : (a : α) → β) a : β) = round a
have simp_rw₂ : ⌊HAdd.hAdd (α := β) ((f : (a : α) → β) a : β) (1 / 2)⌋ =
  ⌊HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) (1 / 2) : β)⌋
Tactic: simp_rw [round_eq, ← map_floor _ hf, map_add, one_div, map_inv₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : FloorRing α
inst_7 : FloorRing β
inst_8 : FunLike F α β
inst_9 : RingHomClass F α β
f : F
hf : StrictMono.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)
a : α
simp_rw : ⌊HAdd.hAdd (α := β) ((f : (a : α) → β) a : β) (1 / 2)⌋ = ⌊a + 1 / 2⌋
simp_rw₁ :
  ⌊HAdd.hAdd (α := β) ((f : (a : α) → β) a : β) (1 / 2)⌋ = floor.{u_3} (α := β) ((f : (a : α) → β) (a + 1 / 2) : β)
simp_rw₂ :
  ⌊HAdd.hAdd (α := β) ((f : (a : α) → β) a : β) (1 / 2)⌋ =
    ⌊HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) (1 / 2) : β)⌋
⊢ round.{u_3} (α := β) ((f : (a : α) → β) a : β) = round a
have simp_rw₃ : ⌊HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) (2⁻¹ : β)⌋ =
  ⌊HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) 2⁻¹ : β)⌋
Tactic: simp_rw [round_eq, ← map_floor _ hf, map_add, one_div, map_inv₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : FloorRing α
inst_7 : FloorRing β
inst_8 : FunLike F α β
inst_9 : RingHomClass F α β
f : F
hf : StrictMono.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)
a : α
simp_rw : ⌊HAdd.hAdd (α := β) ((f : (a : α) → β) a : β) (1 / 2)⌋ = ⌊a + 1 / 2⌋
simp_rw₁ :
  ⌊HAdd.hAdd (α := β) ((f : (a : α) → β) a : β) (1 / 2)⌋ = floor.{u_3} (α := β) ((f : (a : α) → β) (a + 1 / 2) : β)
simp_rw₂ :
  ⌊HAdd.hAdd (α := β) ((f : (a : α) → β) a : β) (1 / 2)⌋ =
    ⌊HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) (1 / 2) : β)⌋
simp_rw₃ :
  ⌊HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) (2⁻¹ : β)⌋ =
    ⌊HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) 2⁻¹ : β)⌋
⊢ round.{u_3} (α := β) ((f : (a : α) → β) a : β) = round a
have simp_rw₄ : ⌊HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) (2⁻¹ : β)⌋ =
  ⌊HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) (((f : (a : α) → β) 2)⁻¹ : β)⌋
Tactic: simp_rw [round_eq, ← map_floor _ hf, map_add, one_div, map_inv₀, map_ofNat]
-- 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 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r_1 : R
a_1 : A
r : R
hr : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) r
a : A
ha : Membership.mem (γ := Set A) (range fun (s : A) ↦ star s * s) a
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a)
have mem : ∀ (r : R),
  Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (s : R) ↦ star s * s) r) a)
Tactic: obtain ⟨r, rfl⟩ := hr
Cleared hypotheses: r, 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 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r_1 : R
a_1 a : A
ha : Membership.mem (γ := Set A) (range fun (s : A) ↦ star s * s) a
r : R
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (s : R) ↦ star s * s) r) a)
have mem : ∀ (a : A),
  Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) ((fun (s : R) ↦ star s * s) r) ((fun (s : A) ↦ star s * s) a))
Tactic: obtain ⟨a, rfl⟩ := ha
Cleared hypotheses: a, ha
-- 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 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r_1 : R
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
r : R
hr : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) r
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a)
have mem : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (HSMul.hSMul (β := A) r 0)
Tactic: induction ha using AddSubmonoid.closure_induction with
  | zero => simp
  | add a₁ a₂ _ _ ha₁ ha₂ => simpa [smul_add] using add_mem ha₁ ha₂
  | mem a ha =>
  obtain ⟨r, rfl⟩ := hr
  obtain ⟨a, rfl⟩ := ha
  exact AddSubmonoid.subset_closure ⟨r • a, by simp [star_smul, smul_mul_smul_comm]⟩
Cleared hypotheses: ha
-- 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 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r_1 : R
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
r : R
hr : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) r
mem :
  Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
    (HSMul.hSMul (β := A) r 0)
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a)
have mem₁ : ∀ (a₁ a₂ : A),
  Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a₁ →
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a₂ →
      ∀ (ha₁ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a₁))
        (ha₂ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a₂)),
        Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • (a₁ + a₂))
Tactic: induction ha using AddSubmonoid.closure_induction with
  | zero => simp
  | add a₁ a₂ _ _ ha₁ ha₂ => simpa [smul_add] using add_mem ha₁ ha₂
  | mem a ha =>
  obtain ⟨r, rfl⟩ := hr
  obtain ⟨a, rfl⟩ := ha
  exact AddSubmonoid.subset_closure ⟨r • a, by simp [star_smul, smul_mul_smul_comm]⟩
Cleared hypotheses: ha
-- 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 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r_1 : R
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
r : R
hr : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) r
mem :
  Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
    (HSMul.hSMul (β := A) r 0)
mem₁ :
  ∀ (a₁ a₂ : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a₁ →
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a₂ →
        ∀ (ha₁ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a₁))
          (ha₂ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a₂)),
          Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • (a₁ + a₂))
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a)
have mem₂ : ∀ (a : A) (ha : Membership.mem (γ := Set A) (range fun (s : A) ↦ star s * s) a),
  Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a)
Tactic: induction ha using AddSubmonoid.closure_induction with
  | zero => simp
  | add a₁ a₂ _ _ ha₁ ha₂ => simpa [smul_add] using add_mem ha₁ ha₂
  | mem a ha =>
  obtain ⟨r, rfl⟩ := hr
  obtain ⟨a, rfl⟩ := ha
  exact AddSubmonoid.subset_closure ⟨r • a, by simp [star_smul, smul_mul_smul_comm]⟩
Cleared hypotheses: ha
-- 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 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r : R
hr : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a)
have zero : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 a)
Tactic: induction hr using AddSubmonoid.closure_induction with
  | zero => simp
  | add r₁ r₂ _ _ hr₁ hr₂ => simpa [add_smul] using add_mem hr₁ hr₂
  | mem r hr =>
  induction ha using AddSubmonoid.closure_induction with
  | zero => simp
  | add a₁ a₂ _ _ ha₁ ha₂ => simpa [smul_add] using add_mem ha₁ ha₂
  | mem a ha =>
  obtain ⟨r, rfl⟩ := hr
  obtain ⟨a, rfl⟩ := ha
  exact AddSubmonoid.subset_closure ⟨r • a, by simp [star_smul, smul_mul_smul_comm]⟩
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 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r : R
hr : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
zero :
  Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 a)
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a)
have add : ∀ (r₁ r₂ : R),
  Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r₁ →
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r₂ →
      ∀ (hr₁ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r₁ • a))
        (hr₂ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r₂ • a)),
        Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) ((r₁ + r₂) • a)
Tactic: induction hr using AddSubmonoid.closure_induction with
  | zero => simp
  | add r₁ r₂ _ _ hr₁ hr₂ => simpa [add_smul] using add_mem hr₁ hr₂
  | mem r hr =>
  induction ha using AddSubmonoid.closure_induction with
  | zero => simp
  | add a₁ a₂ _ _ ha₁ ha₂ => simpa [smul_add] using add_mem ha₁ ha₂
  | mem a ha =>
  obtain ⟨r, rfl⟩ := hr
  obtain ⟨a, rfl⟩ := ha
  exact AddSubmonoid.subset_closure ⟨r • a, by simp [star_smul, smul_mul_smul_comm]⟩
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 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r : R
hr : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
zero :
  Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 a)
add :
  ∀ (r₁ r₂ : R),
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r₁ →
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r₂ →
        ∀ (hr₁ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r₁ • a))
          (hr₂ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r₂ • a)),
          Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) ((r₁ + r₂) • a)
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a)
have mem : ∀ (r : R) (hr : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) r),
  Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a)
Tactic: induction hr using AddSubmonoid.closure_induction with
  | zero => simp
  | add r₁ r₂ _ _ hr₁ hr₂ => simpa [add_smul] using add_mem hr₁ hr₂
  | mem r hr =>
  induction ha using AddSubmonoid.closure_induction with
  | zero => simp
  | add a₁ a₂ _ _ ha₁ ha₂ => simpa [smul_add] using add_mem ha₁ ha₂
  | mem a ha =>
  obtain ⟨r, rfl⟩ := hr
  obtain ⟨a, rfl⟩ := ha
  exact AddSubmonoid.subset_closure ⟨r • a, by simp [star_smul, smul_mul_smul_comm]⟩
Cleared hypotheses: hr
-- 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
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
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 refine_1 : ∀ (h : x ≤ y),
  ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
Tactic: refine ⟨fun h => ?_, ?_⟩
-- 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
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
x y : R
refine_1 :
  ∀ (h : x ≤ y),
    ∃ (p : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
⊢ x ≤ y ↔
    ∃ (p : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
have refine_2 : (∃ (p : R),
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p) →
  x ≤ y
Tactic: refine ⟨fun h => ?_, ?_⟩
-- 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
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
x y : R
h : x ≤ y
⊢ ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
have refine_1 : ∀ (p : R) (hp : y = x + star p * p),
  ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
Tactic: obtain ⟨p, hp⟩ := (h_le_iff x y).mp h
-- 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
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
x y p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
hpxy : y = x + p
⊢ x ≤ y
have refine_2 : ∀ (x y : R) (hpxy : y = x + p), x ≤ y
Tactic: revert x y hpxy
Cleared hypotheses: x, y, hpxy
-- 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
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
⊢ ∀ (x y : R) (hpxy : y = x + p), x ≤ y
have refine_2 : ∀ (x : R) (h : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) x) (x_1 y : R) (hpxy : y = x_1 + x), x_1 ≤ y
Tactic: refine AddSubmonoid.closure_induction ?_ (fun x y h => add_zero x ▸ h.ge) ?_ hp
-- 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
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
refine_2 :
  ∀ (x : R) (h : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) x) (x_1 y : R) (hpxy : y = x_1 + x),
    x_1 ≤ y
⊢ ∀ (x y : R) (hpxy : y = x + p), x ≤ y
have refine_2₁ : ∀ (x y : R) (hx : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x)
  (hy : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) y),
  (∀ (x_1 y : R) (hpxy : y = x_1 + x), x_1 ≤ y) →
    (∀ (x y_1 : R) (hpxy : y_1 = x + y), x ≤ y_1) → ∀ (x_1 y_1 : R) (hpxy : y_1 = x_1 + (x + y)), x_1 ≤ y_1
Tactic: refine AddSubmonoid.closure_induction ?_ (fun x y h => add_zero x ▸ h.ge) ?_ hp
-- 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
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
x_1 y : R
hx : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x_1
hy : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) y
ha : ∀ (x y : R) (hpxy : y = x + x_1), x ≤ y
hb : ∀ (x y_1 : R) (hpxy : y_1 = x + y), x ≤ y_1
x : R
⊢ x ≤ x + (x_1 + y)
have refine_2 : x ≤ x + x_1 + y
Tactic: rw [← add_assoc]