awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
rw :
  (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) ≤
    ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)
⊢ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ≤ (π / 2)⁻¹ * W k

Tactic:
rw [W_eq_integral_sin_pow_div_integral_sin_pow, le_div_iff₀ (integral_sin_pow_pos _)]

Premises used: integral_sin_pow_pos, Real.Wallis.W_eq_integral_sin_pow_div_integral_sin_pow, le_div_iff₀
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1 + 1)) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1))

Tactic:
integral_sin_pow_succ_le (2 * k + 1)

Premises used: HMul.hMul, HAdd.hAdd, integral_sin_pow_succ_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
h :
  (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1 + 1)
⊢ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) ≤
    ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)

Tactic:
convert! integral_sin_pow_succ_le (2 * k + 1)

Premises used: HMul.hMul, HAdd.hAdd, integral_sin_pow_succ_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
h :
  (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / HAdd.hAdd (α := ℝ) (↑(2 * k) : ℝ) 2 +
      HAdd.hAdd (α := ℝ) (↑(2 * k) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * k) : ℝ) 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)
⊢ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1 + 1)

Tactic:
rw [integral_sin_pow (2 * k)]

Premises used: HMul.hMul, integral_sin_pow, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
⊢ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / HAdd.hAdd (α := ℝ) (↑(2 * k) : ℝ) 2 +
      HAdd.hAdd (α := ℝ) (↑(2 * k) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * k) : ℝ) 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
⊢ Tendsto W atTop (𝓝 (π / 2))

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le ?_ tendsto_const_nhds le_W W_le

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, Real.Wallis.W_le, tendsto_const_nhds, Real.Wallis.le_W
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
refine :
  Tendsto (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) * (π / 2)) atTop
    (𝓝 (π / 2))
⊢ Tendsto W atTop (𝓝 (π / 2))

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le ?_ tendsto_const_nhds le_W W_le

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, Real.Wallis.W_le, tendsto_const_nhds, Real.Wallis.le_W
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
rw : 𝓝 (π / 2) = 𝓝 (1 * (π / 2))
rw₁ rw₂ : 𝓝 (π / 2) = 𝓝 (π / 2)
⊢ 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))

Tactic:
rw [sub_zero, one_mul]

Premises used: sub_zero, one_mul
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
⊢ 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))

Tactic:
have : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2)) := by rw [sub_zero, one_mul]
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
rw :
  Tendsto (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) * (π / 2)) atTop
    (𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2)))
⊢ Tendsto (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) * (π / 2)) atTop
    (𝓝 (π / 2))

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
⊢ Tendsto (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) * (π / 2)) atTop
    (𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2)))

Tactic:
Tendsto.mul ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.mul
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
refine :
  Tendsto (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)) atTop
    (𝓝 (HSub.hSub (α := ℝ) 1 0))
⊢ Tendsto (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) * (π / 2)) atTop
    (𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2)))

Tactic:
refine Tendsto.mul ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.mul
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
n : ℕ
rw :
  (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2 - 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)
⊢ (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
    1 - 1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)

Tactic:
rw [sub_div' (ne_of_gt (add_pos_of_nonneg_of_pos (mul_nonneg
      (two_pos : 0 < (2 : ℝ)).le (Nat.cast_nonneg _)) two_pos)), one_mul]

Premises used: mul_nonneg, Nat.cast_nonneg, two_pos, ne_of_gt, LT.lt.le, add_pos_of_nonneg_of_pos, sub_div', one_mul
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
n : ℕ
e_a : HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1 = HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2 - 1
⊢ (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2 - 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
n : ℕ
⊢ HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1 = HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2 - 1

Tactic:
ring
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
⊢ ∀ (n : ℕ),
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
      1 - 1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)

Tactic:
have h : ∀ n : ℕ, ((2 : ℝ) * n + 1) / (2 * n + 2) = 1 - 1 / (2 * n + 2) := by
    intro n
    rw [sub_div' (ne_of_gt (add_pos_of_nonneg_of_pos (mul_nonneg
      (two_pos : 0 < (2 : ℝ)).le (Nat.cast_nonneg _)) two_pos)), one_mul]
    congr 1; ring
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
h :
  ∀ (n : ℕ),
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
      1 - 1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)
simp_rw : Tendsto (fun (i : ℕ) ↦ 1 - 1 / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)) atTop (𝓝 (HSub.hSub (α := ℝ) 1 0))
⊢ Tendsto (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)) atTop
    (𝓝 (HSub.hSub (α := ℝ) 1 0))

