awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : CStarAlgebra A
inst_1 : CStarAlgebra B
inst_2 : FunLike F A B
inst_3 : AlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
h_spec :
  spectrum.{0, u_3} ℝ (A := B) ((StarAlgHom.restrictScalars ℝ (↑φ : A →⋆ₐ[ℂ] B) : (a : A) → B) a : B) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (β := ℝ) (⇑f : (a : ℝ) → ℝ) 0 (spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B))
h_eqOn_x : Set.EqOn (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ) 1 {x}
⊢ cfc (R := ℝ) (p := IsSelfAdjoint) (⇑f : (a : ℝ) → ℝ) ((φ : (a : A) → B) a) =
    cfc (R := ℝ) (p := IsSelfAdjoint) 0 ((φ : (a : A) → B) a)

Tactic:
cfc_congr h_eqOn

Premises used: cfc_congr
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : CStarAlgebra A
inst_1 : CStarAlgebra B
inst_2 : FunLike F A B
inst_3 : AlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
h_spec :
  spectrum.{0, u_3} ℝ (A := B) ((StarAlgHom.restrictScalars ℝ (↑φ : A →⋆ₐ[ℂ] B) : (a : A) → B) a : B) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (β := ℝ) (⇑f : (a : ℝ) → ℝ) 0 (spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B))
h_eqOn_x : Set.EqOn (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ) 1 {x}
⊢ cfc (R := ℝ) (p := IsSelfAdjoint) 0 ((φ : (a : A) → B) a) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : CStarAlgebra A
inst_1 : CStarAlgebra B
inst_2 : FunLike F A B
inst_3 : AlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
h_spec :
  spectrum.{0, u_3} ℝ (A := B) ((StarAlgHom.restrictScalars ℝ (↑φ : A →⋆ₐ[ℂ] B) : (a : A) → B) a : B) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (β := ℝ) (⇑f : (a : ℝ) → ℝ) 0 (spectrum.{0, u_3} ℝ (A := B) ((φ : (a : A) → B) a : B))
h_eqOn_x : Set.EqOn (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ) 1 {x}
calc : cfc (R := ℝ) (p := IsSelfAdjoint) 0 ((φ : (a : A) → B) a) = 0
⊢ Eq.{u_3 + 1} (α := B) ((φ : (a : A) → B) (cfc (R := ℝ) (p := IsSelfAdjoint) (⇑f : (a : ℝ) → ℝ) a) : B) (0 : B)

Tactic:
calc φ (cfc f a) = cfc f (φ a) := StarAlgHomClass.map_cfc φ f a
    _ = cfc (0 : ℝ → ℝ) (φ a) := cfc_congr h_eqOn
    _ = 0 := by simp

Premises used: cfc, cfc_congr, OfNat.ofNat, DFunLike.coe, StarAlgHomClass.map_cfc
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a : A
this :
  ∀ {ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)},
    Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
        (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B) →
      ∀ (a : Unitization ℂ A),
        norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) a : Unitization ℂ B) = ‖a‖
⊢ norm.{u_3} (E := B) ((φ : (a : A) → B) a : B) = ‖a‖

Tactic:
simpa [norm_inr] using this (starMap_injective (φ := (φ : A →⋆ₙₐ[ℂ] B)) hφ) a

Premises used: Unitization.starMap_injective, Unitization.inr, Unitization.norm_inr
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a : A
suffices :
  ∀ {ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)},
    Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
        (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B) →
      ∀ (a : Unitization ℂ A),
        norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) a : Unitization ℂ B) = ‖a‖
⊢ norm.{u_3} (E := B) ((φ : (a : A) → B) a : B) = ‖a‖

Tactic:
suffices ∀ {ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B} (_ : Function.Injective ψ)
      (a : Unitization ℂ A), ‖ψ a‖ = ‖a‖ by
    simpa [norm_inr] using this (starMap_injective (φ := (φ : A →⋆ₙₐ[ℂ] B)) hφ) a
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a_1 : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
hψ :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
    (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B)
a : Unitization ℂ A
⊢ 0 ≤ norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) a : Unitization ℂ B)

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a_1 : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
hψ :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
    (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B)
a : Unitization ℂ A
⊢ 0 ≤ ‖a‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a_1 : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
hψ :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
    (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B)
a : Unitization ℂ A
rw :
  HPow.hPow (β := ℕ)
      (norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) a : Unitization ℂ B)) 2 =
    HPow.hPow (β := ℕ) ‖a‖ 2
⊢ norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) a : Unitization ℂ B) = ‖a‖

Tactic:
rw [← sq_eq_sq₀ (by positivity) (by positivity)]

Premises used: sq_eq_sq₀
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a_1 : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
hψ :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
    (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B)
a : Unitization ℂ A
simp :
  norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) (star a * a) : Unitization ℂ B) =
    ‖star a * a‖
⊢ HPow.hPow (β := ℕ)
      (norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) a : Unitization ℂ B)) 2 =
    HPow.hPow (β := ℕ) ‖a‖ 2

Tactic:
simp only [sq, ← CStarRing.norm_star_mul_self, ← map_star, ← map_mul]

Premises used: StarHomClass.map_star, sq, CStarRing.norm_star_mul_self, map_mul
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a_1 : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
hψ :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
    (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B)
a : Unitization ℂ A
⊢ IsSelfAdjoint (star a * a)

Tactic:
have ha : IsSelfAdjoint (star a * a) := .star_mul_self a
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a_1 : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
hψ :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
    (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B)
a : Unitization ℂ A
ha : IsSelfAdjoint (star a * a)
⊢ norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) (star a * a) : Unitization ℂ B) =
    (spectralRadius.{0, u_3} ℝ (A := Unitization ℂ B)
        ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) (star a * a) : Unitization ℂ B)).toReal

Tactic:
ha.map ψ |>.toReal_spectralRadius_eq_norm.symm

Premises used: Unitization.inl, IsSelfAdjoint.map, IsSelfAdjoint.toReal_spectralRadius_eq_norm, Eq.symm, Unitization.inlRingHom
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a_1 : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
hψ :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
    (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B)
a : Unitization ℂ A
ha : IsSelfAdjoint (star a * a)
⊢ (spectralRadius.{0, u_3} ℝ (A := Unitization ℂ B)
        ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) (star a * a) : Unitization ℂ B)).toReal =
    (spectralRadius ℝ (star a * a)).toReal

Tactic:
simp only [spectralRadius, ha.map_spectrum_real ψ hψ]

Premises used: spectralRadius, IsSelfAdjoint.map_spectrum_real
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a_1 : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
hψ :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
    (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B)
a : Unitization ℂ A
ha : IsSelfAdjoint (star a * a)
⊢ (spectralRadius ℝ (star a * a)).toReal = ‖star a * a‖

Tactic:
ha.toReal_spectralRadius_eq_norm

Premises used: Unitization.inl, IsSelfAdjoint.toReal_spectralRadius_eq_norm, Unitization.inlRingHom
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a_1 : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
hψ :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := Unitization ℂ A) (β := Unitization ℂ B)
    (⇑ψ : (a : Unitization ℂ A) → Unitization ℂ B)
a : Unitization ℂ A
ha : IsSelfAdjoint (star a * a)
calc :
  (spectralRadius.{0, u_3} ℝ (A := Unitization ℂ B)
        ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) (star a * a) : Unitization ℂ B)).toReal =
    (spectralRadius ℝ (star a * a)).toReal
⊢ norm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) (star a * a) : Unitization ℂ B) =
    ‖star a * a‖

Tactic:
calc ‖ψ (star a * a)‖ = (spectralRadius ℝ (ψ (star a * a))).toReal :=
      ha.map ψ |>.toReal_spectralRadius_eq_norm.symm
    _ = (spectralRadius ℝ (star a * a)).toReal := by
      simp only [spectralRadius, ha.map_spectrum_real ψ hψ]
    _ = ‖star a * a‖ := ha.toReal_spectralRadius_eq_norm

Premises used: Real, HMul.hMul, IsSelfAdjoint.map, spectralRadius, ENNReal.toReal, IsSelfAdjoint.toReal_spectralRadius_eq_norm, Eq.symm, DFunLike.coe, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
a : A
⊢ nnnorm.{u_3} (E := B) ((φ : (a : A) → B) a : B) = ‖a‖₊

