mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ ∀ x ∈ univ,
    x ∉ fs →
      (if i₂ = i₁ ∨ True then (↑(n + 1))⁻¹ else 0) * ((if x = i₁ then 1 else 0) - if x = i₂ then 1 else 0) *
          (dist (s.points i₂) (s.points x) * dist (s.points i₂) (s.points x)) =
        0

Tactic:
intro i

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
i : Fin (n + 3)
⊢ i ∈ univ →
    i ∉ fs →
      (if i₂ = i₁ ∨ True then (↑(n + 1))⁻¹ else 0) * ((if i = i₁ then 1 else 0) - if i = i₂ then 1 else 0) *
          (dist (s.points i₂) (s.points i) * dist (s.points i₂) (s.points i)) =
        0
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ ∀ x ∈ univ,
    x ∉ fs →
      (if True ∨ i₁ = i₂ then (↑(n + 1))⁻¹ else 0) * ((if x = i₁ then 1 else 0) - if x = i₂ then 1 else 0) *
          (dist (s.points i₁) (s.points x) * dist (s.points i₁) (s.points x)) =
        0

Tactic:
intro i

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
i : Fin (n + 3)
⊢ i ∈ univ →
    i ∉ fs →
      (if True ∨ i₁ = i₂ then (↑(n + 1))⁻¹ else 0) * ((if i = i₁ then 1 else 0) - if i = i₂ then 1 else 0) *
          (dist (s.points i₁) (s.points i) * dist (s.points i₁) (s.points i)) =
        0
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ ∀ x ∈ univ,
    x ∉ fs →
      -2 / ↑(n + 1) * ((if x = i₁ then 1 else 0) - if x = i₂ then 1 else 0) *
          (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) =
        0

Tactic:
intro i

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
i : Fin (n + 3)
⊢ i ∈ univ →
    i ∉ fs →
      -2 / ↑(n + 1) * ((if i = i₁ then 1 else 0) - if i = i₂ then 1 else 0) *
          (dist s.circumcenter (s.points i) * dist s.circumcenter (s.points i)) =
        0
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ ∀ x ∈ univ,
    x ∉ fs →
      ∑ i₂_1,
          (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
              (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
            (dist (s.points x) (s.pointsWithCircumcenter i₂_1) * dist (s.points x) (s.pointsWithCircumcenter i₂_1)) =
        0

Tactic:
intro i

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
i : Fin (n + 3)
⊢ i ∈ univ →
    i ∉ fs →
      ∑ i₂_1,
          (if i = i₁ ∨ i = i₂ then (↑(n + 1))⁻¹ else 0) *
              (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
            (dist (s.points i) (s.pointsWithCircumcenter i₂_1) * dist (s.points i) (s.pointsWithCircumcenter i₂_1)) =
        0
Module: Mathlib.Geometry.Euclidean.Simplex

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
⊢ ↑2 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i) =
    2 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Geometry.Euclidean.Simplex

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
⊢ (↑2 + 1) * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i) =
    3 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (Submodule.span ℝ (⋃ i, {s.points i₁ -ᵥ s.points ↑i}))ᗮ
hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x ↦ s.points i₁ -ᵥ x) '' s.points '' (Set.univ \ {i₁})
⊢ p -ᵥ s.mongePoint = 0

Tactic:
rw [hu, ← vectorSpan_image_eq_span_vsub_set_left_ne ℝ _ (Set.mem_univ _), Set.image_univ] at hi

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (vectorSpan ℝ (Set.range s.points))ᗮ
hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x ↦ s.points i₁ -ᵥ x) '' s.points '' (Set.univ \ {i₁})
⊢ p -ᵥ s.mongePoint = 0
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
i₃ : Fin 3
h₂ : p ∈ mongePlane t i₃ i₁
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ ∀ (i : Fin 3), i₃ ≠ i → p ∈ mongePlane t i₃ i

Tactic:
intro i

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
i₃ : Fin 3
h₂ : p ∈ mongePlane t i₃ i₁
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
i : Fin 3
⊢ i₃ ≠ i → p ∈ mongePlane t i₃ i
Module: Mathlib.Geometry.Group.Growth.QuotientInter

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x ↦ x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' ↑A ^ m)
hφA : ∀ {a : G ⧸ H}, a ∈ ⇑π '' ↑A ^ m → φ a ∈ A ^ m
hπφ : ∀ {a : G ⧸ H}, a ∈ ⇑π '' ↑A ^ m → π (φ a) = a
⊢ #(image (⇑π) (A ^ m)) * #({x ∈ A ^ n | x ∈ H}) = #(image φ (image (⇑π) (A ^ m))) * #({x ∈ A ^ n | x ∈ H})