Tactic:
simp_rw [h]
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
h :
  ∀ (n : ℕ),
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
      1 - 1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)
⊢ Tendsto (fun (i : ℕ) ↦ 1 - 1 / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)) atTop (𝓝 (HSub.hSub (α := ℝ) 1 0))

Tactic:
(tendsto_const_nhds.div_atTop ?_).const_sub _

Premises used: Filter.Tendsto.div_atTop, tendsto_const_nhds, Filter.Tendsto.const_sub
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
h :
  ∀ (n : ℕ),
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
      1 - 1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)
refine : Tendsto (β := ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) atTop atTop
⊢ Tendsto (fun (i : ℕ) ↦ 1 - 1 / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)) atTop (𝓝 (HSub.hSub (α := ℝ) 1 0))

Tactic:
refine (tendsto_const_nhds.div_atTop ?_).const_sub _

Premises used: Filter.Tendsto.div_atTop, tendsto_const_nhds, Filter.Tendsto.const_sub
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
h :
  ∀ (n : ℕ),
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
      1 - 1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) atTop atTop

Tactic:
Tendsto.atTop_add ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.atTop_add
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
h :
  ∀ (n : ℕ),
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
      1 - 1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)
refine : Tendsto (β := ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑i : ℝ)) atTop atTop
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) atTop atTop

Tactic:
refine Tendsto.atTop_add ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.atTop_add
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
h :
  ∀ (n : ℕ),
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
      1 - 1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑i : ℝ)) atTop atTop

Tactic:
tendsto_natCast_atTop_atTop.const_mul_atTop two_pos

Premises used: Filter.Tendsto.const_mul_atTop, two_pos, tendsto_natCast_atTop_atTop
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
h :
  ∀ (n : ℕ),
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
      1 - 1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑i : ℝ)) atTop atTop

Tactic:
exact tendsto_natCast_atTop_atTop.const_mul_atTop two_pos

Premises used: Filter.Tendsto.const_mul_atTop, tendsto_natCast_atTop_atTop
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
⊢ Tendsto
    (fun (k : ℕ) ↦
      ∏ i ∈ range k,
        (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) *
          ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3)))
    atTop (𝓝 (π / 2))

Tactic:
Real.Wallis.tendsto_W_nhds_pi_div_two

Premises used: Real.Wallis.tendsto_W_nhds_pi_div_two, Real.Wallis.W
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
a : A
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
⟨fun h x hx ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
a : A
refine_1 :
  ∀ (h : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) (x : ℝ)
    (hx : x ∈ spectrum ℝ a), 0 ≤ x
refine_2 :
  ∀ (h : ∀ x ∈ spectrum ℝ a, 0 ≤ x),
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
a : A
h : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
x : ℝ
hx : x ∈ spectrum ℝ a
refine_1 :
  ∀ (x : ℝ≥0) (hx : Membership.mem (α := ℝ) (spectrum ℝ a) ((algebraMap ℝ≥0 ℝ : (a : ℝ≥0) → ℝ) x : ℝ)),
    LE.le (α := ℝ) (0 : ℝ) ((algebraMap ℝ≥0 ℝ : (a : ℝ≥0) → ℝ) x : ℝ)
⊢ 0 ≤ x

Tactic:
obtain ⟨x, -, rfl⟩ := h.algebraMap_image.symm ▸ hx

Premises used: rfl
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
a : A
h : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
x : ℝ≥0
hx : Membership.mem (α := ℝ) (spectrum ℝ a) ((algebraMap ℝ≥0 ℝ : (a : ℝ≥0) → ℝ) x : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((algebraMap ℝ≥0 ℝ : (a : ℝ≥0) → ℝ) x : ℝ)

Tactic:
coe_nonneg x

Premises used: NNReal.coe_nonneg, NNReal.toReal
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
a : A
h : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
x : ℝ≥0
hx : Membership.mem (α := ℝ) (spectrum ℝ a) ((algebraMap ℝ≥0 ℝ : (a : ℝ≥0) → ℝ) x : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((algebraMap ℝ≥0 ℝ : (a : ℝ≥0) → ℝ) x : ℝ)

Tactic:
exact coe_nonneg x

Premises used: NNReal.coe_nonneg
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
a : A
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
.of_subset_range_algebraMap (fun _ ↦ Real.toNNReal_coe) fun x hx ↦ ⟨⟨x, h x hx⟩, rfl⟩

Premises used: Subtype.mk, SpectrumRestricts.of_subset_range_algebraMap, Exists.intro, Real.toNNReal_coe, rfl
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
a : A
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
exact .of_subset_range_algebraMap (fun _ ↦ Real.toNNReal_coe) fun x hx ↦ ⟨⟨x, h x hx⟩, rfl⟩
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
inst_2 : PartialOrder A
inst_3 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
nnreal_iff.mpr <| spectrum_nonneg_of_nonneg ha

Premises used: Iff.mpr, SpectrumRestricts.nnreal_iff, spectrum_nonneg_of_nonneg
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
r : ℝ≥0
⊢ (∀ x ∈ spectrum ℝ≥0 a, r ≤ x) ↔ ∀ x ∈ spectrum ℝ a, (↑r : ℝ) ≤ x

Tactic:
simp [← ha.algebraMap_image]

Premises used: SpectrumRestricts.algebraMap_image
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
r : ℝ≥0
⊢ (∀ x ∈ spectrum ℝ≥0 a, r < x) ↔ ∀ x ∈ spectrum ℝ a, (↑r : ℝ) < x

Tactic:
simp [← ha.algebraMap_image]

Premises used: SpectrumRestricts.algebraMap_image
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
r : ℝ≥0
⊢ (∀ x ∈ spectrum ℝ≥0 a, x ≤ r) ↔ ∀ x ∈ spectrum ℝ a, x ≤ (↑r : ℝ)

Tactic:
simp [← ha.algebraMap_image]

Premises used: SpectrumRestricts.algebraMap_image
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
r : ℝ≥0
⊢ (∀ x ∈ spectrum ℝ≥0 a, x < r) ↔ ∀ x ∈ spectrum ℝ a, x < (↑r : ℝ)

Tactic:
simp [← ha.algebraMap_image]

Premises used: SpectrumRestricts.algebraMap_image
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : IsScalarTower ℝ A A
inst_3 : SMulCommClass ℝ A A
a : A
rw :
  SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℝ A) (↑a : Unitization ℝ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    ∀ x ∈ σₙ ℝ a, 0 ≤ x
rw₁ :
  SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℝ A) (↑a : Unitization ℝ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    ∀ x ∈ spectrum ℝ (A := Unitization ℝ A) (↑a : Unitization ℝ A), 0 ≤ x
rw₂ rw₃ :
  (∀ x ∈ spectrum ℝ (A := Unitization ℝ A) (↑a : Unitization ℝ A), 0 ≤ x) ↔
    ∀ x ∈ spectrum ℝ (A := Unitization ℝ A) (↑a : Unitization ℝ A), 0 ≤ x
⊢ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔ ∀ x ∈ σₙ ℝ a, 0 ≤ x

Tactic:
rw [quasispectrumRestricts_iff_spectrumRestricts_inr,
    Unitization.quasispectrum_eq_spectrum_inr' _ ℝ, SpectrumRestricts.nnreal_iff]

Premises used: Real, SpectrumRestricts.nnreal_iff, quasispectrumRestricts_iff_spectrumRestricts_inr, Unitization.quasispectrum_eq_spectrum_inr'
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : IsScalarTower ℝ A A
inst_3 : SMulCommClass ℝ A A
inst_4 : PartialOrder A
inst_5 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
⊢ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
nnreal_iff.mpr <| quasispectrum_nonneg_of_nonneg _ ha

Premises used: Iff.mpr, QuasispectrumRestricts.nnreal_iff, NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : IsScalarTower ℝ A A
inst_3 : SMulCommClass ℝ A A
a : A
ha : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
r : ℝ≥0
⊢ (∀ x ∈ σₙ ℝ≥0 a, x ≤ r) ↔ ∀ x ∈ σₙ ℝ a, x ≤ (↑r : ℝ)

Tactic:
simp [← ha.algebraMap_image]

Premises used: QuasispectrumRestricts.algebraMap_image
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : IsScalarTower ℝ A A
inst_3 : SMulCommClass ℝ A A
a : A
ha : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
r : ℝ≥0
⊢ (∀ x ∈ σₙ ℝ≥0 a, x < r) ↔ ∀ x ∈ σₙ ℝ a, x < (↑r : ℝ)

Tactic:
simp [← ha.algebraMap_image]

Premises used: QuasispectrumRestricts.algebraMap_image
-- Module: Mathlib.Analysis.Real.Spectrum
Goal:
A : Type u_1
inst : Ring A
inst_1 : PartialOrder A
inst_2 : Algebra ℝ A
inst_3 : NonnegSpectrumClass ℝ A
a : A
x : ℝ≥0
ha : 0 ≤ a
⊢ (↑x : ℝ) ∈ spectrum ℝ a ↔ x ∈ spectrum ℝ≥0 a

Tactic:
simp [← (SpectrumRestricts.nnreal_of_nonneg ha).algebraMap_image, Set.mem_image,
    NNReal.algebraMap_eq_coe]

Premises used: SpectrumRestricts.nnreal_of_nonneg, NNReal.algebraMap_eq_coe, SpectrumRestricts.algebraMap_image, Set.mem_image
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
rw : f (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) (β := E) 0 0) = 0
rw₁ : norm.{u_3} (E := 𝕜) 0 * f 0 = 0
rw₂ : 0 * f 0 = 0
rw₃ rw₄ : Eq (α := ℝ) 0 0
⊢ f 0 = 0

Tactic:
rw [← zero_smul 𝕜 (0 : E), smul, norm_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, norm_zero, zero_smul, OfNat.ofNat
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
x : E
rw : f (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) (-1) x) = f x
rw₁ : norm.{u_3} (E := 𝕜) (-1) * f x = f x
rw₂ : norm.{u_3} (E := 𝕜) 1 * f x = f x
rw₃ : f (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 1 x) = f x
rw₄ rw₅ : f x = f x
⊢ f (-x) = f x

Tactic:
rw [← neg_one_smul 𝕜, smul, norm_neg, ← smul, one_smul]

Premises used: neg_one_smul, one_smul, norm_neg
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
⊢ f (r • x) = ‖r‖ * f x

Tactic:
le_antisymm (smul_le r x) ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
refine : ‖r‖ * f x ≤ f (r • x)
⊢ f (r • x) = ‖r‖ * f x

Tactic:
refine le_antisymm (smul_le r x) ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
pos : ∀ (h : r = 0), ‖r‖ * f x ≤ f (r • x)
neg : ∀ (h : ¬r = 0), ‖r‖ * f x ≤ f (r • x)
⊢ ‖r‖ * f x ≤ f (r • x)

Tactic:
by_cases h : r = 0
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
h : r = 0
⊢ ‖r‖ * f x ≤ f (r • x)

Tactic:
simp [h, map_zero]
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
h : ¬r = 0
neg : ‖r‖⁻¹ * (‖r‖ * f x) ≤ ‖r‖⁻¹ * f (r • x)
⊢ ‖r‖ * f x ≤ f (r • x)

Tactic:
rw [← mul_le_mul_iff_right₀ (inv_pos.mpr (norm_pos_iff.mpr h))]

Premises used: Iff.mpr, norm_pos_iff, inv_pos, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
h : ¬r = 0
neg : f x ≤ ‖r‖⁻¹ * f (r • x)
⊢ ‖r‖⁻¹ * (‖r‖ * f x) ≤ ‖r‖⁻¹ * f (r • x)

Tactic:
rw [inv_mul_cancel_left₀ (norm_ne_zero_iff.mpr h)]

Premises used: Iff.mpr, inv_mul_cancel_left₀, norm_ne_zero_iff
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
h : ¬r = 0
⊢ f (r⁻¹ • r • x) ≤ ‖r⁻¹‖ * f (r • x)

Tactic:
specialize smul_le r⁻¹ (r • x)

Premises used: Inv.inv, HSMul.hSMul
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
r : 𝕜
x : E
h : ¬r = 0
smul_le : f (r⁻¹ • r • x) ≤ ‖r⁻¹‖ * f (r • x)
⊢ f (r⁻¹ • r • x) ≤ ‖r‖⁻¹ * f (r • x)

Tactic:
rw [norm_inv] at smul_le

Premises used: norm_inv
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
r : 𝕜
x : E
h : ¬r = 0
smul_le : f (r⁻¹ • r • x) ≤ ‖r‖⁻¹ * f (r • x)
⊢ f (r⁻¹ • r • x) ≤ ‖r‖⁻¹ * f (r • x)

Tactic:
smul_le