awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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
⊢ Sbtw R (t.points i₁) p p₁
have h₁₃ : i₁ ≠ i₃
Tactic: have h₁₃ : i₁ ≠ i₃ := by
    rintro rfl
    simp at h₂
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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₃
⊢ Sbtw R (t.points i₁) p p₁
have h₂₃ : i₂ ≠ i₃
Tactic: have h₂₃ : i₂ ≠ i₃ := by
    rintro rfl
    simp at h₁
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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₃
⊢ Sbtw R (t.points i₁) p p₁
have h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
Tactic: have h3 : ∀ i : Fin 3, i = i₁ ∨ i = i₂ ∨ i = i₃ := by lia
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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₃
⊢ Sbtw R (t.points i₁) p p₁
have hu : 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
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))
have refine : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p₁
Tactic: refine affineSpan_pair_le_of_mem_of_mem (mem_affineSpan R (Set.mem_range_self _)) ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
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))
have refine : {t.points i₂, t.points i₃} ⊆ Set.range t.points
Tactic: refine affineSpan_mono R ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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₁
have hle : 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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))
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p₁
have 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
Tactic: rw [AffineSubspace.le_def'] at hle
Cleared hypotheses: hle
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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
have hle : 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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))
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range t.points)) p
have 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
Tactic: rw [AffineSubspace.le_def'] at hle
Cleared hypotheses: hle
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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₃}
⊢ Sbtw R (t.points i₁) p p₁
have hp : 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₁'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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
⊢ Sbtw R (t.points i₁) p p₁
have 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₁
Tactic: have h₁i := h₁.mem_image_Ioo
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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₁
⊢ Sbtw R (t.points i₁) p p₁
have 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₂
Tactic: have h₂i := h₂.mem_image_Ioo
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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₂
⊢ Sbtw R (t.points i₁) p p₁
have 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₁
Tactic: rw [Set.mem_image] at h₁i h₂i
Cleared hypotheses: h₁i, h₂i
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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₁
⊢ Sbtw R (t.points i₁) p p₁
have 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₂
Tactic: rw [Set.mem_image] at h₁i h₂i
Cleared hypotheses: h₁i, h₂i
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
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₂
⊢ Sbtw R (t.points i₁) p p₁
have 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₁)
Tactic: rcases h₁i with ⟨r₁, ⟨hr₁0, hr₁1⟩, rfl⟩
Cleared hypotheses: p₁, h₁, h₁', h₁i
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
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
⊢ Sbtw R (t.points i₁) p ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁)
have 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₁)
Tactic: rcases h₂i with ⟨r₂, ⟨hr₂0, hr₂1⟩, rfl⟩
Cleared hypotheses: p₂, h₂, h₂', h₂i
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
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
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
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
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₁)
have rcases : ∀ (w : Fin (HAdd.hAdd (α := ℕ) 2 1) → R) (hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (2 + 1), w i) 1)
  (hp :
    Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R (Set.range t.points))
      ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P))
  (h₁' :
    Membership.mem (α := P) (γ := AffineSubspace R P)
      (affineSpan R
        (insert (t.points i₁) (singleton (α := P) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁ : P))))
      ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P))
  (h₂' :
    Membership.mem (α := P) (γ := AffineSubspace R P)
      (affineSpan R
        (insert (t.points i₂) (singleton (α := P) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂ : P))))
      ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)),
  Sbtw R (t.points i₁) ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w)
    ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁)
Tactic: rcases eq_affineCombination_of_mem_affineSpan_of_fintype hp with ⟨w, hw, rfl⟩
Cleared hypotheses: p, hp, h₁', h₂'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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₂
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₃}
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₃)
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₃)
w : Fin (HAdd.hAdd (α := ℕ) 2 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (2 + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R (Set.range t.points))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (t.points i₁) (singleton (α := P) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁ : P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₂' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (t.points i₂) (singleton (α := P) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂ : P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
⊢ Sbtw R (t.points i₁) ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w)
    ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁)
have h₁s : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
  ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
Tactic: have h₁s :=
    sign_eq_of_affineCombination_mem_affineSpan_single_lineMap t.independent hw (Finset.mem_univ _)
      (Finset.mem_univ _) (Finset.mem_univ _) h₁₂ h₁₃ h₂₃ hr₁0 hr₁1 h₁'