mathlib-initiative/mathlib-tactics huggingface dataset:
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 : True
hXn : X = X ^ 2
x : G
hx : x ∈ X
this✝ : x • X ⊆ X
this : X = x⁻¹ • X
⊢ x⁻¹ ∈ X

Tactic:
]

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 : G
hx : x ∈ X
this✝ : x • X ⊆ X
this : X = x⁻¹ • X
⊢ x⁻¹ ∈ X
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 : True
hXn : X = X ^ 2
x : G
hx : x ∈ X
this✝ : x • X ⊆ X
this : X = x⁻¹ • X
⊢ x⁻¹ ∈ x⁻¹ • X

Tactic:
]

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 : G
hx : x ∈ X
this✝ : x • X ⊆ X
this : X = x⁻¹ • X
⊢ x⁻¹ ∈ x⁻¹ • X
Module: Mathlib.Geometry.Group.Growth.LinearLowerBound

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ ↑X ^ (n - 1) = ↑X ^ (n - m + (m - 1))

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ ↑X ^ (n - 1) = ↑X ^ (n - m + (m - 1))
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₁ 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₃
⊢ t₁.points i₁ ≠ t₂.points j₂ ∧
    t₁.points i₁ ∈ affineSpan ℝ (Set.range t₂.points) ∧
      t₁.points i₁ -ᵥ t₂.points j₂ ∈ (affineSpan ℝ (t₂.points '' {j₂}ᶜ)).directionᗮ

Tactic:
]

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₁ 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₃
⊢ t₁.points i₁ ≠ t₂.points j₂ ∧
    t₁.points i₁ ∈ affineSpan ℝ (Set.range t₂.points) ∧
      t₁.points i₁ -ᵥ t₂.points j₂ ∈ (affineSpan ℝ (t₂.points '' {j₂}ᶜ)).directionᗮ
Module: Mathlib.Geometry.Group.Growth.LinearLowerBound

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ ↑X ^ (n - m) * ↑X ^ (m - 1) = ↑(closure ↑X)

Tactic:
hm,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ ↑X ^ (n - m) * ↑(closure ↑X) = ↑(closure ↑X)
Module: Mathlib.Geometry.Group.Growth.LinearLowerBound

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ ↑(closure ↑X) = ↑(closure ↑X)

Tactic:
]

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
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₃
⊢ t₁.points i₁ ≠ t₁.points i₂ ∧
    t₁.points i₁ ∈ affineSpan ℝ (Set.range t₂.points) ∧
      t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ (t₂.points '' {j₂}ᶜ)).directionᗮ

Tactic:
]

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₁ 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₃
⊢ t₁.points i₁ ≠ t₁.points i₂ ∧
    t₁.points i₁ ∈ affineSpan ℝ (Set.range t₂.points) ∧
      t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ (t₂.points '' {j₂}ᶜ)).directionᗮ
Module: Mathlib.Geometry.Group.Growth.QuotientInter

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x ↦ x ∈ H
inst✝ : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
⊢ ∑ b ∈ image (⇑π) A, #({a ∈ A | π a = b}) ≤ #(image (⇑π) A) * #({x ∈ A ^ 2 | x ∈ H})

Tactic:
]

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x ↦ x ∈ H
inst✝ : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
⊢ ∑ b ∈ image (⇑π) A, #({a ∈ A | π a = b}) ≤ #(image (⇑π) A) * #({x ∈ A ^ 2 | x ∈ H})
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case refine_1
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₃
hu : Set.univ = {j₁, j₂, j₃}
⊢ t₁.orthocenter ∈ ↑(affineSpan ℝ (Set.range t₁.points)) ∧
    t₁.points i₂ ∈ ↑(affineSpan ℝ (Set.range t₁.points)) ∧ t₁.points i₃ ∈ ↑(affineSpan ℝ (Set.range t₁.points))

Tactic:
]

Goal state after:
case refine_1
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₃
hu : Set.univ = {j₁, j₂, j₃}
⊢ t₁.orthocenter ∈ ↑(affineSpan ℝ (Set.range t₁.points)) ∧
    t₁.points i₂ ∈ ↑(affineSpan ℝ (Set.range t₁.points)) ∧ t₁.points i₃ ∈ ↑(affineSpan ℝ (Set.range t₁.points))
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₃
⊢ 2 = 2

Tactic:
]

Goal state after:
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₁ 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₃
he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)
⊢ t₁.points i₁ ∈ affineSpan ℝ (Set.range t₁.points) ∧
    t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ (t₂.points '' {j₂}ᶜ)).directionᗮ

Tactic:
]

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₁ 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₃
he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)
⊢ t₁.points i₁ ∈ affineSpan ℝ (Set.range t₁.points) ∧
    t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ (t₂.points '' {j₂}ᶜ)).directionᗮ
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₁ 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₃
he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)
hu : {j₂}ᶜ = {j₁, j₃}
⊢ t₁.points i₁ -ᵥ t₁.points i₂ ∈ line[ℝ, t₁.orthocenter, t₁.points i₃].directionᗮ

Tactic:
]

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₁ 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₃
he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)
hu : {j₂}ᶜ = {j₁, j₃}
⊢ t₁.points i₁ -ᵥ t₁.points i₂ ∈ line[ℝ, t₁.orthocenter, t₁.points i₃].directionᗮ
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₁ 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₃
he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)
hu : {j₂}ᶜ = {j₁, j₃}
hle : (altitude t₁ i₃).directionᗮ ≤ line[ℝ, t₁.orthocenter, t₁.points i₃].directionᗮ
hui : {i₃}ᶜ = {i₁, i₂}
⊢ t₁.points i₁ -ᵥ t₁.points i₂ ∈ vectorSpan ℝ {t₁.points i₁, t₁.points i₂}

Tactic:
]

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₁ 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₃
he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)
hu : {j₂}ᶜ = {j₁, j₃}
hle : (altitude t₁ i₃).directionᗮ ≤ line[ℝ, t₁.orthocenter, t₁.points i₃].directionᗮ
hui : {i₃}ᶜ = {i₁, i₂}
⊢ t₁.points i₁ -ᵥ t₁.points i₂ ∈ vectorSpan ℝ {t₁.points i₁, t₁.points i₂}
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case refine_1
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₃
⊢ t₁.points i₁ ∈ line[ℝ, t₁.points i₁, t₁.points i₂]

Tactic:
]

Goal state after:
case refine_1
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₃
⊢ t₁.points i₁ ∈ line[ℝ, t₁.points i₁, t₁.points i₂]
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₃
⊢ t₁.points i₁ ∈ line[ℝ, t₁.points i₁, t₁.points i₃]

Tactic:
]

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₃
⊢ t₁.points i₁ ∈ line[ℝ, t₁.points i₁, t₁.points i₃]
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₂ j₃ : Fin 3
h₂ : p i₃ = p i₂
h₃ : t.points j₃ = p i₃
he : j₂ = j₃
⊢ False

Tactic:
]

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 neg
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
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ Set.range t.points
⊢ Set.range p = Set.range t.points

Tactic:
]

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
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
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ Set.range t.points
⊢ Set.range p = Set.range t.points
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
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
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ Set.range t.points
⊢ Fintype.card (Fin (2 + 1)) ≤ Fintype.card (Fin 3)

Tactic:
]

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

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 : ℕ∞ω
x : M
k : 𝕜
f : C^∞⟮I, M; 𝕜⟯⟨x⟩
h : 𝕜
⊢ k * (f x * h) = k * (f x * h)

Tactic:
]

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

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 : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ : C^∞⟮I, 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 : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : f x = y
v : PointDerivation I x
g g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ v (ContMDiffMap.comp g f) + v (ContMDiffMap.comp g' f) = v (ContMDiffMap.comp g f) + v (ContMDiffMap.comp g' f)

Tactic:
]

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

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 : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ : C^∞⟮I, 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 : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : f x = y
v : PointDerivation I x
k : 𝕜
g : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ k * v (ContMDiffMap.comp g f) = k * v (ContMDiffMap.comp g f)

Tactic:
]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
⊢ ↑(Exists.choose hf).toPartialEquiv x ∈ hf.localInverse.source

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
⊢ ↑(Exists.choose hf).toPartialEquiv x ∈ hf.localInverse.source
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case right.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
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₃
⊢ dist (t.points j₂) (Simplex.circumcenter t) = Simplex.circumradius t

Tactic:
]

Goal state after:
case right.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
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₃
⊢ dist (t.points j₂) (Simplex.circumcenter t) = Simplex.circumradius t
Module: Mathlib.Geometry.Manifold.LocalDiffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
y : N
hy : y ∈ hf.localInverse.source
⊢ ↑hf.localInverse.toPartialEquiv y ∈ (Exists.choose hf).symm.target

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
y : N
hy : y ∈ hf.localInverse.source
⊢ ↑hf.localInverse.toPartialEquiv y ∈ (Exists.choose hf).symm.target
Module: Mathlib.Geometry.Manifold.LocalDiffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
y : N
hy : y ∈ hf.localInverse.source
this : ↑hf.localInverse.toPartialEquiv y ∈ (Exists.choose hf).source
⊢ ↑(Exists.choose hf).toPartialEquiv (↑hf.localInverse.toPartialEquiv y) = y

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
y : N
hy : y ∈ hf.localInverse.source
this : ↑hf.localInverse.toPartialEquiv y ∈ (Exists.choose hf).source
⊢ ↑(Exists.choose hf).toPartialEquiv (↑hf.localInverse.toPartialEquiv y) = y