awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
hr : ¬(spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
neg :
  r ∉
    Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
⊢ 0 =
    Multiset.count r
      (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
        (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))

Tactic:
rw [Multiset.count_eq_zero_of_notMem]

Premises used: Multiset.count_eq_zero_of_notMem
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
hr : ¬(spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
hr_mem :
  Membership.mem (γ := Multiset ℝ)
    (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
    r
neg :
  ∀ (e : E)
    (he :
      Membership.mem (γ := Multiset E)
        (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))) e)
    (her : (spectralMulAlgNorm K E : (a : E) → ℝ) e = r), False
⊢ False

Tactic:
obtain ⟨e, he, her⟩ := Multiset.mem_map.mp hr_mem

Premises used: Multiset.mem_map, Iff.mp
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
hr : ¬(spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
hr_mem :
  Membership.mem (γ := Multiset ℝ)
    (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
    r
e : E
he :
  Membership.mem (γ := Multiset E)
    (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))) e
her : (spectralMulAlgNorm K E : (a : E) → ℝ) e = r
⊢ (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r

Tactic:
rw [spectralMulAlgNorm_eq_of_mem_roots K L x he] at her

Premises used: spectralNorm.spectralMulAlgNorm_eq_of_mem_roots
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
hr : ¬(spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
hr_mem :
  Membership.mem (γ := Multiset ℝ)
    (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
    r
e : E
he :
  Membership.mem (γ := Multiset E)
    (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))) e
her : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
⊢ False

Tactic:
hr her
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
hr : ¬(spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
hr_mem :
  Membership.mem (γ := Multiset ℝ)
    (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
    r
e : E
he :
  Membership.mem (γ := Multiset E)
    (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))) e
her : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
⊢ False

Tactic:
exact hr her
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x : L
E : Type v := SplittingField (K := L) (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
⊢ Splits.{v} (R := E) (((mapAlg K E : AlgHom.{u, u, v} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))

Tactic:
have hspl : Splits (mapAlg K E (minpoly K x)) :=
    IsSplittingField.IsScalarTower.splits (K := L) E (minpoly K x)
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x : L
E : Type v := SplittingField (K := L) (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
hspl : Splits.{v} (R := E) (((mapAlg K E : AlgHom.{u, u, v} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
⊢ Algebra.IsAlgebraic L E

Tactic:
have : Algebra.IsAlgebraic L E :=
    IsSplittingField.IsScalarTower.isAlgebraic E (mapAlg K L (minpoly K x))
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x : L
E : Type v := SplittingField (K := L) (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
hspl : Splits.{v} (R := E) (((mapAlg K E : AlgHom.{u, u, v} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
this : Algebra.IsAlgebraic L E
⊢ Algebra.IsAlgebraic K E

Tactic:
have : Algebra.IsAlgebraic K E := Algebra.IsAlgebraic.trans K L E
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x : L
E : Type v := SplittingField (K := L) (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
hspl : Splits.{v} (R := E) (((mapAlg K E : AlgHom.{u, u, v} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
this_1 : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
rw : Monic.{v} (R := E) (((mapAlg K E : AlgHom.{u, u, v} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
rw₁ : Ne (α := ℝ) (↑(natDegree (minpoly K x)) : ℝ) 0
⊢ spectralNorm K L x = ‖coeff (minpoly K x) 0‖ ^ HDiv.hDiv (α := ℝ) 1 (↑(natDegree (minpoly K x)) : ℝ)

Tactic:
rw [one_div, Real.eq_rpow_inv (spectralNorm_nonneg x) (norm_nonneg ((minpoly K x).coeff 0)),
    Real.rpow_natCast, @spectralNorm.eq_of_tower K _ E,
    ← @spectralNorm_extends K _ L _ _ ((minpoly K x).coeff 0),
    @spectralNorm.eq_of_tower K _ E _ _ L, ← spectralMulAlgNorm_def,
    ← spectralMulAlgNorm_def, Polynomial.coeff_zero_of_isScalarTower,
    hspl.coeff_zero_eq_prod_roots_of_monic _, map_mul, map_pow,
    map_neg_eq_map, map_one, one_pow, one_mul, spectralNorm_pow_natDegree_eq_prod_roots _ _ x]

Premises used: one_pow, Polynomial.coeff_zero_of_isScalarTower, Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic, spectralMulAlgNorm_def, spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots, AddGroupSeminormClass.map_neg_eq_map, map_pow, minpoly, Polynomial.coeff, spectralNorm_nonneg, map_mul, spectralNorm_extends, map_one, one_div, spectralNorm.eq_of_tower, OfNat.ofNat, norm_nonneg, one_mul, Real.rpow_natCast, Real.eq_rpow_inv
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x : L
E : Type v := SplittingField (K := L) (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
hspl : Splits.{v} (R := E) (((mapAlg K E : AlgHom.{u, u, v} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
this_1 : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ Monic.{v} (R := E) (((mapAlg K E : AlgHom.{u, u, v} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))

Tactic:
simp [monic_mapAlg_iff, minpoly.monic (Algebra.IsAlgebraic.isAlgebraic x).isIntegral]

Premises used: Algebra.IsAlgebraic.isAlgebraic, minpoly.monic, Polynomial.monic_mapAlg_iff, IsAlgebraic.isIntegral
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x : L
E : Type v := SplittingField (K := L) (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
hspl : Splits.{v} (R := E) (((mapAlg K E : AlgHom.{u, u, v} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
this_1 : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ Ne (α := ℝ) (↑(natDegree (minpoly K x)) : ℝ) 0

Tactic:
exact_mod_cast (minpoly.natDegree_pos (Algebra.IsIntegral.isIntegral x)).ne'

Premises used: Algebra.IsIntegral.isIntegral, LT.lt.ne', minpoly.natDegree_pos
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
h : IsIntegralCurve γ v
s : Set ℝ
⊢ IsIntegralCurveOn γ v s

Tactic:
fun t _ ↦ (h t).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, IsIntegralCurveOn
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
⊢ IsIntegralCurveOn γ v univ ↔ IsIntegralCurve γ v

Tactic:
⟨fun h t ↦ (h t (mem_univ _)).hasDerivAt Filter.univ_mem, fun h ↦ h.isIntegralCurveOn _⟩

Premises used: Set.univ, IsIntegralCurve.isIntegralCurveOn, HasDerivWithinAt.hasDerivAt, Iff.intro, Set.mem_univ, Filter.univ_mem
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
rw : (∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y) ↔ ∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s
⊢ IsIntegralCurveAt γ v t₀ ↔ ∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s

Tactic:
rw [IsIntegralCurveAt, Filter.eventually_iff_exists_mem]

Premises used: IsIntegralCurveAt, Filter.eventually_iff_exists_mem
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
⊢ (∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y) ↔ ∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s

Tactic:
⟨fun ⟨s, hs, h⟩ ↦ ⟨s, hs, fun t ht ↦ (h t ht).hasDerivWithinAt⟩, ?_⟩

Premises used: HasDerivAt.hasDerivWithinAt, Membership.mem, Exists, nhds, And, IsIntegralCurveOn, And.intro, Iff.intro, Exists.intro, _private.0.isIntegralCurveAt_iff_exists_mem_nhds.match_2
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
refine : (∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s) → ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y
⊢ (∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y) ↔ ∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s

Tactic:
refine ⟨fun ⟨s, hs, h⟩ ↦ ⟨s, hs, fun t ht ↦ (h t ht).hasDerivWithinAt⟩, ?_⟩
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsIntegralCurveOn γ v s
⊢ ∃ t ⊆ s, IsOpen t ∧ t₀ ∈ t

Tactic:
rw [mem_nhds_iff] at hs

Premises used: mem_nhds_iff
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsIntegralCurveOn γ v s
hs₁ : ∃ t ⊆ s, IsOpen t ∧ t₀ ∈ t
⊢ IsIntegralCurveOn γ v s

Tactic:
rw [mem_nhds_iff] at hs

Premises used: mem_nhds_iff
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
hs : ∃ t ⊆ s, IsOpen t ∧ t₀ ∈ t
h : IsIntegralCurveOn γ v s
obtain :
  ∀ (s' : Set ℝ) (h₁ : s' ⊆ s) (h₂ : IsOpen s') (h₃ : t₀ ∈ s'), ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y
⊢ ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y

Tactic:
obtain ⟨s', h₁, h₂, h₃⟩ := hs
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
h : IsIntegralCurveOn γ v s
s' : Set ℝ
h₁ : s' ⊆ s
h₂ : IsOpen s'
h₃ : t₀ ∈ s'
⊢ ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y

Tactic:
⟨s', h₂.mem_nhds h₃, ?_⟩

Premises used: And.intro, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
h : IsIntegralCurveOn γ v s
s' : Set ℝ
h₁ : s' ⊆ s
h₂ : IsOpen s'
h₃ : t₀ ∈ s'
refine : ∀ y ∈ s', HasDerivAt γ (v y (γ y)) y
⊢ ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y

Tactic:
refine ⟨s', h₂.mem_nhds h₃, ?_⟩
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
h : IsIntegralCurveOn γ v s
s' : Set ℝ
h₁ : s' ⊆ s
h₂ : IsOpen s'
h₃ : t₀ ∈ s'
t : ℝ
ht : t ∈ s'
apply : s ∈ 𝓝 t
⊢ HasDerivAt γ (v t (γ t)) t

Tactic:
apply (h t (h₁ ht)).hasDerivAt

Premises used: HasDerivWithinAt.hasDerivAt
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
h : IsIntegralCurveOn γ v s
s' : Set ℝ
h₁ : s' ⊆ s
h₂ : IsOpen s'
h₃ : t₀ ∈ s'
t : ℝ
ht : t ∈ s'
rw : ∃ t_1 ⊆ s, IsOpen t_1 ∧ t ∈ t_1
⊢ s ∈ 𝓝 t

Tactic:
rw [mem_nhds_iff]

Premises used: mem_nhds_iff
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
h : IsIntegralCurveOn γ v s
s' : Set ℝ
h₁ : s' ⊆ s
h₂ : IsOpen s'
h₃ : t₀ ∈ s'
t : ℝ
ht : t ∈ s'
⊢ ∃ t_1 ⊆ s, IsOpen t_1 ∧ t ∈ t_1

Tactic:
⟨s', h₁, h₂, ht⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
h : IsIntegralCurveOn γ v s
s' : Set ℝ
h₁ : s' ⊆ s
h₂ : IsOpen s'
h₃ : t₀ ∈ s'
t : ℝ
ht : t ∈ s'
⊢ ∃ t_1 ⊆ s, IsOpen t_1 ∧ t ∈ t_1

Tactic:
exact ⟨s', h₁, h₂, ht⟩
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
rw : (∃ ε > 0, ∀ y ∈ Metric.ball t₀ ε, HasDerivAt γ (v y (γ y)) y) ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ IsIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
rw [IsIntegralCurveAt, Metric.eventually_nhds_iff_ball]

Premises used: IsIntegralCurveAt, Metric.eventually_nhds_iff_ball
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
a :
  ∀ (ε y : ℝ) (hy : y ∈ Metric.ball t₀ ε),
    HasDerivAt γ (v y (γ y)) y ↔ HasDerivWithinAt γ (v y (γ y)) (Metric.ball t₀ ε) y
⊢ (∃ ε > 0, ∀ y ∈ Metric.ball t₀ ε, HasDerivAt γ (v y (γ y)) y) ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
congrm ∃ ε > 0, ∀ (y : ℝ) (hy : y ∈ Metric.ball t₀ ε), ?_
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ ε y : ℝ
hy : y ∈ Metric.ball t₀ ε
⊢ HasDerivAt γ (v y (γ y)) y ↔ HasDerivWithinAt γ (v y (γ y)) (Metric.ball t₀ ε) y

Tactic:
⟨HasDerivAt.hasDerivWithinAt, fun h ↦ h.hasDerivAt (Metric.isOpen_ball.mem_nhds hy)⟩

Premises used: HasDerivAt.hasDerivWithinAt, Metric.isOpen_ball, IsOpen.mem_nhds, HasDerivWithinAt.hasDerivAt, Iff.intro
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ ε y : ℝ
hy : y ∈ Metric.ball t₀ ε
⊢ HasDerivAt γ (v y (γ y)) y ↔ HasDerivWithinAt γ (v y (γ y)) (Metric.ball t₀ ε) y

Tactic:
exact ⟨HasDerivAt.hasDerivWithinAt, fun h ↦ h.hasDerivAt (Metric.isOpen_ball.mem_nhds hy)⟩
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
h : IsIntegralCurve γ v
t : ℝ
⊢ IsIntegralCurveAt γ v t

Tactic:
isIntegralCurveAt_iff_exists_mem_nhds.mpr
    ⟨univ, Filter.univ_mem, fun t _ ↦ (h t).hasDerivWithinAt⟩

Premises used: Iff.mpr, HasDerivAt.hasDerivWithinAt, Set.univ, isIntegralCurveAt_iff_exists_mem_nhds, And.intro, Exists.intro, Filter.univ_mem
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
h : ∀ (t : ℝ), IsIntegralCurveAt γ v t
t : ℝ
obtain : ∀ (s : Set ℝ) (hs : s ∈ 𝓝 t) (h : IsIntegralCurveOn γ v s), HasDerivAt γ (v t (γ t)) t
⊢ HasDerivAt γ (v t (γ t)) t

Tactic:
obtain ⟨s, hs, h⟩ := isIntegralCurveAt_iff_exists_mem_nhds.mp (h t)

Premises used: isIntegralCurveAt_iff_exists_mem_nhds, Iff.mp
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
h_1 : ∀ (t : ℝ), IsIntegralCurveAt γ v t
t : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t
h : IsIntegralCurveOn γ v s
⊢ HasDerivAt γ (v t (γ t)) t

Tactic:
h t (mem_of_mem_nhds hs) |>.hasDerivAt hs

Premises used: mem_of_mem_nhds, HasDerivWithinAt.hasDerivAt
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
h_1 : ∀ (t : ℝ), IsIntegralCurveAt γ v t
t : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t
h : IsIntegralCurveOn γ v s
⊢ HasDerivAt γ (v t (γ t)) t

Tactic:
exact h t (mem_of_mem_nhds hs) |>.hasDerivAt hs

Premises used: mem_of_mem_nhds, HasDerivWithinAt.hasDerivAt
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s s' : Set ℝ
h : IsIntegralCurveOn γ v s
hs : s' ⊆ s
⊢ IsIntegralCurveOn γ v s'

Tactic:
fun t ht ↦ h t (hs ht) |>.mono hs

Premises used: IsIntegralCurveOn, HasDerivWithinAt.mono
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
h : IsIntegralCurveAt γ v t₀
⊢ HasDerivAt γ (v t₀ (γ t₀)) t₀

Tactic:
have ⟨_, hs, h⟩ := isIntegralCurveAt_iff_exists_mem_nhds.mp h
  h t₀ (mem_of_mem_nhds hs) |>.hasDerivAt hs

Premises used: HasDerivAt, _private.0.IsIntegralCurveAt.hasDerivAt.match_1, mem_of_mem_nhds, isIntegralCurveAt_iff_exists_mem_nhds, HasDerivWithinAt.hasDerivAt, Iff.mp
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
t₀ : ℝ
h : IsIntegralCurveOn γ v s
hs : s ∈ 𝓝 t₀
⊢ IsIntegralCurveAt γ v t₀

Tactic:
isIntegralCurveAt_iff_exists_mem_nhds.mpr ⟨s, hs, h⟩

Premises used: Iff.mpr, isIntegralCurveAt_iff_exists_mem_nhds, And.intro, Exists.intro
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
h : ∀ t ∈ s, IsIntegralCurveAt γ v t
t : ℝ
ht : t ∈ s
obtain : ∀ (s' : Set ℝ) (hs' : s' ∈ 𝓝 t) (h : ∀ y ∈ s', HasDerivAt γ (v y (γ y)) y), HasDerivWithinAt γ (v t (γ t)) s t
⊢ HasDerivWithinAt γ (v t (γ t)) s t

Tactic:
obtain ⟨s', hs', h⟩ := Filter.eventually_iff_exists_mem.mp (h t ht)

Premises used: Iff.mp, Filter.eventually_iff_exists_mem
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
h_1 : ∀ t ∈ s, IsIntegralCurveAt γ v t
t : ℝ
ht : t ∈ s
s' : Set ℝ
hs' : s' ∈ 𝓝 t
h : ∀ y ∈ s', HasDerivAt γ (v y (γ y)) y
⊢ HasDerivWithinAt γ (v t (γ t)) s t

Tactic:
h _ (mem_of_mem_nhds hs') |>.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, mem_of_mem_nhds
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
h_1 : ∀ t ∈ s, IsIntegralCurveAt γ v t
t : ℝ
ht : t ∈ s
s' : Set ℝ
hs' : s' ∈ 𝓝 t
h : ∀ y ∈ s', HasDerivAt γ (v y (γ y)) y
⊢ HasDerivWithinAt γ (v t (γ t)) s t

Tactic:
exact h _ (mem_of_mem_nhds hs') |>.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, mem_of_mem_nhds
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hs : IsOpen s
⊢ IsIntegralCurveOn γ v s ↔ ∀ t ∈ s, IsIntegralCurveAt γ v t

Tactic:
⟨fun h _ ht ↦ h.isIntegralCurveAt (hs.mem_nhds ht), IsIntegralCurveAt.isIntegralCurveOn⟩

Premises used: IsIntegralCurveAt.isIntegralCurveOn, IsIntegralCurveOn.isIntegralCurveAt, IsOpen.mem_nhds, Iff.intro
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
t₀ : ℝ
hγ : IsIntegralCurveOn γ v s
ht : t₀ ∈ s
⊢ ContinuousWithinAt γ s t₀

Tactic:
(hγ t₀ ht).continuousWithinAt

Premises used: HasDerivWithinAt.continuousWithinAt
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
⊢ ContinuousOn γ s

Tactic:
(hγ · · |>.continuousWithinAt)

Premises used: ContinuousOn, HasDerivWithinAt.continuousWithinAt
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
hγ : IsIntegralCurveAt γ v t₀
⊢ ContinuousAt γ t₀

Tactic:
have ⟨_, hs, hγ⟩ := isIntegralCurveAt_iff_exists_mem_nhds.mp hγ
  hγ.continuousWithinAt (mem_of_mem_nhds hs) |>.continuousAt hs

Premises used: ContinuousAt, _private.0.IsIntegralCurveAt.hasDerivAt.match_1, mem_of_mem_nhds, isIntegralCurveAt_iff_exists_mem_nhds, Iff.mp, ContinuousWithinAt.continuousAt, IsIntegralCurveOn.continuousWithinAt