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

Goal state before:
pp: case pos.inr
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')
h2 : dist c' b' = 0
h_dist_cb : dist c b = 0
⊢ ∠ a b c = ∠ a' b' c'

Tactic:
dist_eq_zero

Goal state after:
case pos.inr
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')
h2 : c' = b'
h_dist_cb : c = b
⊢ ∠ a b c = ∠ a' b' c'
Module: Mathlib.Geometry.Group.Growth.LinearLowerBound

Goal state before:
pp: G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : 1 ≠ 0
hXn : X ^ 1 = X ^ (1 + 1)
⊢ ↑X ^ 1 = ↑(closure (↑X ^ 1))

Tactic:
simp only [ne_eq, one_ne_zero, not_false_eq_true, Nat.reduceAdd, pow_one] at *

Goal state after:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
⊢ ↑X = ↑(closure ↑X)
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ finrank ℝ ↥(affineSpan ℝ (Set.range t₂.points)).direction = finrank ℝ ↥(affineSpan ℝ (Set.range t₁.points)).direction

Tactic:
direction_affineSpan,

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ finrank ℝ ↥(vectorSpan ℝ (Set.range t₂.points)) = finrank ℝ ↥(affineSpan ℝ (Set.range t₁.points)).direction
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ finrank ℝ ↥(vectorSpan ℝ (Set.range t₂.points)) = finrank ℝ ↥(affineSpan ℝ (Set.range t₁.points)).direction

Tactic:
direction_affineSpan,

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ finrank ℝ ↥(vectorSpan ℝ (Set.range t₂.points)) = finrank ℝ ↥(vectorSpan ℝ (Set.range t₁.points))
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ : Fin 3
h₁ : p i₁ = t.orthocenter
i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h : ∀ (i : Fin 3), i₁ ≠ i → ∃ j, t.points j = p i
j₂ : Fin 3
h₂ : t.points j₂ = p i₂
j₃ : Fin 3
h₃ : t.points j₃ = p i₃
he : j₂ = j₃
⊢ False

Tactic:
rw [he, h₃] at h₂

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ : Fin 3
h₁ : p i₁ = t.orthocenter
i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h : ∀ (i : Fin 3), i₁ ≠ i → ∃ j, t.points j = p i
j₂ j₃ : Fin 3
h₂ : p i₃ = p i₂
h₃ : t.points j₃ = p i₃
he : j₂ = j₃
⊢ False
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case right
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
i : Fin 3
⊢ dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃}))) (Simplex.circumcenter t)) = Simplex.circumradius t

Tactic:
have h₁₂₃ := h₁₂₃ i

Goal state after:
case right
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃✝ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
i : Fin 3
h₁₂₃ : i = i₁ ∨ i = i₂ ∨ i = i₃
⊢ dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃}))) (Simplex.circumcenter t)) = Simplex.circumradius t
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
⊢ finrank ℝ ↥(affineSpan ℝ (Set.range p)).direction = finrank ℝ ↥(affineSpan ℝ (Set.range t.points)).direction

Tactic:
direction_affineSpan,

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
⊢ finrank ℝ ↥(vectorSpan ℝ (Set.range p)) = finrank ℝ ↥(affineSpan ℝ (Set.range t.points)).direction
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
⊢ finrank ℝ ↥(vectorSpan ℝ (Set.range p)) = finrank ℝ ↥(affineSpan ℝ (Set.range t.points)).direction

Tactic:
direction_affineSpan,

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
⊢ finrank ℝ ↥(vectorSpan ℝ (Set.range p)) = finrank ℝ ↥(vectorSpan ℝ (Set.range t.points))
Module: Mathlib.Geometry.Manifold.Complex

Goal state before:
pp: case inr
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
a b : M
hd : MDiff[U] f
hpc : IsPreconnected U
hc : IsCompact U
ho : IsOpen[inst✝²] U
ha : a ∈ U
hb : b ∈ U
this : ∀ {f : M → F}, MDiff[U] f → f b = 0 → f a = f b
hb₀ : ¬f b = 0
⊢ f a = f b

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
U : Set M
a b : M
hpc : IsPreconnected U
hc : IsCompact U
ho : IsOpen[inst✝²] U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDiff[U] f
hb₀ : f b = 0
⊢ f a = f b

Tactic:
· have hd' : MDiff[U] (f · - f b) := fun x hx ↦
      ⟨(hd x hx).1.sub continuousWithinAt_const, (hd x hx).2.sub_const _⟩
    simpa [sub_eq_zero] using this hd' (sub_self _)

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
U : Set M
a b : M
hpc : IsPreconnected U
hc : IsCompact U
ho : IsOpen[inst✝²] U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDiff[U] f
hb₀ : f b = 0
⊢ f a = f b
Module: Mathlib.Geometry.Manifold.Instances.Real

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

Tactic:
dsimp at hx hy ⊢; positivity

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

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

Tactic:
by dsimp at hx hy ⊢; positivity

Goal state after:
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}
i : Fin n
⊢ (↑⟨toLp 2 fun i ↦ max (x.ofLp i) 0, ⋯⟩).ofLp i = x.ofLp i

