awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q : M
⊢ HasMFDerivWithinAt I I (M' := M ⊕ M') Sum.inl s q (ContinuousLinearMap.id 𝕜 (TangentSpace I q))
have refine : HasFDerivWithinAt (writtenInExtChartAt (M' := M ⊕ M') I I q Sum.inl) (ContinuousLinearMap.id 𝕜 (TangentSpace I q))
  ((↑(extChartAt I q).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I q) : M → E) q)
Tactic: refine ⟨by fun_prop, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q : M
⊢ HasFDerivWithinAt (writtenInExtChartAt (M' := M ⊕ M') I I q Sum.inl) (ContinuousLinearMap.id 𝕜 (TangentSpace I q))
    ((↑(extChartAt I q).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I q) : M → E) q)
have this : writtenInExtChartAt (M' := M ⊕ M') I I q
    Sum.inl =ᶠ[𝓝[(↑(extChartAt I q).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I q) : M → E) q]
  id
Tactic: have : (writtenInExtChartAt I I q (@Sum.inl M M'))
      =ᶠ[𝓝[(extChartAt I q).symm ⁻¹' s ∩ Set.range I] (extChartAt I q q)] id :=
    writtenInExtChartAt_sumInl_eventuallyEq_id.filter_mono (nhdsWithin_mono _ (fun _y hy ↦ hy.2))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
t : Set M'
⊢ HasMFDerivWithinAt I I (M' := M ⊕ M') Sum.inr t q' (ContinuousLinearMap.id 𝕜 (TangentSpace I q'))
have refine : HasFDerivWithinAt (writtenInExtChartAt (M' := M ⊕ M') I I q' Sum.inr) (ContinuousLinearMap.id 𝕜 (TangentSpace I q'))
  ((↑(extChartAt I q').symm : E → M') ⁻¹' t ∩ range (↑I : H → E)) ((↑(extChartAt I q') : M' → E) q')
Tactic: refine ⟨by fun_prop, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
t : Set M'
⊢ HasFDerivWithinAt (writtenInExtChartAt (M' := M ⊕ M') I I q' Sum.inr) (ContinuousLinearMap.id 𝕜 (TangentSpace I q'))
    ((↑(extChartAt I q').symm : E → M') ⁻¹' t ∩ range (↑I : H → E)) ((↑(extChartAt I q') : M' → E) q')
have this : writtenInExtChartAt (M' := M ⊕ M') I I q'
    Sum.inr =ᶠ[𝓝[(↑(extChartAt I q').symm : E → M') ⁻¹' t ∩ range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q']
  id
Tactic: have : (writtenInExtChartAt I I q' (@Sum.inr M M'))
      =ᶠ[𝓝[(extChartAt I q').symm ⁻¹' t ∩ Set.range I] (extChartAt I q' q')] id :=
    writtenInExtChartAt_sumInr_eventuallyEq_id.filter_mono (nhdsWithin_mono _ (fun _y hy ↦ hy.2))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
z : M
ι : Type
t : Finset ι
f : ι → M → E'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ t, f i) s z (∑ i ∈ t, f' i)
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)),
  HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ ∅, f i) s z (∑ i ∈ ∅, f' i)
Tactic: induction t using Finset.induction_on with
  | empty => simpa using hasMFDerivWithinAt_const ..
  | insert i s hi IH => grind [HasMFDerivWithinAt.add]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
z : M
ι : Type
t : Finset ι
f : ι → M → E'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ ∅, f i) s z (∑ i ∈ ∅, f' i)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ t, f i) s z (∑ i ∈ t, f' i)
have insert : ∀ (i : ι) (s_1 : Finset ι) (hi : i ∉ s_1)
  (IH :
    ∀ (hf : ∀ i ∈ s_1, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)),
      HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ s_1, f i) s z (∑ i ∈ s_1, f' i))
  (hf : ∀ i_1 ∈ insert i s_1, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i_1) s z (f' i_1)),
  HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ insert i s_1, f i) s z (∑ i ∈ insert i s_1, f' i)
Tactic: induction t using Finset.induction_on with
  | empty => simpa using hasMFDerivWithinAt_const ..
  | insert i s hi IH => grind [HasMFDerivWithinAt.add]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
z : M
ι : Type
t : Finset ι
f : ι → M → E'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ t, f i) s z (∑ i ∈ t, f' i)
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)),
  HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ ∅, f i) s z (∑ i ∈ ∅, f' i)
Tactic: classical
  induction t using Finset.induction_on with
  | empty => simpa using hasMFDerivWithinAt_const ..
  | insert i s hi IH => grind [HasMFDerivWithinAt.add]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
z : M
ι : Type
t : Finset ι
f : ι → M → E'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ ∅, f i) s z (∑ i ∈ ∅, f' i)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ t, f i) s z (∑ i ∈ t, f' i)
have insert : ∀ (i : ι) (s_1 : Finset ι) (hi : i ∉ s_1)
  (IH :
    ∀ (hf : ∀ i ∈ s_1, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)),
      HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ s_1, f i) s z (∑ i ∈ s_1, f' i))
  (hf : ∀ i_1 ∈ insert i s_1, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i_1) s z (f' i_1)),
  HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ insert i s_1, f i) s z (∑ i ∈ insert i s_1, f' i)
Tactic: classical
  induction t using Finset.induction_on with
  | empty => simpa using hasMFDerivWithinAt_const ..
  | insert i s hi IH => grind [HasMFDerivWithinAt.add]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
ι : Type
t : Finset ι
f : ι → M → E'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : ∀ i ∈ t, HasMFDerivAt I 𝓘(𝕜, E') (f i) z (f' i)
⊢ HasMFDerivAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ t, f i) z (∑ i ∈ t, f' i)
have simp_all : ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) univ z (f' i)),
  HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ t, f i) univ z (∑ i ∈ t, f' i)
Tactic: simp_all only [← hasMFDerivWithinAt_univ]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
ι : Type
t : Finset ι
f : ι → M → E'
hf : ∀ i ∈ t, MDiffAt (f i) z
⊢ MDiffAt (∑ i ∈ t, f i) z
have hf₁ : ∀ i ∈ t, MDiffAt[univ] (f i) z
Tactic: simp_all only [← mdifferentiableWithinAt_univ]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
f : M → E'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : HasMFDerivAt I 𝓘(𝕜, E') (-f) z (-f')
⊢ HasMFDerivAt I 𝓘(𝕜, E') f z f'
have h : f = - -f
Tactic: convert! hf.neg
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
f : M → E'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : HasMFDerivAt I 𝓘(𝕜, E') (-f) z (-f')
h : f = - -f
⊢ HasMFDerivAt I 𝓘(𝕜, E') f z f'
have h₁ : f = - -f → f' = - -f'
Tactic: convert! hf.neg
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
f : M → E'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : HasMFDerivAt I 𝓘(𝕜, E') (-f) z (-f')
⊢ f = - -f
have h : f = f
Tactic: rw [neg_neg]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
f : M → E'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : HasMFDerivAt I 𝓘(𝕜, E') (-f) z (-f')
e_21 : f = - -f
⊢ f' = - -f'
have h : f' = f'
Tactic: rw [neg_neg]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
z : M
f : M → E'
hf : MDiffAt[s] (-f) z
⊢ MDiffAt[s] f z
have h : f = - -f
Tactic: convert hf.neg
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
z : M
f : M → E'
hf : MDiffAt[s] (-f) z
⊢ f = - -f
have h : f = f
Tactic: rw [neg_neg]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
f : M → E'
hf : MDiffAt (-f) z
⊢ MDiffAt f z
have h : f = - -f
Tactic: convert! hf.neg
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
f : M → E'
hf : MDiffAt (-f) z
⊢ f = - -f
have h : f = f
Tactic: rw [neg_neg]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
f : M → E'
x : M
hs : UniqueMDiffWithinAt I s x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (mfderivWithin I 𝓘(𝕜, E') (-f) s x) (-mfderivWithin I 𝓘(𝕜, E') f s x)
have simp_rw : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
  (if MDiffAt[s] (-f) x then
    fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f)) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
  else 0)
  (-if MDiffAt[s] f x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x)
    else 0)
Tactic: simp_rw [mfderivWithin]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
f : M → E'
x : M
hs : UniqueMDiffWithinAt I s x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
    else 0)
    (-if MDiffAt[s] f x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f)
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
      else 0)
have pos : ∀ (hf : MDiffAt[s] f x),
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
    else 0)
    (-if MDiffAt[s] f x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f)
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
      else 0)
Tactic: by_cases hf : MDiffAt[s] f x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
f : M → E'
x : M
hs : UniqueMDiffWithinAt I s x
pos :
  ∀ (hf : MDiffAt[s] f x),
    Eq (α :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
      (if MDiffAt[s] (-f) x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
      else 0)
      (-if MDiffAt[s] f x then
          fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f)
            ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
        else 0)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
    else 0)
    (-if MDiffAt[s] f x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f)
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
      else 0)
have neg : ∀ (hf : ¬MDiffAt[s] f x),
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
    else 0)
    (-if MDiffAt[s] f x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f)
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
      else 0)
Tactic: by_cases hf : MDiffAt[s] f x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
f : M → E'
x : M
hs : UniqueMDiffWithinAt I s x
hf : ¬MDiffAt[s] f x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
    else 0)
    (-if MDiffAt[s] f x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f)
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
      else 0)
have neg : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
  (if MDiffAt[s] (-f) x then
    fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f)) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
  else 0)
  (-0)
Tactic: rw [if_neg hf]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
f : M → E'
x : M
hs : UniqueMDiffWithinAt I s x
hf : ¬MDiffAt[s] f x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
    else 0)
    (-0)
have hf₁ : ¬MDiffAt[s] (-f) x
Tactic: rw [← mdifferentiableWithinAt_neg] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
f : M → E'
x : M
hs : UniqueMDiffWithinAt I s x
hf : ¬MDiffAt[s] (-f) x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
    else 0)
    (-0)
have neg : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x))) 0
  (-0)
Tactic: rw [if_neg hf, neg_zero]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
f : M → E'
x : M
hs : UniqueMDiffWithinAt I s x
hf : ¬MDiffAt[s] (-f) x
neg :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    0 (-0)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
    else 0)
    (-0)
have neg₁ : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x))) 0
  0
Tactic: rw [if_neg hf, neg_zero]