awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
h' : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
⊢ affineSegment R (s.points ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 0))
      (s.points ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 1)) =
    affineSegment R (s.points (min i j)) (s.points (max i j))
have e_x : (Finset.orderEmbOfFin {i, j} sorry : (a : Fin (1 + 1)) → Fin (n + 1)) 0 = min i j
Tactic: congr 2
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
h' : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
e_x : (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 0 = min i j
⊢ affineSegment R (s.points ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 0))
      (s.points ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 1)) =
    affineSegment R (s.points (min i j)) (s.points (max i j))
have e_y : (Finset.orderEmbOfFin {i, j} sorry : (a : Fin (1 + 1)) → Fin (n + 1)) 1 = max i j
Tactic: congr 2
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
h' : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
⊢ (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 0 = min i j
have h₁ : min i j = Finset.min' {i, j} sorry
Tactic: convert! Finset.orderEmbOfFin_zero _ _
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
h' : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
h₁ : min i j = Finset.min' {i, j} ⋯
⊢ (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 0 = min i j
have e_x : 0 < HAdd.hAdd (α := ℕ) 1 1
Tactic: convert! Finset.orderEmbOfFin_zero _ _
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
h' : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
⊢ (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 1 = max i j
have h₁ : max i j = Finset.max' {i, j} sorry
Tactic: convert! Finset.orderEmbOfFin_last _ _
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
h' : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
h₁ : max i j = Finset.max' {i, j} ⋯
⊢ (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 1 = max i j
have e_y : 0 < HAdd.hAdd (α := ℕ) 1 1
Tactic: convert! Finset.orderEmbOfFin_last _ _
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
⊢ p ∈ (s.face (fs := {i, j}) ⋯).closedInterior ↔ Wbtw R (s.points i) p (s.points j)
have rw : p ∈ affineSegment R (s.points i) (s.points j) ↔ Wbtw R (s.points i) p (s.points j)
Tactic: rw [s.closedInterior_face_eq_affineSegment h, Wbtw]
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
rw : p ∈ affineSegment R (s.points i) (s.points j) ↔ Wbtw R (s.points i) p (s.points j)
⊢ p ∈ (s.face (fs := {i, j}) ⋯).closedInterior ↔ Wbtw R (s.points i) p (s.points j)
have rw₁ : p ∈ affineSegment R (s.points i) (s.points j) ↔ p ∈ affineSegment R (s.points i) (s.points j)
Tactic: rw [s.closedInterior_face_eq_affineSegment h, Wbtw]
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
⊢ s.interior = Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1)
have h : ∀ (p : P),
  p ∈ s.interior ↔
    Membership.mem (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1)) p
Tactic: ext p
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
p : P
⊢ p ∈ s.interior ↔
    Membership.mem (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1)) p
have h : p ∈ s.interior →
  Membership.mem (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1)) p
Tactic: constructor
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
p : P
h :
  p ∈ s.interior →
    Membership.mem (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1)) p
⊢ p ∈ s.interior ↔
    Membership.mem (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1)) p
have h₁ : Membership.mem (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1)) p →
  p ∈ s.interior
Tactic: constructor
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (1 + 1), w i) 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Ioo 0 1) (w i)
⊢ w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
have hw₁ : w 0 + w 1 = 1
Tactic: rw [Fin.sum_univ_two] at hw
Cleared hypotheses: hw, h01
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : w 0 + w 1 = 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Ioo 0 1) (w i)
⊢ w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
have h : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), w i = Finset.affineCombinationLineMapWeights 0 1 (w 1) i
Tactic: ext 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : w 0 + w 1 = 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Ioo 0 1) (w i)
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ w i = Finset.affineCombinationLineMapWeights 0 1 (w 1) i
have h : w ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) =
  Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 (w 1)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : w 0 + w 1 = 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Ioo 0 1) (w i)
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  w ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) =
    Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 (w 1)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩)
⊢ w i = Finset.affineCombinationLineMapWeights 0 1 (w 1) i
have h₁ : w ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) =
  Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 (w 1)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (1 + 1), w i) 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Ioo 0 1) (w i)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1))
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (1 + 1) → R) → P) w : P)
have h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
Tactic: have h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1) := by
      rw [Fin.sum_univ_two] at hw
      ext i
      fin_cases i <;> simp [← hw]
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (1 + 1), w i) 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Ioo 0 1) (w i)
h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1))
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (1 + 1) → R) → P) w : P)
have h₁ : Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
  (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1))
  ((lineMap (s.points 0) (s.points 1) : (a : R) → P) (w 1) : P)
Tactic: rw [h, Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
      (Finset.mem_univ _)]
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 < r
h1 : r < 1
⊢ Membership.mem (α := P) s.interior ((lineMap (s.points 0) (s.points 1) : (a : R) → P) r : P)
have h : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)),
  Membership.mem (γ := Set R) (Set.Ioo 0 1) (Finset.affineCombinationLineMapWeights 0 1 r i)
Tactic: rw [← Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
      (Finset.mem_univ _), affineCombination_mem_interior_iff
        (Finset.sum_affineCombinationLineMapWeights _ (Finset.mem_univ _) (Finset.mem_univ _) _)]
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 < r
h1 : r < 1
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ Membership.mem (γ := Set R) (Set.Ioo 0 1) (Finset.affineCombinationLineMapWeights 0 1 r i)
have h : Membership.mem (γ := Set R) (Set.Ioo 0 1)
  (Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 r
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))))
Tactic: fin_cases i
Cleared hypotheses: 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 < r
h1 : r < 1
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  Membership.mem (γ := Set R) (Set.Ioo 0 1)
    (Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 r
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))))
⊢ Membership.mem (γ := Set R) (Set.Ioo 0 1) (Finset.affineCombinationLineMapWeights 0 1 r i)
have h₁ : Membership.mem (γ := Set R) (Set.Ioo 0 1)
  (Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 r
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))))
Tactic: fin_cases i
Cleared hypotheses: 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
s : Simplex R P 1
p : P
⊢ p ∈ s.interior ↔ Sbtw R (s.points 0) p (s.points 1)
have rw : Membership.mem (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1)) p ↔
  Membership.mem (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1)) p ∧
    s.points 0 ≠ s.points 1
Tactic: rw [interior_eq_image_Ioo, sbtw_iff_mem_image_Ioo_and_ne]
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
⊢ Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
have inl : ∀ (hij : i < j), Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
Tactic: rcases h.lt_or_gt with hij | hji
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
inl : ∀ (hij : i < j), Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
have inr : ∀ (hji : j < i), Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
Tactic: rcases h.lt_or_gt with hij | hji
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
hji : j < i
⊢ Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
have inr : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (max i j)) p (s.points (min i j))
Tactic: nth_rw 2 [sbtw_comm]
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
⊢ p ∈ (s.face (fs := {i, j}) ⋯).interior ↔ Sbtw R (s.points i) p (s.points j)
have h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
Tactic: have h' : Sbtw R (s.points i) p (s.points j) ↔
      Sbtw R (s.points (min i j)) p (s.points (max i j)) := by
    rcases h.lt_or_gt with hij | hji
    · simp [min_eq_left hij.le, max_eq_right hij.le]
    · nth_rw 2 [sbtw_comm]
      simp [max_eq_left hji.le, min_eq_right hji.le]
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ p ∈ (s.face (fs := {i, j}) ⋯).interior ↔ Sbtw R (s.points i) p (s.points j)
have rw : Sbtw R (s.points ((Finset.orderEmbOfFin {i, j} sorry : (a : Fin (1 + 1)) → Fin (n + 1)) 0)) p
    (s.points ((Finset.orderEmbOfFin {i, j} sorry : (a : Fin (1 + 1)) → Fin (n + 1)) 1)) ↔
  Sbtw R (s.points (min i j)) p (s.points (max i j))
Tactic: rw [h', mem_interior_iff_sbtw, face_points, face_points]
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ Sbtw R (s.points ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 0)) p
      (s.points ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 1)) ↔
    Sbtw R (s.points (min i j)) p (s.points (max i j))
have a : (Finset.orderEmbOfFin {i, j} sorry : (a : Fin (1 + 1)) → Fin (n + 1)) 0 = min i j
Tactic: congr! 4
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
a : (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 0 = min i j
⊢ Sbtw R (s.points ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 0)) p
      (s.points ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 1)) ↔
    Sbtw R (s.points (min i j)) p (s.points (max i j))
have a₁ : (Finset.orderEmbOfFin {i, j} sorry : (a : Fin (1 + 1)) → Fin (n + 1)) 1 = max i j
Tactic: congr! 4
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 0 = min i j
have h₁ : min i j = Finset.min' {i, j} sorry
Tactic: convert! Finset.orderEmbOfFin_zero _ _
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
h₁ : min i j = Finset.min' {i, j} ⋯
⊢ (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 0 = min i j
have a : 0 < HAdd.hAdd (α := ℕ) 1 1
Tactic: convert! Finset.orderEmbOfFin_zero _ _
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 1 = max i j
have h₁ : max i j = Finset.max' {i, j} sorry
Tactic: convert! Finset.orderEmbOfFin_last _ _
-- 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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
h₁ : max i j = Finset.max' {i, j} ⋯
⊢ (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 1 = max i j
have a : 0 < HAdd.hAdd (α := ℕ) 1 1
Tactic: convert! Finset.orderEmbOfFin_last _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : Wbtw R x y z
⊢ SameRay R (y -ᵥ x) (z -ᵥ x)
have rcases : ∀ (t : R) (ht0 : 0 ≤ t), t ≤ 1 → SameRay R ((lineMap x z : (a : R) → P) t -ᵥ x) (z -ᵥ x)
Tactic: rcases h with ⟨t, ⟨ht0, _⟩, rfl⟩
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : Wbtw R x y z
⊢ SameRay R (z -ᵥ x) (z -ᵥ y)
have rcases : ∀ (t : R), 0 ≤ t → ∀ (ht1 : t ≤ 1), SameRay R (z -ᵥ x) (z -ᵥ (lineMap x z : (a : R) → P) t)
Tactic: rcases h with ⟨t, ⟨_, ht1⟩, rfl⟩
Cleared hypotheses: y, h