awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
p : P
h :
  p ∈ Simplex.setInterior I (s.reindex e) →
    ∀ (w : Fin (m + 1) → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1) (hwI : ∀ (i : Fin (m + 1)), w i ∈ I)
      (h : (affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w = p),
      p ∈ Simplex.setInterior I s
h₁ :
  p ∈ Simplex.setInterior I s →
    ∀ (w : Fin (n + 1) → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1) (hwI : ∀ (i : Fin (n + 1)), w i ∈ I)
      (h : (affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w = p),
      p ∈ Simplex.setInterior I (s.reindex e)
⊢ p ∈ Simplex.setInterior I (s.reindex e) ↔ p ∈ Simplex.setInterior I s

Tactic:
refine ⟨fun ⟨w, hw, hwI, h⟩ ↦ ?_, fun ⟨w, hw, hwI, h⟩ ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
p : P
h_1 : p ∈ Simplex.setInterior I (s.reindex e)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
h : (affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w = p
h₁ :
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
      ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P) →
    Membership.mem (α := P) (Simplex.setInterior I s)
      ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)
⊢ p ∈ Simplex.setInterior I s

Tactic:
subst h
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
h_1 :
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)
h :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) : (a : Fin (m + 1) → k) → P) w :
      P)
⊢ Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)

Tactic:
simp_rw [reindex]

Premises used: Affine.Simplex.reindex
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
h_1 :
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)
h :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) : P)
⊢ Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) : (a : Fin (m + 1) → k) → P) w :
      P)

Tactic:
rw [← Function.comp_id w, ← e.self_comp_symm, ← Function.comp_assoc,
      ← Equiv.coe_toEmbedding, ← Finset.univ.affineCombination_map e.symm.toEmbedding,
      map_univ_equiv]

Premises used: Function.comp_id, Finset.univ, Equiv.coe_toEmbedding, Finset.map_univ_equiv, Finset.affineCombination_map, Equiv.self_comp_symm, Equiv.toEmbedding, Equiv.symm, Function.comp_assoc
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)
rwa : (Finset.map e.toEmbedding univ).sum w = 1
rwa₁ rwa₂ rwa₃ rwa₄ : Finset.sum univ w = 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) i) 1

Tactic:
rwa [sum_comp_equiv, map_univ_equiv]

Premises used: Finset.map_univ_equiv, Finset.sum_comp_equiv
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)
⊢ Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) i) 1

Tactic:
have hw' : ∑ i, (w ∘ e) i = 1 := by rwa [sum_comp_equiv, map_univ_equiv]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
h_1 :
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)
hw' : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) i) 1
h : ∀ (i : Fin (n + 1)), (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) i ∈ I
⊢ Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) : P)

Tactic:
rw [affineCombination_mem_setInterior_iff hw']

Premises used: Affine.Simplex.affineCombination_mem_setInterior_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)
hw' : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) i) 1
⊢ ∀ (i : Fin (n + 1)), (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) i ∈ I

Tactic:
fun i ↦ hwI (e i)

Premises used: Set.Mem, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)
hw' : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) i) 1
⊢ ∀ (i : Fin (n + 1)), (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) i ∈ I

Tactic:
exact fun i ↦ hwI (e i)

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
p : P
h_1 : p ∈ Simplex.setInterior I s
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h : (affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w = p
h₁ :
  Membership.mem (α := P) (Simplex.setInterior I s)
      ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) →
    Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
      ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ p ∈ Simplex.setInterior I (s.reindex e)

Tactic:
subst h
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h_1 :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
h :
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) : (a : Fin (m + 1) → k) → P)
        (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
      P)
⊢ Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)

Tactic:
rw [← Function.comp_id w, ← Function.comp_id s.points, ← e.symm_comp_self,
      ← Function.comp_assoc, ← Function.comp_assoc, ← e.coe_toEmbedding,
      ← Finset.univ.affineCombination_map e.toEmbedding, map_univ_equiv]

Premises used: Affine.Simplex.points, Function.comp_id, Equiv.symm_comp_self, Finset.univ, Equiv.coe_toEmbedding, Finset.map_univ_equiv, Finset.affineCombination_map, Equiv.toEmbedding, Function.comp_assoc
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h_1 :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
h :
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P)
        (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
      P)
