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:
preimage_inversion_perpBisector hR hy

Goal state after:
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
⊢ sphere (inversion c R y) (R ^ 2 / dist y c) \ {c} = sphere (inversion c R y) (R ^ 2 / dist y c) \ {c}
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ Similar v₁ v₂ ↔ ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)

Tactic:
simp_rw [similar_iff_exists_pairwise_edist_eq, edist_nndist]

Goal state after:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ (∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ ↑(nndist (v₁ i₁) (v₁ i₂)) = ↑r * ↑(nndist (v₂ i₁) (v₂ i₂))) ↔
    ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)
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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).AcuteAngled ↔ s.AcuteAngled

Tactic:
by
  refine ⟨fun h {i₁ i₂ i₃} h₁₂ h₁₃ h₂₃ ↦ ?_, fun h {i₁ i₂ i₃} h₁₂ h₁₃ h₂₃ ↦ ?_⟩
  · convert! h (i₁ := e i₁) (i₂ := e i₂) (i₃ := e i₃) ?_ ?_ ?_ using 1 <;> simp [*]
  · convert! h (i₁ := e.symm i₁) (i₂ := e.symm i₂) (i₃ := e.symm i₃) ?_ ?_ ?_ using 1 <;> simp [*]

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

Goal state before:
pp: case neg
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₂
⊢ ⟪(univ.weightedVSub s.pointsWithCircumcenter) (mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂),
      (univ.weightedVSub s.pointsWithCircumcenter)
        (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂)⟫ =
    0

Tactic:
have hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0 := by
    simp

Goal state after:
case neg
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
⊢ ⟪(univ.weightedVSub s.pointsWithCircumcenter) (mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂),
      (univ.weightedVSub s.pointsWithCircumcenter)
        (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂)⟫ =
    0
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ₐᵢ
p₁' : ↥S := ⟨p₁, ⋯⟩
p' : ↥S := ⟨p, ⋯⟩
p₃' : ↥S := ⟨p₃, ⋯⟩
p₂' : ↥S := ⟨p₂, hp₂⟩
⊢ Cospherical {p₁, p₂, p₃, p₄}

Tactic:
let p₄' : S := ⟨p₄, hp₄⟩

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₁, ⋯⟩
p' : ↥S := ⟨p, ⋯⟩
p₃' : ↥S := ⟨p₃, ⋯⟩
p₂' : ↥S := ⟨p₂, hp₂⟩
p₄' : ↥S := ⟨p₄, hp₄⟩
⊢ Cospherical {p₁, p₂, 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ₐᵢ
p₁' : ↥S := ⟨p₁, ⋯⟩
p' : ↥S := ⟨p, ⋯⟩
p₃' : ↥S := ⟨p₃, ⋯⟩
p₂' : ↥S := ⟨p₂, hp₂⟩
p₄' : ↥S := ⟨p₄, hp₄⟩
⊢ dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'

Tactic:
simpa [dist_eq_norm_vsub, ← s_isom.dist_map] using 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₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos :
  r * dist a' c' * (r * dist a' c') =
    r * dist a' b' * (r * dist a' b') + r * dist c' b' * (r * dist c' b') -
      2 * (r * dist a' b') * (r * dist c' b') * Real.cos (∠ a b c)
⊢ ∠ a b c = ∠ a' b' c'

Tactic:
field_simp at h_cos

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₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : 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.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
⊢ ∃ r, ∀ (t : Triangle ℝ P), Set.range t.points ⊆ s → Simplex.circumradius t = r

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

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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
⊢ ∃ r, ∀ (t : Triangle ℝ P), Set.range t.points ⊆ s → Simplex.circumradius t = r
Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent

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
p : TangentBundle I M
q : TangentBundle I H
h : q.proj ∈ (chartAt H p.proj).target
⊢ tangentMap I I (↑(chartAt H p.proj).symm) q = ↑(chartAt (ModelProd H E) p).symm ((TotalSpace.toProd H E) q)

Tactic:
by
  dsimp only [tangentMap]
  rw [MDifferentiableAt.mfderiv (mdifferentiableAt_atlas_symm (chart_mem_atlas _ _) h)]
  simp only [TangentBundle.chartAt, tangentBundleCore,
    mfld_simps]
  -- `simp` fails to apply `PartialEquiv.prod_symm` with `ModelProd`
  congr
  exact ((chartAt H (TotalSpace.proj p)).right_inv h).symm

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
s : (x : B) → E x
u : Set B
x₀ : B
hs : MDiffAt[u] (T% s) x₀
⊢ (MDiffAt[u] fun x ↦ ⟨x, (-s) x⟩) x₀

Tactic:
rw [mdifferentiableWithinAt_section] at hs ⊢

Goal state after:
𝕜 : 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
s : (x : B) → E x
u : Set B
x₀ : B
hs : (MDiffAt[u] fun b ↦ (↑(trivializationAt F E x₀) ⟨b, s b⟩).2) x₀
⊢ (MDiffAt[u] fun b ↦ (↑(trivializationAt F E x₀) ⟨b, (-s) b⟩).2) x₀
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
s : (x : B) → E x
x₀ : B
hs : MDiffAt[univ] (T% s) x₀
⊢ (MDiffAt[univ] fun x ↦ ⟨x, (-s) x⟩) x₀

Tactic:
exact mdifferentiableWithinAt_neg_section hs

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
f : B → 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hf : MDiffAt[u] f x₀
hs : MDiffAt[u] (T% s) x₀
⊢ (MDiffAt[u] fun x ↦ ⟨x, (f • s) x⟩) x₀

Tactic:
rw [mdifferentiableWithinAt_section] at hs ⊢

Goal state after:
𝕜 : 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
f : B → 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hf : MDiffAt[u] f x₀
hs : (MDiffAt[u] fun b ↦ (↑(trivializationAt F E x₀) ⟨b, s b⟩).2) x₀
⊢ (MDiffAt[u] fun b ↦ (↑(trivializationAt F E x₀) ⟨b, (f • s) b⟩).2) x₀
Module: Mathlib.Topology.VectorBundle.Hom

Goal state before:
pp: 𝕜₁ : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝²⁰ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁹ : NormedAddCommGroup F₁
inst✝¹⁸ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁷ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁶ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹⁵ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹⁴ : NormedAddCommGroup F₂
inst✝¹³ : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝¹² : (x : B) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : TopologicalSpace B
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁸ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁷ : FiberBundle F₁ E₁
inst✝⁶ : VectorBundle 𝕜₁ F₁ E₁
inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
inst✝³ : VectorBundle 𝕜₂ F₂ E₂
inst✝² : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝¹ : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)
inst✝ : RingHomIsometric σ
⊢ ∀ (b : B),
    IsInducing (↑(continuousLinearMap σ (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) ∘ TotalSpace.mk b)

Tactic:
intro b

Goal state after:
𝕜₁ : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝²⁰ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁹ : NormedAddCommGroup F₁
inst✝¹⁸ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁷ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁶ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹⁵ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹⁴ : NormedAddCommGroup F₂
inst✝¹³ : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝¹² : (x : B) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : TopologicalSpace B
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁸ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁷ : FiberBundle F₁ E₁
inst✝⁶ : VectorBundle 𝕜₁ F₁ E₁
inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
inst✝³ : VectorBundle 𝕜₂ F₂ E₂
inst✝² : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝¹ : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)
inst✝ : RingHomIsometric σ
b : B
⊢ IsInducing (↑(continuousLinearMap σ (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) ∘ TotalSpace.mk b)
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
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
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
⊢ ↑(h.codChart.extend J) '' f '' h.domChart.source ⊆ (h.codChart.extend J).target

Tactic:
← PartialEquiv.image_source_eq_target

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
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
⊢ ↑(h.codChart.extend J) '' f '' h.domChart.source ⊆ ↑(h.codChart.extend J) '' (h.codChart.extend J).source
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ Convex ℝ {y | 0 ≤ y.ofLp 0}

Tactic:
exact EuclideanHalfSpace.convex (n := n)

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

Goal state before:
pp: n : ℕ
⊢ Convex ℝ (range Subtype.val)

Tactic:
rw [range_euclideanQuadrant]

Goal state after:
n : ℕ
⊢ Convex ℝ {y | ∀ (i : Fin n), 0 ≤ y.ofLp i}
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
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
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
⊢ ContMDiffOn I J n f h.domChart.source

Tactic:
rw [← h.domChart.contMDiffOn_writtenInExtend_iff h.domChart_mem_maximalAtlas
    h.codChart_mem_maximalAtlas le_rfl h.mapsto_domChart_source_codChart_source,
    ← h.domChart.extend_target_eq_image_source]

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
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
⊢ ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E'') n (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm)
    (h.domChart.extend I).target
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) :=
  ContinuousLinearEquiv.prodUnique ℝ (EuclideanSpace ℝ (Fin 1)) Unit
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := φ₀.trans (PiLp.equivOfUnique 2 ℝ fun x ↦ ℝ)
hz : ↑z < y
⊢ (Homeomorph.addLeft (-x)).toOpenPartialHomeomorph ∈ maximalAtlas 𝓘(ℝ, ℝ) n ℝ

pp: case pos
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) := ⋯
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := ⋯
hz : ↑z < y
⊢ EqOn
    (↑((Homeomorph.addLeft (-x)).toOpenPartialHomeomorph.extend 𝓘(ℝ, ℝ)) ∘
      (fun z ↦ ↑z) ∘ ↑((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).symm)
    (⇑φ ∘ fun x ↦ (x, 0)) ((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).target

Tactic:
· apply OpenPartialHomeomorph.mem_maximalAtlas_of_contMDiffOn
      · have : ContDiff ℝ n (fun y ↦ -x + y) := by fun_prop
        simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ]
      · have : ContDiff ℝ n (fun y ↦ x + y) := by fun_prop
        simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ, Homeomorph.addLeft]

Goal state after:
case pos
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) := ⋯
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := ⋯
hz : ↑z < y
⊢ EqOn
    (↑((Homeomorph.addLeft (-x)).toOpenPartialHomeomorph.extend 𝓘(ℝ, ℝ)) ∘
      (fun z ↦ ↑z) ∘ ↑((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).symm)
    (⇑φ ∘ fun x ↦ (x, 0)) ((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).target
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ¬↑(projIcc x y ⋯ z) < y
this✝ :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x ↦ y - w;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
this : y - max x (min y w) = y - w
⊢ (((Subtype.val ∘ ↑(IccRightChart x y)) ∘ projIcc x y ⋯ ∘ ↑(chartAt ℝ z).symm) w).ofLp i =
    (have this := toLp 2 fun x ↦ y - w;
        this).ofLp
      i

Tactic:
simpa [modelWithCornersEuclideanHalfSpace, IccRightChart]

Goal state after:
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 : M → M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiff[s]
x₀ : TangentBundle I M
hx₀ : x₀ ∈ TotalSpace.proj ⁻¹' s
s' : Set (TangentBundle I M) := TotalSpace.proj ⁻¹' s
⊢ ContMDiffWithinAt I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s) x₀

Tactic:
let b₁ : TangentBundle I M → M := fun p ↦ p.1

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 : M → M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiff[s]
x₀ : TangentBundle I M
hx₀ : x₀ ∈ TotalSpace.proj ⁻¹' s
s' : Set (TangentBundle I M) := TotalSpace.proj ⁻¹' s
b₁ : TangentBundle I M → M := fun p ↦ p.proj
⊢ ContMDiffWithinAt I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s) x₀
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: case hxs
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)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ UniqueDiffWithinAt ℝ (Icc a b) t

Tactic:
exact uniqueDiffOn_Icc h _ ht

Goal state after: