awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring S
inst_5 : PartialOrder S
inst_6 : StarRing S
inst_7 : StarOrderedRing S
f : R →⋆ₙ+* S
x y : R
hxy : x ≤ y
⊢ LE.le.{u_5} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
have rw : ∀
  (hxy :
    ∃ (p : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p),
  ∃ (p : S),
    Membership.mem (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s)) p ∧
      (f : (a : R) → S) y = HAdd.hAdd (α := S) ((f : (a : R) → S) x : S) p
Tactic: rw [StarOrderedRing.le_iff] at hxy ⊢
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring S
inst_5 : PartialOrder S
inst_6 : StarRing S
inst_7 : StarOrderedRing S
f : R →⋆ₙ+* S
x y : R
hxy :
  ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
⊢ ∃ (p : S),
    Membership.mem (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s)) p ∧
      (f : (a : R) → S) y = HAdd.hAdd (α := S) ((f : (a : R) → S) x : S) p
have obtain : ∀ (p : R) (hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p),
  ∃ (p_1 : S),
    Membership.mem (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s)) p_1 ∧
      (f : (a : R) → S) (x + p) = HAdd.hAdd (α := S) ((f : (a : R) → S) x : S) p_1
Tactic: obtain ⟨p, hp, rfl⟩ := hxy
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring S
inst_5 : PartialOrder S
inst_6 : StarRing S
inst_7 : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
⊢ ∃ (p_1 : S),
    Membership.mem (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s)) p_1 ∧
      (f : (a : R) → S) (x + p) = HAdd.hAdd (α := S) ((f : (a : R) → S) x : S) p_1
have refine : Membership.mem.{u_5, u_5} (α := S) (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s))
  ((f : (a : R) → S) p : S)
Tactic: refine ⟨f p, ?_, map_add f _ _⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (hypothesis)
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring S
inst_5 : PartialOrder S
inst_6 : StarRing S
inst_7 : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
⊢ Membership.mem.{u_5, u_5} (α := S) (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s))
    ((f : (a : R) → S) p : S)
have hf : ∀ (r : R), Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) (star r) : S) (star ((f : (a : R) → S) r) : S)
Tactic: have hf : ∀ r, f (star r) = star (f r) := map_star _
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring S
inst_5 : PartialOrder S
inst_6 : StarRing S
inst_7 : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
hf : ∀ (r : R), Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) (star r) : S) (star ((f : (a : R) → S) r) : S)
⊢ Membership.mem.{u_5, u_5} (α := S) (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s))
    ((f : (a : R) → S) p : S)
have mem : ∀ (x : R),
  Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) x →
    Membership.mem.{u_5, u_5} (α := S) (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s))
      ((f : (a : R) → S) x : S)
Tactic: induction hp using AddSubmonoid.closure_induction
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring S
inst_5 : PartialOrder S
inst_6 : StarRing S
inst_7 : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
hf : ∀ (r : R), Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) (star r) : S) (star ((f : (a : R) → S) r) : S)
mem :
  ∀ (x : R),
    Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) x →
      Membership.mem.{u_5, u_5} (α := S) (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s))
        ((f : (a : R) → S) x : S)
⊢ Membership.mem.{u_5, u_5} (α := S) (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s))
    ((f : (a : R) → S) p : S)
have zero : Membership.mem.{u_5, u_5} (α := S) (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s))
  ((f : (a : R) → S) 0 : S)
Tactic: induction hp using AddSubmonoid.closure_induction
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring S
inst_5 : PartialOrder S
inst_6 : StarRing S
inst_7 : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
hf : ∀ (r : R), Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) (star r) : S) (star ((f : (a : R) → S) r) : S)
mem :
  ∀ (x : R),
    Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) x →
      Membership.mem.{u_5, u_5} (α := S) (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s))
        ((f : (a : R) → S) x : S)
zero :
  Membership.mem.{u_5, u_5} (α := S) (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s))
    ((f : (a : R) → S) 0 : S)
⊢ Membership.mem.{u_5, u_5} (α := S) (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s))
    ((f : (a : R) → S) p : S)
have add : ∀ (x y : R),
  Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x →
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) y →
      Membership.mem.{u_5, u_5} (α := S) (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s))
          ((f : (a : R) → S) x : S) →
        Membership.mem.{u_5, u_5} (α := S) (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s))
            ((f : (a : R) → S) y : S) →
          Membership.mem.{u_5, u_5} (α := S) (γ := AddSubmonoid S)
            (AddSubmonoid.closure (range fun (s : S) ↦ star s * s)) ((f : (a : R) → S) (x + y) : S)
Tactic: induction hp using AddSubmonoid.closure_induction
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R_1 : Type u_1
A : Type u_2
F : Type u_3
R : Type u_4
S : Type u_5
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring S
inst_5 : PartialOrder S
inst_6 : StarRing S
inst_7 : StarOrderedRing S
inst_8 : EquivLike F R S
inst_9 : StarRingEquivClass F R S
f : F
x y : R
⊢ LE.le.{u_5} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) ↔ x ≤ y
have refine : ∀ (h : LE.le.{u_5} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)), x ≤ y
Tactic: refine ⟨fun h ↦ ?_, map_rel f⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (hypothesis)
Goal:
R_1 : Type u_1
A : Type u_2
F : Type u_3
R : Type u_4
S : Type u_5
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring S
inst_5 : PartialOrder S
inst_6 : StarRing S
inst_7 : StarOrderedRing S
inst_8 : EquivLike F R S
inst_9 : StarRingEquivClass F R S
f : F
x y : R
h : LE.le.{u_5} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
f_inv : S →⋆ₙ+* R := (↑(StarRingEquiv.symm (↑f : R ≃⋆+* S)) : S →⋆ₙ+* R)
⊢ x ≤ y
have f_inv_f : ∀ (r : R), (f_inv : (a : S) → R) ((f : (a : R) → S) r : S) = r
Tactic: have f_inv_f (r : R) : f_inv (f r) = r := EquivLike.inv_apply_apply f r
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (goal)
Goal:
R_1 : Type u_1
A : Type u_2
F : Type u_3
R : Type u_4
S : Type u_5
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : NonUnitalSemiring S
inst_5 : PartialOrder S
inst_6 : StarRing S
inst_7 : StarOrderedRing S
inst_8 : EquivLike F R S
inst_9 : StarRingEquivClass F R S
f : F
x y : R
h : LE.le.{u_5} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
f_inv : S →⋆ₙ+* R := (↑(StarRingEquiv.symm (↑f : R ≃⋆+* S)) : S →⋆ₙ+* R)
f_inv_f : ∀ (r : R), (f_inv : (a : S) → R) ((f : (a : R) → S) r : S) = r
⊢ x ≤ y
have rw : LE.le.{u_4} (α := R) ((f_inv : (a : S) → R) ((f : (a : R) → S) x : S) : R)
  ((f_inv : (a : S) → R) ((f : (a : R) → S) y : S) : R)
Tactic: rw [← f_inv_f x, ← f_inv_f y]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Basic (hypothesis)
Goal:
R : Type u_1
A : Type u_2
a b : ℕ
⊢ a ≤ b ↔
    ∃ (p : ℕ),
      Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure (range fun (s : ℕ) ↦ star s * s)) p ∧ b = a + p