⊢ Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) : (a : Fin (m + 1) → k) → P)
        (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
      P)

Tactic:
change Finset.univ.affineCombination k (s.reindex e).points _ ∈ _

Premises used: Affine.Simplex.points, Finset.univ, Affine.Simplex.reindex, Finset.affineCombination, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
rwa : (Finset.map e.symm.toEmbedding univ).sum w = 1
rwa₁ rwa₂ rwa₃ rwa₄ : Finset.sum univ w = 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i) 1

Tactic:
rwa [sum_comp_equiv, map_univ_equiv]

Premises used: Finset.map_univ_equiv, Finset.sum_comp_equiv
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i) 1

Tactic:
have hw' : ∑ i, (w ∘ e.symm) i = 1 := by rwa [sum_comp_equiv, map_univ_equiv]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h_1 :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
hw' : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i) 1
h : ∀ (i : Fin (m + 1)), (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i ∈ I
⊢ Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P)
        (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
      P)

Tactic:
rw [affineCombination_mem_setInterior_iff hw']

Premises used: Affine.Simplex.affineCombination_mem_setInterior_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
hw' : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i) 1
⊢ ∀ (i : Fin (m + 1)), (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i ∈ I

Tactic:
fun i ↦ hwI (e.symm i)

Premises used: Set.Mem, Equiv.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
hw' : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i) 1
⊢ ∀ (i : Fin (m + 1)), (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i ∈ I

Tactic:
exact fun i ↦ hwI (e.symm i)

Premises used: Equiv.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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 J : Set k
hij : I ⊆ J
n : ℕ
s : Simplex k P n
⊢ Simplex.setInterior I s ⊆ Simplex.setInterior J s

Tactic:
fun _ ⟨w, hw, hw01, hww⟩ ↦ ⟨w, hw, fun i ↦ hij (hw01 i), hww⟩

Premises used: Affine.Simplex.setInterior, Membership.mem, Set.Subset, _private.0.Affine.Simplex.setInterior_reindex.match_2, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hi : ∀ (i : Fin (n + 1)), w i ∈ I
⊢ Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)

Tactic:
affineCombination_mem_affineSpan_of_nonempty hw _

Premises used: Set.Mem, affineCombination_mem_affineSpan_of_nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hi : ∀ (i : Fin (n + 1)), w i ∈ I
⊢ Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)

Tactic:
exact affineCombination_mem_affineSpan_of_nonempty hw _

Premises used: affineCombination_mem_affineSpan_of_nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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₂)
h :
  ∀ (p : P₂),
    p ∈ Simplex.setInterior I (s.map f hf) ↔
      Membership.mem (γ := Set P₂) ((⇑f : (a : P) → P₂) '' Simplex.setInterior I s) p
⊢ Simplex.setInterior I (s.map f hf) = (⇑f : (a : P) → P₂) '' Simplex.setInterior I s

Tactic:
ext p
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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₂
pos :
  ∀ (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
neg :
  ∀ (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
⊢ p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p

Tactic:
by_cases hp : p ∈ affineSpan k (Set.range (s.map f hf).points)

Premises used: Affine.Simplex.points, affineSpan, Affine.Simplex.map, Set.range
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
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
⊢ 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

Premises used: eq_affineCombination_of_mem_affineSpan_of_fintype
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
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₂)
⊢ p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p

Tactic:
rw [hw, Affine.Simplex.affineCombination_mem_setInterior_iff hw1, Simplex.map_points,
      ← Finset.map_affineCombination _ _ _ hw1]

Premises used: Finset.map_affineCombination, Affine.Simplex.affineCombination_mem_setInterior_iff, Affine.Simplex.map_points
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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
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
⊢ (∀ (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:
simp_rw [hf.eq_iff]

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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,
      x = (affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) fun (i : Fin (n + 1)) ↦ w i

Tactic:
simp [Affine.Simplex.affineCombination_mem_setInterior_iff hw1]

Premises used: Affine.Simplex.affineCombination_mem_setInterior_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
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)
neg₁ : ¬∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p
⊢ p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p

Tactic:
apply iff_of_false

Premises used: iff_of_false