awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
h₁ :
  HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
⊢ (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
have calc : (a • x + b • y)⁻¹ʳ =
  (HSMul.hSMul (β := A) a ((conjSqrt x : (a : A) → A) 1 : A) +
      HSMul.hSMul (β := A) b ((conjSqrt x : (a : A) → A) z : A))⁻¹ʳ
Tactic: calc _ = (a • conjSqrt x 1 + b • conjSqrt x z)⁻¹ʳ := by
        rw [conjSqrt_conjSqrt_ringInverse _ _ xpos, conjSqrt_one x xpos.nonneg]
      _ = (conjSqrt x (a • 1 + b • z))⁻¹ʳ := by simp
      _ = conjSqrt x⁻¹ʳ ((a • 1 + b • z) ^ (-1 : ℝ)) := by
        rw [ringInverse_conjSqrt _ _ xpos, ← inverse_eq_rpow_neg_one]
      _ ≤ conjSqrt x⁻¹ʳ (a • 1 + b • z ^ (-1 : ℝ)) := by
        gcongr
        rw [h₁, h₂]
        refine (cfc_le_iff _ _ _ ?_ ?_).mpr ?_
        · apply ContinuousOn.rpow_const (by fun_prop)
          intro r hr
          have := zpos.spectrum_pos hr
          have : 0 ≤ b * r := by positivity
          cases lt_or_eq_of_le ha <;> grind
        · refine ContinuousOn.const_add (ContinuousOn.const_mul ?_ _) _
          exact ContinuousOn.rpow_const (by fun_prop) (by grind)
        · intro r hr
          suffices (a • 1 + b • r) ^ (-1 : ℤ) ≤ a • 1 ^ (-1 : ℤ) + b • r ^ (-1 : ℤ) by
            simp_rw [← Real.rpow_intCast] at this
            simpa using this
          have : ConvexOn ℝ (Set.Ioi 0) (fun z : ℝ => z ^ (-1 : ℤ)) := convexOn_zpow (-1)
          grind [ConvexOn, IsStrictlyPositive.spectrum_pos]
      _ = conjSqrt x⁻¹ʳ (a • 1 + b • z⁻¹ʳ) := by rw [← inverse_eq_rpow_neg_one]
      _ = a • inverse x + b • conjSqrt x⁻¹ʳ z⁻¹ʳ := by
        simp [conjSqrt_one x⁻¹ʳ (by grind)]
      _ = _ := by
        rw [← ringInverse_conjSqrt _ _ xpos, conjSqrt_conjSqrt_ringInverse _ _ xpos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
h₁ :
  HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
calc :
  (a • x + b • y)⁻¹ʳ =
    (HSMul.hSMul (β := A) a ((conjSqrt x : (a : A) → A) 1 : A) +
        HSMul.hSMul (β := A) b ((conjSqrt x : (a : A) → A) z : A))⁻¹ʳ
⊢ (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
have calc₁ : (HSMul.hSMul (β := A) a ((conjSqrt x : (a : A) → A) 1 : A) +
      HSMul.hSMul (β := A) b ((conjSqrt x : (a : A) → A) z : A))⁻¹ʳ =
  ((conjSqrt x : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z))⁻¹ʳ
Tactic: calc _ = (a • conjSqrt x 1 + b • conjSqrt x z)⁻¹ʳ := by
        rw [conjSqrt_conjSqrt_ringInverse _ _ xpos, conjSqrt_one x xpos.nonneg]
      _ = (conjSqrt x (a • 1 + b • z))⁻¹ʳ := by simp
      _ = conjSqrt x⁻¹ʳ ((a • 1 + b • z) ^ (-1 : ℝ)) := by
        rw [ringInverse_conjSqrt _ _ xpos, ← inverse_eq_rpow_neg_one]
      _ ≤ conjSqrt x⁻¹ʳ (a • 1 + b • z ^ (-1 : ℝ)) := by
        gcongr
        rw [h₁, h₂]
        refine (cfc_le_iff _ _ _ ?_ ?_).mpr ?_
        · apply ContinuousOn.rpow_const (by fun_prop)
          intro r hr
          have := zpos.spectrum_pos hr
          have : 0 ≤ b * r := by positivity
          cases lt_or_eq_of_le ha <;> grind
        · refine ContinuousOn.const_add (ContinuousOn.const_mul ?_ _) _
          exact ContinuousOn.rpow_const (by fun_prop) (by grind)
        · intro r hr
          suffices (a • 1 + b • r) ^ (-1 : ℤ) ≤ a • 1 ^ (-1 : ℤ) + b • r ^ (-1 : ℤ) by
            simp_rw [← Real.rpow_intCast] at this
            simpa using this
          have : ConvexOn ℝ (Set.Ioi 0) (fun z : ℝ => z ^ (-1 : ℤ)) := convexOn_zpow (-1)
          grind [ConvexOn, IsStrictlyPositive.spectrum_pos]
      _ = conjSqrt x⁻¹ʳ (a • 1 + b • z⁻¹ʳ) := by rw [← inverse_eq_rpow_neg_one]
      _ = a • inverse x + b • conjSqrt x⁻¹ʳ z⁻¹ʳ := by
        simp [conjSqrt_one x⁻¹ʳ (by grind)]
      _ = _ := by
        rw [← ringInverse_conjSqrt _ _ xpos, conjSqrt_conjSqrt_ringInverse _ _ xpos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
h₁ :
  HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
calc :
  (a • x + b • y)⁻¹ʳ =
    (HSMul.hSMul (β := A) a ((conjSqrt x : (a : A) → A) 1 : A) +
        HSMul.hSMul (β := A) b ((conjSqrt x : (a : A) → A) z : A))⁻¹ʳ
calc₁ :
  (HSMul.hSMul (β := A) a ((conjSqrt x : (a : A) → A) 1 : A) +
        HSMul.hSMul (β := A) b ((conjSqrt x : (a : A) → A) z : A))⁻¹ʳ =
    ((conjSqrt x : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z))⁻¹ʳ
⊢ (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
have calc₂ : Eq (α := A) (((conjSqrt x : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z))⁻¹ʳ : A)
  ((conjSqrt x⁻¹ʳ : (a : A) → A) (HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1)) : A)
Tactic: calc _ = (a • conjSqrt x 1 + b • conjSqrt x z)⁻¹ʳ := by
        rw [conjSqrt_conjSqrt_ringInverse _ _ xpos, conjSqrt_one x xpos.nonneg]
      _ = (conjSqrt x (a • 1 + b • z))⁻¹ʳ := by simp
      _ = conjSqrt x⁻¹ʳ ((a • 1 + b • z) ^ (-1 : ℝ)) := by
        rw [ringInverse_conjSqrt _ _ xpos, ← inverse_eq_rpow_neg_one]
      _ ≤ conjSqrt x⁻¹ʳ (a • 1 + b • z ^ (-1 : ℝ)) := by
        gcongr
        rw [h₁, h₂]
        refine (cfc_le_iff _ _ _ ?_ ?_).mpr ?_
        · apply ContinuousOn.rpow_const (by fun_prop)
          intro r hr
          have := zpos.spectrum_pos hr
          have : 0 ≤ b * r := by positivity
          cases lt_or_eq_of_le ha <;> grind
        · refine ContinuousOn.const_add (ContinuousOn.const_mul ?_ _) _
          exact ContinuousOn.rpow_const (by fun_prop) (by grind)
        · intro r hr
          suffices (a • 1 + b • r) ^ (-1 : ℤ) ≤ a • 1 ^ (-1 : ℤ) + b • r ^ (-1 : ℤ) by
            simp_rw [← Real.rpow_intCast] at this
            simpa using this
          have : ConvexOn ℝ (Set.Ioi 0) (fun z : ℝ => z ^ (-1 : ℤ)) := convexOn_zpow (-1)
          grind [ConvexOn, IsStrictlyPositive.spectrum_pos]
      _ = conjSqrt x⁻¹ʳ (a • 1 + b • z⁻¹ʳ) := by rw [← inverse_eq_rpow_neg_one]
      _ = a • inverse x + b • conjSqrt x⁻¹ʳ z⁻¹ʳ := by
        simp [conjSqrt_one x⁻¹ʳ (by grind)]
      _ = _ := by
        rw [← ringInverse_conjSqrt _ _ xpos, conjSqrt_conjSqrt_ringInverse _ _ xpos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
h₁ :
  HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
calc :
  (a • x + b • y)⁻¹ʳ =
    (HSMul.hSMul (β := A) a ((conjSqrt x : (a : A) → A) 1 : A) +
        HSMul.hSMul (β := A) b ((conjSqrt x : (a : A) → A) z : A))⁻¹ʳ
calc₁ :
  (HSMul.hSMul (β := A) a ((conjSqrt x : (a : A) → A) 1 : A) +
        HSMul.hSMul (β := A) b ((conjSqrt x : (a : A) → A) z : A))⁻¹ʳ =
    ((conjSqrt x : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z))⁻¹ʳ
calc₂ :
  Eq (α := A) (((conjSqrt x : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z))⁻¹ʳ : A)
    ((conjSqrt x⁻¹ʳ : (a : A) → A) (HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1)) : A)
⊢ (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
have calc₃ : LE.le (α := A) ((conjSqrt x⁻¹ʳ : (a : A) → A) (HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1)) : A)
  ((conjSqrt x⁻¹ʳ : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1)) : A)
Tactic: calc _ = (a • conjSqrt x 1 + b • conjSqrt x z)⁻¹ʳ := by
        rw [conjSqrt_conjSqrt_ringInverse _ _ xpos, conjSqrt_one x xpos.nonneg]
      _ = (conjSqrt x (a • 1 + b • z))⁻¹ʳ := by simp
      _ = conjSqrt x⁻¹ʳ ((a • 1 + b • z) ^ (-1 : ℝ)) := by
        rw [ringInverse_conjSqrt _ _ xpos, ← inverse_eq_rpow_neg_one]
      _ ≤ conjSqrt x⁻¹ʳ (a • 1 + b • z ^ (-1 : ℝ)) := by
        gcongr
        rw [h₁, h₂]
        refine (cfc_le_iff _ _ _ ?_ ?_).mpr ?_
        · apply ContinuousOn.rpow_const (by fun_prop)
          intro r hr
          have := zpos.spectrum_pos hr
          have : 0 ≤ b * r := by positivity
          cases lt_or_eq_of_le ha <;> grind
        · refine ContinuousOn.const_add (ContinuousOn.const_mul ?_ _) _
          exact ContinuousOn.rpow_const (by fun_prop) (by grind)
        · intro r hr
          suffices (a • 1 + b • r) ^ (-1 : ℤ) ≤ a • 1 ^ (-1 : ℤ) + b • r ^ (-1 : ℤ) by
            simp_rw [← Real.rpow_intCast] at this
            simpa using this
          have : ConvexOn ℝ (Set.Ioi 0) (fun z : ℝ => z ^ (-1 : ℤ)) := convexOn_zpow (-1)
          grind [ConvexOn, IsStrictlyPositive.spectrum_pos]
      _ = conjSqrt x⁻¹ʳ (a • 1 + b • z⁻¹ʳ) := by rw [← inverse_eq_rpow_neg_one]
      _ = a • inverse x + b • conjSqrt x⁻¹ʳ z⁻¹ʳ := by
        simp [conjSqrt_one x⁻¹ʳ (by grind)]
      _ = _ := by
        rw [← ringInverse_conjSqrt _ _ xpos, conjSqrt_conjSqrt_ringInverse _ _ xpos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
⊢ ConvexOn ℝ (β := A) (Ici 0) fun (x : A) ↦ Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
have this : ∀ (x : A),
  Membership.mem (γ := Set A) (Ici 0) x →
    IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
Tactic: have : ∀ x ∈ Ici (0 : A), IsStrictlyPositive (algebraMap ℝ A t + x) := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
⊢ ConvexOn ℝ (β := A) (Ici 0) fun (x : A) ↦ Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
have haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
Tactic: have haddl : Function.Injective addl := by intro _ _; simp [addl]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
⊢ Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
have rw : Eq.{u_1 + 1} (α := Set A) (Ici 0) (Ici 0)
Tactic: rw [Set.preimage_image_eq _ haddl]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
⊢ ConvexOn ℝ (β := A) (Ici 0) fun (x : A) ↦ Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
have hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
Tactic: have hici : Ici (0 : A) = addl ⁻¹' addl '' Ici 0 := by
    rw [Set.preimage_image_eq _ haddl]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
⊢ ConvexOn ℝ (β := A) (Ici 0) fun (x : A) ↦ Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
have simp_rw : ConvexOn ℝ (β := A) (Ici 0) fun (x : A) ↦ Ring.inverse (HAdd.hAdd (β := A) x ((algebraMap ℝ A : (a : ℝ) → A) t : A))
Tactic: simp_rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
⊢ ConvexOn ℝ (β := A) (Ici 0) fun (x : A) ↦ Ring.inverse (HAdd.hAdd (β := A) x ((algebraMap ℝ A : (a : ℝ) → A) t : A))
have change : ConvexOn ℝ (E := A) (β := A) (Ici 0) (Ring.inverse ∘ (⇑addl : (a : A) → A))
Tactic: change ConvexOn ℝ (Ici 0) (Ring.inverse ∘ addl)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
⊢ ConvexOn ℝ (E := A) (β := A) (Ici 0) (Ring.inverse ∘ (⇑addl : (a : A) → A))
have rw : ConvexOn ℝ (E := A) (β := A) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
  (Ring.inverse ∘ (⇑addl : (a : A) → A))
Tactic: rw [hici]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
⊢ ConvexOn ℝ (E := A) (β := A) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
    (Ring.inverse ∘ (⇑addl : (a : A) → A))
have hf : ConvexOn ℝ (E := A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)) Ring.inverse
Tactic: apply ConvexOn.comp_affineMap
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
⊢ ConvexOn ℝ (E := A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)) Ring.inverse
have hf : Subset (α := Set A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)) {a : A | IsStrictlyPositive a}
Tactic: refine ConvexOn.subset CStarAlgebra.convexOn_ringInverse ?_ (Convex.affine_image _ (convex_Ici _))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
⊢ Subset (α := Set A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)) {a : A | IsStrictlyPositive a}
have hf : Subset (α := Set A) (Ici ((algebraMap ℝ A : (a : ℝ) → A) t) : Set A) ({a : A | IsStrictlyPositive a} : Set A)
Tactic: simp only [AffineMap.toConstProdLinearMap_symm_apply, AffineMap.coe_add,
    LinearMap.coe_toAffineMap, LinearMap.id_coe, AffineMap.coe_const, Pi.add_apply, id_eq,
    Function.const_apply, image_add_right, preimage_add_const_Ici, sub_neg_eq_add, zero_add, addl]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
α β : ℚ
⊢ (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice ↔ α.den = 1 ∧ β.den = 1
have refine_1 : ∀ (H : (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice), α.den = 1 ∧ β.den = 1
Tactic: refine ⟨fun H ↦ ?_, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
α β : ℚ
refine_1 : ∀ (H : (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice), α.den = 1 ∧ β.den = 1
⊢ (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice ↔ α.den = 1 ∧ β.den = 1
have refine_2 : α.den = 1 ∧ β.den = 1 → ∀ (h₁ : α.den = 1) (h₂ : β.den = 1), (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
Tactic: refine ⟨fun H ↦ ?_, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
α β : ℚ
H : (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
⊢ α.den = 1 ∧ β.den = 1
have refine_1 : ∀ (m n : ℤ) (e : (↑m : ℂ) * L.ω₁ + (↑n : ℂ) * L.ω₂ = (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂), α.den = 1 ∧ β.den = 1
Tactic: obtain ⟨m, n, e⟩ := mem_lattice.mp H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
α β : ℚ
H : (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
m n : ℤ
e : (↑m : ℂ) * L.ω₁ + (↑n : ℂ) * L.ω₂ = (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂
⊢ HSub.hSub (α := ℝ) (↑m : ℝ) (↑α : ℝ) • L.ω₁ + HSub.hSub (α := ℝ) (↑n : ℝ) (↑β : ℝ) • L.ω₂ = 0
have simp : HSub.hSub (α := ℂ) (↑m : ℂ) (↑α : ℂ) * L.ω₁ + HSub.hSub (α := ℂ) (↑n : ℂ) (↑β : ℂ) * L.ω₂ = 0
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
α β : ℚ
H : (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
m n : ℤ
e : (↑m : ℂ) * L.ω₁ + (↑n : ℂ) * L.ω₂ = (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂
⊢ α.den = 1 ∧ β.den = 1
have this : HSub.hSub (α := ℝ) (↑m : ℝ) (↑α : ℝ) = 0 ∧ HSub.hSub (α := ℝ) (↑n : ℝ) (↑β : ℝ) = 0
Tactic: have := LinearIndependent.pair_iff.mp L.indep (m - α) (n - β)
      (by simp; linear_combination e)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
α β : ℚ
H : (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
m n : ℤ
e : (↑m : ℂ) * L.ω₁ + (↑n : ℂ) * L.ω₂ = (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂
this : HSub.hSub (α := ℝ) (↑m : ℝ) (↑α : ℝ) = 0 ∧ HSub.hSub (α := ℝ) (↑n : ℝ) (↑β : ℝ) = 0
⊢ α.den = 1 ∧ β.den = 1
have this₁ : Eq (α := ℝ) (↑m : ℝ) (↑α : ℝ) ∧ Eq (α := ℝ) (↑n : ℝ) (↑β : ℝ)
Tactic: simp only [sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
α β : ℚ
H : (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
m n : ℤ
e : (↑m : ℂ) * L.ω₁ + (↑n : ℂ) * L.ω₂ = (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂
this : Eq (α := ℝ) (↑m : ℝ) (↑α : ℝ) ∧ Eq (α := ℝ) (↑n : ℝ) (↑β : ℝ)
⊢ α.den = 1 ∧ β.den = 1
have this₁ : (↑m : ℚ) = α ∧ (↑n : ℚ) = β
Tactic: norm_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
α β : ℚ
h : α.den = 1 ∧ β.den = 1
h₁ : α.den = 1
h₂ : β.den = 1
⊢ (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
have refine_2 : ∀ (α : ℤ), Rat.den (↑α : ℚ) = 1 ∧ β.den = 1 → (↑(↑α : ℚ) : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
Tactic: lift α to ℤ using h₁
Cleared hypotheses: α, h, h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
β : ℚ
h₂ : β.den = 1
α : ℤ
h : Rat.den (↑α : ℚ) = 1 ∧ β.den = 1
⊢ (↑(↑α : ℚ) : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
have refine_2 : ∀ (β : ℤ), Rat.den (↑α : ℚ) = 1 ∧ Rat.den (↑β : ℚ) = 1 → (↑(↑α : ℚ) : ℂ) * L.ω₁ + (↑(↑β : ℚ) : ℂ) * L.ω₂ ∈ L.lattice
Tactic: lift β to ℤ using h₂
Cleared hypotheses: β, h₂, h