harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem coeff_restriction {p : R[X]} {n : ℕ} : ↑(coeff (restriction p) n) = coeff p n

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
⊢ ↑(p.restriction.coeff n) = p.coeff n

Tactic:
simp only [restriction, coeff_monomial, finset_sum_coeff, mem_support_iff, Finset.sum_ite_eq',
  Ne, ite_not]

Result:
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
⊢ ↑(if p.coeff n = 0 then 0 else ⟨p.coeff n, ⋯⟩) = p.coeff n

Proof state:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = p.coeff n

Tactic:
rw [h]

Result:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = 0

Proof state:
case neg
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ ↑⟨p.coeff n, ⋯⟩ = p.coeff n

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
⊢ ↑(if p.coeff n = 0 then 0 else ⟨p.coeff n, ⋯⟩) = p.coeff n

Tactic:
split_ifs with h

Result:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = p.coeff n

case neg
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ ↑⟨p.coeff n, ⋯⟩ = p.coeff n

Proof state:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/Schreier.lean
theorem card_commutator_le_of_finite_commutatorSet [Finite (commutatorSet G)] :
    Nat.card (_root_.commutator G) ≤ cardCommutatorBound (Nat.card (commutatorSet G))

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  (center ↥(closureCommutatorRepresentatives G)).index ≤
    Nat.card ↑(commutatorSet G) ^ Group.rank ↥(closureCommutatorRepresentatives G)
h2 :
  Nat.card ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) ∣
    (center ↥(closureCommutatorRepresentatives G)).index ^
      ((center ↥(closureCommutatorRepresentatives G)).index * Nat.card ↑(commutatorSet G) + 1)
⊢ Nat.card ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))

Tactic:
rw [card_commutator_closureCommutatorRepresentatives] at h2

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  (center ↥(closureCommutatorRepresentatives G)).index ≤
    Nat.card ↑(commutatorSet G) ^ Group.rank ↥(closureCommutatorRepresentatives G)
h2 :
  Nat.card ↥(_root_.commutator G) ∣
    (center ↥(closureCommutatorRepresentatives G)).index ^
      ((center ↥(closureCommutatorRepresentatives G)).index * Nat.card ↑(commutatorSet G) + 1)
⊢ Nat.card ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
-- Mathlib/Analysis/Complex/Periodic.lean
theorem exp_decay_of_zero_at_inf (hh : 0 < h) (hf : Periodic f h)
    (h_hol : ∀ᶠ z in I∞, DifferentiableAt ℂ f z) (h_zer : ZeroAtFilter I∞ f) :
    f =O[I∞] fun z ↦ Real.exp (-2 * π * im z / h)

Proof state:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_zer : I∞.ZeroAtFilter f
⊢ cuspFunction h f =O[𝓝[≠] 0] id

Tactic:
simpa only [cuspFunction_zero_of_zero_at_inf hh h_zer, sub_zero] using
  (differentiableAt_cuspFunction_zero hh hf h_hol h_zer.boundedAtFilter).isBigO_sub.mono
    nhdsWithin_le_nhds

Result:
no goals

Proof state:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_zer : I∞.ZeroAtFilter f
this : cuspFunction h f =O[?m.40668] id
⊢ f =O[I∞] fun z => rexp (-2 * π * z.im / h)

Tactic:
simpa only [comp_def, eq_cuspFunction hh.ne' hf, id_eq, norm_qParam]
  using (this.comp_tendsto (qParam_tendsto hh)).norm_right

Result:
no goals

Proof state:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_zer : I∞.ZeroAtFilter f
⊢ f =O[I∞] fun z => rexp (-2 * π * z.im / h)

Tactic:
suffices cuspFunction h f =O[_] id by
  simpa only [comp_def, eq_cuspFunction hh.ne' hf, id_eq, norm_qParam]
    using (this.comp_tendsto (qParam_tendsto hh)).norm_right

Result:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_zer : I∞.ZeroAtFilter f
⊢ cuspFunction h f =O[𝓝[≠] 0] id
-- Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean
/-- The argument of `1 + z` for `z` in the open unit disc is always in `(-π / 2, π / 2)`. -/
lemma arg_one_add_mem_Ioo {z : ℂ} (hz : ‖z‖ < 1) : (1 + z).arg ∈ Set.Ioo (-(π / 2)) (π / 2)

Proof state:
z : ℂ
hz : ‖z‖ < 1
⊢ -1 < z.re ∨ 1 + z = 0

Tactic:
exact Or.inl (abs_lt.mp ((abs_re_le_norm z).trans_lt hz)).1

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ < 1
⊢ (1 + z).arg ∈ Set.Ioo (-(π / 2)) (π / 2)

Tactic:
rw [Set.mem_Ioo, ← abs_lt, abs_arg_lt_pi_div_two_iff, add_re, one_re, ← neg_lt_iff_pos_add']

Result:
z : ℂ
hz : ‖z‖ < 1
⊢ -1 < z.re ∨ 1 + z = 0
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem iInf_localization_eq_bot [Algebra R K] [hK : IsFractionRing R K] :
    (⨅ v : HeightOneSpectrum R,
        Localization.subalgebra.ofField K _ v.asIdeal.primeCompl_le_nonZeroDivisors) = ⊥

Proof state:
case h.mpr
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ x ∈ ⊥ → ∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯

Tactic:
rw [← MaximalSpectrum.iInf_localization_eq_bot, Algebra.mem_iInf]

Result:
case h.mpr
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) →
    ∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
lemma variableChange_comp (C C' : VariableChange R) (W : WeierstrassCurve R) :
    W.variableChange (C.comp C') = (W.variableChange C').variableChange C

Proof state:
case a₄
R : Type u
inst✝ : CommRing R
C C' : VariableChange R
W : WeierstrassCurve R
⊢ (↑C.u⁻¹ * ↑C'.u⁻¹) ^ 4 *
      (W.a₄ - (↑C'.u * C.s + C'.s) * W.a₃ + 2 * (C.r * ↑C'.u ^ 2 + C'.r) * W.a₂ -
            (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t + (C.r * ↑C'.u ^ 2 + C'.r) * (↑C'.u * C.s + C'.s)) * W.a₁ +
          3 * (C.r * ↑C'.u ^ 2 + C'.r) ^ 2 -
        2 * (↑C'.u * C.s + C'.s) * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t)) =
    ↑C.u⁻¹ ^ 4 *
      (↑C'.u⁻¹ ^ 4 *
                  (W.a₄ - C'.s * W.a₃ + 2 * C'.r * W.a₂ - (C'.t + C'.r * C'.s) * W.a₁ + 3 * C'.r ^ 2 -
                    2 * C'.s * C'.t) -
                C.s * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) +
              2 * C.r * (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2)) -
            (C.t + C.r * C.s) * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) +
          3 * C.r ^ 2 -
        2 * C.s * C.t)

Tactic:
linear_combination
  C.s * (-W.a₃ - C'.r * W.a₁ - C'.t * 2) * C.u⁻¹ ^ 4 * C'.u⁻¹ ^ 3 * C'.u.inv_mul
    + C.u⁻¹ ^ 4 * C'.u⁻¹ ^ 2 * (C.r * C'.r * 6 + C.r * W.a₂ * 2 - C'.s * C.r * W.a₁ * 2
      - C'.s ^ 2 * C.r * 2) * pow_mul_pow_eq_one 2 C'.u.inv_mul
    - C.u⁻¹ ^ 4 * ↑C'.u⁻¹ * (C.s * C'.s * C.r * 2 + C.s * C.r * W.a₁ + C'.s * C.t * 2
      + C.t * W.a₁) * pow_mul_pow_eq_one 3 C'.u.inv_mul
    + C.u⁻¹ ^ 4 * (C.r ^ 2 * 3 - C.s * C.t * 2) * pow_mul_pow_eq_one 4 C'.u.inv_mul

Result:
no goals

Proof state:
case a₁
R : Type u
inst✝ : CommRing R
C C' : VariableChange R
W : WeierstrassCurve R
⊢ ↑C.u⁻¹ * ↑C'.u⁻¹ * (W.a₁ + 2 * (↑C'.u * C.s + C'.s)) = ↑C.u⁻¹ * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s) + 2 * C.s)

Tactic:
linear_combination ↑C.u⁻¹ * C.s * 2 * C'.u.inv_mul

Result:
no goals

Proof state:
case a₂
R : Type u
inst✝ : CommRing R
C C' : VariableChange R
W : WeierstrassCurve R
⊢ (↑C.u⁻¹ * ↑C'.u⁻¹) ^ 2 *
      (W.a₂ - (↑C'.u * C.s + C'.s) * W.a₁ + 3 * (C.r * ↑C'.u ^ 2 + C'.r) - (↑C'.u * C.s + C'.s) ^ 2) =
    ↑C.u⁻¹ ^ 2 *
      (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2) - C.s * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) + 3 * C.r -
        C.s ^ 2)

Tactic:
linear_combination
  C.s * (-C'.s * 2 - W.a₁) * C.u⁻¹ ^ 2 * ↑C'.u⁻¹ * C'.u.inv_mul
    + (C.r * 3 - C.s ^ 2) * C.u⁻¹ ^ 2 * pow_mul_pow_eq_one 2 C'.u.inv_mul

Result:
no goals

Proof state:
case a₃
R : Type u
inst✝ : CommRing R
C C' : VariableChange R
W : WeierstrassCurve R
⊢ (↑C.u⁻¹ * ↑C'.u⁻¹) ^ 3 *
      (W.a₃ + (C.r * ↑C'.u ^ 2 + C'.r) * W.a₁ + 2 * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t)) =
    ↑C.u⁻¹ ^ 3 * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t) + C.r * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) + 2 * C.t)

Tactic:
linear_combination
  C.r * (C'.s * 2 + W.a₁) * C.u⁻¹ ^ 3 * ↑C'.u⁻¹ * pow_mul_pow_eq_one 2 C'.u.inv_mul
    + C.t * 2 * C.u⁻¹ ^ 3 * pow_mul_pow_eq_one 3 C'.u.inv_mul

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
lemma krullDim_nonpos_of_subsingleton [Subsingleton α] : krullDim α ≤ 0

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Subsingleton α
⊢ krullDim α ≤ 0

Tactic:
rw [krullDim_nonpos_iff_forall_isMax]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Subsingleton α
⊢ ∀ (x : α), IsMax x

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Subsingleton α
⊢ ∀ (x : α), IsMax x

Tactic:
exact fun x y h ↦ (Subsingleton.elim x y).ge

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourierBasis_repr (f : Lp ℂ 2 <| @haarAddCircle T hT) (i : ℤ) :
    fourierBasis.repr f i = fourierCoeff f i

Proof state:
case h
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
a✝ : AddCircle T
ht : ↑↑(fourierLp 2 i) a✝ = (fourier i) a✝
⊢ (starRingEnd ℂ) (↑↑(fourierLp 2 i) a✝) * ↑↑f a✝ = (fourier (-i)) a✝ • ↑↑f a✝

Tactic:
rw [ht, ← fourier_neg, smul_eq_mul]

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ↑(fourierBasis.repr f) i = fourierCoeff (↑↑f) i

Tactic:
trans ∫ t : AddCircle T, conj ((@fourierLp T hT 2 _ i : AddCircle T → ℂ) t) * f t ∂haarAddCircle

Result:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ↑(fourierBasis.repr f) i = ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle

T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle = fourierCoeff (↑↑f) i

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle = fourierCoeff (↑↑f) i

Tactic:
apply integral_congr_ae

Result:
case h
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ (fun a => (starRingEnd ℂ) (↑↑(fourierLp 2 i) a) * ↑↑f a) =ᶠ[ae haarAddCircle] fun a => (fourier (-i)) a • ↑↑f a

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ∫ (a : AddCircle T), inner (↑↑(fourierLp 2 i) a) (↑↑f a) ∂haarAddCircle =
    ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle

Tactic:
simp only [RCLike.inner_apply]

Result:
no goals

Proof state:
case h
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ (fun a => (starRingEnd ℂ) (↑↑(fourierLp 2 i) a) * ↑↑f a) =ᶠ[ae haarAddCircle] fun a => (fourier (-i)) a • ↑↑f a

Tactic:
filter_upwards [coeFn_fourierLp 2 i] with _ ht

Result:
case h
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
a✝ : AddCircle T
ht : ↑↑(fourierLp 2 i) a✝ = (fourier i) a✝
⊢ (starRingEnd ℂ) (↑↑(fourierLp 2 i) a✝) * ↑↑f a✝ = (fourier (-i)) a✝ • ↑↑f a✝

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ↑(fourierBasis.repr f) i = ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle

Tactic:
rw [fourierBasis.repr_apply_apply f i, MeasureTheory.L2.inner_def, coe_fourierBasis]

Result:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ∫ (a : AddCircle T), inner (↑↑(fourierLp 2 i) a) (↑↑f a) ∂haarAddCircle =
    ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle
-- Mathlib/NumberTheory/LSeries/Basic.lean
/-- If `f n` is bounded in absolute value by a constant times `n^(x-1)` and `re s > x`,
then the `LSeries` of `f` is summable at `s`. -/
lemma LSeriesSummable_of_le_const_mul_rpow {f : ℕ → ℂ} {x : ℝ} {s : ℂ} (hs : x < s.re)
    (h : ∃ C, ∀ n ≠ 0, ‖f n‖ ≤ C * n ^ (x - 1)) :
    LSeriesSummable f s

Proof state:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
⊢ Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖

Tactic:
simp_rw [div_eq_mul_inv, norm_mul, ← cpow_neg]

Result:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
⊢ Summable fun n => ‖↑C‖ * ‖↑n ^ (-(s + (1 - ↑x)))‖
-- Mathlib/Topology/UrysohnsBounded.lean
theorem exists_bounded_mem_Icc_of_closed_of_le {X : Type*} [TopologicalSpace X] [NormalSpace X]
    {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) {a b : ℝ} (hle : a ≤ b) :
    ∃ f : X →ᵇ ℝ, EqOn f (Function.const X a) s ∧ EqOn f (Function.const X b) t ∧
    ∀ x, f x ∈ Icc a b :=
  let ⟨f, hfs, hft, hf01⟩ := exists_bounded_zero_one_of_closed hs ht hd
  ⟨BoundedContinuousFunction.const X a + (b - a) • f, fun x hx => by simp [hfs hx], fun x hx => by
    simp [hft hx], fun x =>
    ⟨by dsimp; nlinarith [(hf01 x).1], by dsimp; nlinarith [(hf01 x).2]⟩⟩

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
⊢ a + (b - a) * f x ≤ b

Tactic:
nlinarith [(hf01 x).2]

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
⊢ a ≤ (BoundedContinuousFunction.const X a + (b - a) • f) x

Tactic:
dsimp

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
⊢ a ≤ a + (b - a) * f x

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
⊢ (BoundedContinuousFunction.const X a + (b - a) • f) x ≤ b

Tactic:
dsimp

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
⊢ a + (b - a) * f x ≤ b

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
⊢ a ≤ a + (b - a) * f x

Tactic:
nlinarith [(hf01 x).1]

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
hx : x ∈ t
⊢ (BoundedContinuousFunction.const X a + (b - a) • f) x = Function.const X b x

Tactic:
simp [hft hx]

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
hx : x ∈ s
⊢ (BoundedContinuousFunction.const X a + (b - a) • f) x = Function.const X a x

Tactic:
simp [hfs hx]

Result:
no goals
-- Mathlib/Data/List/EditDistance/Defs.lean
theorem List.eq_of_length_one (x : List α) (w : x.length = 1) :
    have : 0 < x.length := lt_of_lt_of_eq Nat.zero_lt_one w.symm
    x = [x[0]]

Proof state:
α : Type u_1
x : List α
w : x.length = 1
⊢ let_fun this := ⋯;
  x = [x[0]]

Tactic:
match x, w with
| [r], _ => rfl

Result:
no goals

Proof state:
α : Type u_1
x : List α
w : x.length = 1
r : α
x✝ : [r].length = 1
⊢ let_fun this := ⋯;
  [r] = [[r][0]]

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.inner_finsupp_eq_zero {v : ι → E} (hv : Orthonormal 𝕜 v) {s : Set ι} {i : ι}
    (hi : i ∉ s) {l : ι →₀ 𝕜} (hl : l ∈ Finsupp.supported 𝕜 𝕜 s) :
    ⟪Finsupp.linearCombination 𝕜 v l, v i⟫ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
s : Set ι
i : ι
hi : i ∉ s
l : ι →₀ 𝕜
hl : l ∈ supported 𝕜 𝕜 s
⊢ inner ((linearCombination 𝕜 v) l) (v i) = 0

Tactic:
rw [Finsupp.mem_supported'] at hl

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
s : Set ι
i : ι
hi : i ∉ s
l : ι →₀ 𝕜
hl : ∀ x ∉ s, l x = 0
⊢ inner ((linearCombination 𝕜 v) l) (v i) = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
s : Set ι
i : ι
hi : i ∉ s
l : ι →₀ 𝕜
hl : ∀ x ∉ s, l x = 0
⊢ inner ((linearCombination 𝕜 v) l) (v i) = 0

Tactic:
simp only [hv.inner_left_finsupp, hl i hi, map_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
theorem posLog_eq_log {x : ℝ} (hx : 1 ≤ |x|) : log⁺ x = log x

Proof state:
x : ℝ
hx : 1 ≤ |x|
⊢ log⁺ x = log x

Tactic:
simp only [posLog, sup_eq_right]

Result:
x : ℝ
hx : 1 ≤ |x|
⊢ 0 ≤ log x

Proof state:
x : ℝ
hx : 1 ≤ |x|
⊢ 0 ≤ log x

Tactic:
rw [← log_abs]

Result:
x : ℝ
hx : 1 ≤ |x|
⊢ 0 ≤ log |x|

Proof state:
x : ℝ
hx : 1 ≤ |x|
⊢ 0 ≤ log |x|

Tactic:
apply log_nonneg hx

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma IsSelfAdjoint.le_algebraMap_norm_self {a : A} (ha : IsSelfAdjoint a

Proof state:
case neg
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
nontriv : ¬Nontrivial A
⊢ a ≤ (algebraMap ℝ A) ‖a‖

Tactic:
rw [not_nontrivial_iff_subsingleton] at nontriv

Result:
case neg
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
nontriv : Subsingleton A
⊢ a ≤ (algebraMap ℝ A) ‖a‖

Proof state:
case pos
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
nontriv : Nontrivial A
r : ℝ
hr : r ∈ spectrum ℝ a
⊢ r ≤ ‖a‖

Tactic:
calc r ≤ ‖r‖ := Real.le_norm_self r
  _ ≤ ‖a‖ := spectrum.norm_le_norm_of_mem hr

Result:
no goals

Proof state:
case neg
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
nontriv : Subsingleton A
⊢ a ≤ (algebraMap ℝ A) ‖a‖

Tactic:
simp

Result:
no goals

Proof state:
case pos
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
nontriv : Nontrivial A
⊢ a ≤ (algebraMap ℝ A) ‖a‖

Tactic:
refine le_algebraMap_of_spectrum_le fun r hr => ?_

Result:
case pos
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
nontriv : Nontrivial A
r : ℝ
hr : r ∈ spectrum ℝ a
⊢ r ≤ ‖a‖

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ a ≤ (algebraMap ℝ A) ‖a‖

Tactic:
by_cases nontriv : Nontrivial A

Result:
case pos
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
nontriv : Nontrivial A
⊢ a ≤ (algebraMap ℝ A) ‖a‖

case neg
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
nontriv : ¬Nontrivial A
⊢ a ≤ (algebraMap ℝ A) ‖a‖
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem mem_comp_comp {V W M : Set (β × β)} (hW' : SymmetricRel W) {p : β × β} :
    p ∈ V ○ M ○ W ↔ (ball p.1 V ×ˢ ball p.2 W ∩ M).Nonempty

Proof state:
case mk.mp
β : Type ub
V W M : Set (β × β)
hW' : SymmetricRel W
x y : β
⊢ (x, y) ∈ V ○ M ○ W → (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty

Tactic:
rintro ⟨z, ⟨w, hpw, hwz⟩, hzy⟩

Result:
case mk.mp.intro.intro.intro.intro
β : Type ub
V W M : Set (β × β)
hW' : SymmetricRel W
x y z : β
hzy : (z, (x, y).2) ∈ W
w : β
hpw : (((x, y).1, z).1, w) ∈ V
hwz : (w, ((x, y).1, z).2) ∈ M
⊢ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty

Proof state:
case mk.mpr
β : Type ub
V W M : Set (β × β)
hW' : SymmetricRel W
x y : β
⊢ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty → (x, y) ∈ V ○ M ○ W

Tactic:
rintro ⟨⟨w, z⟩, ⟨w_in, z_in⟩, hwz⟩

Result:
case mk.mpr.intro.mk.intro.intro
β : Type ub
V W M : Set (β × β)
hW' : SymmetricRel W
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).1 ∈ ball (x, y).1 V
z_in : (w, z).2 ∈ ball (x, y).2 W
⊢ (x, y) ∈ V ○ M ○ W

Proof state:
β : Type ub
V W M : Set (β × β)
hW' : SymmetricRel W
p : β × β
⊢ p ∈ V ○ M ○ W ↔ (ball p.1 V ×ˢ ball p.2 W ∩ M).Nonempty

Tactic:
obtain ⟨x, y⟩ := p

Result:
case mk
β : Type ub
V W M : Set (β × β)
hW' : SymmetricRel W
x y : β
⊢ (x, y) ∈ V ○ M ○ W ↔ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty

Proof state:
case mk.mpr.intro.mk.intro.intro
β : Type ub
V W M : Set (β × β)
hW' : SymmetricRel W
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).1 ∈ ball (x, y).1 V
z_in : (x, y).2 ∈ ball (w, z).2 W
⊢ (x, y) ∈ V ○ M ○ W

Tactic:
exact ⟨z, ⟨w, w_in, hwz⟩, z_in⟩

Result:
no goals

Proof state:
β : Type ub
V W M : Set (β × β)
hW' : SymmetricRel W
x y z : β
hzy : (z, (x, y).2) ∈ W
w : β
hpw : (((x, y).1, z).1, w) ∈ V
hwz : (w, ((x, y).1, z).2) ∈ M
⊢ (w, z).2 ∈ ball (x, y).2 W

Tactic:
rwa [mem_ball_symmetry hW']

Result:
no goals

Proof state:
case mk.mp.intro.intro.intro.intro
β : Type ub
V W M : Set (β × β)
hW' : SymmetricRel W
x y z : β
hzy : (z, (x, y).2) ∈ W
w : β
hpw : (((x, y).1, z).1, w) ∈ V
hwz : (w, ((x, y).1, z).2) ∈ M
⊢ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty

Tactic:
exact ⟨(w, z), ⟨hpw, by rwa [mem_ball_symmetry hW']⟩, hwz⟩

Result:
no goals

Proof state:
case mk.mpr.intro.mk.intro.intro
β : Type ub
V W M : Set (β × β)
hW' : SymmetricRel W
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).1 ∈ ball (x, y).1 V
z_in : (w, z).2 ∈ ball (x, y).2 W
⊢ (x, y) ∈ V ○ M ○ W

Tactic:
rw [mem_ball_symmetry hW'] at z_in

Result:
case mk.mpr.intro.mk.intro.intro
β : Type ub
V W M : Set (β × β)
hW' : SymmetricRel W
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).1 ∈ ball (x, y).1 V
z_in : (x, y).2 ∈ ball (w, z).2 W
⊢ (x, y) ∈ V ○ M ○ W

Proof state:
case mk
β : Type ub
V W M : Set (β × β)
hW' : SymmetricRel W
x y : β
⊢ (x, y) ∈ V ○ M ○ W ↔ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty

Tactic:
constructor

Result:
case mk.mp
β : Type ub
V W M : Set (β × β)
hW' : SymmetricRel W
x y : β
⊢ (x, y) ∈ V ○ M ○ W → (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty

case mk.mpr
β : Type ub
V W M : Set (β × β)
hW' : SymmetricRel W
x y : β
⊢ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty → (x, y) ∈ V ○ M ○ W
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma nnnorm_le_iff_of_nonneg (a : A) (r : ℝ≥0) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
r : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
⊢ ↑‖a‖₊ ≤ ↑r ↔ a ≤ (algebraMap ℝ≥0 A) r

Tactic:
exact norm_le_iff_le_algebraMap a r.2

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
r : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
⊢ ‖a‖₊ ≤ r ↔ a ≤ (algebraMap ℝ≥0 A) r

Tactic:
rw [← NNReal.coe_le_coe]

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
r : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
⊢ ↑‖a‖₊ ≤ ↑r ↔ a ≤ (algebraMap ℝ≥0 A) r