have this : Eq (α := AddSubmonoid ℕ) (AddSubmonoid.closure (range fun (x : ℕ) ↦ x * x)) ⊤
Tactic: have : AddSubmonoid.closure (range fun x : ℕ ↦ x * x) = ⊤ :=
      eq_top_mono
        (AddSubmonoid.closure_mono <| singleton_subset_iff.2 <| mem_range.2 ⟨1, one_mul _⟩)
        Nat.addSubmonoidClosure_one
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Conjneg (goal)
Goal:
G : Type u_1
R : Type u_2
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : PartialOrder R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
f : G → R
⊢ 0 < conjneg f ↔ 0 < f
have simp_rw : 0 ≤ conjneg f ∧ 0 ≠ conjneg f ↔ 0 ≤ f ∧ 0 ≠ f
Tactic: simp_rw [lt_iff_le_and_ne, ne_comm, conjneg_nonneg, conjneg_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Conjneg (goal)
Goal:
G : Type u_1
R : Type u_2
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : PartialOrder R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
f : G → R
simp_rw : 0 ≤ conjneg f ∧ 0 ≠ conjneg f ↔ 0 ≤ f ∧ 0 ≠ f
⊢ 0 < conjneg f ↔ 0 < f
have simp_rw₁ : 0 ≤ conjneg f ∧ conjneg f ≠ 0 ↔ 0 ≤ f ∧ f ≠ 0
Tactic: simp_rw [lt_iff_le_and_ne, ne_comm, conjneg_nonneg, conjneg_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Conjneg (goal)
Goal:
G : Type u_1
R : Type u_2
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : PartialOrder R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
f : G → R
simp_rw : 0 ≤ conjneg f ∧ 0 ≠ conjneg f ↔ 0 ≤ f ∧ 0 ≠ f
simp_rw₁ : 0 ≤ conjneg f ∧ conjneg f ≠ 0 ↔ 0 ≤ f ∧ f ≠ 0
⊢ 0 < conjneg f ↔ 0 < f
have simp_rw₂ : 0 ≤ f ∧ conjneg f ≠ 0 ↔ 0 ≤ f ∧ f ≠ 0
Tactic: simp_rw [lt_iff_le_and_ne, ne_comm, conjneg_nonneg, conjneg_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Conjneg (goal)
Goal:
G : Type u_1
R : Type u_2
inst : AddGroup G
inst_1 : CommRing R
inst_2 : PartialOrder R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
f : G → R
⊢ conjneg f ≤ 0 ↔ f ≤ 0
have simp_rw : 0 ≤ -conjneg f ↔ 0 ≤ -f
Tactic: simp_rw [← neg_nonneg, ← conjneg_neg, conjneg_nonneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Conjneg (goal)
Goal:
G : Type u_1
R : Type u_2
inst : AddGroup G
inst_1 : CommRing R
inst_2 : PartialOrder R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
f : G → R
simp_rw : 0 ≤ -conjneg f ↔ 0 ≤ -f
⊢ conjneg f ≤ 0 ↔ f ≤ 0
have simp_rw₁ : 0 ≤ conjneg (-f) ↔ 0 ≤ -f
Tactic: simp_rw [← neg_nonneg, ← conjneg_neg, conjneg_nonneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Conjneg (goal)
Goal:
G : Type u_1
R : Type u_2
inst : AddGroup G
inst_1 : CommRing R
inst_2 : PartialOrder R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
f : G → R
⊢ conjneg f < 0 ↔ f < 0
have simp_rw : 0 < -conjneg f ↔ 0 < -f
Tactic: simp_rw [← neg_pos, ← conjneg_neg, conjneg_pos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Conjneg (goal)
Goal:
G : Type u_1
R : Type u_2
inst : AddGroup G
inst_1 : CommRing R
inst_2 : PartialOrder R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
f : G → R
simp_rw : 0 < -conjneg f ↔ 0 < -f
⊢ conjneg f < 0 ↔ f < 0
have simp_rw₁ : 0 < conjneg (-f) ↔ 0 < -f
Tactic: simp_rw [← neg_pos, ← conjneg_neg, conjneg_pos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Pi (goal)
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa xy : (i : ι) → A i
⊢ Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
    (pi (M := A) Set.univ fun (i : ι) ↦ closure (Set.range fun (s : A i) ↦ star s * s))
have rw : Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
  (closure (Set.pi (α := A) Set.univ fun (i : ι) ↦ Set.range fun (s : A i) ↦ star s * s))
Tactic: rw [← closure_pi fun _ => Set.mem_range.mpr ⟨0, by simp⟩]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Pi (goal)
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa xy : (i : ι) → A i
⊢ Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
    (closure (Set.pi (α := A) Set.univ fun (i : ι) ↦ Set.range fun (s : A i) ↦ star s * s))
have e_s : Eq (α := Set ((i : ι) → A i)) (Set.range fun (s : (i : ι) → A i) ↦ star s * s)
  (Set.pi (α := A) Set.univ fun (i : ι) ↦ Set.range fun (s : A i) ↦ star s * s)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Pi (goal)
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa xy : (i : ι) → A i
⊢ Eq (α := Set ((i : ι) → A i)) (Set.range fun (s : (i : ι) → A i) ↦ star s * s)
    (Set.pi (α := A) Set.univ fun (i : ι) ↦ Set.range fun (s : A i) ↦ star s * s)
have e_s : ∀ (x : (i : ι) → A i),
  Membership.mem (γ := Set ((i : ι) → A i)) (Set.range fun (s : (i : ι) → A i) ↦ star s * s) x ↔
    Membership.mem (γ := Set ((i : ι) → A i))
      (Set.pi (α := A) Set.univ fun (i : ι) ↦ Set.range fun (s : A i) ↦ star s * s) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Pi (goal)
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa xy x : (i : ι) → A i
⊢ Membership.mem (γ := Set ((i : ι) → A i)) (Set.range fun (s : (i : ι) → A i) ↦ star s * s) x ↔
    Membership.mem (γ := Set ((i : ι) → A i))
      (Set.pi (α := A) Set.univ fun (i : ι) ↦ Set.range fun (s : A i) ↦ star s * s) x
have e_s : (∃ (y : (i : ι) → A i), ∀ (x_1 : ι), star (y x_1) * y x_1 = x x_1) ↔ ∀ (i : ι), ∃ (y : A i), star y * y = x i
Tactic: simp only [Set.mem_range, funext_iff, mul_apply, star_apply, Set.mem_pi,
        Set.mem_univ, forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Pi (hypothesis)
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa xy : (i : ι) → A i
⊢ xa ≤ xy ↔
    ∃ (p : (i : ι) → A i),
      Membership.mem (γ := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s)) p ∧
        xy = xa + p
have this : Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
  (pi (M := A) Set.univ fun (i : ι) ↦ closure (Set.range fun (s : A i) ↦ star s * s))
Tactic: have : closure (Set.range fun s : Π i, A i ↦ star s * s) =
        pi Set.univ fun i => (closure <| Set.range fun s : A i ↦ star s * s) := by
      rw [← closure_pi fun _ => Set.mem_range.mpr ⟨0, by simp⟩]
      congr
      ext x
      simp only [Set.mem_range, funext_iff, mul_apply, star_apply, Set.mem_pi,
        Set.mem_univ, forall_const]
      exact ⟨fun ⟨y, hy⟩ i => ⟨y i, hy i⟩, fun h => ⟨fun i => h i |>.choose,
        fun i => h i |>.choose_spec⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Pi (goal)
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa xy : (i : ι) → A i
this :
  Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
    (pi (M := A) Set.univ fun (i : ι) ↦ closure (Set.range fun (s : A i) ↦ star s * s))
⊢ xa ≤ xy ↔
    ∃ (p : (i : ι) → A i),
      Membership.mem (γ := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s)) p ∧
        xy = xa + p
have simp : (∀ (i : ι),
    ∃ (p : A i),
      Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧ xy i = xa i + p) ↔
  ∃ (p : (i : ι) → A i),
    (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
      xy = xa + p
Tactic: simp only [this, Pi.le_def, StarOrderedRing.le_iff, mem_pi, Set.mem_univ, forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Pi (goal)
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa xy : (i : ι) → A i
this :
  Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
    (pi (M := A) Set.univ fun (i : ι) ↦ closure (Set.range fun (s : A i) ↦ star s * s))
⊢ (∀ (i : ι),
      ∃ (p : A i),
        Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧ xy i = xa i + p) ↔
    ∃ (p : (i : ι) → A i),
      (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
        xy = xa + p
have refine_1 : ∀
  (h :
    ∀ (i : ι),
      ∃ (p : A i),
        Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧ xy i = xa i + p),
  ∃ (p : (i : ι) → A i),
    (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
      xy = xa + p
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Pi (goal)
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa xy : (i : ι) → A i
this :
  Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
    (pi (M := A) Set.univ fun (i : ι) ↦ closure (Set.range fun (s : A i) ↦ star s * s))
refine_1 :
  ∀
    (h :
      ∀ (i : ι),
        ∃ (p : A i),
          Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧
            xy i = xa i + p),
    ∃ (p : (i : ι) → A i),
      (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
        xy = xa + p
⊢ (∀ (i : ι),
      ∃ (p : A i),
        Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧ xy i = xa i + p) ↔
    ∃ (p : (i : ι) → A i),
      (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
        xy = xa + p
have refine_2 : (∃ (p : (i : ι) → A i),
    (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
      xy = xa + p) →
  ∀ (i : ι),
    ∃ (p : A i),
      Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧ xy i = xa i + p
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Pi (goal)
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa xy : (i : ι) → A i
this :
  Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
    (pi (M := A) Set.univ fun (i : ι) ↦ closure (Set.range fun (s : A i) ↦ star s * s))
h :
  ∀ (i : ι),
    ∃ (p : A i),
      Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧ xy i = xa i + p
⊢ ∃ (p : (i : ι) → A i),
    (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
      xy = xa + p
have refine_1 : ∃ (p : (i : ι) → A i),
  (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
    ∀ (x : ι), xy x = xa x + p x
Tactic: simp only [funext_iff, add_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Pi (goal)
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa xy : (i : ι) → A i
this :
  Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
    (pi (M := A) Set.univ fun (i : ι) ↦ closure (Set.range fun (s : A i) ↦ star s * s))
⊢ (∃ (p : (i : ι) → A i),
      (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
        xy = xa + p) →
    ∀ (i : ι),
      ∃ (p : A i),
        Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧ xy i = xa i + p
have refine_2 : ∀ (x : (i : ι) → A i),
  (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (x i)) →
    xy = xa + x →
      ∀ (i : ι),
        ∃ (p : A i),
          Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧ xy i = xa i + p
Tactic: simp only [forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NonUnitalSemiring α
inst_1 : NonUnitalSemiring β
inst_2 : PartialOrder α
inst_3 : PartialOrder β
inst_4 : StarRing α
inst_5 : StarRing β
inst_6 : StarOrderedRing α
inst_7 : StarOrderedRing β
xa : α
xy : β
ya : α
yb : β
⊢ Eq (α := AddSubmonoid (α × β)) (closure (Set.range fun (s : α × β) ↦ star s * s))
    (prod (closure (Set.range fun (s : α) ↦ star s * s)) (closure (Set.range fun (s : β) ↦ star s * s)))
have rw : Eq (α := AddSubmonoid (α × β)) (closure (Set.range fun (s : α × β) ↦ star s * s))
  (closure (Set.range fun (p : α × β) ↦ (star p.1 * p.1, star p.2 * p.2)))
Tactic: rw [← closure_prod (Set.mem_range.2 ⟨0, by simp⟩) (Set.mem_range.2 ⟨0, by simp⟩),
        Set.prod_range_range_eq]