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

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
s : Sphere P
p p' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
⊢ Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))

Tactic:
by_cases h : p' = p; · simp [h]
  refine
    wbtw_of_collinear_of_dist_center_le_radius (s.secondInter_collinear p p') hp hp'
      ((Sphere.secondInter_mem _).2 hp) ?_
  intro he
  rw [eq_comm, Sphere.secondInter_eq_self_iff, ← neg_neg (p' -ᵥ p), inner_neg_left,
    neg_vsub_eq_vsub_rev, neg_eq_zero, eq_comm] at he
  exact ((inner_pos_or_eq_of_dist_le_radius hp hp').resolve_right (Ne.symm h)).ne he

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
⊢ t.orthocenter = 3 • (Finset.centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t

Tactic:
by
  rw [orthocenter_eq_mongePoint, mongePoint_eq_smul_vsub_vadd_circumcenter]
  simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

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
s : Sphere P
n : ℕ
inst✝ : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Ioo 0 1
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P := (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points) w)) r
hp' : p' -ᵥ sx.points i = r • ((Finset.affineCombination ℝ Finset.univ sx.points) w -ᵥ sx.points i)
⊢ r • (Finset.univ.weightedVSub sx.points) (w - Pi.single i 1) +ᵥ
      (Finset.affineCombination ℝ Finset.univ sx.points) (Pi.single i 1) ∈
    (sx.faceOpposite i).interior

Tactic:
← LinearMap.map_smul,

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : Sphere P
n : ℕ
inst✝ : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Ioo 0 1
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P := (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points) w)) r
hp' : p' -ᵥ sx.points i = r • ((Finset.affineCombination ℝ Finset.univ sx.points) w -ᵥ sx.points i)
⊢ (Finset.univ.weightedVSub sx.points) (r • (w - Pi.single i 1)) +ᵥ
      (Finset.affineCombination ℝ Finset.univ sx.points) (Pi.single i 1) ∈
    (sx.faceOpposite i).interior
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

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
s : Sphere P
n : ℕ
inst✝ : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Ioo 0 1
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P := (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points) w)) r
hp' : p' -ᵥ sx.points i = r • ((Finset.affineCombination ℝ Finset.univ sx.points) w -ᵥ sx.points i)
⊢ (∀ i_1 ∈ {i}ᶜ, 0 < (r • (w - Pi.single i 1) + Pi.single i 1) i_1) ∧
    ∀ i_1 ∉ {i}ᶜ, (r • (w - Pi.single i 1) + Pi.single i 1) i_1 = 0

Tactic:
simp only [Finset.mem_compl, Finset.mem_singleton, Pi.add_apply, Pi.smul_apply, Pi.sub_apply,
      smul_eq_mul, Decidable.not_not, forall_eq, Pi.single_eq_same]
    refine ⟨fun j hj ↦ ?_, by grind⟩
    simp [hj, hrpos, (hw01 j).1]

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

Goal state before:
pp: case inr.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {X : Finset G} {n : ℕ},
    1 ∈ X → X.Nontrivial → n ≠ 0 → X ^ n = X ^ (n + 1) → n = 1 → ↑X ^ n = ↑(closure (↑X ^ n))
hn₁ : ¬n = 1
⊢ ↑X ^ n = ↑(closure (↑X ^ n))

Tactic:
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)

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 : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
x : G
hx : x ∈ X
this✝ : x • X ⊆ X
this : X = x⁻¹ • X
⊢ x⁻¹ ∈ x⁻¹ • X

Tactic:
simpa [mem_inv_smul_finset_iff]

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
s : Set P
ho : OrthocentricSystem s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
⊢ AffineIndependent ℝ p

Tactic:
rcases ho with ⟨t, hto, hst⟩

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hst : s = insert t.orthocenter (Set.range t.points)
⊢ AffineIndependent ℝ p
Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g✝ h : G
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^∞⟮I, G; 𝕜⟯⟨g⟩
hX : (↑X (Y (ContMDiffMap.comp f (𝑳 I g)))) 1 = ((Derivation.evalAt g) ↑X) (Y f)
hY : (↑Y (X (ContMDiffMap.comp f (𝑳 I g)))) 1 = ((Derivation.evalAt g) ↑Y) (X f)
⊢ (↑X (↑Y (ContMDiffMap.comp f (𝑳 I g)))) 1 - (↑Y (↑X (ContMDiffMap.comp f (𝑳 I g)))) 1 =
    ((Derivation.evalAt g) ⁅↑X, ↑Y⁆) f

Tactic:
coe_derivation

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g✝ h : G
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^∞⟮I, G; 𝕜⟯⟨g⟩
hX : (↑X (Y (ContMDiffMap.comp f (𝑳 I g)))) 1 = ((Derivation.evalAt g) ↑X) (Y f)
hY : (↑Y (X (ContMDiffMap.comp f (𝑳 I g)))) 1 = ((Derivation.evalAt g) ↑Y) (X f)
⊢ (X (↑Y (ContMDiffMap.comp f (𝑳 I g)))) 1 - (↑Y (X (ContMDiffMap.comp f (𝑳 I g)))) 1 =
    ((Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g✝ h : G
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^∞⟮I, G; 𝕜⟯⟨g⟩
hX : (↑X (Y (ContMDiffMap.comp f (𝑳 I g)))) 1 = ((Derivation.evalAt g) ↑X) (Y f)
hY : (↑Y (X (ContMDiffMap.comp f (𝑳 I g)))) 1 = ((Derivation.evalAt g) ↑Y) (X f)
⊢ (X (↑Y (ContMDiffMap.comp f (𝑳 I g)))) 1 - (↑Y (X (ContMDiffMap.comp f (𝑳 I g)))) 1 =
    ((Derivation.evalAt g) ⁅↑X, ↑Y⁆) f

Tactic:
coe_derivation

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g✝ h : G
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^∞⟮I, G; 𝕜⟯⟨g⟩
hX : (X (Y (ContMDiffMap.comp f (𝑳 I g)))) 1 = ((Derivation.evalAt g) ↑X) (Y f)
hY : (Y (X (ContMDiffMap.comp f (𝑳 I g)))) 1 = ((Derivation.evalAt g) ↑Y) (X f)
⊢ (X (Y (ContMDiffMap.comp f (𝑳 I g)))) 1 - (Y (X (ContMDiffMap.comp f (𝑳 I g)))) 1 = ((Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_1
𝕜 : 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)
e e' : Trivialization F TotalSpace.proj
inst✝³ : MemTrivializationAtlas e
inst✝² : MemTrivializationAtlas e'
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : ContMDiffVectorBundle 1 F E IB
s : Set M
f : M → B
g : M → F
x : M
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
this : e.baseSet ∩ e'.baseSet ∈ 𝓝 (f x)
⊢ (fun y ↦ e.coordChange e' (f y) (g y)) =ᶠ[𝓝[s] x] fun x ↦ ↑(Trivialization.coordChangeL 𝕜 e e' (f x)) (g x)

Tactic:
filter_upwards [hf.continuousWithinAt this] with y hy

Goal state after:
𝕜 : 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)
e e' : Trivialization F TotalSpace.proj
inst✝³ : MemTrivializationAtlas e
inst✝² : MemTrivializationAtlas e'
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : ContMDiffVectorBundle 1 F E IB
s : Set M
f : M → B
g : M → F
x : M
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
this : e.baseSet ∩ e'.baseSet ∈ 𝓝 (f x)
y : M
hy : y ∈ f ⁻¹' (e.baseSet ∩ e'.baseSet)
⊢ e.coordChange e' (f y) (g y) = ↑(Trivialization.coordChangeL 𝕜 e e' (f y)) (g y)
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case insert
𝕜 : 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
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
i : ι
s : Finset ι
hi : i ∉ s
h : (∀ i ∈ s, MDiffAt[u] (T% t) x₀) → (MDiffAt[u] fun x ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀
hs : ∀ i_1 ∈ insert i s, MDiffAt[u] (T% t) x₀
⊢ (MDiffAt[u] fun x ↦ ⟨x, ∑ i ∈ insert i s, t i x⟩) x₀

Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at hs
    simpa [Finset.sum_insert hi] using mdifferentiableWithinAt_add_section (hs.1) (h hs.2)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst✝³] s
hxs : x ∈ s
⊢ s' ∩ g ⁻¹' hf.codChart.source ⊆ g ⁻¹' hf.codChart.source

Tactic:
exact inter_subset_right

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'
f : M → M'
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
y₀ : M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
hV : ContMDiffWithinAt I' I'.tangent m (fun x ↦ ⟨x, V x⟩) t y₀
hf : ContMDiffAt I I' n f x₀
hf' : (mfderiv% f x₀).IsInvertible
hmn : m + 1 ≤ n
hy₀ : y₀ = f x₀
⊢ ContMDiffWithinAt I I.tangent m (fun x ↦ ⟨x, mpullback I I' f V x⟩) (f ⁻¹' t) x₀

Tactic:
by
  subst hy₀
  exact ContMDiffWithinAt.mpullback_vectorField_preimage hV hf hf' hmn

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
F' : Type u_6
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
inst✝¹¹ : NormedAddCommGroup E''
inst✝¹⁰ : NormedSpace 𝕜 E''
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : NormedAddCommGroup F'
inst✝⁶ : NormedSpace 𝕜 F'
H : Type u_7
inst✝⁵ : TopologicalSpace H
G : Type u_9
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_13
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
h : IsImmersionAtOfComplement F I J n f x
e : F ≃L[𝕜] F'
⊢ ImmersionAtProp F' I J M N f h.domChart h.codChart

Tactic:
use ((ContinuousLinearEquiv.refl 𝕜 E).prodCongr e.symm).trans h.equiv

Goal state after:
case h
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
F' : Type u_6
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
inst✝¹¹ : NormedAddCommGroup E''
inst✝¹⁰ : NormedSpace 𝕜 E''
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : NormedAddCommGroup F'
inst✝⁶ : NormedSpace 𝕜 F'
H : Type u_7
inst✝⁵ : TopologicalSpace H
G : Type u_9
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_13
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
h : IsImmersionAtOfComplement F I J n f x
e : F ≃L[𝕜] F'
⊢ EqOn (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm)
    (⇑(((ContinuousLinearEquiv.refl 𝕜 E).prodCongr e.symm).trans h.equiv) ∘ fun x ↦ (x, 0)) (h.domChart.extend I).target
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: case pos
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ↑z < y
⊢ z ∈ (if ↑z < y then IccLeftChart x y else IccRightChart x y).source

pp: case neg
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ¬↑z < y
⊢ z ∈ (if ↑z < y then IccLeftChart x y else IccRightChart x y).source

Tactic:
· simp only [h', if_true]
      exact h'

Goal state after:
case neg
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ¬↑z < y
⊢ z ∈ (if ↑z < y then IccLeftChart x y else IccRightChart x y).source
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: case neg
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : ¬MDiffAt f w
⊢ (mfderiv[Icc x y] (f ∘ projIcc x y ⋯) ↑w) 1 = (mfderiv% f w) 1

Tactic:
rw [mfderiv_zero_of_not_mdifferentiableAt hw, mfderivWithin_zero_of_not_mdifferentiableWithinAt]
    · rfl
    · rwa [mdifferentiableWithinAt_comp_projIcc_iff]

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

Goal state before:
pp: case h
𝕜 : 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 := t ∩ g ⁻¹' (extChartAt I (g x₀)).source
ht't : t' ⊆ t
hx₀gx₀ : (x₀, g x₀) ∈ t ×ˢ u
h4f✝ : ContinuousWithinAt (fun x ↦ f x (g x)) t x₀
h4f : (fun x ↦ f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝[t] x₀
h3f : ∀ᶠ (x' : N × M) in 𝓝[t ×ˢ u] (x₀, g x₀), ContMDiffWithinAt (J.prod I) I' 1 (uncurry f) (t ×ˢ u) x'
h2f : ∀ᶠ (x₂ : N) in 𝓝[t] x₀, ContMDiffWithinAt I I' 1 (f x₂) u (g x₂)
h2g : g ⁻¹' (extChartAt I (g x₀)).source ∈ 𝓝[t] x₀
this✝ :
  ContDiffWithinAt 𝕜 m
    (fun x ↦
      fderivWithin 𝕜 (↑(extChartAt I' (f x₀ (g x₀))) ∘ f (↑(extChartAt J x₀).symm x) ∘ ↑(extChartAt I (g x₀)).symm)
        ((extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u)
        (↑(extChartAt I (g x₀)) (g (↑(extChartAt J x₀).symm x))))
    (↑(extChartAt J x₀).symm ⁻¹' t' ∩ range ↑J) (↑(extChartAt J x₀) x₀)
this :
  ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (fun x ↦
      fderivWithin 𝕜 (↑(extChartAt I' (f x₀ (g x₀))) ∘ f x ∘ ↑(extChartAt I (g x₀)).symm)
        ((extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u) (↑(extChartAt I (g x₀)) (g x)))
    t' x₀
x : N
hx : ContMDiffWithinAt I I' 1 (f x) u (g x)
h'x : x ∈ (fun x ↦ f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source
h2 : x ∈ g ⁻¹' (extChartAt I (g x₀)).source
hxt : x ∈ t
h1 : g x ∈ u
h3 : UniqueMDiffAt[(extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u] (↑(extChartAt I (g x₀)) (g x))
A :
  mfderiv[range ↑I] ↑(extChartAt I (g x₀)).symm (↑(extChartAt I (g x₀)) (g x)) =
    mfderiv[(extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u] ↑(extChartAt I (g x₀)).symm
      (↑(extChartAt I (g x₀)) (g x))
⊢ (extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u ⊆ ↑(extChartAt I (g x₀)).symm ⁻¹' u

Tactic:
exact inter_subset_right

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: case e'_3.hs
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (ℝ ∙ ↑(-v))ᗮ.subtypeL (U.symm 0)
⊢ -↑v ∈ ℝ ∙ -↑v

Tactic:
exact Submodule.mem_span_singleton_self (-v : E)

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: case neg
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
a t : ℝ
ht : t ∈ Ioo (-a) a
hlt : a ≤ |t| + 1
⊢ (fun t ↦ γ (|t| + 1) t) t = γ a t

Tactic:
· exact eqOn_of_isMIntegralCurveOn_Ioo hv γ hγx hγ
      (neg_lt_self_iff.mp <| lt_trans ht.1 ht.2) hlt ht |>.symm

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
⊢ ContMDiff (𝓡∂ 1) I 1 f

Tactic:
rw [← contMDiffOn_comp_projIcc_iff]

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
⊢ ContMDiffOn 𝓘(ℝ, ℝ) I 1 (f ∘ projIcc 0 1 ⋯) (Icc 0 1)
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
t : ℝ
ht : t ∈ Icc 0 1
⊢ (f ∘ projIcc 0 1 ⋯) t = (γ ∘ ⇑η) t

Tactic:
simp only [Function.comp_apply, f, projIcc_of_mem, ht]

Goal state after: