mathlib-initiative/mathlib-tactics huggingface dataset:
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₄⟩
h_dist' : dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
hf2 : Fact (finrank ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := (finBasisOfFinrankEq ℝ ↥S.direction ⋯).orientation }
⊢ ¬Collinear ℝ {p₁', p', p₃'}

Tactic:
← affineIndependent_iff_not_collinear_set,

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₄⟩
h_dist' : dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
hf2 : Fact (finrank ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := (finBasisOfFinrankEq ℝ ↥S.direction ⋯).orientation }
⊢ AffineIndependent ℝ ![p₁', p', p₃']
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

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
s : Sphere P
p p' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
h : ¬p' = p
he : s.secondInter p (p' -ᵥ p) = p
⊢ False

Tactic:
Sphere.secondInter_eq_self_iff,

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
s : Sphere P
p p' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
h : ¬p' = p
he : ⟪p' -ᵥ p, p -ᵥ s.center⟫ = 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Similarity

Goal state before:
pp: case pos
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' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b 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')
heq : dist a' b' * dist c' b' * 2 = 0
⊢ ∠ a b c = ∠ a' b' c'

pp: case neg
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' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b 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')
heq : ¬dist a' b' * dist c' b' * 2 = 0
⊢ ∠ a b c = ∠ a' b' c'

Tactic:
· rw [mul_eq_zero_iff_right (by norm_num), mul_eq_zero] at heq
    rcases heq with h1 | h2
    · have h_dist_ab : dist a b = 0 := by grind
      rw [dist_eq_zero] at h_dist_ab h1
      simp_rw [h_dist_ab, h1, angle_self_left]
    · have h_dist_cb : dist c b = 0 := by grind
      rw [dist_eq_zero] at h_dist_cb h2
      simp_rw [h_dist_cb, h2, angle_self_right]

Goal state after:
case neg
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' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b 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')
heq : ¬dist a' b' * dist c' b' * 2 = 0
⊢ ∠ a b c = ∠ a' b' c'
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
n : WithTop ℕ∞
inst✝ : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : e ∈ atlas H M
he' : e' ∈ atlas H M
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : ↑(e.extend I) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange e e'
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
h : Surjective ⇑(fderivWithin 𝕜 (↑φ) φ.source (↑(e.extend I) x)) → ↑(e'.extend I) x ∈ interior (range ↑I)
⊢ ↑(e'.extend I) x ∈ interior (e'.extend I).target

Tactic:
refine e'.mem_interior_extend_target (by simp [hex']) <| h ?_
    exact (isInvertible_fderivWithin_extendCoordChange hn (IsManifold.subset_maximalAtlas he)
      (IsManifold.subset_maximalAtlas he') <| by simp [hex, hex']).surjective

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

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
U : Set M
c : M
hd : MDiff[U] f
hc : IsPreconnected U
ho : IsOpen[inst✝²] U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
⊢ U ⊆ V

Tactic:
have hVo : IsOpen V := by
    refine isOpen_iff_mem_nhds.2 fun x hx ↦ inter_mem (ho.mem_nhds hx.1) ?_
    replace hm : IsLocalMax (‖f ·‖) x :=
      mem_of_superset (ho.mem_nhds hx.1) fun z hz ↦ (hm hz).out.trans_eq hx.2.symm
    replace hd : ∀ᶠ y in 𝓝 x, MDiffAt f y :=
      (eventually_mem_nhds_iff.2 (ho.mem_nhds hx.1)).mono fun z ↦ hd.mdifferentiableAt
    exact (Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax hd hm).mono fun _ ↦
      (Eq.trans · hx.2)

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
U : Set M
c : M
hd : MDiff[U] f
hc : IsPreconnected U
ho : IsOpen[inst✝²] U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
hVo : IsOpen[inst✝²] V
⊢ U ⊆ V
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
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
⊢ (MDiffAt[s] fun x ↦
        (↑(extChartAt IB (f x₀).proj) (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).1,
          id (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).2))
      x₀ ↔
    (MDiffAt[s] fun x ↦ ↑(extChartAt IB (f x₀).proj) (f x).proj) x₀ ∧
      (MDiffAt[s] fun x ↦ id (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀

Tactic:
Function.id_def,

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
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
⊢ (MDiffAt[s] fun x ↦
        (↑(extChartAt IB (f x₀).proj) (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).1,
          (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).2))
      x₀ ↔
    (MDiffAt[s] fun x ↦ ↑(extChartAt IB (f x₀).proj) (f x).proj) x₀ ∧
      (MDiffAt[s] fun x ↦ (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀
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
E₁ : B → Type u_6
E₂ : B → Type u_7
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)
HB : Type u_9
inst✝⁸ : TopologicalSpace HB
inst✝⁷ : TopologicalSpace B
inst✝⁶ : ChartedSpace HB B
inst✝⁵ : FiberBundle F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₁ E₁
inst✝³ : FiberBundle F₂ E₂
inst✝² : VectorBundle 𝕜 F₂ E₂
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
y₀ y : TotalSpace (F₁ →L[𝕜] F₂) fun b ↦ E₁ b →L[𝕜] E₂ b
⊢ (fun p ↦ (↑(chartAt HB y₀.proj) p.1, id p.2))
      (↑(trivializationAt (F₁ →L[𝕜] F₂) (fun x ↦ E₁ x →L[𝕜] E₂ x) y₀.proj) y) =
    (↑(chartAt HB y₀.proj) y.proj, inCoordinates F₁ E₁ F₂ E₂ y₀.proj y.proj y₀.proj y.proj y.snd)

Tactic:
Function.id_def,

Goal state after:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
E₁ : B → Type u_6
E₂ : B → Type u_7
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)
HB : Type u_9
inst✝⁸ : TopologicalSpace HB
inst✝⁷ : TopologicalSpace B
inst✝⁶ : ChartedSpace HB B
inst✝⁵ : FiberBundle F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₁ E₁
inst✝³ : FiberBundle F₂ E₂
inst✝² : VectorBundle 𝕜 F₂ E₂
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
y₀ y : TotalSpace (F₁ →L[𝕜] F₂) fun b ↦ E₁ b →L[𝕜] E₂ b
⊢ (fun p ↦ (↑(chartAt HB y₀.proj) p.1, (fun x ↦ x) p.2))
      (↑(trivializationAt (F₁ →L[𝕜] F₂) (fun x ↦ E₁ x →L[𝕜] E₂ x) y₀.proj) y) =
    (↑(chartAt HB y₀.proj) y.proj, inCoordinates F₁ E₁ F₂ E₂ y₀.proj y.proj y₀.proj y.proj y.snd)
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
ht : t ∈ 𝓝 x
y : M
hy : y ∈ t
⊢ (s ∩ t) y = s y

Tactic:
change (y ∈ s ∩ t) = (y ∈ s)

Goal state after:
𝕜 : 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
ht : t ∈ 𝓝 x
y : M
hy : y ∈ t
⊢ (y ∈ s ∩ t) = (y ∈ s)
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

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
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
⊢ mpullback I I (fun x ↦ g * x) (mulInvariantVectorField v) h = mulInvariantVectorField v h

Tactic:
simp only [mpullback, inverse_mfderiv_mul_left, mulInvariantVectorField]

Goal state after:
𝕜 : 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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
⊢ ((mfderiv% fun b ↦ g⁻¹ * b) (g * h)) (((mfderiv% fun x ↦ g * h * x) 1) v) = ((mfderiv% fun x ↦ h * x) 1) v
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 : ℕ∞ω
g : M → N
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
⊢ IsOpen[inst✝³] {x | LiftSourceTargetPropertyAt I J n g x P}

Tactic:
by
  rw [isOpen_iff_forall_mem_open]
  intro x hx
  -- Suppose the lifted property `P` holds at `x`:
  -- choose slice charts `φ` near `x` and `ψ` near `f x` s.t. `P f φ ψ` holds.
  -- Then the same charts witness that `P f φ ψ` holds at any `y ∈ φ.source`.
  refine ⟨hx.domChart.source, fun y hy ↦ ?_, hx.domChart.open_source, hx.mem_domChart_source⟩
  exact ⟨hx.domChart, hx.codChart, hy, hx.source_subset_preimage_source hy,
    hx.domChart_mem_maximalAtlas, hx.codChart_mem_maximalAtlas, hx.source_subset_preimage_source,
    hx.property⟩

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
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
equiv : (E × F) ≃L[𝕜] E''
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : domChart ∈ IsManifold.maximalAtlas I n M
hcodChart : codChart ∈ IsManifold.maximalAtlas J n N
hsource : domChart.source ⊆ f ⁻¹' codChart.source
hwrittenInExtend :
  EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (⇑equiv ∘ fun x ↦ (x, 0)) (domChart.extend I).target
⊢ IsImmersionAtOfComplement F I J n f x

Tactic:
use domChart, codChart

Goal state after:
case property
𝕜 : 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
equiv : (E × F) ≃L[𝕜] E''
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : domChart ∈ IsManifold.maximalAtlas I n M
hcodChart : codChart ∈ IsManifold.maximalAtlas J n N
hsource : domChart.source ⊆ f ⁻¹' codChart.source
hwrittenInExtend :
  EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (⇑equiv ∘ fun x ↦ (x, 0)) (domChart.extend I).target
⊢ ImmersionAtProp F I J M N f domChart codChart
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
x✝⁶ : EuclideanSpace ℝ (Fin n)
hx : x✝⁶ ∈ {x | ∀ (i : Fin n), 0 ≤ x.ofLp i}
x✝⁵ : EuclideanSpace ℝ (Fin n)
hy : x✝⁵ ∈ {x | ∀ (i : Fin n), 0 ≤ x.ofLp i}
x✝⁴ x✝³ : ℝ
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
i : Fin n
⊢ 0 ≤ (x✝⁴ • x✝⁶ + x✝³ • x✝⁵).ofLp i

Tactic:
by dsimp at hx hy ⊢; specialize hx i; specialize hy i; positivity

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ interior (range ↑(𝓡∂ n)) = interior {y | 0 ≤ y.ofLp 0}

Tactic:
congr!

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ range ↑(𝓡∂ n) = {y | 0 ≤ y.ofLp 0}
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ frontier (range ↑(𝓡∂ n)) = frontier {y | 0 ≤ y.ofLp 0}

Tactic:
congr!

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ range ↑(𝓡∂ n) = {y | 0 ≤ y.ofLp 0}
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝²⁸ : NontriviallyNormedField 𝕜
E : Type u_2
E' : Type u_3
E''' : Type u_4
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 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
H' : Type u_8
inst✝¹⁴ : TopologicalSpace H'
G : Type u_9
inst✝¹³ : TopologicalSpace G
G' : Type u_10
inst✝¹² : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
M' : Type u_12
inst✝⁹ : TopologicalSpace M'
inst✝⁸ : ChartedSpace H' M'
N : Type u_13
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
N' : Type u_14
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f✝ : M → N
g✝ : M' → N'
x' : M'
inst✝³ : IsManifold I n M
inst✝² : IsManifold I' n M'
inst✝¹ : IsManifold J n N
inst✝ : IsManifold J' n N'
hf : IsImmersionAtOfComplement F I J n f✝ x
hg : IsImmersionAtOfComplement F' I' J' n g✝ x'
f : M → N
φ₁ : OpenPartialHomeomorph M H
ψ₁ : OpenPartialHomeomorph N G
g : M' → N'
φ₂ : OpenPartialHomeomorph M' H'
ψ₂ : OpenPartialHomeomorph N' G'
equiv₁ : (E × F) ≃L[𝕜] E''
hfprop : EqOn (↑(ψ₁.extend J) ∘ f ∘ ↑(φ₁.extend I).symm) (⇑equiv₁ ∘ fun x ↦ (x, 0)) (φ₁.extend I).target
equiv₂ : (E' × F') ≃L[𝕜] E'''
hgprop : EqOn (↑(ψ₂.extend J') ∘ g ∘ ↑(φ₂.extend I').symm) (⇑equiv₂ ∘ fun x ↦ (x, 0)) (φ₂.extend I').target
⊢ EqOn (Prod.fst ∘ ↑((ψ₁.extend J).prod (ψ₂.extend J')) ∘ Prod.map f g ∘ ↑((φ₁.extend I).prod (φ₂.extend I')).symm)
      (Prod.fst ∘
        ⇑((ContinuousLinearEquiv.prodProdProdComm 𝕜 E E' F F').trans (equiv₁.prodCongr equiv₂)) ∘ fun x ↦ (x, 0))
      ((φ₁.extend I).target ×ˢ (φ₂.extend I').target) ∧
    EqOn (Prod.snd ∘ ↑((ψ₁.extend J).prod (ψ₂.extend J')) ∘ Prod.map f g ∘ ↑((φ₁.extend I).prod (φ₂.extend I')).symm)
      (Prod.snd ∘
        ⇑((ContinuousLinearEquiv.prodProdProdComm 𝕜 E E' F F').trans (equiv₁.prodCongr equiv₂)) ∘ fun x ↦ (x, 0))
      ((φ₁.extend I).target ×ˢ (φ₂.extend I').target)

Tactic:
exact ⟨fun x ⟨hx, hx'⟩ ↦ by simpa using hfprop hx, fun x ⟨hx, hx'⟩ ↦ by simpa using hgprop hx'⟩

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

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : x < ↑p ∧ ↑p < y
⊢ 0 < (↑((IccLeftChart x y).extend (𝓡∂ 1)) p).ofLp 0

Tactic:
iccLeftChart_extend_zero

Goal state after:
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : x < ↑p ∧ ↑p < y
⊢ 0 < ↑p - x
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
hf : ContMDiff (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A : riemannianEDist I x y ≤ ∫⁻ (x_1 : ↑unitInterval), ‖(mfderiv% ⇑g x_1) 1‖ₑ
E : pathELength I (⇑g ∘ projIcc 0 1 ⋯) 0 1 = pathELength I (γ ∘ ⇑η) 0 1
⊢ MDiff[Icc (η 0) (η 1)] γ

Tactic:
simpa [η, ContinuousAffineMap.coe_lineMap_eq] using hγ.mdifferentiableOn one_ne_zero

Goal state after: