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

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
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ ↥⊤.direction = n
hc : Cospherical ps
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c

Tactic:
refine exists_circumcenter_eq_of_cospherical_subset ?_ hd hc

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ ↥⊤.direction = n
hc : Cospherical ps
⊢ ps ⊆ ↑⊤
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : ¬angle y z = π
H6 :
  Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle x y) * Real.sin (angle y z) *
        ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
Hw : Real.sin (angle x y) * Real.sin (angle y z) ≠ 0
H8 : ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫ = -1
H9 : ortho y x ≠ 0
⊢ ortho y z ≠ 0

Tactic:
grind [ortho_ne_zero_of_not_collinear]

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

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 : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
hs :
  SignType.sign
      (s.touchpointWeights signs i j * ‖s.points j -ᵥ ↑((s.faceOpposite j).orthogonalProjectionSpan (s.points j))‖) =
    SignType.sign (s.excenterWeights signs j)
⊢ SignType.sign (s.touchpointWeights signs i j) = SignType.sign (s.excenterWeights signs j)

Tactic:
← hs,

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
hs :
  SignType.sign
      (s.touchpointWeights signs i j * ‖s.points j -ᵥ ↑((s.faceOpposite j).orthogonalProjectionSpan (s.points j))‖) =
    SignType.sign (s.excenterWeights signs j)
⊢ SignType.sign (s.touchpointWeights signs i j) =
    SignType.sign
      (s.touchpointWeights signs i j * ‖s.points j -ᵥ ↑((s.faceOpposite j).orthogonalProjectionSpan (s.points j))‖)
Module: Mathlib.Geometry.Euclidean.Congruence

Goal state before:
pp: P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ ![a, b, c] ≅ ![a', b', c']

Tactic:
rw [triangle_congruent_iff_dist_eq]
  intro i j
  fin_cases i <;> fin_cases j <;> simp_all [dist_comm]

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

Goal state before:
pp: case inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
⊢ Simplex.excenter t Finset.univ = Simplex.incenter t ∨ ∃ i, Simplex.excenter t Finset.univ = Simplex.excenter t {i}

Tactic:
exact .inl t.excenter_univ

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ line[ℝ, t.points i₂, t.points i₃].SSameSide (Simplex.excenter t {i₂}) (t.points i₁)

Tactic:
by
  convert! t.sSameSide_excenter_singleton_point h₁₂
  simp
  grind

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

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 : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ ‖↑n‖ * ‖s.faceOppositeCentroid i -ᵥ (((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖

Tactic:
← norm_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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ ‖↑n • (s.faceOppositeCentroid i -ᵥ (((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case h
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := ⋯
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
⊢ 0 < r ∧ Pairwise fun i₁ i₂ ↦ dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)

Tactic:
refine ⟨hr_pos, ?_⟩

Goal state after:
case h
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
⊢ Pairwise fun i₁ i₂ ↦ dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
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 q : P
hp : p ∈ s
p' : P
hp' : p' ∈ line[ℝ, p, q]
⊢ p' = p ∨ p' = s.secondInter p (q -ᵥ p) ↔ p' ∈ s

Tactic:
convert! s.eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem hp ?_
  convert! hp'
  rw [AffineSubspace.eq_iff_direction_eq_of_mem (AffineSubspace.self_mem_mk' p _)
    (left_mem_affineSpan_pair _ _ _)]
  simp [direction_affineSpan, vectorSpan_pair_rev]

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

Goal state before:
pp: case zero
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)
hn₁ : ¬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 = ↑(closure ↑X)
⊢ X ^ (n + 0) = X ^ n

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: E : Type u_5
H : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, F a < F (f x)
h : ∀ (y : E), F ((fderiv ℝ f x) y) = 0
y : H
hy : y ∈ interior s
⊢ ¬Surjective ⇑(fderiv ℝ f x)

Tactic:
unfold Function.Surjective

Goal state after:
E : Type u_5
H : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, F a < F (f x)
h : ∀ (y : E), F ((fderiv ℝ f x) y) = 0
y : H
hy : y ∈ interior s
⊢ ¬∀ (b : H), ∃ a, (fderiv ℝ f x) a = b
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; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
X : LeftInvariantDerivation I G
g : G
⊢ (𝒅ₕ ⋯) ((Derivation.evalAt 1) (r • ↑X)) = (Derivation.evalAt g) (r • ↑X)

Tactic:
simp only [LinearMap.map_smul_of_tower, map_smul]

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; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
X : LeftInvariantDerivation I G
g : G
⊢ r • (𝒅ₕ ⋯) ((Derivation.evalAt 1) ↑X) = r • (Derivation.evalAt g) ↑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✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
inst✝³ : Trivialization.IsLinear 𝕜₁ e₁
inst✝² : Trivialization.IsLinear 𝕜₁ e₁'
inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂
inst✝ : Trivialization.IsLinear 𝕜₂ e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
L : F₁ →SL[σ] F₂
v : F₁
⊢ (↑(Trivialization.coordChangeL 𝕜₂ e₂ e₂' b) ∘SL L ∘SL ↑(Trivialization.coordChangeL 𝕜₁ e₁' e₁ b).symm.symm) v =
    (↑(continuousLinearMap σ e₁' e₂') { proj := b, snd := (continuousLinearMap σ e₁ e₂).symm b L }).2 v

Tactic:
continuousLinearMap_apply,

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✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
inst✝³ : Trivialization.IsLinear 𝕜₁ e₁
inst✝² : Trivialization.IsLinear 𝕜₁ e₁'
inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂
inst✝ : Trivialization.IsLinear 𝕜₂ e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
L : F₁ →SL[σ] F₂
v : F₁
⊢ (↑(Trivialization.coordChangeL 𝕜₂ e₂ e₂' b) ∘SL L ∘SL ↑(Trivialization.coordChangeL 𝕜₁ e₁' e₁ b).symm.symm) v =
    (Trivialization.continuousLinearMapAt 𝕜₂ e₂' b ∘SL
        (continuousLinearMap σ e₁ e₂).symm b L ∘SL Trivialization.symmL 𝕜₁ e₁' b)
      v
Module: Mathlib.Geometry.Manifold.VectorBundle.Hom

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
inst✝¹⁷ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
EB : Type u_4
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹³ : TopologicalSpace B
inst✝¹² : ChartedSpace HB B
E₁ : B → Type u_6
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), IsTopologicalAddGroup (E₁ x)
inst✝⁴ : ∀ (x : B), ContinuousSMul 𝕜 (E₁ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : ContMDiffVectorBundle n F₁ E₁ IB
e : Trivialization F₁ TotalSpace.proj
inst✝ : MemTrivializationAtlas e
x : B
hx : x ∈ e.baseSet
hx' : x ∈ (trivializationAt F₁ E₁ x).baseSet
b : B
hb : b ∈ e.baseSet
⊢ b ∈ (trivializationAt F₁ E₁ x).baseSet →
    (↑(trivializationAt (F₁ →L[𝕜] F₁) (fun x ↦ F₁ →L[𝕜] E₁ x) x) ⟨b, symmL 𝕜 e b⟩).2 =
      ↑(coordChangeL 𝕜 e (trivializationAt F₁ E₁ x) b)

Tactic:
hb'

Goal state after:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
inst✝¹⁷ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
EB : Type u_4
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹³ : TopologicalSpace B
inst✝¹² : ChartedSpace HB B
E₁ : B → Type u_6
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), IsTopologicalAddGroup (E₁ x)
inst✝⁴ : ∀ (x : B), ContinuousSMul 𝕜 (E₁ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : ContMDiffVectorBundle n F₁ E₁ IB
e : Trivialization F₁ TotalSpace.proj
inst✝ : MemTrivializationAtlas e
x : B
hx : x ∈ e.baseSet
hx' : x ∈ (trivializationAt F₁ E₁ x).baseSet
b : B
hb : b ∈ e.baseSet
hb' : b ∈ (trivializationAt F₁ E₁ x).baseSet
⊢ (↑(trivializationAt (F₁ →L[𝕜] F₁) (fun x ↦ F₁ →L[𝕜] E₁ x) x) ⟨b, symmL 𝕜 e b⟩).2 =
    ↑(coordChangeL 𝕜 e (trivializationAt F₁ E₁ x) b)
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
D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ fun x ↦ g * h * x
⊢ ((mfderiv% fun b ↦ g⁻¹ * b) (g * h)) (((mfderiv% fun x ↦ g * h * x) 1) v) =
    (mfderiv% ((fun b ↦ g⁻¹ * b) ∘ fun x ↦ g * h * x) 1) v

Tactic:
mfderiv_comp (I' := I)

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
D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ fun x ↦ g * h * x
⊢ ((mfderiv% fun b ↦ g⁻¹ * b) (g * h)) (((mfderiv% fun x ↦ g * h * x) 1) v) =
    ((mfderiv% fun b ↦ g⁻¹ * b) (g * h * 1) ∘SL (mfderiv% fun x ↦ g * h * x) 1) v

case hg
𝕜 : 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
D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ fun x ↦ g * h * x
⊢ (MDiffAt fun b ↦ g⁻¹ * b) (g * h * 1)

case hf
𝕜 : 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
D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ fun x ↦ g * h * x
⊢ (MDiffAt fun x ↦ g * h * x) 1
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
N : Type u_13
inst✝ : TopologicalSpace N
f g : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hfg : EqOn f g φ.source
⊢ ImmersionAtProp F I J M N f φ ψ → ImmersionAtProp F I J M N g φ ψ

Tactic:
intro ⟨equiv, hf⟩

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
N : Type u_13
inst✝ : TopologicalSpace N
f g : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hfg : EqOn f g φ.source
equiv : (E × F) ≃L[𝕜] E''
hf : EqOn (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (⇑equiv ∘ fun x ↦ (x, 0)) (φ.extend I).target
⊢ ImmersionAtProp F I J M N g φ ψ
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case hf
𝕜 : 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'
inst✝³ : IsManifold I 2 M
inst✝² : IsManifold I' 2 M'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
A' : x₀ = ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)
h'f : MDiffAt[s] f x₀
this : (mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)).inverse = mfderiv% ↑(extChartAt I x₀) x₀
⊢ MDiffAt[↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)

Tactic:
exact (mdifferentiableWithinAt_extChartAt_symm (mem_extChartAt_target x₀)).mono
      inter_subset_right

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

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
⊢ ↑((IccLeftChart x y).extend (𝓡∂ 1)) ⊥ ∈ frontier (range ↑(𝓡∂ 1))

Tactic:
by
  rw [IccLeftChart_extend_bot, frontier_range_modelWithCornersEuclideanHalfSpace,
    mem_ofPred, PiLp.zero_apply]

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

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
z : EuclideanHalfSpace 1
hz : (↑z).ofLp 0 ≤ y - x
⊢ ↑(IccRightChart x y).symm z = ⟨y - (↑z).ofLp 0, ⋯⟩

Tactic:
ext
  simp only [IccRightChart_symm_apply, sup_eq_left]
  linarith

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

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
⊢ (𝓡∂ 1).IsBoundaryPoint ⊥

Tactic:
rw [ModelWithCorners.isBoundaryPoint_iff, extChartAt,
    Icc_chartedSpaceChartAt_of_le_top (by simp [hxy.out])]
  exact IccLeftChart_extend_bot_mem_frontier

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

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
⊢ (𝓡∂ 1).IsBoundaryPoint ⊥

Tactic:
by
  rw [ModelWithCorners.isBoundaryPoint_iff, extChartAt,
    Icc_chartedSpaceChartAt_of_le_top (by simp [hxy.out])]
  exact IccLeftChart_extend_bot_mem_frontier

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
s : Set ℝ
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc : γ t ∈ (chartAt H (γ t₀)).source
⊢ ∀ (x : TangentSpace 𝓘(ℝ, ℝ) t),
    (mfderiv% ↑(chartAt H (γ t₀)) (γ t) ∘SL ContinuousLinearMap.smulRight 1 (v (γ t))) x =
      (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) x

Tactic:
intro a

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
s : Set ℝ
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc : γ t ∈ (chartAt H (γ t₀)).source
a : TangentSpace 𝓘(ℝ, ℝ) t
⊢ (mfderiv% ↑(chartAt H (γ t₀)) (γ t) ∘SL ContinuousLinearMap.smulRight 1 (v (γ t))) a =
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) a
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
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
hsrc : γ t ∈ (chartAt H (γ t₀)).source
⊢ ∀ (x : TangentSpace 𝓘(ℝ, ℝ) t),
    (mfderiv% ↑(chartAt H (γ t₀)) (γ t) ∘SL ContinuousLinearMap.smulRight 1 (v (γ t))) x =
      (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) x

Tactic:
intro a

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₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
hsrc : γ t ∈ (chartAt H (γ t₀)).source
a : TangentSpace 𝓘(ℝ, ℝ) t
⊢ (mfderiv% ↑(chartAt H (γ t₀)) (γ t) ∘SL ContinuousLinearMap.smulRight 1 (v (γ t))) a =
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) a