awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃

Tactic:
have h3 : ∀ i : Fin 3, i = i₁ ∨ i = i₂ ∨ i = i₃ := by lia
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
⊢ Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}

Tactic:
decide +revert
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
⊢ Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}

Tactic:
have hu : (Finset.univ : Finset (Fin 3)) = {i₁, i₂, i₃} := by
    clear h₁ h₂ h₁' h₂'
    decide +revert
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
⊢ LE.le (α := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) (affineSpan R (Set.range t.points))

Tactic:
affineSpan_pair_le_of_mem_of_mem (mem_affineSpan R (Set.mem_range_self _)) ?_

Premises used: Set.mem_range_self, affineSpan_pair_le_of_mem_of_mem, mem_affineSpan
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
refine : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p₁
⊢ LE.le (α := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) (affineSpan R (Set.range t.points))

Tactic:
refine affineSpan_pair_le_of_mem_of_mem (mem_affineSpan R (Set.mem_range_self _)) ?_

Premises used: Set.mem_range_self, affineSpan_pair_le_of_mem_of_mem, mem_affineSpan
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
⊢ LE.le (α := AffineSubspace R P) (affineSpan R {t.points i₂, t.points i₃}) (affineSpan R (Set.range t.points))

Tactic:
affineSpan_mono R ?_

Premises used: affineSpan_mono
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
refine : {t.points i₂, t.points i₃} ⊆ Set.range t.points
⊢ LE.le (α := AffineSubspace R P) (affineSpan R {t.points i₂, t.points i₃}) (affineSpan R (Set.range t.points))

Tactic:
refine affineSpan_mono R ?_

Premises used: affineSpan_mono
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
⊢ {t.points i₂, t.points i₃} ⊆ Set.range t.points

Tactic:
simp [Set.insert_subset_iff]

Premises used: Set.insert_subset_iff
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
⊢ LE.le (α := AffineSubspace R P) (affineSpan R {t.points i₂, t.points i₃}) (affineSpan R (Set.range t.points))

Tactic:
have hle : line[R, t.points i₂, t.points i₃] ≤ affineSpan R (Set.range t.points) := by
        refine affineSpan_mono R ?_
        simp [Set.insert_subset_iff]
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
hle : LE.le (α := AffineSubspace R P) (affineSpan R {t.points i₂, t.points i₃}) (affineSpan R (Set.range t.points))
⊢ ∀ (p : P),
    Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, t.points i₃}) p →
      Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p

Tactic:
rw [AffineSubspace.le_def'] at hle

Premises used: AffineSubspace.le_def'
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
hle :
  ∀ (p : P),
    Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, t.points i₃}) p →
      Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p₁

Tactic:
hle _ h₁.wbtw.mem_affineSpan

Premises used: Sbtw.wbtw, Wbtw.mem_affineSpan
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
hle :
  ∀ (p : P),
    Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, t.points i₃}) p →
      Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p₁

Tactic:
exact hle _ h₁.wbtw.mem_affineSpan

Premises used: Sbtw.wbtw, Wbtw.mem_affineSpan
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
⊢ LE.le (α := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) (affineSpan R (Set.range t.points))

Tactic:
have hle : line[R, t.points i₁, p₁] ≤ affineSpan R (Set.range t.points) := by
      refine affineSpan_pair_le_of_mem_of_mem (mem_affineSpan R (Set.mem_range_self _)) ?_
      have hle : line[R, t.points i₂, t.points i₃] ≤ affineSpan R (Set.range t.points) := by
        refine affineSpan_mono R ?_
        simp [Set.insert_subset_iff]
      rw [AffineSubspace.le_def'] at hle
      exact hle _ h₁.wbtw.mem_affineSpan
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
hle : LE.le (α := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) (affineSpan R (Set.range t.points))
⊢ ∀ (p : P),
    Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p →
      Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p

Tactic:
rw [AffineSubspace.le_def'] at hle

Premises used: AffineSubspace.le_def'
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
hle :
  ∀ (p : P),
    Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p →
      Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p

Tactic:
hle _ h₁'
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
hle :
  ∀ (p : P),
    Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p →
      Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p

Tactic:
exact hle _ h₁'
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p

Tactic:
have hp : p ∈ affineSpan R (Set.range t.points) := by
    have hle : line[R, t.points i₁, p₁] ≤ affineSpan R (Set.range t.points) := by
      refine affineSpan_pair_le_of_mem_of_mem (mem_affineSpan R (Set.mem_range_self _)) ?_
      have hle : line[R, t.points i₂, t.points i₃] ≤ affineSpan R (Set.range t.points) := by
        refine affineSpan_mono R ?_
        simp [Set.insert_subset_iff]
      rw [AffineSubspace.le_def'] at hle
      exact hle _ h₁.wbtw.mem_affineSpan
    rw [AffineSubspace.le_def'] at hle
    exact hle _ h₁'
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
hp : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p
⊢ Membership.mem (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (t.points i₂) (t.points i₃)) : (a : R) → P) (Set.Ioo 0 1)) p₁

Tactic:
have h₁i := h₁.mem_image_Ioo
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
hp : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p
h₁i :
  Membership.mem (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (t.points i₂) (t.points i₃)) : (a : R) → P) (Set.Ioo 0 1)) p₁
⊢ Membership.mem (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (t.points i₁) (t.points i₃)) : (a : R) → P) (Set.Ioo 0 1)) p₂

Tactic:
have h₂i := h₂.mem_image_Ioo
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
hp : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p
h₁i :
  Membership.mem (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (t.points i₂) (t.points i₃)) : (a : R) → P) (Set.Ioo 0 1)) p₁
h₂i :
  Membership.mem (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (t.points i₁) (t.points i₃)) : (a : R) → P) (Set.Ioo 0 1)) p₂
⊢ ∃ (x : R), Membership.mem (γ := Set R) (Set.Ioo 0 1) x ∧ (lineMap (t.points i₂) (t.points i₃) : (a : R) → P) x = p₁

Tactic:
rw [Set.mem_image] at h₁i h₂i

Premises used: Set.mem_image
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
hp : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p
h₁i :
  Membership.mem (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (t.points i₂) (t.points i₃)) : (a : R) → P) (Set.Ioo 0 1)) p₁
h₂i :
  Membership.mem (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (t.points i₁) (t.points i₃)) : (a : R) → P) (Set.Ioo 0 1)) p₂
h₁i₁ :
  ∃ (x : R), Membership.mem (γ := Set R) (Set.Ioo 0 1) x ∧ (lineMap (t.points i₂) (t.points i₃) : (a : R) → P) x = p₁
⊢ ∃ (x : R), Membership.mem (γ := Set R) (Set.Ioo 0 1) x ∧ (lineMap (t.points i₁) (t.points i₃) : (a : R) → P) x = p₂

Tactic:
rw [Set.mem_image] at h₁i h₂i

Premises used: Set.mem_image
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
hp : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p
h₁i :
  ∃ (x : R), Membership.mem (γ := Set R) (Set.Ioo 0 1) x ∧ (lineMap (t.points i₂) (t.points i₃) : (a : R) → P) x = p₁
h₂i :
  ∃ (x : R), Membership.mem (γ := Set R) (Set.Ioo 0 1) x ∧ (lineMap (t.points i₁) (t.points i₃) : (a : R) → P) x = p₂
rcases :
  ∀ (r₁ : R) (hr₁0 : 0 < r₁) (hr₁1 : r₁ < 1)
    (h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁) (t.points i₃))
    (h₁' :
      Membership.mem (γ := AffineSubspace R P)
        (affineSpan R
          (insert (t.points i₁) (singleton (α := P) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁ : P))))
        p),
    Sbtw R (t.points i₁) p ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁)
⊢ Sbtw R (t.points i₁) p p₁

Tactic:
rcases h₁i with ⟨r₁, ⟨hr₁0, hr₁1⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₂ p : P
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
hp : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p
h₂i :
  ∃ (x : R), Membership.mem (γ := Set R) (Set.Ioo 0 1) x ∧ (lineMap (t.points i₁) (t.points i₃) : (a : R) → P) x = p₂
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁) (t.points i₃)
h₁' :
  Membership.mem (γ := AffineSubspace R P)
    (affineSpan R
      (insert (t.points i₁) (singleton (α := P) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁ : P))))
    p
rcases :
  ∀ (r₂ : R) (hr₂0 : 0 < r₂) (hr₂1 : r₂ < 1)
    (h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂) (t.points i₃))
    (h₂' :
      Membership.mem (γ := AffineSubspace R P)
        (affineSpan R
          (insert (t.points i₂) (singleton (α := P) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂ : P))))
        p),
    Sbtw R (t.points i₁) p ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁)
⊢ Sbtw R (t.points i₁) p ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁)

Tactic:
rcases h₂i with ⟨r₂, ⟨hr₂0, hr₂1⟩, rfl⟩

Premises used: rfl