awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → (↑({x : A | 0 ≤ x} ∩ ball 0 1) : Type u_1)
i : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ i
simp_rw : Tendsto (fun (x_1 : A) ↦ c i • (x_1 * (↑(x i) : A))) l (𝓝 (c i • (↑(x i) : A)))
⊢ Tendsto (fun (x_1 : A) ↦ x_1 * c i • (↑(x i) : A)) l (𝓝 (c i • (↑(x i) : A)))

Tactic:
simp_rw [mul_smul_comm]

Premises used: mul_smul_comm
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → (↑({x : A | 0 ≤ x} ∩ ball 0 1) : Type u_1)
i : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ i
⊢ ‖(↑(x i) : A)‖ < 1

Tactic:
simpa using (x i).2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → (↑({x : A | 0 ≤ x} ∩ ball 0 1) : Type u_1)
i : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ i
⊢ Tendsto (fun (x_1 : A) ↦ c i • (x_1 * (↑(x i) : A))) l (𝓝 (c i • (↑(x i) : A)))

Tactic:
exact tendsto_const_nhds.smul <| h (x i) (x i).2.1 <| by simpa using (x i).2.2

Premises used: tendsto_const_nhds, And.left, Filter.Tendsto.smul, Subtype.val, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
⊢ (∀ (m : A), Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)) ↔ ∀ (m : A), Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)

Tactic:
⟨fun h m ↦ ?_, fun h m ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
refine_1 : ∀ (h : ∀ (m : A), Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)) (m : A), Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
refine_2 : ∀ (h : ∀ (m : A), Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)) (m : A), Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)
⊢ (∀ (m : A), Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)) ↔ ∀ (m : A), Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)

Tactic:
refine ⟨fun h m ↦ ?_, fun h m ↦ ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)
m : A
refine_1 : l.EventuallyEq (β := A) (star ∘ fun (x : A) ↦ star m * x) fun (x : A) ↦ x * m
⊢ Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)

Tactic:
apply (star_star m ▸ (continuous_star.tendsto _ |>.comp <| h (star m))).congr'
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)
m : A
h₁ : ∀ (x : A) (hx : IsSelfAdjoint x), (star ∘ fun (x : A) ↦ star m * x) x = x * m
⊢ l.EventuallyEq (β := A) (star ∘ fun (x : A) ↦ star m * x) fun (x : A) ↦ x * m

Tactic:
filter_upwards [hl] with x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)
m x : A
hx : IsSelfAdjoint x
⊢ (star ∘ fun (x : A) ↦ star m * x) x = x * m

Tactic:
simp [hx.star_eq]

Premises used: IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
m : A
refine_2 : l.EventuallyEq (β := A) (star ∘ fun (x : A) ↦ x * star m) fun (x : A) ↦ m * x
⊢ Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)

Tactic:
apply (star_star m ▸ (continuous_star.tendsto _ |>.comp <| h (star m))).congr'
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
m : A
h₁ : ∀ (x : A) (hx : IsSelfAdjoint x), (star ∘ fun (x : A) ↦ x * star m) x = m * x
⊢ l.EventuallyEq (β := A) (star ∘ fun (x : A) ↦ x * star m) fun (x : A) ↦ m * x

Tactic:
filter_upwards [hl] with x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
m x : A
hx : IsSelfAdjoint x
⊢ (star ∘ fun (x : A) ↦ x * star m) x = m * x

Tactic:
simp [hx.star_eq]

Premises used: IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ LE.le.{u_1} (α := A) 0 0 ∧ norm.{u_1} (E := A) 0 < 1

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y : A
hx : 0 ≤ x ∧ ‖x‖ < 1
hy : 0 ≤ y ∧ ‖y‖ < 1
⊢ Membership.mem (γ := Set A) ({x : A | 0 ≤ x} ∩ ball 0 1) x

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y : A
hx : 0 ≤ x ∧ ‖x‖ < 1
hy : 0 ≤ y ∧ ‖y‖ < 1
⊢ Membership.mem (γ := Set A) ({x : A | 0 ≤ x} ∩ ball 0 1) y

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y : A
hx : 0 ≤ x ∧ ‖x‖ < 1
hy : 0 ≤ y ∧ ‖y‖ < 1
h :
  ∀ (z : A)
    (hz :
      Membership.mem (γ := Set A) ({x : A | 0 ≤ x} ∩ ball 0 1) z ∧
        (fun (x1 x2 : A) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : A) ↦ x1 ≤ x2) y z),
    (0 ≤ z ∧ ‖z‖ < 1) ∧ Subset.{u_1} (α := Set A) {x : A | z ≤ x} ({x_1 : A | x ≤ x_1} ∩ {x : A | y ≤ x})
⊢ ∃ (k : A), (0 ≤ k ∧ ‖k‖ < 1) ∧ Subset.{u_1} (α := Set A) {x : A | k ≤ x} ({x_1 : A | x ≤ x_1} ∩ {x : A | y ≤ x})

Tactic:
peel directedOn_nonneg_ball x (by simpa) y (by simpa) with z hz

Premises used: CStarAlgebra.directedOn_nonneg_ball
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y : A
hx : 0 ≤ x ∧ ‖x‖ < 1
hy : 0 ≤ y ∧ ‖y‖ < 1
z : A
hz :
  Membership.mem (γ := Set A) ({x : A | 0 ≤ x} ∩ ball 0 1) z ∧
    (fun (x1 x2 : A) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : A) ↦ x1 ≤ x2) y z
⊢ 0 ≤ z ∧ ‖z‖ < 1

Tactic:
simpa using hz.1

Premises used: And.left
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y : A
hx : 0 ≤ x ∧ ‖x‖ < 1
hy : 0 ≤ y ∧ ‖y‖ < 1
z : A
hz :
  Membership.mem (γ := Set A) ({x : A | 0 ≤ x} ∩ ball 0 1) z ∧
    (fun (x1 x2 : A) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : A) ↦ x1 ≤ x2) y z
⊢ (0 ≤ z ∧ ‖z‖ < 1) ∧ Subset.{u_1} (α := Set A) {x : A | z ≤ x} ({x_1 : A | x ≤ x_1} ∩ {x : A | y ≤ x})

Tactic:
exact ⟨by simpa using hz.1, fun a ha ↦ ⟨hz.2.1.trans ha, hz.2.2.trans ha⟩⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ (approximateUnit A).HasBasis (fun (x : A) ↦ 0 ≤ x ∧ ‖x‖ < 1) fun (x : A) ↦ {x_1 : A | x ≤ x_1} ∩ closedBall 0 1

Tactic:
isBasis_nonneg_sections A |>.hasBasis.inf_principal (closedBall 0 1)

Premises used: Filter.IsBasis.hasBasis, CStarAlgebra.approximateUnit, Filter.HasBasis.inf_principal, Metric.closedBall, CStarAlgebra.isBasis_nonneg_sections, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
nth_rw : ‖1 * z - y * z‖₊ ≤ c
⊢ ‖z - y * z‖₊ ≤ c

Tactic:
nth_rw 1 [← one_mul z]

Premises used: one_mul
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
rw : ‖star ((1 - y) * z) * ((1 - y) * z)‖₊ ≤ HPow.hPow (β := ℕ) c 2
⊢ ‖1 * z - y * z‖₊ ≤ c

Tactic:
rw [← sqrt_sq c, le_sqrt_iff_sq_le, ← sub_mul, sq, ← CStarRing.nnnorm_star_mul_self]

Premises used: NNReal.sqrt_sq, NNReal.le_sqrt_iff_sq_le, sq, sub_mul, CStarRing.nnnorm_star_mul_self
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
simp : ‖star z * (1 - star y) * ((1 - y) * z)‖₊ ≤ HPow.hPow (β := ℕ) c 2
⊢ ‖star ((1 - y) * z) * ((1 - y) * z)‖₊ ≤ HPow.hPow (β := ℕ) c 2

Tactic:
simp only [star_mul, star_sub, star_one]

Premises used: StarMul.star_mul, star_sub, star_one
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
⊢ Membership.mem (γ := Set A) (Set.Icc 0 1) y

Tactic:
have hy₀ : y ∈ Set.Icc 0 1 := ⟨hx₀.trans hy.1, hy.2⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
⊢ Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)

Tactic:
have hy' : 1 - y ∈ Set.Icc 0 1 := Set.sub_mem_Icc_zero_iff_right.mpr hy₀
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
rw : ‖star z * HPow.hPow (β := ℕ) (1 - y) 2 * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
⊢ ‖star z * (1 - star y) * ((1 - y) * z)‖₊ ≤ HPow.hPow (β := ℕ) c 2

Tactic:
rw [hy₀.1.star_eq, ← mul_assoc, mul_assoc (star _), ← sq]

Premises used: LE.le.star_eq, mul_assoc, sq, And.left, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
⊢ ‖star z * HPow.hPow (β := ℕ) (1 - y) 2 * z‖₊ ≤ HPow.hPow (β := ℕ) c 2

Tactic:
nnnorm_le_nnnorm_of_nonneg_of_le (star_left_conjugate_nonneg (pow_nonneg hy'.1 2) _) ?_
    |>.trans h

Premises used: CStarAlgebra.pow_nonneg, And.left, LE.le.trans, CStarAlgebra.nnnorm_le_nnnorm_of_nonneg_of_le, OfNat.ofNat, star_left_conjugate_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
refine : star z * HPow.hPow (β := ℕ) (1 - y) 2 * z ≤ star z * (1 - x) * z
⊢ ‖star z * HPow.hPow (β := ℕ) (1 - y) 2 * z‖₊ ≤ HPow.hPow (β := ℕ) c 2

Tactic:
refine nnnorm_le_nnnorm_of_nonneg_of_le (star_left_conjugate_nonneg (pow_nonneg hy'.1 2) _) ?_
    |>.trans h

Premises used: CStarAlgebra.pow_nonneg, And.left, LE.le.trans, CStarAlgebra.nnnorm_le_nnnorm_of_nonneg_of_le, OfNat.ofNat, star_left_conjugate_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
⊢ star z * HPow.hPow (β := ℕ) (1 - y) 2 * z ≤ star z * (1 - x) * z

Tactic:
star_left_conjugate_le_conjugate ?_ _

Premises used: star_left_conjugate_le_conjugate
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
refine : HPow.hPow (β := ℕ) (1 - y) 2 ≤ 1 - x
⊢ star z * HPow.hPow (β := ℕ) (1 - y) 2 * z ≤ star z * (1 - x) * z

Tactic:
refine star_left_conjugate_le_conjugate ?_ _

Premises used: star_left_conjugate_le_conjugate
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
trans : HPow.hPow (β := ℕ) (1 - y) 2 ≤ 1 - y
trans₁ : 1 - y ≤ 1 - x
⊢ HPow.hPow (β := ℕ) (1 - y) 2 ≤ 1 - x

Tactic:
trans (1 - y)

Premises used: HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
⊢ HPow.hPow (β := ℕ) (1 - y) 2 ≤ 1 - y

Tactic:
simpa using pow_antitone hy'.1 hy'.2 one_le_two

Premises used: And.right, And.left, CStarAlgebra.pow_antitone, one_le_two
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
h₁ : x ≤ y
⊢ 1 - y ≤ 1 - x

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
⊢ x ≤ y

Tactic:
hy.1

Premises used: And.left
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
⊢ x ≤ y

Tactic:
exact hy.1

Premises used: And.left
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ
hc : 0 ≤ c
h : ‖star z * (1 - x) * z‖ ≤ HPow.hPow (β := ℕ) c 2
⊢ ‖z - y * z‖ ≤ c

Tactic:
nnnorm_sub_mul_self_le z hx₀ hy h (c := ⟨c, hc⟩)

Premises used: CStarAlgebra.nnnorm_sub_mul_self_le
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h :
  ‖star (↑z : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑x : Unitization ℂ A) * (↑z : Unitization ℂ A)‖ ≤
    HPow.hPow (β := ℕ) c 2
rw : ‖(↑z : Unitization ℂ A) - HMul.hMul (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑z : Unitization ℂ A)‖ ≤ c
⊢ ‖z - y * z‖ ≤ c

Tactic:
rw [← norm_inr (𝕜 := ℂ), inr_sub, inr_mul]

Premises used: Unitization.inr_sub, Unitization.inr_mul, Unitization.norm_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h :
  ‖star (↑z : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑x : Unitization ℂ A) * (↑z : Unitization ℂ A)‖ ≤
    HPow.hPow (β := ℕ) c 2
⊢ ‖(↑z : Unitization ℂ A) - HMul.hMul (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑z : Unitization ℂ A)‖ ≤ c

Tactic:
norm_sub_mul_self_le _ ?_ ?_ hc h

Premises used: CStarAlgebra.norm_sub_mul_self_le
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h :
  ‖star (↑z : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑x : Unitization ℂ A) * (↑z : Unitization ℂ A)‖ ≤
    HPow.hPow (β := ℕ) c 2
refine_1 : LE.le (α := Unitization ℂ A) 0 (↑x : Unitization ℂ A)
refine_2 : Membership.mem (γ := Set (Unitization ℂ A)) (Set.Icc (↑x : Unitization ℂ A) 1) (↑y : Unitization ℂ A)
⊢ ‖(↑z : Unitization ℂ A) - HMul.hMul (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑z : Unitization ℂ A)‖ ≤ c

Tactic:
refine norm_sub_mul_self_le _ ?_ ?_ hc h

Premises used: CStarAlgebra.norm_sub_mul_self_le
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h :
  ‖star (↑z : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑x : Unitization ℂ A) * (↑z : Unitization ℂ A)‖ ≤
    HPow.hPow (β := ℕ) c 2
refine_1 refine_1₁ refine_1₂ refine_1₃ : 0 ≤ x
⊢ LE.le (α := Unitization ℂ A) 0 (↑x : Unitization ℂ A)

Tactic:
rwa [inr_nonneg_iff]

Premises used: Unitization.inr_nonneg_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h :
  ‖star (↑z : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑x : Unitization ℂ A) * (↑z : Unitization ℂ A)‖ ≤
    HPow.hPow (β := ℕ) c 2
⊢ 0 ≤ y

Tactic:
have hy := hx₀.trans hxy
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h :
  ‖star (↑z : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑x : Unitization ℂ A) * (↑z : Unitization ℂ A)‖ ≤
    HPow.hPow (β := ℕ) c 2
hy : 0 ≤ y
refine_2 : x ≤ y ∧ ‖y‖ ≤ 1
⊢ Membership.mem (γ := Set (Unitization ℂ A)) (Set.Icc (↑x : Unitization ℂ A) 1) (↑y : Unitization ℂ A)

Tactic:
rw [Set.mem_Icc, inr_le_iff _ _ hx₀.isSelfAdjoint hy.isSelfAdjoint,
      ← norm_le_one_iff_of_nonneg _, norm_inr]

Premises used: Unitization.inr_le_iff, LE.le.isSelfAdjoint, Set.mem_Icc, CStarAlgebra.norm_le_one_iff_of_nonneg, Unitization.norm_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h :
  ‖star (↑z : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑x : Unitization ℂ A) * (↑z : Unitization ℂ A)‖ ≤
    HPow.hPow (β := ℕ) c 2
hy : 0 ≤ y
⊢ x ≤ y ∧ ‖y‖ ≤ 1

Tactic:
⟨hxy, hy₁⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h :
  ‖star (↑z : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑x : Unitization ℂ A) * (↑z : Unitization ℂ A)‖ ≤
    HPow.hPow (β := ℕ) c 2
hy : 0 ≤ y
⊢ x ≤ y ∧ ‖y‖ ≤ 1

Tactic:
exact ⟨hxy, hy₁⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : A
⊢ Tendsto (fun (x : A) ↦ x * m) (approximateUnit A) (𝓝 m)

Tactic:
tendsto_mul_right_of_forall_nonneg_tendsto (fun m hm₁ hm₂ ↦ ?_) m

Premises used: CStarAlgebra.tendsto_mul_right_of_forall_nonneg_tendsto
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : A
refine : ∀ (m : A) (hm₁ : 0 ≤ m) (hm₂ : ‖m‖ < 1), Tendsto (fun (x : A) ↦ x * m) (approximateUnit A) (𝓝 m)
⊢ Tendsto (fun (x : A) ↦ x * m) (approximateUnit A) (𝓝 m)

Tactic:
refine tendsto_mul_right_of_forall_nonneg_tendsto (fun m hm₁ hm₂ ↦ ?_) m

Premises used: CStarAlgebra.tendsto_mul_right_of_forall_nonneg_tendsto
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
rw :
  ∀ (ib : ℝ),
    0 < ib →
      ∃ (ia : A),
        (0 ≤ ia ∧ ‖ia‖ < 1) ∧
          ∀ (x : A), Membership.mem (γ := Set A) ({x : A | ia ≤ x} ∩ closedBall 0 1) x → x * m ∈ closedBall m ib
⊢ Tendsto (fun (x : A) ↦ x * m) (approximateUnit A) (𝓝 m)

Tactic:
rw [(hasBasis_approximateUnit A).tendsto_iff nhds_basis_closedBall]

Premises used: Filter.HasBasis.tendsto_iff, Metric.nhds_basis_closedBall, CStarAlgebra.hasBasis_approximateUnit
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ
hε : 0 < ε
⊢ 0 ≤ ε

Tactic:
hε.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ
hε : 0 < ε
lift :
  ∀ (ε : ℝ≥0) (hε : 0 < (↑ε : ℝ)),
    ∃ (ia : A),
      (0 ≤ ia ∧ ‖ia‖ < 1) ∧
        ∀ (x : A), Membership.mem (γ := Set A) ({x : A | ia ≤ x} ∩ closedBall 0 1) x → x * m ∈ closedBall m (↑ε : ℝ)
⊢ ∃ (ia : A),
    (0 ≤ ia ∧ ‖ia‖ < 1) ∧
      ∀ (x : A), Membership.mem (γ := Set A) ({x : A | ia ≤ x} ∩ closedBall 0 1) x → x * m ∈ closedBall m ε

Tactic:
lift ε to ℝ≥0 using hε.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
⊢ 0 < ε

Tactic:
rw [coe_pos] at hε

Premises used: NNReal.coe_pos
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ (ia : A),
    (0 ≤ ia ∧ ‖ia‖ < 1) ∧
      ∀ (x : A), Membership.mem (γ := Set A) ({x : A | ia ≤ x} ∩ closedBall 0 1) x → x * m ∈ closedBall m (↑ε : ℝ)

Tactic:
⟨cfcₙ (fun y : ℝ≥0 ↦ 1 - (1 + y)⁻¹) (ε⁻¹ ^ 2 • m),
    ⟨cfcₙ_nonneg_of_predicate, norm_cfcₙ_one_sub_one_add_inv_lt_one (ε⁻¹ ^ 2 • m)⟩, ?_⟩

Premises used: cfcₙ, HSub.hSub, Inv.inv, HPow.hPow, HAdd.hAdd, And.intro, Exists.intro, norm_cfcₙ_one_sub_one_add_inv_lt_one, HSMul.hSMul, OfNat.ofNat, cfcₙ_nonneg_of_predicate