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
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
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₁)
⊢ Sbtw R (t.points i₁) p ((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⟩

Premises used: eq_affineCombination_of_mem_affineSpan_of_fintype, 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₂
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)
⊢ 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₁'
-- 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₂
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)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
⊢ 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₁₂.symm h₂₃ h₁₃ hr₂0 hr₂1 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₂
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 (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ 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)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
⊢ Sbtw.{u_1, u_2, u_4} R (P := P)
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
        (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
      P)
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
        (Finset.affineCombinationLineMapWeights i₂ i₃ r₁) :
      P)

Tactic:
Sbtw.affineCombination_of_mem_affineSpan_pair t.independent hw (Fintype.sum_pi_single' _ _)
      (Finset.univ.sum_affineCombinationLineMapWeights (Finset.mem_univ _) (Finset.mem_univ _) _)
      h₁' (Finset.mem_univ i₁) ?_

Premises used: Finset.mem_univ, Finset.univ, Sbtw.affineCombination_of_mem_affineSpan_pair, Finset.sum_affineCombinationLineMapWeights, Affine.Simplex.independent, Fintype.sum_pi_single'
-- 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₂
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 (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ 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)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hw₁ :
  Sbtw R (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1 i₁) (w i₁)
    (Finset.affineCombinationLineMapWeights i₂ i₃ r₁ i₁)
⊢ Sbtw.{u_1, u_2, u_4} R (P := P)
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
        (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
      P)
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
        (Finset.affineCombinationLineMapWeights i₂ i₃ r₁) :
      P)

Tactic:
refine
    Sbtw.affineCombination_of_mem_affineSpan_pair t.independent hw (Fintype.sum_pi_single' _ _)
      (Finset.univ.sum_affineCombinationLineMapWeights (Finset.mem_univ _) (Finset.mem_univ _) _)
      h₁' (Finset.mem_univ i₁) ?_

Premises used: Finset.mem_univ, Finset.univ, Sbtw.affineCombination_of_mem_affineSpan_pair, Finset.sum_affineCombinationLineMapWeights, Affine.Simplex.independent, Fintype.sum_pi_single'
-- 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₂
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 (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ 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)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
rw : Membership.mem (γ := Set R) (Set.Ioo 0 1) (w i₁)
⊢ Sbtw R (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1 i₁) (w i₁)
    (Finset.affineCombinationLineMapWeights i₂ i₃ r₁ i₁)

Tactic:
rw [Pi.single_eq_same,
    Finset.affineCombinationLineMapWeights_apply_of_ne h₁₂ h₁₃, sbtw_one_zero_iff]

Premises used: Pi.single_eq_same, sbtw_one_zero_iff, Finset.affineCombinationLineMapWeights_apply_of_ne
-- 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₃ : Fin 3
h₂₃ : 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
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₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
i : Fin 3
h₁₂ : i ≠ i₂
h₁₃ : i ≠ i₃
h3 : ∀ (i_1 : Fin 3), i_1 = i ∨ i_1 = i₂ ∨ i_1 = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i, i₂, i₃}
h₂ : Sbtw R (t.points i) ((lineMap (t.points i) (t.points i₃) : (a : R) → P) r₂) (t.points i₃)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ 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)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)

Tactic:
h₂s
-- 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₃ : Fin 3
h₂₃ : 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
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₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
i : Fin 3
h₁₂ : i ≠ i₂
h₁₃ : i ≠ i₃
h3 : ∀ (i_1 : Fin 3), i_1 = i ∨ i_1 = i₂ ∨ i_1 = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i, i₂, i₃}
h₂ : Sbtw R (t.points i) ((lineMap (t.points i) (t.points i₃) : (a : R) → P) r₂) (t.points i₃)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ 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)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)

Tactic:
exact h₂s
-- 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₃ : Fin 3
h₁₃ : i₁ ≠ i₃
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
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₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
i : Fin 3
h₁₂ : i₁ ≠ i
h₂₃ : i ≠ i₃
h3 : ∀ (i_1 : Fin 3), i_1 = i₁ ∨ i_1 = i ∨ i_1 = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i, i₃}
h₁ : Sbtw R (t.points i) ((lineMap (t.points i) (t.points i₃) : (a : R) → P) r₁) (t.points i₃)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i i₃ 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)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)

Tactic:
h₁s
-- 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₃ : Fin 3
h₁₃ : i₁ ≠ i₃
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
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₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
i : Fin 3
h₁₂ : i₁ ≠ i
h₂₃ : i ≠ i₃
h3 : ∀ (i_1 : Fin 3), i_1 = i₁ ∨ i_1 = i ∨ i_1 = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i, i₃}
h₁ : Sbtw R (t.points i) ((lineMap (t.points i) (t.points i₃) : (a : R) → P) r₁) (t.points i₃)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i i₃ 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)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)

Tactic:
exact h₁s