Tactic:
simp only [hx i, sup_of_le_left]

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

Goal state before:
pp: case left
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ Continuous Subtype.val

pp: case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ ∀ (x : { x // x ∈ sphere 0 1 }) (y : E),
    ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) x).symm)
      ((extChartAt (𝓡 n) x).target ∩ ↑(extChartAt (𝓡 n) x).symm ⁻¹' Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y).source)

Tactic:
· exact continuous_subtype_val

Goal state after:
case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ ∀ (x : { x // x ∈ sphere 0 1 }) (y : E),
    ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) x).symm)
      ((extChartAt (𝓡 n) x).target ∩ ↑(extChartAt (𝓡 n) x).symm ⁻¹' Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y).source)
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
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 : 1 ≤ n
hs : UniqueMDiff[s]
this : ContMDiffOn I.tangent I'.tangent 0 (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s)
⊢ ContinuousOn (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s)

Tactic:
exact this.continuousOn

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

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✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : ¬BddAbove s
⊢ ∃ γ, γ 0 = x ∧ IsMIntegralCurve γ v

Tactic:
rw [not_bddAbove_iff] at hbdd
    rw [exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo hv]
    intro a
    obtain ⟨y, ⟨γ, hγ1, hγ2⟩, hlt⟩ := hbdd a
    exact ⟨γ, hγ1, hγ2.mono <| Ioo_subset_Ioo (neg_le_neg hlt.le) hlt.le⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.Sheaf.Smooth

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
⊢ (forgetStalk IM I M R x).inv ≫ ↾⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) = smoothSheaf.evalHom IM I R x

Tactic:
apply Limits.colimit.hom_ext

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
⊢ ∀ (j : (OpenNhds x)ᵒᵖ),
    colimit.ι
          (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑(TopCat.of M))ᵒᵖ (Type u)).obj (OpenNhds.inclusion x).op).obj
            (smoothSheaf IM I M R).presheaf)
          j ≫
        (forgetStalk IM I M R x).inv ≫ ↾⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) =
      colimit.ι
          (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑(TopCat.of M))ᵒᵖ (Type u)).obj (OpenNhds.inclusion x).op).obj
            (smoothSheaf IM I M R).presheaf)
          j ≫
        smoothSheaf.evalHom IM I R x
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁸ : TopologicalSpace B
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → NormedAddCommGroup (E x)
inst✝³ : (x : B) → InnerProductSpace ℝ (E x)
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle ℝ F E
M : Type u_4
inst✝ : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
x : M
hv : ContinuousAt (fun m ↦ { proj := b m, snd := v m }) x
hw : ContinuousAt (fun m ↦ { proj := b m, snd := w m }) x
⊢ ContinuousAt (fun b_1 ↦ ⟪v b_1, w b_1⟫) x

Tactic:
by
  simp only [← continuousWithinAt_univ] at hv hw ⊢
  exact ContinuousWithinAt.inner_bundle hv hw

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

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

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

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

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
inst✝⁷ : NormedSpace 𝕜 F
n✝ : ℕ∞ω
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u u' : Set M
x : M
n : ℕ∞ω
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : FiniteDimensional 𝕜 F
hs : IsLocalFrameOn I F n s u
hx : x ∈ u
⊢ FiniteDimensional 𝕜 (V x)

Tactic:
let phi := (trivializationAt F V x).linearEquivAt 𝕜 x
      (FiberBundle.mem_baseSet_trivializationAt' x)

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
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n✝ : ℕ∞ω
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u u' : Set M
x : M
n : ℕ∞ω
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : FiniteDimensional 𝕜 F
hs : IsLocalFrameOn I F n s u
hx : x ∈ u
phi : V x ≃ₗ[𝕜] F := Trivialization.linearEquivAt 𝕜 (trivializationAt F V x) x ⋯
⊢ FiniteDimensional 𝕜 (V x)
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

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
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ᶠ (x : M) in 𝓝 x, σ x = σ' x
⊢ cov σ x = cov σ' x

Tactic:
by
  rw [eventually_iff_exists_mem] at hσσ'
  choose s' hs' b using hσσ'
  exact (hcov.mono inter_subset_left).congr_of_eqOn hσ hσ' (inter_mem hxs hs') fun x hx ↦ b x hx.2

Goal state after:
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
⊢ Polygon.HasNondegenerateVertices R (toPolygon t)

Tactic:
have h : AffineIndependent R ![t.points 0, t.points 1, t.points 2] := by
    simpa [← ht] using t.independent

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
⊢ Polygon.HasNondegenerateVertices R (toPolygon t)
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
x y z : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
hz : z ≠ 1
hzx : z ≠ x
hzy : z ≠ y
⊢ z = x * y

Tactic:
by
  classical
  let _ := Fintype.ofFinite G
  apply eq_of_mem_insert_of_notMem <| (eq_finset_univ hx hy hxy).symm ▸ mem_univ _
  simpa only [mem_singleton, mem_insert, not_or] using ⟨hzx, hzy, hz⟩

Goal state after: