awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
rw : t.orthocenter -ᵥ circumcenter t = HAdd.hAdd (α := ℕ) 0 1 • (mongePoint t -ᵥ circumcenter t)
rw₁ : t.orthocenter -ᵥ circumcenter t = HSMul.hSMul (α := ℕ) 1 (mongePoint t -ᵥ circumcenter t)
rw₂ : t.orthocenter -ᵥ circumcenter t = mongePoint t -ᵥ circumcenter t
rw₃ rw₄ : mongePoint t -ᵥ circumcenter t = mongePoint t -ᵥ circumcenter t
⊢ t.orthocenter -ᵥ circumcenter t = ∑ i : Fin (2 + 1), (t.points i -ᵥ circumcenter t)

Tactic:
rw [← t.smul_mongePoint_vsub_circumcenter_eq_sum_vsub, zero_add, one_smul,
    orthocenter_eq_mongePoint]

Premises used: Affine.Simplex.smul_mongePoint_vsub_circumcenter_eq_sum_vsub, zero_add, one_smul, Affine.Triangle.orthocenter_eq_mongePoint
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) t.orthocenter

Tactic:
t.mongePoint_mem_affineSpan

Premises used: Set.Mem, Affine.Triangle.orthocenter, Affine.Simplex.mongePoint_mem_affineSpan
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
h : Set.range t₁.points = Set.range t₂.points
⊢ t₁.orthocenter = t₂.orthocenter

Tactic:
mongePoint_eq_of_range_eq h

Premises used: Affine.Simplex.mongePoint_eq_of_range_eq, Affine.Triangle.orthocenter
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Eq (α := Finset (Fin 3)) {i₂, i₃}ᶜ {i₁}

Tactic:
decide +revert
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Eq (α := Finset (Fin 3)) {i₂, i₃}ᶜ {i₁}

Tactic:
have hs : ({i₂, i₃}ᶜ : Finset (Fin 3)) = {i₁} := by decide +revert
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : Eq (α := Finset (Fin 3)) {i₂, i₃}ᶜ {i₁}
⊢ Eq (α := Set (Fin 3)) {i₁}ᶜ {i₂, i₃}

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : Eq (α := Finset (Fin 3)) {i₂, i₃}ᶜ {i₁}
⊢ Eq (α := Set (Fin 3)) {i₁}ᶜ {i₂, i₃}

Tactic:
have he : ({i₁}ᶜ : Set (Fin 3)) = {i₂, i₃} := by grind
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : Eq (α := Finset (Fin 3)) {i₂, i₃}ᶜ {i₁}
he : Eq (α := Set (Fin 3)) {i₁}ᶜ {i₂, i₃}
rw :
  Eq (α := AffineSubspace ℝ P)
    (mk' (t.points i₁) (Submodule.span ℝ ((fun (x : P) ↦ t.points i₂ -ᵥ x) '' t.points '' ({i₂, i₃} \ {i₂})))ᗮ ⊓
      affineSpan ℝ (Set.range t.points))
    (mk' (t.points i₁) (ℝ ∙ (t.points i₂ -ᵥ t.points i₃))ᗮ ⊓ affineSpan ℝ (Set.range t.points))
⊢ altitude t i₁ = mongePlane t i₂ i₃

Tactic:
rw [mongePlane_def, altitude_def, direction_affineSpan, hs, he, centroid_singleton,
    vectorSpan_image_eq_span_vsub_set_left_ne ℝ _ (Set.mem_insert i₂ _)]

Premises used: direction_affineSpan, Real, vectorSpan_image_eq_span_vsub_set_left_ne, Affine.Simplex.mongePlane_def, Finset.centroid_singleton, Set.mem_insert, Affine.Simplex.altitude_def
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : Eq (α := Finset (Fin 3)) {i₂, i₃}ᶜ {i₁}
he : Eq (α := Set (Fin 3)) {i₁}ᶜ {i₂, i₃}
⊢ Eq (α := AffineSubspace ℝ P)
    (mk' (t.points i₁) (Submodule.span ℝ ((fun (x : P) ↦ t.points i₂ -ᵥ x) '' t.points '' ({i₂, i₃} \ {i₂})))ᗮ ⊓
      affineSpan ℝ (Set.range t.points))
    (mk' (t.points i₁) (ℝ ∙ (t.points i₂ -ᵥ t.points i₃))ᗮ ⊓ affineSpan ℝ (Set.range t.points))

Tactic:
simp [h₂₃]
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ : Fin 3
⊢ ∃ (i₂ : Fin 3) (i₃ : Fin 3), i₁ ≠ i₂ ∧ i₂ ≠ i₃ ∧ i₁ ≠ i₃

Tactic:
decide +revert
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ : Fin 3
obtain : ∀ (i₂ i₃ : Fin 3) (h₁₂ : i₁ ≠ i₂) (h₂₃ : i₂ ≠ i₃) (h₁₃ : i₁ ≠ i₃), t.orthocenter ∈ altitude t i₁
⊢ t.orthocenter ∈ altitude t i₁

Tactic:
obtain ⟨i₂, i₃, h₁₂, h₂₃, h₁₃⟩ : ∃ i₂ i₃, i₁ ≠ i₂ ∧ i₂ ≠ i₃ ∧ i₁ ≠ i₃ := by
    decide +revert
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
rw : mongePoint t ∈ mongePlane t i₂ i₃
⊢ t.orthocenter ∈ altitude t i₁

Tactic:
rw [orthocenter_eq_mongePoint, t.altitude_eq_mongePlane h₁₂ h₁₃ h₂₃]

Premises used: Affine.Triangle.orthocenter_eq_mongePoint, Affine.Triangle.altitude_eq_mongePlane
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ mongePoint t ∈ mongePlane t i₂ i₃

Tactic:
t.mongePoint_mem_mongePlane

Premises used: Set.Mem, Affine.Simplex.mongePoint_mem_mongePlane
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ mongePoint t ∈ mongePlane t i₂ i₃

Tactic:
exact t.mongePoint_mem_mongePlane

Premises used: Affine.Simplex.mongePoint_mem_mongePlane
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
⊢ ∃ (i₃ : Fin 3), i₂ ≠ i₃ ∧ i₁ ≠ i₃

Tactic:
decide +revert
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
h₁ : p ∈ altitude t i₁
h₂ : p ∈ altitude t i₂
obtain : ∀ (i₃ : Fin 3) (h₂₃ : i₂ ≠ i₃) (h₁₃ : i₁ ≠ i₃), p = t.orthocenter
⊢ p = t.orthocenter

Tactic:
obtain ⟨i₃, h₂₃, h₁₃⟩ : ∃ i₃, i₂ ≠ i₃ ∧ i₁ ≠ i₃ := by
    clear h₁ h₂
    decide +revert
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
h₁ : p ∈ altitude t i₁
h₂ : p ∈ altitude t i₂
i₃ : Fin 3
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ p ∈ mongePlane t i₃ i₂

Tactic:
rw [t.altitude_eq_mongePlane h₁₃ h₁₂ h₂₃.symm] at h₁

Premises used: Ne.symm, Affine.Triangle.altitude_eq_mongePlane
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
h₁ : p ∈ altitude t i₁
h₂ : p ∈ altitude t i₂
i₃ : Fin 3
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
h₃ : p ∈ mongePlane t i₃ i₂
⊢ i₂ ≠ i₃

Tactic:
rw [t.altitude_eq_mongePlane h₁₃ h₁₂ h₂₃.symm] at h₁

Premises used: Ne.symm, Affine.Triangle.altitude_eq_mongePlane
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
h₁ : p ∈ altitude t i₁
h₂ : p ∈ altitude t i₂
i₃ : Fin 3
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
h₃ : p ∈ mongePlane t i₃ i₂
h₂₄ : i₂ ≠ i₃
⊢ i₁ ≠ i₃

Tactic:
rw [t.altitude_eq_mongePlane h₁₃ h₁₂ h₂₃.symm] at h₁

Premises used: Ne.symm, Affine.Triangle.altitude_eq_mongePlane
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
h₂ : p ∈ altitude t i₂
i₃ : Fin 3
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ p ∈ mongePlane t i₃ i₁

Tactic:
rw [t.altitude_eq_mongePlane h₂₃ h₁₂.symm h₁₃.symm] at h₂

Premises used: Ne.symm, Affine.Triangle.altitude_eq_mongePlane
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
h₂ : p ∈ altitude t i₂
i₃ : Fin 3
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
h₃ : p ∈ mongePlane t i₃ i₁
⊢ p ∈ mongePlane t i₃ i₂

Tactic:
rw [t.altitude_eq_mongePlane h₂₃ h₁₂.symm h₁₃.symm] at h₂

Premises used: Ne.symm, Affine.Triangle.altitude_eq_mongePlane
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
h₂ : p ∈ altitude t i₂
i₃ : Fin 3
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
h₃ : p ∈ mongePlane t i₃ i₁
h₄ : p ∈ mongePlane t i₃ i₂
⊢ i₂ ≠ i₃

Tactic:
rw [t.altitude_eq_mongePlane h₂₃ h₁₂.symm h₁₃.symm] at h₂

Premises used: Ne.symm, Affine.Triangle.altitude_eq_mongePlane
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
h₂ : p ∈ altitude t i₂
i₃ : Fin 3
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
h₃ : p ∈ mongePlane t i₃ i₁
h₄ : p ∈ mongePlane t i₃ i₂
h₂₄ : i₂ ≠ i₃
⊢ i₁ ≠ i₃

Tactic:
rw [t.altitude_eq_mongePlane h₂₃ h₁₂.symm h₁₃.symm] at h₂

Premises used: Ne.symm, Affine.Triangle.altitude_eq_mongePlane
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
i₃ : Fin 3
h₂ : p ∈ mongePlane t i₃ i₁
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
i : Fin 3
hi : i₃ ≠ i
⊢ i₁ = i ∨ i₂ = i

Tactic:
lia
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
i₃ : Fin 3
h₂ : p ∈ mongePlane t i₃ i₁
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
i : Fin 3
hi : i₃ ≠ i
inl : ∀ (hi : i₃ ≠ i₁), p ∈ mongePlane t i₃ i₁
inr : ∀ (hi : i₃ ≠ i₂), p ∈ mongePlane t i₃ i₂
⊢ p ∈ mongePlane t i₃ i

Tactic:
obtain rfl | rfl : i₁ = i ∨ i₂ = i := by lia

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
i₃ : Fin 3
h₂ : p ∈ mongePlane t i₃ i₁
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
hi : i₃ ≠ i₁
⊢ p ∈ mongePlane t i₃ i₁

Tactic:
assumption
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
i₃ : Fin 3
h₂ : p ∈ mongePlane t i₃ i₁
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
hi : i₃ ≠ i₂
⊢ p ∈ mongePlane t i₃ i₂

Tactic:
assumption
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
i₃ : Fin 3
h₂ : p ∈ mongePlane t i₃ i₁
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ ∀ (i : Fin 3), i₃ ≠ i → p ∈ mongePlane t i₃ i

Tactic:
have ha : ∀ i, i₃ ≠ i → p ∈ t.mongePlane i₃ i := by
    intro i hi
    obtain rfl | rfl : i₁ = i ∨ i₂ = i := by lia
    all_goals assumption
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
i₃ : Fin 3
h₂ : p ∈ mongePlane t i₃ i₁
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
ha : ∀ (i : Fin 3), i₃ ≠ i → p ∈ mongePlane t i₃ i
⊢ p = mongePoint t

Tactic:
eq_mongePoint_of_forall_mem_mongePlane ha

Premises used: Affine.Simplex.eq_mongePoint_of_forall_mem_mongePlane
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
i₃ : Fin 3
h₂ : p ∈ mongePlane t i₃ i₁
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
ha : ∀ (i : Fin 3), i₃ ≠ i → p ∈ mongePlane t i₃ i
⊢ p = mongePoint t

Tactic:
exact eq_mongePoint_of_forall_mem_mongePlane ha

Premises used: Affine.Simplex.eq_mongePoint_of_forall_mem_mongePlane
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
rw :
  HDiv.hDiv (α := ℝ)
      (-∑ i₁_1 : PointsWithCircumcenterIndex 2,
          ∑ i₂_1 : PointsWithCircumcenterIndex 2,
            HSub.hSub (α := PointsWithCircumcenterIndex 2 → ℝ) (mongePointWeightsWithCircumcenter 0)
                  (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) i₁_1 *
                HSub.hSub (α := PointsWithCircumcenterIndex 2 → ℝ) (mongePointWeightsWithCircumcenter 0)
                  (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) i₂_1 *
              (dist (pointsWithCircumcenter t i₁_1) (pointsWithCircumcenter t i₂_1) *
                dist (pointsWithCircumcenter t i₁_1) (pointsWithCircumcenter t i₂_1)))
      2 =
    circumradius t * circumradius t
⊢ dist t.orthocenter ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) (circumcenter t)) =
    circumradius t