Tactic:
Subtype.ext <| norm_map φ hφ a

Premises used: NNReal, NonUnitalStarAlgHom.norm_map, Subtype.ext
-- Module: Mathlib.Analysis.CStarAlgebra.Hom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
⊢ Isometry.{u_2, u_3} (α := A) (β := B) (⇑φ : (a : A) → B)

Tactic:
AddMonoidHomClass.isometry_of_norm φ (norm_map φ hφ)

Premises used: AddMonoidHomClass.isometry_of_norm, NonUnitalStarAlgHom.norm_map
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
hf : HasLineDerivWithinAt 𝕜 f f' s x v
hst : t ⊆ s
⊢ HasLineDerivWithinAt 𝕜 f f' t x v

Tactic:
HasDerivWithinAt.mono hf (preimage_mono hst)

Premises used: HasLineDerivWithinAt, Set.preimage_mono, HasDerivWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
f' : F
x v : E
hf : HasLineDerivAt 𝕜 f f' x v
s : Set E
⊢ HasLineDerivWithinAt 𝕜 f f' s x v

Tactic:
HasDerivAt.hasDerivWithinAt hf

Premises used: HasDerivAt.hasDerivWithinAt, HasLineDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
f' : F
s : Set E
x v : E
hf : HasLineDerivWithinAt 𝕜 f f' s x v
⊢ LineDifferentiableWithinAt 𝕜 f s x v

Tactic:
HasDerivWithinAt.differentiableWithinAt hf

Premises used: HasDerivWithinAt.differentiableWithinAt, LineDifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
f' : F
x v : E
hf : HasLineDerivAt 𝕜 f f' x v
⊢ LineDifferentiableAt 𝕜 f x v

Tactic:
HasDerivAt.differentiableAt hf

Premises used: LineDifferentiableAt, HasDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
h : LineDifferentiableWithinAt 𝕜 f s x v
⊢ HasLineDerivWithinAt 𝕜 f (lineDerivWithin 𝕜 f s x v) s x v

Tactic:
DifferentiableWithinAt.hasDerivWithinAt h

Premises used: HasLineDerivWithinAt, DifferentiableWithinAt.hasDerivWithinAt, lineDerivWithin
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
h : LineDifferentiableAt 𝕜 f x v
⊢ HasLineDerivAt 𝕜 f (lineDeriv 𝕜 f x v) x v

Tactic:
DifferentiableAt.hasDerivAt h

Premises used: DifferentiableAt.hasDerivAt, HasLineDerivAt, lineDeriv
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
f' : F
x v : E
⊢ HasLineDerivWithinAt 𝕜 f f' univ x v ↔ HasLineDerivAt 𝕜 f f' x v

Tactic:
simp only [HasLineDerivWithinAt, HasLineDerivAt, preimage_univ, hasDerivWithinAt_univ]

Premises used: HasLineDerivWithinAt, hasDerivWithinAt_univ, Set.preimage_univ, HasLineDerivAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
h : ¬LineDifferentiableWithinAt 𝕜 f s x v
⊢ lineDerivWithin 𝕜 f s x v = 0

Tactic:
derivWithin_zero_of_not_differentiableWithinAt h

Premises used: lineDerivWithin, derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
h : ¬LineDifferentiableAt 𝕜 f x v
⊢ lineDeriv 𝕜 f x v = 0

Tactic:
deriv_zero_of_not_differentiableAt h

