awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
p : P₂
hp : Membership.mem (γ := AffineSubspace k P₂) (affineSpan k (Set.range (s.map f hf).points)) p
⊢ p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p
have pos : ∀ (w : Fin (n + 1) → k) (hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1)
  (hw : p = (affineCombination k univ (s.map f hf).points : (a : Fin (n + 1) → k) → P₂) w),
  p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p
Tactic: obtain ⟨w, hw1, hw⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
p : P₂
hp : Membership.mem (γ := AffineSubspace k P₂) (affineSpan k (Set.range (s.map f hf).points)) p
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hw : p = (affineCombination k univ (s.map f hf).points : (a : Fin (n + 1) → k) → P₂) w
⊢ p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p
have pos : (∀ (i : Fin (n + 1)), w i ∈ I) ↔
  ∃ x ∈ Simplex.setInterior I s,
    Eq.{u_5 + 1} (α := P₂) ((f : (a : P) → P₂) x : P₂)
      ((f : (a : P) → P₂)
          ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) fun (i : Fin (n + 1)) ↦ w i : P) :
        P₂)
Tactic: rw [hw, Affine.Simplex.affineCombination_mem_setInterior_iff hw1, Simplex.map_points,
      ← Finset.map_affineCombination _ _ _ hw1]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
p : P₂
hp : Membership.mem (γ := AffineSubspace k P₂) (affineSpan k (Set.range (s.map f hf).points)) p
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hw : p = (affineCombination k univ (s.map f hf).points : (a : Fin (n + 1) → k) → P₂) w
⊢ (∀ (i : Fin (n + 1)), w i ∈ I) ↔
    ∃ x ∈ Simplex.setInterior I s,
      Eq.{u_5 + 1} (α := P₂) ((f : (a : P) → P₂) x : P₂)
        ((f : (a : P) → P₂)
            ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) fun (i : Fin (n + 1)) ↦ w i : P) :
          P₂)
have pos : (∀ (i : Fin (n + 1)), w i ∈ I) ↔
  ∃ x ∈ Simplex.setInterior I s,
    x = (affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) fun (i : Fin (n + 1)) ↦ w i
Tactic: simp_rw [hf.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
p : P₂
hp : p ∉ affineSpan k (Set.range (s.map f hf).points)
⊢ p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p
have neg : p ∉ Simplex.setInterior I (s.map f hf)
Tactic: apply iff_of_false
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
p : P₂
hp : p ∉ affineSpan k (Set.range (s.map f hf).points)
neg : p ∉ Simplex.setInterior I (s.map f hf)
⊢ p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p
have neg₁ : ¬∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p
Tactic: apply iff_of_false
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
p : P₂
hp : p ∉ affineSpan k (Set.range (s.map f hf).points)
⊢ ¬∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p
have neg : ∀ (hp : ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p),
  Membership.mem (γ := AffineSubspace k P₂) (affineSpan k (Set.range (s.map f hf).points)) p
Tactic: contrapose hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
p : P₂
hp : ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p
⊢ Membership.mem (γ := AffineSubspace k P₂) (affineSpan k (Set.range (s.map f hf).points)) p
have neg : ∀ (q : P) (hq : q ∈ Simplex.setInterior I s) (hqp : (f : (a : P) → P₂) q = p),
  Membership.mem (γ := AffineSubspace k P₂) (affineSpan k (Set.range (s.map f hf).points)) p
Tactic: obtain ⟨q, hq, hqp⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
p : P₂
q : P
hq : q ∈ Simplex.setInterior I s
hqp : (f : (a : P) → P₂) q = p
⊢ Membership.mem (γ := AffineSubspace k P₂) (affineSpan k (Set.range (s.map f hf).points)) p
have neg : ∃ (y : P), Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) y ∧ (f : (a : P) → P₂) y = p
Tactic: rw [s.map_points, Set.range_comp, ← AffineSubspace.map_span, AffineSubspace.mem_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
I : Set k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
this : Nonempty.{u_4 + 1} ↥S := ⋯
⊢ Simplex.setInterior I (s.restrict S hS) = (⇑S.subtype : (a : ↥S) → P) ⁻¹' Simplex.setInterior I s
have rw : Simplex.setInterior I ((s.restrict S hS).map S.subtype sorry) = Simplex.setInterior I s
Tactic: rw [← S.subtype_injective.image_injective.eq_iff,
    Set.image_preimage_eq_of_subset (s.setInterior_subset_affineSpan.trans (by simpa using hS)),
    ← (s.restrict S hS).setInterior_map I S.subtype_injective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
⊢ s.points i ∉ s.interior
have rw : ∃ (x : Fin (n + 1)), (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) i 1 x : k) ∉ Set.Ioo 0 1
Tactic: rw [← Finset.univ.affineCombination_piSingle k s.points (Finset.mem_univ i),
    affineCombination_mem_interior_iff (Fintype.sum_pi_single' _ _), not_forall]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
⊢ s.points i ∈ s.closedInterior
have rw : ∀ (i_1 : Fin (n + 1)),
  Membership.mem.{u_1, u_1} (α := k) (γ := Set k) (Set.Icc 0 1) (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) i 1 i_1 : k)
Tactic: rw [← Finset.univ.affineCombination_piSingle k s.points (Finset.mem_univ i),
    affineCombination_mem_closedInterior_iff (Fintype.sum_pi_single' _ _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
i j : Fin (n + 1)
⊢ Membership.mem.{u_1, u_1} (α := k) (γ := Set k) (Set.Icc 0 1) (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) i 1 j : k)
have inl : Membership.mem.{u_1, u_1} (α := k) (γ := Set k) (Set.Icc 0 1) (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) j 1 j : k)
Tactic: obtain rfl | hj := eq_or_ne j i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
i j : Fin (n + 1)
inl :
  Membership.mem.{u_1, u_1} (α := k) (γ := Set k) (Set.Icc 0 1) (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) j 1 j : k)
⊢ Membership.mem.{u_1, u_1} (α := k) (γ := Set k) (Set.Icc 0 1) (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) i 1 j : k)
have inr : ∀ (hj : j ≠ i),
  Membership.mem.{u_1, u_1} (α := k) (γ := Set k) (Set.Icc 0 1) (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) i 1 j : k)
Tactic: obtain rfl | hj := eq_or_ne j i
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
⊢ s.interior ⊂ s.closedInterior
have rw : s.interior ⊆ s.closedInterior ∧ ∃ x ∈ s.closedInterior, x ∉ s.interior
Tactic: rw [Set.ssubset_iff_exists]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
s : Simplex k P 0
⊢ s.interior = ∅
have h : ∀ (p : P), p ∈ s.interior ↔ Membership.mem (γ := Set P) ∅ p
Tactic: ext p
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
s : Simplex k P 0
p : P
⊢ p ∈ s.interior ↔ Membership.mem (γ := Set P) ∅ p
have h : ∀ (x : Fin 1 → k),
  x 0 = 1 → (∀ (i : Fin 1), 0 < x i ∧ x i < 1) → ¬(affineCombination k {0} s.points : (a : Fin 1 → k) → P) x = p
Tactic: simp only [Simplex.interior, Simplex.setInterior, Nat.reduceAdd, univ_unique, Fin.default_eq_zero,
    Fin.isValue, sum_singleton, Set.mem_Ioo, Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false,
    not_exists, not_and]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
s : Simplex k P 0
⊢ s.closedInterior = {s.points 0}
have h : ∀ (p : P), p ∈ s.closedInterior ↔ Membership.mem (γ := Set P) {s.points 0} p
Tactic: ext p
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
s : Simplex k P 0
p : P
⊢ p ∈ s.closedInterior ↔ Membership.mem (γ := Set P) {s.points 0} p
have h : (∃ (w : Fin 1 → k),
    w 0 = 1 ∧ (∀ (i : Fin 1), 0 ≤ w i ∧ w i ≤ 1) ∧ (affineCombination k {0} s.points : (a : Fin 1 → k) → P) w = p) ↔
  p = s.points 0
Tactic: simp only [Simplex.closedInterior, Simplex.setInterior, Nat.reduceAdd, univ_unique,
    Fin.default_eq_zero, Fin.isValue, sum_singleton, Set.mem_Icc, Set.mem_setOf_eq,
    Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
s : Simplex k P 0
p : P
⊢ (∃ (w : Fin 1 → k),
      w 0 = 1 ∧ (∀ (i : Fin 1), 0 ≤ w i ∧ w i ≤ 1) ∧ (affineCombination k {0} s.points : (a : Fin 1 → k) → P) w = p) ↔
    p = s.points 0
have h : (∃ (w : Fin 1 → k),
    w 0 = 1 ∧ (∀ (i : Fin 1), 0 ≤ w i ∧ w i ≤ 1) ∧ (affineCombination k {0} s.points : (a : Fin 1 → k) → P) w = p) →
  p = s.points 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
s : Simplex k P 0
p : P
h :
  (∃ (w : Fin 1 → k),
      w 0 = 1 ∧ (∀ (i : Fin 1), 0 ≤ w i ∧ w i ≤ 1) ∧ (affineCombination k {0} s.points : (a : Fin 1 → k) → P) w = p) →
    p = s.points 0
⊢ (∃ (w : Fin 1 → k),
      w 0 = 1 ∧ (∀ (i : Fin 1), 0 ≤ w i ∧ w i ≤ 1) ∧ (affineCombination k {0} s.points : (a : Fin 1 → k) → P) w = p) ↔
    p = s.points 0
have h₁ : p = s.points 0 →
  ∃ (w : Fin 1 → k),
    w 0 = 1 ∧ (∀ (i : Fin 1), 0 ≤ w i ∧ w i ≤ 1) ∧ (affineCombination k {0} s.points : (a : Fin 1 → k) → P) w = p
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
inst_6 : NeZero m
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
⊢ Membership.mem (α := P) (s.face h).interior ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) ↔
    (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0
have rw : ((∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Ioo 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0) ↔
  (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0
Tactic: rw [s.affineCombination_mem_interior_face_iff_mem_Ioo h hw]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
inst_6 : NeZero m
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
⊢ ((∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Ioo 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0) ↔
    (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0
have refine : ((∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0) →
  ∀ (hii : ∀ i ∈ fs, 0 < w i) (hi0 : ∀ i ∉ fs, w i = 0) (i : Fin (n + 1)) (hi : i ∈ fs), w i < 1
Tactic: refine ⟨by grind, fun ⟨hii, hi0⟩ ↦ ⟨fun i hi ↦ ⟨hii i hi, ?_⟩, hi0⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
inst_6 : NeZero m
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h_1 : (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, 0 < w i
hi0 : ∀ i ∉ fs, w i = 0
i : Fin (n + 1)
hi : i ∈ fs
⊢ w i < 1
have rw : w i < ∑ x ∈ fs, w x
Tactic: rw [← hw, ← Finset.sum_subset (Finset.subset_univ fs) fun j _ ↦ hi0 j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
inst_6 : NeZero m
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h_1 : (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, 0 < w i
hi0 : ∀ i ∉ fs, w i = 0
i : Fin (n + 1)
hi : i ∈ fs
⊢ w i < ∑ x ∈ fs, w x
have obtain : ∀ (j : Fin (n + 1)) (hj : j ∈ fs) (hji : j ≠ i), w i < ∑ x ∈ fs, w x
Tactic: obtain ⟨j, hj, hji⟩ := fs.exists_mem_ne (by grind [→ NeZero.ne]) i
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
⊢ Membership.mem (α := P) (s.face h).closedInterior
      ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) ↔
    (∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0
have rw : ((∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0) ↔
  (∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0
Tactic: rw [s.affineCombination_mem_closedInterior_face_iff_mem_Icc h hw]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
⊢ ((∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0) ↔
    (∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0
have refine : ((∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0) →
  ∀ (hii : ∀ i ∈ fs, 0 ≤ w i) (hi0 : ∀ i ∉ fs, w i = 0) (i : Fin (n + 1)) (hi : i ∈ fs), w i ≤ 1
Tactic: refine ⟨by grind, fun ⟨hii, hi0⟩ ↦ ⟨fun i hi ↦ ⟨hii i hi, ?_⟩, hi0⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h_1 : (∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, 0 ≤ w i
hi0 : ∀ i ∉ fs, w i = 0
i : Fin (n + 1)
hi : i ∈ fs
⊢ w i ≤ 1
have rw : w i ≤ ∑ x ∈ fs, w x
Tactic: rw [← hw, ← Finset.sum_subset (Finset.subset_univ fs) fun j _ ↦ hi0 j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
p : P
hp : p ∈ (s.face h).closedInterior
⊢ p ∈ s.closedInterior
have hp' : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) p
Tactic: have hp' : p ∈ affineSpan k (Set.range s.points) :=
    Set.mem_of_mem_of_subset hp <|
      (s.face h).closedInterior_subset_affineSpan.trans <|
        affineSpan_mono k <| by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
p : P
hp : p ∈ (s.face h).closedInterior
hp' : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) p
⊢ p ∈ s.closedInterior
have obtain : ∀ (w : Fin (n + 1) → k) (hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1)
  (hp :
    Membership.mem (α := P) (s.face h).closedInterior
      ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P))
  (hp' :
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range s.points))
      ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)),
  Membership.mem (α := P) s.closedInterior ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
Tactic: obtain ⟨w, hw1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hp'
Cleared hypotheses: p, hp, hp'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (s.face h).closedInterior
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
hp' :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range s.points))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ Membership.mem (α := P) s.closedInterior ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
have hp₁ : (∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0
Tactic: rw [affineCombination_mem_closedInterior_face_iff_mem_Icc _ _ hw1] at hp
Cleared hypotheses: hp, hp'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : (∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0
hp' :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range s.points))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ Membership.mem (α := P) s.closedInterior ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
have rw : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
Tactic: rw [affineCombination_mem_closedInterior_iff hw1]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : (∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0
hp' :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range s.points))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
i : Fin (n + 1)
⊢ Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
have pos : ∀ (hi : i ∈ fs), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
Tactic: by_cases hi : i ∈ fs