Tactic:
rw [← mul_self_inj_of_nonneg dist_nonneg t.circumradius_nonneg,
    t.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter h,
    t.orthocenter_eq_mongePoint, mongePoint_eq_affineCombination_of_pointsWithCircumcenter,
    dist_affineCombination t.pointsWithCircumcenter (sum_mongePointWeightsWithCircumcenter _)
      (sum_reflectionCircumcenterWeightsWithCircumcenter h)]

Premises used: mul_self_inj_of_nonneg, Affine.Simplex.circumradius_nonneg, Affine.Simplex.pointsWithCircumcenter, Affine.Simplex.sum_mongePointWeightsWithCircumcenter, dist_nonneg, Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenter, Affine.Simplex.sum_reflectionCircumcenterWeightsWithCircumcenter, Affine.Triangle.orthocenter_eq_mongePoint, EuclideanGeometry.dist_affineCombination, Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ Subset (α := Finset (Fin 3)) {i₁, i₂} univ

Tactic:
have hu : ({i₁, i₂} : Finset (Fin 3)) ⊆ univ := subset_univ _
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
hu : Subset (α := Finset (Fin 3)) {i₁, i₂} univ
⊢ ∃ (i₃ : Fin 3), Eq (α := Finset (Fin 3)) (univ \ {i₁, i₂}) {i₃} ∧ i₃ ≠ i₁ ∧ i₃ ≠ i₂

Tactic:
decide +revert
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
simp :
  dist t.orthocenter ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) (circumcenter t)) =
    circumradius t
⊢ dist t.orthocenter
      ((reflection (affineSpan ℝ (t.points '' (↑{i₁, i₂} : Set (Fin (2 + 1))))) : (a : P) → P) (circumcenter t)) =
    circumradius t

Tactic:
simp only [coe_insert, coe_singleton]

Premises used: Finset.coe_singleton, Finset.coe_insert
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist t.orthocenter ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) (circumcenter t)) =
    circumradius t

Tactic:
dist_orthocenter_reflection_circumcenter _ h

Premises used: Set.Mem, Affine.Triangle.dist_orthocenter_reflection_circumcenter
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist t.orthocenter ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) (circumcenter t)) =
    circumradius t

Tactic:
exact dist_orthocenter_reflection_circumcenter _ h

Premises used: Affine.Triangle.dist_orthocenter_reflection_circumcenter
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
rw :
  dist ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) (circumcenter t)) t.orthocenter =
    circumradius t
rw₁ :
  dist t.orthocenter ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) (circumcenter t)) =
    circumradius t
rw₂ rw₃ : circumradius t = circumradius t
⊢ dist (circumcenter t) ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) t.orthocenter) =
    circumradius t

Tactic:
rw [EuclideanGeometry.dist_reflection, dist_comm, dist_orthocenter_reflection_circumcenter t h]

Premises used: Affine.Triangle.dist_orthocenter_reflection_circumcenter, dist_comm, EuclideanGeometry.dist_reflection
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
simp :
  dist (circumcenter t) ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) t.orthocenter) =
    circumradius t
⊢ dist (circumcenter t)
      ((reflection (affineSpan ℝ (t.points '' (↑{i₁, i₂} : Set (Fin (2 + 1))))) : (a : P) → P) t.orthocenter) =
    circumradius t

Tactic:
simp only [coe_insert, coe_singleton]

Premises used: Finset.coe_singleton, Finset.coe_insert
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist (circumcenter t) ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) t.orthocenter) =
    circumradius t

Tactic:
dist_circumcenter_reflection_orthocenter _ h

Premises used: Set.Mem, Affine.Triangle.dist_circumcenter_reflection_orthocenter
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist (circumcenter t) ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) t.orthocenter) =
    circumradius t

Tactic:
exact dist_circumcenter_reflection_orthocenter _ h

Premises used: Affine.Triangle.dist_circumcenter_reflection_orthocenter
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
⊢ affineSpan ℝ {t.orthocenter, t.points i} ≤ altitude t i

Tactic:
affineSpan_le_of_subset_coe ?_

Premises used: affineSpan_le_of_subset_coe
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
refine : {t.orthocenter, t.points i} ⊆ (↑(altitude t i) : Set P)
⊢ affineSpan ℝ {t.orthocenter, t.points i} ≤ altitude t i

Tactic:
refine affineSpan_le_of_subset_coe ?_

Premises used: affineSpan_le_of_subset_coe
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
rw : t.orthocenter ∈ (↑(altitude t i) : Set P) ∧ t.points i ∈ (↑(altitude t i) : Set P)
⊢ {t.orthocenter, t.points i} ⊆ (↑(altitude t i) : Set P)

Tactic:
rw [Set.insert_subset_iff, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Set.insert_subset_iff
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
⊢ t.orthocenter ∈ (↑(altitude t i) : Set P) ∧ t.points i ∈ (↑(altitude t i) : Set P)

Tactic:
⟨t.orthocenter_mem_altitude, t.mem_altitude i⟩

Premises used: Affine.Triangle.orthocenter_mem_altitude, And.intro, Affine.Simplex.mem_altitude
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
⊢ t.orthocenter ∈ (↑(altitude t i) : Set P) ∧ t.points i ∈ (↑(altitude t i) : Set P)

Tactic:
exact ⟨t.orthocenter_mem_altitude, t.mem_altitude i⟩
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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₃
symm : affineSpan ℝ {t₁.points i₁, t₁.points i₂} = altitude t₂ j₂
⊢ altitude t₂ j₂ = affineSpan ℝ {t₁.points i₁, t₁.points i₂}

Tactic:
symm