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
n : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
h :
  {i₁, i₂}ᶜ =
    Finset.map e.toEmbedding
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
          (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ
h₁ :
  s.points =
    Function.comp (β := Fin (n + 3)) (s.points ∘ (⇑e.symm : (a : Fin (n + 2 + 1)) → Fin (n + 2 + 1)))
      (⇑e.toEmbedding : (a : Fin (n + 3)) → Fin (n + 3))
h₂ :
  Eq (α := Fin (n + 3) → ℝ)
    (centroidWeights ℝ
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
          (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ)
    (Function.comp (β := Fin (n + 3)) (centroidWeights ℝ {i₁, i₂}ᶜ) (⇑e.toEmbedding : (a : Fin (n + 3)) → Fin (n + 3)))
⊢ Eq.{u_2 + 1} (α := P)
    ((affineCombination ℝ {i₁, i₂}ᶜ (s.points ∘ (⇑e.symm : (a : Fin (n + 2 + 1)) → Fin (n + 2 + 1))) :
          (a : Fin (n + 3) → ℝ) → P)
        (centroidWeights ℝ {i₁, i₂}ᶜ) :
      P)
    ((affineCombination ℝ
            (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
                (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ
            s.points :
          (a : Fin (n + 3) → ℝ) → P)
        (centroidWeights ℝ
          (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
              (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ) :
      P)

Tactic:
convert! Finset.affineCombination_map {e.symm i₁, e.symm i₂}ᶜ e.toEmbedding _ _ using 3

Premises used: Compl.compl, Insert.insert, Finset.affineCombination_map, Equiv.toEmbedding, Equiv.symm, Singleton.singleton, DFunLike.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
n : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
h :
  ∀ (i : Fin (n + 3)),
    Membership.mem (γ := Finset (Fin (n + 3))) {i₁, i₂}ᶜ i ↔
      i ∈
        Finset.map e.toEmbedding
          (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
              (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ
⊢ {i₁, i₂}ᶜ =
    Finset.map e.toEmbedding
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
          (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ

Tactic:
ext 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
n : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ i : Fin (n + 3)
⊢ Membership.mem (γ := Finset (Fin (n + 3))) {i₁, i₂}ᶜ i ↔
    i ∈
      Finset.map e.toEmbedding
        (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
            (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ

Tactic:
simp
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ s.points =
    Function.comp (β := Fin (n + 3)) (s.points ∘ (⇑e.symm : (a : Fin (n + 2 + 1)) → Fin (n + 2 + 1)))
      (⇑e.toEmbedding : (a : Fin (n + 3)) → Fin (n + 3))

Tactic:
simp [Function.comp_assoc]

Premises used: Function.comp_assoc
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
h :
  Eq (α := Fin (n + 3) → ℝ)
    (Function.const (Fin (n + 3))
      (↑(Fintype.card (Fin (n + 3)) -
              card (α := Fin (n + 3))
                (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
                  (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))) :
          ℝ)⁻¹)
    (Function.const (Fin (n + 3)) (↑(Fintype.card (Fin (n + 3)) - card (α := Fin (n + 3)) {i₁, i₂}) : ℝ)⁻¹)
⊢ Eq (α := Fin (n + 3) → ℝ)
    (centroidWeights ℝ
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
          (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ)
    (Function.comp (β := Fin (n + 3)) (centroidWeights ℝ {i₁, i₂}ᶜ) (⇑e.toEmbedding : (a : Fin (n + 3)) → Fin (n + 3)))

Tactic:
simp_rw [centroidWeights, Function.const_comp, Finset.card_compl]

Premises used: Finset.card_compl, Function.const_comp, Finset.centroidWeights
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
h :
  card (α := Fin (n + 3))
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
        (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3)))) =
    card (α := Fin (n + 3)) {i₁, i₂}
⊢ Eq (α := Fin (n + 3) → ℝ)
    (Function.const (Fin (n + 3))
      (↑(Fintype.card (Fin (n + 3)) -
              card (α := Fin (n + 3))
                (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
                  (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))) :
          ℝ)⁻¹)
    (Function.const (Fin (n + 3)) (↑(Fintype.card (Fin (n + 3)) - card (α := Fin (n + 3)) {i₁, i₂}) : ℝ)⁻¹)

Tactic:
congr 4
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
pos :
  ∀ (h : i₁ = i₂),
    card (α := Fin (n + 3))
        (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
          (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3)))) =
      card (α := Fin (n + 3)) {i₁, i₂}
neg :
  ∀ (h : ¬i₁ = i₂),
    card (α := Fin (n + 3))
        (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
          (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3)))) =
      card (α := Fin (n + 3)) {i₁, i₂}
⊢ card (α := Fin (n + 3))
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
        (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3)))) =
    card (α := Fin (n + 3)) {i₁, i₂}

Tactic:
by_cases h : i₁ = 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
n : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
h : i₁ = i₂
⊢ card (α := Fin (n + 3))
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
        (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3)))) =
    card (α := Fin (n + 3)) {i₁, i₂}

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
n : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
⊢ card (α := Fin (n + 3))
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
        (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3)))) =
    card (α := Fin (n + 3)) {i₁, i₂}

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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
e_a : Eq (α := Finset (Fin (n + 3))) {i₁, i₂}ᶜ {i₂, i₁}ᶜ
e_a₁ : Eq (α := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) (ℝ ∙ (s.points i₂ -ᵥ s.points i₁))
⊢ Eq (α := AffineSubspace ℝ P)
    (mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ affineSpan ℝ (Set.range s.points))
    (mk' (Finset.centroid ℝ {i₂, i₁}ᶜ s.points) (ℝ ∙ (s.points i₂ -ᵥ s.points i₁))ᗮ ⊓ affineSpan ℝ (Set.range s.points))

Tactic:
congr 3
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
e_a : Eq (α := Finset (Fin (n + 3))) {i₁, i₂} {i₂, i₁}
⊢ Eq (α := Finset (Fin (n + 3))) {i₁, i₂}ᶜ {i₂, i₁}ᶜ

Tactic:
congr 1
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
⊢ Eq (α := Finset (Fin (n + 3))) {i₁, i₂} {i₂, i₁}

Tactic:
pair_comm _ _

Premises used: Finset.pair_comm
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
⊢ Eq (α := Finset (Fin (n + 3))) {i₁, i₂} {i₂, i₁}

Tactic:
exact pair_comm _ _

Premises used: Finset.pair_comm
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
e_a :
  ∀ (x : V),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) x ↔
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₂ -ᵥ s.points i₁)) x
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) (ℝ ∙ (s.points i₂ -ᵥ s.points i₁))

Tactic:
ext
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
x : V
e_a : (∃ (a : ℝ), a • (s.points i₁ -ᵥ s.points i₂) = x) ↔ ∃ (a : ℝ), a • (s.points i₂ -ᵥ s.points i₁) = x
⊢ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) x ↔
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₂ -ᵥ s.points i₁)) x

Tactic:
simp_rw [Submodule.mem_span_singleton]

Premises used: Submodule.mem_span_singleton
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
x : V
e_a : (∃ (a : ℝ), a • (s.points i₁ -ᵥ s.points i₂) = x) → ∃ (a : ℝ), a • (s.points i₂ -ᵥ s.points i₁) = x
e_a₁ : (∃ (a : ℝ), a • (s.points i₂ -ᵥ s.points i₁) = x) → ∃ (a : ℝ), a • (s.points i₁ -ᵥ s.points i₂) = x
⊢ (∃ (a : ℝ), a • (s.points i₁ -ᵥ s.points i₂) = x) ↔ ∃ (a : ℝ), a • (s.points i₂ -ᵥ s.points i₁) = x

Tactic:
constructor
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
h : -r • (s.points i₂ -ᵥ s.points i₁) = r • (s.points i₁ -ᵥ s.points i₂)
⊢ ∃ (a : ℝ), a • (s.points i₂ -ᵥ s.points i₁) = r • (s.points i₁ -ᵥ s.points i₂)

Tactic:
use -r
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
h : -(r • (s.points i₂ -ᵥ s.points i₁)) = r • (s.points i₁ -ᵥ s.points i₂)
h₁ : r • -(s.points i₂ -ᵥ s.points i₁) = r • (s.points i₁ -ᵥ s.points i₂)
h₂ h₃ : r • (s.points i₁ -ᵥ s.points i₂) = r • (s.points i₁ -ᵥ s.points i₂)
⊢ -r • (s.points i₂ -ᵥ s.points i₁) = r • (s.points i₁ -ᵥ s.points i₂)

Tactic:
rw [neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]

Premises used: neg_smul, smul_neg, neg_vsub_eq_vsub_rev
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
h : -r • (s.points i₁ -ᵥ s.points i₂) = r • (s.points i₂ -ᵥ s.points i₁)
⊢ ∃ (a : ℝ), a • (s.points i₁ -ᵥ s.points i₂) = r • (s.points i₂ -ᵥ s.points i₁)

Tactic:
use -r
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
h : -(r • (s.points i₁ -ᵥ s.points i₂)) = r • (s.points i₂ -ᵥ s.points i₁)
h₁ : r • -(s.points i₁ -ᵥ s.points i₂) = r • (s.points i₂ -ᵥ s.points i₁)
h₂ h₃ : r • (s.points i₂ -ᵥ s.points i₁) = r • (s.points i₂ -ᵥ s.points i₁)
⊢ -r • (s.points i₁ -ᵥ s.points i₂) = r • (s.points i₂ -ᵥ s.points i₁)

Tactic:
rw [neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]

Premises used: neg_smul, smul_neg, neg_vsub_eq_vsub_rev
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
rw :
  (∀ (u : V),
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) u →
        ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, u⟫ = 0) ∧
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.mongePoint
⊢ s.mongePoint ∈ s.mongePlane i₁ i₂

