awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
⊢ LE.le.{u_5} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)

Tactic:
rw [StarOrderedRing.le_iff] at hxy ⊢

Premises used: StarOrderedRing.le_iff
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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
⊢ ∃ (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:
obtain ⟨p, hp, rfl⟩ := hxy

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

Tactic:
⟨f p, ?_, map_add f _ _⟩

Premises used: map_add, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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)
⊢ ∃ (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:
refine ⟨f p, ?_, map_add f _ _⟩
-- Module: Mathlib.Algebra.Order.Star.Basic
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
⊢ ∀ (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 _
-- Module: Mathlib.Algebra.Order.Star.Basic
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)
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)
⊢ 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:
induction hp using AddSubmonoid.closure_induction
-- Module: Mathlib.Algebra.Order.Star.Basic
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
hf : ∀ (r : R), Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) (star r) : S) (star ((f : (a : R) → S) r) : S)
x_1 : R
h : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) x_1
⊢ Membership.mem.{u_5, u_5} (α := S) (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s))
    ((f : (a : R) → S) x_1 : S)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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) 0 : S)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Star.Basic
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
hf : ∀ (r : R), Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) (star r) : S) (star ((f : (a : R) → S) r) : S)
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
h :
  Membership.mem.{u_5, u_5} (α := S) (γ := AddSubmonoid S) (AddSubmonoid.closure (range fun (s : S) ↦ star s * s))
    ((f : (a : R) → S) x_1 : S)
h_1 :
  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_1 + y) : S)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Star.Basic
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

Tactic:
⟨fun h ↦ ?_, map_rel f⟩

Premises used: RelHomClass.map_rel, Iff.intro
-- Module: Mathlib.Algebra.Order.Star.Basic
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
refine : ∀ (h : LE.le.{u_5} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)), x ≤ y
⊢ 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⟩
-- Module: Mathlib.Algebra.Order.Star.Basic
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)
⊢ ∀ (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
-- Module: Mathlib.Algebra.Order.Star.Basic
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
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)
⊢ x ≤ y

Tactic:
rw [← f_inv_f x, ← f_inv_f y]
-- Module: Mathlib.Algebra.Order.Star.Basic
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
⊢ 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:
NonUnitalStarRingHom.map_le_map_of_map_star f_inv h

Premises used: NonUnitalStarRingHom.map_le_map_of_map_star
-- Module: Mathlib.Algebra.Order.Star.Basic
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
⊢ 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:
exact NonUnitalStarRingHom.map_le_map_of_map_star f_inv h

Premises used: NonUnitalStarRingHom.map_le_map_of_map_star
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
a b : ℕ
⊢ 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
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
a b : ℕ
this : Eq (α := AddSubmonoid ℕ) (AddSubmonoid.closure (range fun (x : ℕ) ↦ x * x)) ⊤
⊢ a ≤ b ↔
    ∃ (p : ℕ),
      Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure (range fun (s : ℕ) ↦ star s * s)) p ∧ b = a + p

Tactic:
simp [this, le_iff_exists_add]

Premises used: le_iff_exists_add
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
p : R
hp : IsStarProjection p
⊢ 0 ≤ 1 - p

Tactic:
hp.one_sub.nonneg

Premises used: IsStarProjection.one_sub, IsStarProjection.nonneg
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
p : R
hp : IsStarProjection p
⊢ p ≤ 1

Tactic:
sub_nonneg.mp hp.one_sub_nonneg

Premises used: Iff.mp, sub_nonneg, IsStarProjection.one_sub_nonneg
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
p : R
hp : IsStarProjection p
⊢ Membership.mem (γ := Set R) (Icc 0 1) p

Tactic:
simp only [Set.mem_Icc, hp.nonneg, hp.le_one, and_self]

Premises used: and_self, IsStarProjection.le_one, Set.mem_Icc, IsStarProjection.nonneg
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
hpq : p * q = p
⊢ p ≤ q

Tactic:
sub_nonneg.mp (hp.sub_of_mul_eq_left hq hpq).nonneg

Premises used: IsStarProjection.sub_of_mul_eq_left, Iff.mp, sub_nonneg, IsStarProjection.nonneg
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
hpq : q * p = p
⊢ p ≤ q

Tactic:
sub_nonneg.mp (hp.sub_of_mul_eq_right hq hpq).nonneg

Premises used: Iff.mp, IsStarProjection.sub_of_mul_eq_right, sub_nonneg, IsStarProjection.nonneg
-- Module: Mathlib.Algebra.Order.Star.Conjneg
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
⊢ ∀ (b : G),
    0 ((Equiv.symm (Equiv.neg G) : (a : G) → G) b) ≤ conjneg f ((Equiv.symm (Equiv.neg G) : (a : G) → G) b) ↔ 0 b ≤ f b

Tactic:
simp [starRingEnd_apply]

Premises used: starRingEnd_apply
-- Module: Mathlib.Algebra.Order.Star.Conjneg
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
simp_rw₂ : 0 ≤ f ∧ conjneg f ≠ 0 ↔ 0 ≤ f ∧ f ≠ 0
⊢ 0 < conjneg f ↔ 0 < f

Tactic:
simp_rw [lt_iff_le_and_ne, ne_comm, conjneg_nonneg, conjneg_ne_zero]

Premises used: lt_iff_le_and_ne, ne_comm, conjneg_nonneg, conjneg_ne_zero
-- Module: Mathlib.Algebra.Order.Star.Conjneg
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
simp_rw₁ : 0 ≤ conjneg (-f) ↔ 0 ≤ -f
⊢ conjneg f ≤ 0 ↔ f ≤ 0

Tactic:
simp_rw [← neg_nonneg, ← conjneg_neg, conjneg_nonneg]

Premises used: conjneg_neg, neg_nonneg, conjneg_nonneg
-- Module: Mathlib.Algebra.Order.Star.Conjneg
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
simp_rw₁ : 0 < conjneg (-f) ↔ 0 < -f
⊢ conjneg f < 0 ↔ f < 0

Tactic:
simp_rw [← neg_pos, ← conjneg_neg, conjneg_pos]

Premises used: neg_pos, conjneg_pos, conjneg_neg
-- Module: Mathlib.Algebra.Order.Star.Pi
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
x : ι
⊢ HMul.hMul (α := A x) (star 0) 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Star.Pi
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
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))
⊢ 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:
rw [← closure_pi fun _ => Set.mem_range.mpr ⟨0, by simp⟩]

Premises used: Iff.mpr, Set.mem_range, AddSubmonoid.closure_pi, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Star.Pi
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
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)
⊢ 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:
congr
-- Module: Mathlib.Algebra.Order.Star.Pi
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
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
⊢ 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:
ext x
-- Module: Mathlib.Algebra.Order.Star.Pi
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
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
⊢ 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:
simp only [Set.mem_range, funext_iff, mul_apply, star_apply, Set.mem_pi,
        Set.mem_univ, forall_const]

Premises used: Set.mem_range, Pi.mul_apply, funext_iff, Set.mem_pi, Pi.star_apply, Set.mem_univ, forall_const
-- Module: Mathlib.Algebra.Order.Star.Pi
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
⊢ (∃ (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:
⟨fun ⟨y, hy⟩ i => ⟨y i, hy i⟩, fun h => ⟨fun i => h i |>.choose,
        fun i => h i |>.choose_spec⟩⟩

Premises used: Exists.choose_spec, HMul.hMul, Exists, _private.0.Pi.instStarOrderedRing.match_5, Iff.intro, Exists.intro, Exists.choose, Eq, Star.star
-- Module: Mathlib.Algebra.Order.Star.Pi
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
⊢ (∃ (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:
exact ⟨fun ⟨y, hy⟩ i => ⟨y i, hy i⟩, fun h => ⟨fun i => h i |>.choose,
        fun i => h i |>.choose_spec⟩⟩
-- Module: Mathlib.Algebra.Order.Star.Pi
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))

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⟩⟩
-- Module: Mathlib.Algebra.Order.Star.Pi
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))
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
⊢ 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

Tactic:
simp only [this, Pi.le_def, StarOrderedRing.le_iff, mem_pi, Set.mem_univ, forall_const]

Premises used: StarOrderedRing.le_iff, Set.mem_univ, forall_const, AddSubmonoid.mem_pi, Pi.le_def
-- Module: Mathlib.Algebra.Order.Star.Pi
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

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro