mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.ContMDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst✝ : DecidablePred fun x ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∈ interior s
y : M
hy : y ∈ interior s
⊢ s.piecewise f g y = f y

Tactic:
piecewise_eq_of_mem

Goal state after:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst✝ : DecidablePred fun x ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∈ interior s
y : M
hy : y ∈ interior s
⊢ f y = f y

case hi
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst✝ : DecidablePred fun x ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∈ interior s
y : M
hy : y ∈ interior s
⊢ y ∈ s
Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝⁴ : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
f : M → N
h : ContMDiff I J n (Sum.inl ∘ f)
⊢ ContMDiff I J n f

Tactic:
nontriviality N
  inhabit N
  let aux : N ⊕ N' → N := Sum.elim (@id N) (fun _ ↦ inhabited_h.default)
  have : aux ∘ (@Sum.inl N N') ∘ f = f := by ext; simp [aux]
  rw [← this]
  rw [← contMDiffOn_univ] at h ⊢
  apply (contMDiff_id.sumElim contMDiff_const).contMDiffOn (s := @Sum.inl N N' '' univ).comp h
  intro x _hx
  rw [mem_preimage, Function.comp_apply]
  use f x, trivial

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Prod

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial E
e : E
he : e ≠ 0
this : ‖e‖ ≤ ‖fst 𝕜 E F‖ * ‖e‖
⊢ 1 ≤ ‖fst 𝕜 E F‖

Tactic:
rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr he), one_mul]

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
e : OpenPartialHomeomorph M H
e' : OpenPartialHomeomorph M' H'
f : M → M'
s : Set M
n : ℕ∞ω
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I' n M'
hs : s ⊆ e.source
h2s : MapsTo f s e'.source
⊢ ContMDiffOn I I' n f s ↔
    ContinuousOn f s ∧ ContDiffOn 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s)

Tactic:
ContinuousOn,

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
e : OpenPartialHomeomorph M H
e' : OpenPartialHomeomorph M' H'
f : M → M'
s : Set M
n : ℕ∞ω
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I' n M'
hs : s ⊆ e.source
h2s : MapsTo f s e'.source
⊢ ContMDiffOn I I' n f s ↔
    (∀ x ∈ s, ContinuousWithinAt f s x) ∧ ContDiffOn 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s)
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
e : OpenPartialHomeomorph M H
e' : OpenPartialHomeomorph M' H'
he : e ∈ maximalAtlas I 1 M
he' : e' ∈ maximalAtlas I' 1 M'
hs : s ⊆ e.source
h2s : MapsTo f s e'.source
⊢ MDiff[s] f ↔ ContinuousOn f s ∧ DifferentiableOn 𝕜 (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s)

Tactic:
ContinuousOn,

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
e : OpenPartialHomeomorph M H
e' : OpenPartialHomeomorph M' H'
he : e ∈ maximalAtlas I 1 M
he' : e' ∈ maximalAtlas I' 1 M'
hs : s ⊆ e.source
h2s : MapsTo f s e'.source
⊢ MDiff[s] f ↔
    (∀ x ∈ s, ContinuousWithinAt f s x) ∧
      DifferentiableOn 𝕜 (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s)
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_7
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : φ ∈ maximalAtlas I n M
hψ : ψ ∈ maximalAtlas J n N
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I)
      (↑(φ.extend I) y) ↔
    ContMDiffWithinAt I J n f s y

Tactic:
rw [contMDiffWithinAt_iff_of_mem_maximalAtlas hφ hψ hy hgy]

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_7
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : φ ∈ maximalAtlas I n M
hψ : ψ ∈ maximalAtlas J n N
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I)
      (↑(φ.extend I) y) ↔
    ContinuousWithinAt f s y ∧
      ContDiffWithinAt 𝕜 n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I)
        (↑(φ.extend I) y)
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
a✝ : Nontrivial E
this : Nontrivial (TangentSpace I x)
hf : ¬MDiffAt[s] f x
⊢ ¬Injective ⇑0

Tactic:
exact not_injective_const

Goal state after:
Module: Mathlib.Topology.VectorBundle.Constructions

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : (b ∈ e₁.baseSet ∧ b ∈ e₂.baseSet) ∧ b ∈ e₁'.baseSet ∧ b ∈ e₂'.baseSet
v₁ : F₁
v₂ : F₂
⊢ ↑(coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) (v₁, v₂) =
    Prod.map ⇑↑(coordChangeL 𝕜 e₁ e₁' b) ⇑↑(coordChangeL 𝕜 e₂ e₂' b) (v₁, v₂)