Tactic:
rw [mongePlane_def, mem_inf_iff, ← vsub_right_mem_direction_iff_mem (self_mem_mk' _ _),
    direction_mk', Submodule.mem_orthogonal']

Premises used: AffineSubspace.self_mem_mk', Affine.Simplex.mongePlane_def, Submodule.mem_orthogonal', AffineSubspace.mem_inf_iff, AffineSubspace.direction_mk', AffineSubspace.vsub_right_mem_direction_iff_mem
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
⊢ (∀ (u : V),
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) u →
        ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, u⟫ = 0) ∧
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.mongePoint

Tactic:
⟨?_, s.mongePoint_mem_affineSpan⟩

Premises used: And.intro, 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
refine :
  ∀ (u : V),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) u →
      ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, u⟫ = 0
⊢ (∀ (u : V),
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) u →
        ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, u⟫ = 0) ∧
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.mongePoint

Tactic:
refine ⟨?_, s.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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) v
rcases :
  ∀ (r : ℝ)
    (hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) (r • (s.points i₁ -ᵥ s.points i₂))),
    ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, r • (s.points i₁ -ᵥ s.points i₂)⟫ = 0
⊢ ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, v⟫ = 0

Tactic:
rcases Submodule.mem_span_singleton.mp hv with ⟨r, rfl⟩

Premises used: Submodule.mem_span_singleton, Iff.mp, 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) (r • (s.points i₁ -ᵥ s.points i₂))
rw : r * ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, s.points i₁ -ᵥ s.points i₂⟫ = 0
rw₁ : r * 0 = 0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, r • (s.points i₁ -ᵥ s.points i₂)⟫ = 0

Tactic:
rw [inner_smul_right, s.inner_mongePoint_vsub_face_centroid_vsub, mul_zero]

Premises used: Affine.Simplex.inner_mongePoint_vsub_face_centroid_vsub, MulZeroClass.mul_zero, inner_smul_right
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
rw :
  Eq (α := Submodule ℝ V)
    (direction
      (mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓
        affineSpan ℝ (Set.range s.points)))
    ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₁ :
  Eq (α := Submodule ℝ V)
    (direction (mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ) ⊓
      direction (affineSpan ℝ (Set.range s.points)))
    ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₂ :
  Eq (α := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ direction (affineSpan ℝ (Set.range s.points)))
    ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₃ rw₄ :
  Eq (α := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
    ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
⊢ (s.mongePlane i₁ i₂).direction = (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Tactic:
rw [mongePlane_def, direction_inf_of_mem_inf s.mongePoint_mem_mongePlane, direction_mk',
    direction_affineSpan]

Premises used: direction_affineSpan, Affine.Simplex.mongePoint_mem_mongePlane, Affine.Simplex.mongePlane_def, AffineSubspace.direction_inf_of_mem_inf, AffineSubspace.direction_mk'
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
rw : p -ᵥ s.mongePoint = 0
⊢ p = s.mongePoint

Tactic:
rw [← @vsub_eq_zero_iff_eq V]

Premises used: vsub_eq_zero_iff_eq
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
i₂ : Fin (n + 3)
hne : i₁ ≠ i₂
rw : p ∈ s.mongePlane i₁ i₂
⊢ Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
    (p -ᵥ s.mongePoint)

Tactic:
rw [← s.direction_mongePlane, vsub_right_mem_direction_iff_mem s.mongePoint_mem_mongePlane]

Premises used: Affine.Simplex.mongePoint_mem_mongePlane, Affine.Simplex.direction_mongePlane, AffineSubspace.vsub_right_mem_direction_iff_mem
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
i₂ : Fin (n + 3)
hne : i₁ ≠ i₂
⊢ p ∈ s.mongePlane i₁ i₂

Tactic:
h i₂ hne
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
i₂ : Fin (n + 3)
hne : i₁ ≠ i₂
⊢ p ∈ s.mongePlane i₁ i₂

Tactic:
exact h i₂ hne
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
⊢ ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)

Tactic:
have h' : ∀ i₂, i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈
      (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points) := by
    intro i₂ hne
    rw [← s.direction_mongePlane, vsub_right_mem_direction_iff_mem s.mongePoint_mem_mongePlane]
    exact h i₂ hne
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
rw :
  ∀ (i : { i : Fin (n + 3) // i₁ ≠ i }),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))))ᗮ (p -ᵥ s.mongePoint)
⊢ Membership.mem (γ := Submodule ℝ V)
    (⨅ (i₂ : { i : Fin (n + 3) // i₁ ≠ i }), (ℝ ∙ (s.points i₁ -ᵥ s.points (↑i₂ : Fin (n + 3))))ᗮ) (p -ᵥ s.mongePoint)

Tactic:
rw [Submodule.mem_iInf]

Premises used: Submodule.mem_iInf
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
⊢ ∀ (i : { i : Fin (n + 3) // i₁ ≠ i }),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))))ᗮ (p -ᵥ s.mongePoint)

Tactic:
fun i => (Submodule.mem_inf.1 (h' i i.property)).1

Premises used: Submodule.mem_inf, And.left, Iff.mp, Subtype.val, Subtype.property