Premises used: deriv_zero_of_not_differentiableAt, lineDeriv
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
f' : F
x v : E
⊢ HasLineDerivAt 𝕜 f f' x v ↔
    IsLittleO.{u_1, u_2, u_1} (E := F) (F := 𝕜) (𝓝 0) (fun (t : 𝕜) ↦ f (x + t • v) - f x - t • f') fun (t : 𝕜) ↦ t

Tactic:
simp only [HasLineDerivAt, hasDerivAt_iff_isLittleO_nhds_zero, zero_add, zero_smul, add_zero]

Premises used: zero_add, zero_smul, hasDerivAt_iff_isLittleO_nhds_zero, HasLineDerivAt, add_zero
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
f₀' f₁' : F
x v : E
h₀ : HasLineDerivAt 𝕜 f f₀' x v
h₁ : HasLineDerivAt 𝕜 f f₁' x v
⊢ f₀' = f₁'

Tactic:
HasDerivAt.unique h₀ h₁

Premises used: HasDerivAt.unique
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
f' : F
x v : E
h : HasLineDerivAt 𝕜 f f' x v
rw rw₁ : lineDeriv 𝕜 f x v = lineDeriv 𝕜 f x v
⊢ lineDeriv 𝕜 f x v = f'

Tactic:
rw [h.unique h.lineDifferentiableAt.hasLineDerivAt]

Premises used: HasLineDerivAt.lineDifferentiableAt, HasLineDerivAt.unique, LineDifferentiableAt.hasLineDerivAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
⊢ LineDifferentiableWithinAt 𝕜 f univ x v ↔ LineDifferentiableAt 𝕜 f x v

Tactic:
simp only [LineDifferentiableWithinAt, LineDifferentiableAt, preimage_univ,
    differentiableWithinAt_univ]

Premises used: LineDifferentiableAt, LineDifferentiableWithinAt, Set.preimage_univ, differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
h : LineDifferentiableAt 𝕜 f x v
⊢ LineDifferentiableWithinAt 𝕜 f s x v

Tactic:
(differentiableWithinAt_univ.2 h).mono (subset_univ _)

Premises used: Iff.mpr, Set.subset_univ, LineDifferentiableWithinAt, DifferentiableWithinAt.mono, differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
⊢ lineDerivWithin 𝕜 f univ x v = lineDeriv 𝕜 f x v

Tactic:
simp [lineDerivWithin, lineDeriv]

Premises used: lineDerivWithin, lineDeriv
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s t : Set E
x v : E
h : LineDifferentiableWithinAt 𝕜 f t x v
st : s ⊆ t
⊢ LineDifferentiableWithinAt 𝕜 f s x v

Tactic:
(h.hasLineDerivWithinAt.mono st).lineDifferentiableWithinAt

Premises used: LineDifferentiableWithinAt.hasLineDerivWithinAt, HasLineDerivWithinAt.mono, HasLineDerivWithinAt.lineDifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f f₁ : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' s x v
ht : EqOn f₁ f t
hx : f₁ x = f x
h₁ : t ⊆ s
⊢ f₁ (x + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v) = f (x + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f f₁ : E → F
f' : F
s : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' s x v
hs : EqOn f₁ f s
hx : f₁ x = f x
⊢ HasLineDerivWithinAt 𝕜 f₁ f' s x v

Tactic:
h.congr_mono hs hx (Subset.refl _)

Premises used: Set.Subset.refl, HasLineDerivWithinAt.congr_mono
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f f₁ : E → F
f' : F
s : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' s x v
hs : EqOn f₁ f s
hx : x ∈ s
⊢ HasLineDerivWithinAt 𝕜 f₁ f' s x v

Tactic:
h.congr hs (hs hx)

Premises used: HasLineDerivWithinAt.congr
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f f₁ : E → F
s t : Set E
x v : E
h : LineDifferentiableWithinAt 𝕜 f s x v
ht : EqOn f₁ f t
hx : f₁ x = f x
h₁ : t ⊆ s
⊢ LineDifferentiableWithinAt 𝕜 f₁ t x v

Tactic:
(HasLineDerivWithinAt.congr_mono h.hasLineDerivWithinAt ht hx h₁).differentiableWithinAt

Premises used: LineDifferentiableWithinAt.hasLineDerivWithinAt, HasDerivWithinAt.differentiableWithinAt, LineDifferentiableWithinAt, HasLineDerivWithinAt.congr_mono
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f f₁ : E → F
s : Set E
x v : E
h : LineDifferentiableWithinAt 𝕜 f s x v
ht : ∀ x ∈ s, f₁ x = f x
hx : f₁ x = f x
⊢ LineDifferentiableWithinAt 𝕜 f₁ s x v

Tactic:
LineDifferentiableWithinAt.congr_mono h ht hx (Subset.refl _)

Premises used: Set.Subset.refl, LineDifferentiableWithinAt.congr_mono