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 : 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.Icc 0 1) (w i)
h : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), w i = Finset.affineCombinationLineMapWeights 0 1 (w 1) i
⊢ w = Finset.affineCombinationLineMapWeights 0 1 (w 1)

Tactic:
ext i
-- Module: Mathlib.Analysis.Convex.Between
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.Icc 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, ⋯⟩)
h₁ :
  w ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, ⋯⟩ : 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, ⋯⟩)
⊢ w i = Finset.affineCombinationLineMapWeights 0 1 (w 1) i

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.Convex.Between
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.Icc 0 1) (w i)
⊢ 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, ⋯⟩)

Tactic:
simp [← hw]
-- Module: Mathlib.Analysis.Convex.Between
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.Icc 0 1) (w i)
⊢ w ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, ⋯⟩ : 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, ⋯⟩)

Tactic:
simp [← hw]
-- Module: Mathlib.Analysis.Convex.Between
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.Icc 0 1) (w i)
⊢ 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]
-- Module: Mathlib.Analysis.Convex.Between
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.Icc 0 1) (w i)
h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
h₁ :
  Membership.mem (α := P) (affineSegment R (s.points 0) (s.points 1))
    ((lineMap (s.points 0) (s.points 1) : (a : R) → P) (w 1) : P)
⊢ Membership.mem (α := P) (affineSegment R (s.points 0) (s.points 1))
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (1 + 1) → R) → P) w : P)

Tactic:
rw [h, Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
      (Finset.mem_univ _)]

Premises used: Finset.mem_univ, Finset.univ, Finset.affineCombination_affineCombinationLineMapWeights
-- Module: Mathlib.Analysis.Convex.Between
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.Icc 0 1) (w i)
h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
⊢ Membership.mem (α := P) (affineSegment R (s.points 0) (s.points 1))
    ((lineMap (s.points 0) (s.points 1) : (a : R) → P) (w 1) : P)

Tactic:
Set.mem_image_of_mem _ (h01 _)

Premises used: affineSegment, Set.Mem, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Between
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.Icc 0 1) (w i)
h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
⊢ Membership.mem (α := P) (affineSegment R (s.points 0) (s.points 1))
    ((lineMap (s.points 0) (s.points 1) : (a : R) → P) (w 1) : P)

Tactic:
exact Set.mem_image_of_mem _ (h01 _)

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Between
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
h :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)),
    Membership.mem (γ := Set R) (Set.Icc 0 1) (Finset.affineCombinationLineMapWeights 0 1 r i)
⊢ Membership.mem (α := P) s.closedInterior ((lineMap (s.points 0) (s.points 1) : (a : R) → P) r : P)

Tactic:
rw [← Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
      (Finset.mem_univ _), affineCombination_mem_closedInterior_iff
        (Finset.sum_affineCombinationLineMapWeights _ (Finset.mem_univ _) (Finset.mem_univ _) _)]

Premises used: Affine.Simplex.affineCombination_mem_closedInterior_iff, Finset.mem_univ, Finset.univ, Finset.affineCombination_affineCombinationLineMapWeights, Finset.sum_affineCombinationLineMapWeights
-- Module: Mathlib.Analysis.Convex.Between
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.Icc 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))))
h₁ :
  Membership.mem (γ := Set R) (Set.Icc 0 1)
    (Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 r
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))))
⊢ Membership.mem (γ := Set R) (Set.Icc 0 1) (Finset.affineCombinationLineMapWeights 0 1 r i)

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.Convex.Between
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 (γ := Set R) (Set.Icc 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))))

Tactic:
simp [h0, h1]
-- Module: Mathlib.Analysis.Convex.Between
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 (γ := Set R) (Set.Icc 0 1)
    (Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 r
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))))

Tactic:
simp [h0, h1]
-- Module: Mathlib.Analysis.Convex.Between
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
rw : p ∈ affineSegment R (s.points 0) (s.points 1) ↔ Wbtw R (s.points 0) p (s.points 1)
rw₁ rw₂ : p ∈ affineSegment R (s.points 0) (s.points 1) ↔ p ∈ affineSegment R (s.points 0) (s.points 1)
⊢ p ∈ s.closedInterior ↔ Wbtw R (s.points 0) p (s.points 1)

Tactic:
rw [closedInterior_eq_affineSegment, Wbtw]

Premises used: Wbtw, Affine.Simplex.closedInterior_eq_affineSegment
-- Module: Mathlib.Analysis.Convex.Between
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
inl :
  ∀ (hij : i < j), affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
inr :
  ∀ (hji : j < i), affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
⊢ affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))

Tactic:
rcases h.lt_or_gt with hij | hji

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.Convex.Between
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
hij : i < j
⊢ affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))

Tactic:
simp [min_eq_left hij.le, max_eq_right hij.le]

Premises used: LT.lt.le, max_eq_right, min_eq_left
-- Module: Mathlib.Analysis.Convex.Between
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
hji : j < i
inr : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (max i j)) (s.points (min i j))
⊢ affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))

Tactic:
nth_rw 2 [affineSegment_comm]

Premises used: affineSegment_comm
-- Module: Mathlib.Analysis.Convex.Between
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
hji : j < i
⊢ affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (max i j)) (s.points (min i j))

Tactic:
simp [max_eq_left hji.le, min_eq_right hji.le]

Premises used: LT.lt.le, max_eq_left, min_eq_right
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))

Tactic:
have h' : affineSegment R (s.points i) (s.points j) =
      affineSegment R (s.points (min i j)) (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 [affineSegment_comm]
      simp [max_eq_left hji.le, min_eq_right hji.le]
-- Module: Mathlib.Analysis.Convex.Between
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))
rw :
  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))
⊢ (s.face (fs := {i, j}) ⋯).closedInterior = affineSegment R (s.points i) (s.points j)

Tactic:
rw [h', (s.face (Finset.card_pair h)).closedInterior_eq_affineSegment, face_points, face_points]

Premises used: Affine.Simplex.face_points, Affine.Simplex.closedInterior_eq_affineSegment, Affine.Simplex.face, Finset.card_pair
-- Module: Mathlib.Analysis.Convex.Between
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
e_y : (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 1 = 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))

Tactic:
congr 2
-- Module: Mathlib.Analysis.Convex.Between
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))
⊢ Eq (α := Fin (n + 1))
    ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1))
        ⟨0, closedInterior_face_eq_affineSegment._proof_1⟩ :
      Fin (n + 1))
    (Finset.min' {i, j} ⋯ : Fin (n + 1))

Tactic:
Finset.orderEmbOfFin_zero _ _

Premises used: Finset.orderEmbOfFin_zero
-- Module: Mathlib.Analysis.Convex.Between
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} ⋯
e_x : 0 < HAdd.hAdd (α := ℕ) 1 1
⊢ (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 0 = min i j

Tactic:
convert! Finset.orderEmbOfFin_zero _ _

Premises used: Finset.orderEmbOfFin_zero
-- Module: Mathlib.Analysis.Convex.Between
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))
⊢ min i j = Finset.min' {i, j} ⋯

Tactic:
(Finset.min'_pair i j).symm

Premises used: Finset.min'_pair, Eq.symm
-- Module: Mathlib.Analysis.Convex.Between
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))
⊢ min i j = Finset.min' {i, j} ⋯

Tactic:
exact (Finset.min'_pair i j).symm

Premises used: Finset.min'_pair, Eq.symm
-- Module: Mathlib.Analysis.Convex.Between
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))
⊢ 0 < HAdd.hAdd (α := ℕ) 1 1

Tactic:
lia
-- Module: Mathlib.Analysis.Convex.Between
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))
⊢ Eq (α := Fin (n + 1))
    ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) ⟨HAdd.hAdd (α := ℕ) 1 1 - 1, ⋯⟩ : Fin (n + 1))
    (Finset.max' {i, j} ⋯ : Fin (n + 1))

Tactic:
Finset.orderEmbOfFin_last _ _

Premises used: Finset.orderEmbOfFin_last
-- Module: Mathlib.Analysis.Convex.Between
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} ⋯
e_y : 0 < HAdd.hAdd (α := ℕ) 1 1
⊢ (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 1 = max i j

Tactic:
convert! Finset.orderEmbOfFin_last _ _

Premises used: Finset.orderEmbOfFin_last
-- Module: Mathlib.Analysis.Convex.Between
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))
⊢ max i j = Finset.max' {i, j} ⋯

Tactic:
(Finset.max'_pair i j).symm

Premises used: Finset.max'_pair, Eq.symm
-- Module: Mathlib.Analysis.Convex.Between
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))
⊢ max i j = Finset.max' {i, j} ⋯

Tactic:
exact (Finset.max'_pair i j).symm

Premises used: Finset.max'_pair, Eq.symm
-- Module: Mathlib.Analysis.Convex.Between
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)
rw₁ rw₂ : p ∈ affineSegment R (s.points i) (s.points j) ↔ p ∈ affineSegment R (s.points i) (s.points j)
⊢ p ∈ (s.face (fs := {i, j}) ⋯).closedInterior ↔ Wbtw R (s.points i) p (s.points j)

Tactic:
rw [s.closedInterior_face_eq_affineSegment h, Wbtw]

Premises used: Wbtw, Affine.Simplex.closedInterior_face_eq_affineSegment
-- Module: Mathlib.Analysis.Convex.Between
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
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
⊢ s.interior = Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1)

Tactic:
ext p
-- Module: Mathlib.Analysis.Convex.Between
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
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
⊢ 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
-- Module: Mathlib.Analysis.Convex.Between
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 0 + w 1 = 1

Tactic:
rw [Fin.sum_univ_two] at hw

Premises used: Fin.sum_univ_two
-- Module: Mathlib.Analysis.Convex.Between
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)
hw₁ : w 0 + w 1 = 1
⊢ ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Ioo 0 1) (w i)

Tactic:
rw [Fin.sum_univ_two] at hw

Premises used: Fin.sum_univ_two
-- Module: Mathlib.Analysis.Convex.Between
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)
h : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), w i = Finset.affineCombinationLineMapWeights 0 1 (w 1) i
⊢ w = Finset.affineCombinationLineMapWeights 0 1 (w 1)

Tactic:
ext i
-- Module: Mathlib.Analysis.Convex.Between
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, ⋯⟩)
h₁ :
  w ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, ⋯⟩ : 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, ⋯⟩)
⊢ w i = Finset.affineCombinationLineMapWeights 0 1 (w 1) i

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.Convex.Between
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 ((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, ⋯⟩)

Tactic:
simp [← hw]