Tactic:
change
    (e₁.prod e₂).coordChangeL 𝕜 (e₁'.prod e₂') b (v₁, v₂) =
      (e₁.coordChangeL 𝕜 e₁' b v₁, e₂.coordChangeL 𝕜 e₂' b v₂)

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : (b ∈ e₁.baseSet ∧ b ∈ e₂.baseSet) ∧ b ∈ e₁'.baseSet ∧ b ∈ e₂'.baseSet
v₁ : F₁
v₂ : F₂
⊢ (coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) (v₁, v₂) = ((coordChangeL 𝕜 e₁ e₁' b) v₁, (coordChangeL 𝕜 e₂ e₂' b) v₂)
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
x : M × M'
⊢ HasMFDerivAt% Prod.fst x (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Tactic:
by
  refine ⟨continuous_fst.continuousAt, ?_⟩
  have :
    ∀ᶠ y in 𝓝[range (I.prod I')] extChartAt (I.prod I') x x,
      (extChartAt I x.1 ∘ Prod.fst ∘ (extChartAt (I.prod I') x).symm) y = y.1 := by
    /- porting note: was
    apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin (I.prod I') x)
    mfld_set_tac
    -/
    filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
    rw [extChartAt_prod] at hy
    exact (extChartAt I x.1).right_inv hy.1
  apply HasFDerivWithinAt.congr_of_eventuallyEq hasFDerivWithinAt_fst this
  -- Porting note: next line was `simp only [mfld_simps]`
  exact (extChartAt I x.1).right_inv <| (extChartAt I x.1).map_source (mem_extChartAt_source _)

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffAt[range ↑I] y
⊢ mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) ∘SL mfderiv[range ↑I] ↑(extChartAt I x).symm y =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y)

Tactic:
have h'y : (extChartAt I x).symm y ∈ (extChartAt I x).source := (extChartAt I x).map_target hy

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffAt[range ↑I] y
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
⊢ mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) ∘SL mfderiv[range ↑I] ↑(extChartAt I x).symm y =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y)
Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ mfderiv[range ↑I] ↑(extChartAt I x).symm y ∘SL mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) =
    ContinuousLinearMap.id 𝕜 (TangentSpace I (↑(extChartAt I x).symm y))

Tactic:
have h'y : (extChartAt I x).symm y ∈ (extChartAt I x).source := (extChartAt I x).map_target hy

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
⊢ mfderiv[range ↑I] ↑(extChartAt I x).symm y ∘SL mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) =
    ContinuousLinearMap.id 𝕜 (TangentSpace I (↑(extChartAt I x).symm y))
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst✝¹] (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst✝¹] (t b)
htf : LocallyFinite t
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
⊢ ∃ v, (∀ (a : ι), IsOpen[inst✝¹] (v a)) ∧ ⋃ i, v i = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a

Tactic:
choose U hxU hU using htf

Goal state after:
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst✝¹] (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst✝¹] (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | (t i ∩ U x).Nonempty}.Finite
⊢ ∃ v, (∀ (a : ι), IsOpen[inst✝¹] (v a)) ∧ ⋃ i, v i = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
s t : (x : M) → V x
x₀ : M
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, s x⟩) x₀
ht : ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t x⟩) x₀
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, (s + t) x⟩) x₀

Tactic:
by
  rw [← contMDiffWithinAt_univ] at hs ⊢
  exact hs.add_section ht

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
i : ι
s : Set X
⊢ ⇑(BumpCovering.single i s) = Pi.single i 1

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst✝⁵] s
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst✝⁵] (U i)
hU : s ⊆ ⋃ i, U i
⊢ ∃ f, f.IsSubordinate U

Tactic:
have : LocallyCompactSpace H := I.locallyCompactSpace
  have : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M
  -- porting note(https://github.com/leanprover-community/batteries/issues/116):
  -- split `rcases` into `have` + `rcases`
  have := BumpCovering.exists_isSubordinate_of_prop (ContMDiff I 𝓘(ℝ) ∞) ?_ hs U ho hU
  · rcases this with ⟨f, hf, hfU⟩
    exact ⟨f.toSmoothPartitionOfUnity hf, hfU.toSmoothPartitionOfUnity hf⟩
  · intro s t hs ht hd
    rcases exists_contMDiffMap_zero_one_of_isClosed I hs ht hd with ⟨f, hf⟩
    exact ⟨f, f.contMDiff, hf⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), (fun x ↦ c (f x)) =ᵐ[μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable ↑d
s : ↑d → StrongDual 𝕜 E
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : ↑d
hx : dist a ↑x < ‖a‖ / 2
I : ‖a‖ / 2 < ‖↑x‖
h : (s x) a = 0
⊢ 1 * ‖↑x - a‖ < ‖a‖ / 2

Tactic:
by rw [one_mul]; rwa [dist_eq_norm'] at hx

Goal state after:
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst✝¹] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ (↑?m.76) f
f_range : range f ⊆ Icc 0 1
⊢ ∃ f, support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n) f ∧ range f ⊆ Icc 0 1

Tactic:
refine ⟨f ∘ I, ?_, ?_, ?_⟩

Goal state after:
case refine_1
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst✝¹] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ (↑?m.76) f
f_range : range f ⊆ Icc 0 1
⊢ support (f ∘ ↑I) = s

case refine_2
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst✝¹] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ (↑?m.76) f
f_range : range f ⊆ Icc 0 1
⊢ ContMDiff I 𝓘(ℝ, ℝ) (↑n) (f ∘ ↑I)

case refine_3
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst✝¹] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ (↑?m.76) f
f_range : range f ⊆ Icc 0 1
⊢ range (f ∘ ↑I) ⊆ Icc 0 1
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case refine_1.refine_1
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
⊢ ∑ᶠ (c : M), (f c) x * g c (↑(chartAt H c) x) ≠ 0

Tactic:
apply ne_of_gt

Goal state after:
case refine_1.refine_1
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
⊢ 0 < ∑ᶠ (c : M), (f c) x * g c (↑(chartAt H c) x)
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
h_neg : 0 ≤ᵐ[μ.restrict t] -f
⊢ f ≤ᵐ[μ.restrict t] 0

Tactic:
refine h_neg.mono fun x hx => ?_
    rw [Pi.neg_apply] at hx
    simpa using hx

Goal state after: