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

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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R ⁻¹' ↑(perpBisector c y) = sphere (inversion c R y) (R ^ 2 / dist y c) \ {c}

Tactic:
by
  rw [← dist_inversion_center, ← preimage_inversion_perpBisector_inversion hR,
    inversion_inversion] <;> simp [*]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
f : ι' → ι
r : ℝ≥0
hr : r ≠ 0
h : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)
x✝¹ x✝ : ι'
⊢ edist ((v₁ ∘ f) x✝¹) ((v₁ ∘ f) x✝) = ↑r * edist ((v₂ ∘ f) x✝¹) ((v₂ ∘ f) x✝)

Tactic:
apply h

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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
h_not_col : ¬Collinear ℝ {a, b, c}
h_not_col' : ¬Collinear ℝ {a', b', c'}
h : ∠ a b c = ∠ a' b' c'
dist_a'b' : dist a' b' ≠ 0
dist_b'c' : dist b' c' ≠ 0
k : ℝ := dist a b / dist a' b'
hd : k = dist b c / dist b' c'
hk : k = dist a b / dist a' b'
k_pos : 0 < k
h_ab : dist a b = k * dist a' b'
h_bc : dist c b = k * dist c' b'
hcos : dist a c ^ 2 = k ^ 2 * (dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c'))
hcos' :
  dist a' c' * dist a' c' =
    dist a' b' * dist a' b' + dist c' b' * dist c' b' - 2 * dist a' b' * dist c' b' * Real.cos (∠ a' b' c')
⊢ ![a, b, c] ∼ ![a', b', c']

Tactic:
field_simp at hcos'

Goal state after:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
h_not_col : ¬Collinear ℝ {a, b, c}
h_not_col' : ¬Collinear ℝ {a', b', c'}
h : ∠ a b c = ∠ a' b' c'
dist_a'b' : dist a' b' ≠ 0
dist_b'c' : dist b' c' ≠ 0
k : ℝ := dist a b / dist a' b'
hd : k = dist b c / dist b' c'
hk : k = dist a b / dist a' b'
k_pos : 0 < k
h_ab : dist a b = k * dist a' b'
h_bc : dist c b = k * dist c' b'
hcos : dist a c ^ 2 = k ^ 2 * (dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c'))
hcos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
⊢ ![a, b, c] ∼ ![a', b', c']
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
P : Type u_2
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
⊢ ∠ p₁ p p₄ = ∠ p₃ p p₂

Tactic:
grind [angle_comm, angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi hp₃p₄]

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₁ 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 _ hi
    simp [hfs i hi]

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
P : Type u_2
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ {p₁, p₂, p₃}
h_notcol_p₁pp₄ : ¬Collinear ℝ {p₁, p, p₄}
h_notcol_p₃pp₂ : ¬Collinear ℝ {p₃, p, p₂}
⊢ Similar ![p₁, p, p₄] ![p₃, p, p₂]

Tactic:
apply similar_of_side_angle_side h_notcol_p₁pp₄ h_notcol_p₃pp₂ h_angle_eq ?_

Goal state after:
V : Type u_1
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
P : Type u_2
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ {p₁, p₂, p₃}
h_notcol_p₁pp₄ : ¬Collinear ℝ {p₁, p, p₄}
h_notcol_p₃pp₂ : ¬Collinear ℝ {p₃, p, p₂}
⊢ dist p₁ p * dist p p₂ = dist p p₄ * dist p₃ p
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := S.subtypeₐᵢ
⊢ Cospherical {p₁, p₂, p₃, p₄}

Tactic:
let p₁' : S := ⟨p₁, mem_affineSpan ℝ (s := Set.range t.points) (by aesop)⟩

Goal state after:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := S.subtypeₐᵢ
p₁' : ↥S := ⟨p₁, ⋯⟩
⊢ Cospherical {p₁, p₂, p₃, p₄}
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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
x : M
h : I.IsInteriorPoint x ∧ I.IsBoundaryPoint x
⊢ ↑(extChartAt I x) x ∈ interior ?m.84 ∧ ↑(extChartAt I x) x ∈ frontier ?m.84

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
x : M
h : I.IsInteriorPoint x ∧ I.IsBoundaryPoint x
⊢ Set E

Tactic:
exact h

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
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left✝ : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : affineSpan ℝ s = affineSpan ℝ (Set.range t.points)
hfd : FiniteDimensional ℝ ↥(affineSpan ℝ s).direction
⊢ 2 = finrank ℝ ↥(vectorSpan ℝ (Set.range t.points))

Tactic:
t.independent.finrank_vectorSpan (Fintype.card_fin _)

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
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left✝ : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : affineSpan ℝ s = affineSpan ℝ (Set.range t.points)
hfd : FiniteDimensional ℝ ↥(affineSpan ℝ s).direction
⊢ 2 = 2
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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'✝
N✝ : Type u_7
inst✝¹² : TopologicalSpace N✝
inst✝¹¹ : ChartedSpace H'✝ N✝
𝕜 : 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'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h✝ : IsRCLikeNormedField 𝕜
x✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝ : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x)
hf' : Surjective ⇑(fderiv ℝ (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x))
⊢ I'.IsInteriorPoint (f x)

Tactic:
replace hf'' := hf''.restrictScalars ℝ

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'✝
N✝ : Type u_7
inst✝¹² : TopologicalSpace N✝
inst✝¹¹ : ChartedSpace H'✝ N✝
𝕜 : 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'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h✝ : IsRCLikeNormedField 𝕜
x✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝ : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' : Surjective ⇑(fderiv ℝ (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x))
hf'' : DifferentiableAt ℝ (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x)
⊢ I'.IsInteriorPoint (f x)
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: case mpr
𝕜 : 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'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux : interior (range ↑I) ×ˢ interior (range ↑J) = interior (range ↑(I.prod J))
hp : p ∈ ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N
h : p.1 ∈ {x | I.IsInteriorPoint x} ∧ p.2 ∈ ModelWithCorners.interior N
⊢ (↑(extChartAt (I.prod J) p) p).1 ∈ interior (range ↑I) ∧ (↑(extChartAt (I.prod J) p) p).2 ∈ interior (range ↑J)

Tactic:
exact h

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_6
inst✝²⁸ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E₁ : B → Type u_7
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)
E₂ : B → Type u_8
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)
EB : Type u_10
inst✝¹⁵ : NormedAddCommGroup EB
inst✝¹⁴ : NormedSpace 𝕜 EB
HB : Type u_11
inst✝¹³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹² : TopologicalSpace B
inst✝¹¹ : ChartedSpace HB B
EM : Type u_12
inst✝¹⁰ : NormedAddCommGroup EM
inst✝⁹ : NormedSpace 𝕜 EM
HM : Type u_13
inst✝⁸ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace HM M
inst✝⁵ : FiberBundle F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₁ E₁
inst✝³ : FiberBundle F₂ E₂
inst✝² : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
x : M
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)
hv : ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F₁)) n (fun m ↦ ⟨b m, v m⟩) s x
hϕ :
  ContMDiffWithinAt IM IB n (fun x ↦ b x) s x ∧
    ContMDiffWithinAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂) n (fun x_1 ↦ inCoordinates F₁ E₁ F₂ E₂ (b x) (b x_1) (b x) (b x_1) (ϕ x_1)) s
      x
⊢ ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F₂)) n (fun m ↦ ⟨b m, (ϕ m) (v m)⟩) s x

Tactic:
exact hϕ.2.clm_apply_of_inCoordinates hv hϕ.1

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_6
inst✝²⁸ : NontriviallyNormedField 𝕜
E₁ : B → Type u_7
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)
E₂ : B → Type u_8
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)
EB : Type u_10
inst✝¹⁵ : NormedAddCommGroup EB
inst✝¹⁴ : NormedSpace 𝕜 EB
HB : Type u_11
inst✝¹³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹² : TopologicalSpace B
inst✝¹¹ : ChartedSpace HB B
EM : Type u_12
inst✝¹⁰ : NormedAddCommGroup EM
inst✝⁹ : NormedSpace 𝕜 EM
HM : Type u_13
inst✝⁸ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace HM M
inst✝⁵ : FiberBundle F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₁ E₁
inst✝³ : FiberBundle F₂ E₂
inst✝² : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
x : M
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)
hv : MDiffAt[s] (T% v) x
hϕ : (MDiffAt[s] fun x ↦ b x) x ∧ (MDiffAt[s] fun x_1 ↦ inCoordinates F₁ E₁ F₂ E₂ (b x) (b x_1) (b x) (b x_1) (ϕ x_1)) x
⊢ (MDiffAt[s] fun m ↦ ⟨b m, (ϕ m) (v m)⟩) x

Tactic:
exact hϕ.2.clm_apply_of_inCoordinates hv hϕ.1

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

Goal state before:
pp: case refine_2
𝕜 : 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
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → TopologicalSpace (V x)
inst✝¹ : FiberBundle F V
inst✝ : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization F TotalSpace.proj := trivializationAt F V x
w : F := (↑t ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) k (fun _x ↦ w) x
⊢ x ∈ t.baseSet

Tactic:
· exact FiberBundle.mem_baseSet_trivializationAt' x

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

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
V : M → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F V)
inst✝⁷ : (x : M) → AddCommGroup (V x)
inst✝⁶ : (x : M) → TopologicalSpace (V x)
inst✝⁵ : FiberBundle F V
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : (x : M) → Module 𝕜 (V x)
W : Type u_7
inst✝² : AddCommGroup W
inst✝¹ : Module 𝕜 W
inst✝ : TopologicalSpace W
x : M
⊢ Function.Injective fun A Z x_1 ↦ A (Z x)

Tactic:
intro X X' h
  ext σ₀
  simpa using congr($h (extend F σ₀) (mdifferentiableAt_extend ..))

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

Goal state before:
pp: 𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
M : Type u_13
inst✝²⁰ : NontriviallyNormedField 𝕜
E₁ : B → Type u_14
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)
E₂ : B → Type u_15
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 M
inst✝⁵ : FiberBundle F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₁ E₁
inst✝³ : FiberBundle F₂ E₂
inst✝² : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
x : M
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)
hv : ContinuousWithinAt (fun m ↦ TotalSpace.mk' F₁ (b m) (v m)) s x
hϕ :
  ContinuousWithinAt (fun x ↦ b x) s x ∧
    ContinuousWithinAt (fun x_1 ↦ inCoordinates F₁ E₁ F₂ E₂ (b x) (b x_1) (b x) (b x_1) (ϕ x_1)) s x
⊢ ContinuousWithinAt (fun m ↦ TotalSpace.mk' F₂ (b m) ((ϕ m) (v m))) s x

Tactic:
exact hϕ.2.clm_apply_of_inCoordinates hv hϕ.1

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

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
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ mlieBracketWithin I V W s x = mlieBracketWithin I V W t x

Tactic:
simp only [mlieBracketWithin_apply]
  congr 1
  suffices A : ((extChartAt I x).symm ⁻¹' s ∩ range I : Set E)
    =ᶠ[𝓝[{(extChartAt I x) x}ᶜ] (extChartAt I x x)]
      ((extChartAt I x).symm ⁻¹' t ∩ range I : Set E) by
    apply lieBracketWithin_congr_set' _ A
  exact preimage_extChartAt_eventuallyEq_compl_singleton y h

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

Goal state before:
pp: case hn
𝕜 : 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
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ minSmoothness 𝕜 2 ≤ minSmoothness 𝕜 3

Tactic:
· exact minSmoothness_monotone (by norm_cast)

Goal state after:
Module: Mathlib.Topology.Homeomorph.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
e : α ≃ β
this : TopologicalSpace α := e.topologicalSpace
⊢ Continuous ⇑e.symm

Tactic:
convert! continuous_coinduced_rng

Goal state after:
case e'_4
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
e : α ≃ β
this : TopologicalSpace α := e.topologicalSpace
⊢ e.topologicalSpace = TopologicalSpace.coinduced (⇑e.symm) inst✝
Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic

Goal state before:
pp: case mpr
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
⊢ (∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)) → ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s

Tactic:
· intro ⟨ε, hε, h⟩
    exact ⟨Metric.ball t₀ ε, Metric.ball_mem_nhds _ hε, h⟩

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

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
h : ∀ (t : ℝ), IsMIntegralCurveAt γ v t
t : ℝ
⊢ HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))

Tactic:
by
    obtain ⟨s, hs, h⟩ := isMIntegralCurveAt_iff.mp (h t)
    exact h t (mem_of_mem_nhds hs) |>.hasMFDerivAt hs

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv✝ : ‖v‖ = 1
x : ↑(sphere 0 1)
hv : ‖↑x‖ = 1
hx : x ∈ {⟨v, ⋯⟩}ᶜ
h : ↑x = v
⊢ ↑x = v

Tactic:
exact h

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

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun x ↦ x + dt) v (Metric.ball (t₀ - dt) ε)

Tactic:
refine ⟨ε, hε, ?_⟩

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ IsMIntegralCurveOn (γ ∘ fun x ↦ x + dt) v (Metric.ball (t₀ - dt) ε)