Tactic:
by
      rw [Finset.card_image_of_injOn (f := φ) (mod_cast hφ)]

Goal state after:
Module: Mathlib.Geometry.Group.Growth.LinearLowerBound

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hXclosure : ↑X ^ n ≠ ↑(closure ↑X)
⊢ X ^ n ⊂ X ^ (n + 1)

Tactic:
by
  obtain rfl | hn := eq_or_ne n 0
  · simpa [ssubset_iff_subset_not_subset, hX₁, -Finset.subset_singleton_iff]
      using! hX.not_subset_singleton
  refine (pow_subset_pow_right hX₁ <| n.le_add_right _).ssubset_of_ne ?_
  contrapose hXclosure with hXn
  rw [← closure_pow (mod_cast hX₁) hn]
  wlog hn₁ : n = 1
  · simp +contextual only [pow_one] at this
    replace hXn d : X ^ (n + d) = X ^ n := by
      induction d with
      | zero => rw [add_zero]
      | succ d hd =>
        rw [pow_add, pow_one] at hXn
        rw [← add_assoc, pow_add, pow_one, hd, ← hXn]
    exact mod_cast this (one_mem_pow hX₁) (hX.pow hn) one_ne_zero
      (by simp [hXn, ← pow_mul, mul_two]) (by simp)
  subst hn₁
  simp only [ne_eq, one_ne_zero, not_false_eq_true, Nat.reduceAdd, pow_one] at *
  let Xgp : Subgroup G :=
  { carrier := X
    mul_mem' := fun {x y} hx hy ↦ by
      norm_cast at *
      simpa [← hXn, ← sq] using! mul_mem_mul hx hy
    one_mem' := hX₁
    inv_mem' := fun {x} hx ↦ by
      norm_cast at *
      have : x • X ⊆ X := by
        simpa [← hXn, add_assoc, ← sq] using! smul_finset_subset_mul (t := X) hx
      have : x • X = X := eq_of_subset_of_card_le this (card_smul_finset ..).ge
      rw [← eq_inv_smul_iff] at this
      rw [this]
      simpa [mem_inv_smul_finset_iff] }
  exact subset_closure.antisymm <| (closure_le Xgp).2 subset_rfl

Goal state after:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ : Fin 3
h₁ : p i₁ = t.orthocenter
i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
⊢ ∀ (i : Fin 3), i₁ ≠ i → ∃ j, t.points j = p i

Tactic:
intro i

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ : Fin 3
h₁ : p i₁ = t.orthocenter
i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
i : Fin 3
⊢ i₁ ≠ i → ∃ j, t.points j = p i
Module: Mathlib.Geometry.Manifold.LocalDiffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
x' : M
hx' : x' ∈ hf.localInverse.target
⊢ ↑hf.localInverse.toPartialEquiv (f x') = x'

Tactic:
rw [hf.choose_spec.2 (hf.choose.symm_target ▸ hx')]

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
x' : M
hx' : x' ∈ hf.localInverse.target
⊢ ↑hf.localInverse.toPartialEquiv (↑(Exists.choose hf).toPartialEquiv x') = x'
Module: Mathlib.Geometry.Manifold.DerivationBundle

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 : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ : C^∞⟮I, 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 : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : f x = y
v : PointDerivation I x
g g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ g y * v (ContMDiffMap.comp g' f) + g' y * v (ContMDiffMap.comp g f) =
    g • v (ContMDiffMap.comp g' f) + g' • v (ContMDiffMap.comp g f)

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : NormedAddCommGroup F
inst✝¹⁹ : NormedSpace 𝕜 F
inst✝¹⁸ : TopologicalSpace (TotalSpace F E)
inst✝¹⁷ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst✝¹³ : NormedAddCommGroup EM
inst✝¹² : NormedSpace 𝕜 EM
HM : Type u_11
inst✝¹¹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace HM M
inst✝⁸ : TopologicalSpace B
inst✝⁷ : ChartedSpace HB B
inst✝⁶ : FiberBundle F E
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module 𝕜 (E x)
inst✝³ : VectorBundle 𝕜 F E
inst✝² : ContMDiffVectorBundle 1 F E IB
e : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e'
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : MDiffAt[s] (TotalSpace.proj ∘ f) x₀
he'f : (MDiffAt[s] fun x ↦ (↑e (f x)).2) x₀
he : (f x₀).proj ∈ e.baseSet
he' : (f x₀).proj ∈ e'.baseSet
⊢ (↑e' (f x₀)).2 = e.coordChange e' ((TotalSpace.proj ∘ f) x₀) (↑e (f x₀)).2

Tactic:
simp [he]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
ι : Type u_9
s : Finset ι
t : ι → (x : B) → E x
x₀ : B
hs : ∀ i ∈ s, MDiffAt (T% t) x₀
⊢ (MDiffAt fun x ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀

Tactic:
simp_rw [← mdifferentiableWithinAt_univ] at hs ⊢
  exact MDifferentiableWithinAt.sum_section hs

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

Goal state before:
pp: 𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B₁) → AddCommGroup (E₁ x)
inst✝¹⁷ : (x : B₁) → Module 𝕜 (E₁ x)
inst✝¹⁶ : NormedAddCommGroup F₁
inst✝¹⁵ : NormedSpace 𝕜 F₁
inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹³ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝¹² : (x : B₂) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B₂) → TopologicalSpace (E₂ x)
inst✝⁶ : TopologicalSpace B₁
inst✝⁵ : TopologicalSpace B₂
inst✝⁴ : TopologicalSpace M
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ : ContinuousWithinAt (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) s m₀
hv : ContinuousWithinAt (fun m ↦ { proj := b₁ m, snd := v m }) s m₀
hb₂ : ContinuousWithinAt b₂ s m₀
⊢ ContinuousWithinAt (fun m ↦ { proj := b₂ m, snd := (ϕ m) (v m) }) s m₀

Tactic:
rw [← continuousWithinAt_insert_self] at hϕ hv hb₂ ⊢

Goal state after:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B₁) → AddCommGroup (E₁ x)
inst✝¹⁷ : (x : B₁) → Module 𝕜 (E₁ x)
inst✝¹⁶ : NormedAddCommGroup F₁
inst✝¹⁵ : NormedSpace 𝕜 F₁
inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹³ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝¹² : (x : B₂) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B₂) → TopologicalSpace (E₂ x)
inst✝⁶ : TopologicalSpace B₁
inst✝⁵ : TopologicalSpace B₂
inst✝⁴ : TopologicalSpace M
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ : ContinuousWithinAt (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) (insert m₀ s) m₀
hv : ContinuousWithinAt (fun m ↦ { proj := b₁ m, snd := v m }) (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
⊢ ContinuousWithinAt (fun m ↦ { proj := b₂ m, snd := (ϕ m) (v m) }) (insert m₀ s) m₀
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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 : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiff[u]
t' : Set N := ⋯
ht't : t' ⊆ t
this :
  ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv[u] (f x) (g x)) x₀) t' x₀
⊢ t' ∈ 𝓝[t] x₀

Tactic:
apply inter_mem self_mem_nhdsWithin

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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 : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiff[u]
t' : Set N := ⋯
ht't : t' ⊆ t
this :
  ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv[u] (f x) (g x)) x₀) t' x₀
⊢ g ⁻¹' (extChartAt I (g x₀)).source ∈ 𝓝[t] x₀
Module: Mathlib.Geometry.Manifold.VectorField.Pullback

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁵ : TopologicalSpace H
E : Type u_3
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace H M
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
E' : Type u_6
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁷ : TopologicalSpace M'
inst✝⁶ : ChartedSpace H' M'
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
E'' : Type u_9
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝² : TopologicalSpace M''
inst✝¹ : ChartedSpace H'' M''
f : M → M'
s t : Set M
x x₀ : M
inst✝ : IsManifold I (minSmoothness 𝕜 3) M
⊢ 2 ≤ 3

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorField.Pullback

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁵ : TopologicalSpace H
E : Type u_3
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace H M
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
E' : Type u_6
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁷ : TopologicalSpace M'
inst✝⁶ : ChartedSpace H' M'
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
E'' : Type u_9
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝² : TopologicalSpace M''
inst✝¹ : ChartedSpace H'' M''
f : M → M'
s t : Set M
x x₀ : M
inst✝ : IsManifold I (minSmoothness 𝕜 2) M
⊢ 1 ≤ 2

Tactic:
norm_cast

Goal state after: