awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w j) 1
i : Fin (n + 1)
⊢ WOppSide (affineSpan R (Set.range (s.faceOpposite i).points))
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w) (s.points i) ↔
    w i ≤ 0
have rw : WOppSide (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points i)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w) ↔
  w i ≤ 0
Tactic: rw [wOppSide_comm, s.wOppSide_affineSpan_faceOpposite_point_left_iff hw]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w j) 1
i : Fin (n + 1)
rw :
  WOppSide (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points i)
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w) ↔
    w i ≤ 0
⊢ WOppSide (affineSpan R (Set.range (s.faceOpposite i).points))
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w) (s.points i) ↔
    w i ≤ 0
have rw₁ : w i ≤ 0 ↔ w i ≤ 0
Tactic: rw [wOppSide_comm, s.wOppSide_affineSpan_faceOpposite_point_left_iff hw]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (hypothesis)
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
s : Finset ι
hs : s ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
⊢ s.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ s → b.Nonempty → b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
have hs₁ : (∃ (v : ι), s = {v}) ∨ ∃ x ∈ G.edgeSet, x.toFinset = s
Tactic: simp only [Set.mem_union, Set.mem_setOf_eq, Set.mem_image] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
s : Finset ι
hs : (∃ (v : ι), s = {v}) ∨ ∃ x ∈ G.edgeSet, x.toFinset = s
⊢ s.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ s → b.Nonempty → b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
have inl : ∀ (v : ι),
  Finset.Nonempty (α := ι) {v} ∧
    ∀ ⦃b : Finset ι⦄, b ≤ {v} → b.Nonempty → b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
Tactic: rcases hs with ⟨v, rfl⟩ | ⟨e, he, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
s : Finset ι
hs : (∃ (v : ι), s = {v}) ∨ ∃ x ∈ G.edgeSet, x.toFinset = s
inl :
  ∀ (v : ι),
    Finset.Nonempty (α := ι) {v} ∧
      ∀ ⦃b : Finset ι⦄, b ≤ {v} → b.Nonempty → b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
⊢ s.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ s → b.Nonempty → b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
have inr : ∀ (e : Sym2 ι) (he : e ∈ G.edgeSet),
  e.toFinset.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ e.toFinset → b.Nonempty → b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
Tactic: rcases hs with ⟨v, rfl⟩ | ⟨e, he, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
⊢ e.toFinset.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ e.toFinset → b.Nonempty → b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
have inr : e.toFinset.Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
inr : e.toFinset.Nonempty
⊢ e.toFinset.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ e.toFinset → b.Nonempty → b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
have inr₁ : ∀ ⦃b : Finset ι⦄, b ≤ e.toFinset → b.Nonempty → b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
b : Finset ι
hb_sub : b ≤ e.toFinset
hb_nonempty : b.Nonempty
⊢ b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
have pos : ∀ (h : #b = 1), b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
Tactic: by_cases h : b.card = 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
b : Finset ι
hb_sub : b ≤ e.toFinset
hb_nonempty : b.Nonempty
pos : ∀ (h : #b = 1), b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
⊢ b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
have neg : ∀ (h : ¬#b = 1), b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
Tactic: by_cases h : b.card = 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ Subset (α := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) ((↑s : Set E) ∩ (↑t : Set E)) : Set E)
have a : Eq (α := Set E)
  ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
  ((convexHull 𝕜 : (a : Set E) → Set E) ((↑s : Set E) ∩ (↑t : Set E)) : Set E)
Tactic: apply subset_of_eq
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ Eq (α := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) ((↑s : Set E) ∩ (↑t : Set E)) : Set E)
have a : AffineIndependent 𝕜 (P := E) (ι := ↥(s ∪ t)) (Subtype.val (p := fun (x : E) ↦ x ∈ s ∪ t))
Tactic: rw [AffineIndependent.convexHull_inter (R := 𝕜) (s := s ∪ t)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
a : AffineIndependent 𝕜 (P := E) (ι := ↥(s ∪ t)) (Subtype.val (p := fun (x : E) ↦ x ∈ s ∪ t))
⊢ Eq (α := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) ((↑s : Set E) ∩ (↑t : Set E)) : Set E)
have a₁ : s ⊆ s ∪ t
Tactic: rw [AffineIndependent.convexHull_inter (R := 𝕜) (s := s ∪ t)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
a : AffineIndependent 𝕜 (P := E) (ι := ↥(s ∪ t)) (Subtype.val (p := fun (x : E) ↦ x ∈ s ∪ t))
a₁ : s ⊆ s ∪ t
⊢ Eq (α := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) ((↑s : Set E) ∩ (↑t : Set E)) : Set E)
have a₂ : t ⊆ s ∪ t
Tactic: rw [AffineIndependent.convexHull_inter (R := 𝕜) (s := s ∪ t)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ AffineIndependent 𝕜 (P := E) (ι := ↥(s ∪ t)) (Subtype.val (p := fun (x : E) ↦ x ∈ s ∪ t))
have a : (↑(s ∪ t) : Set E) ⊆ ⋃ s ∈ abstract.faces, (↑s : Set E)
Tactic: apply indep.mono
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ (↑(s ∪ t) : Set E) ⊆ ⋃ s ∈ abstract.faces, (↑s : Set E)
have a : (↑s : Set E) ∪ (↑t : Set E) ⊆ ⋃ s ∈ abstract.faces, (↑s : Set E)
Tactic: simp only [Finset.coe_union]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : DecidableEq 𝕜
inst_2 : Field 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : IsStrictOrderedRing 𝕜
abstract : PreAbstractSimplicialComplex ι
⊢ AffineIndependent 𝕜 (P := ι →₀ 𝕜) (ι :=
    { x : ι →₀ 𝕜 //
      Membership.mem (γ := Set (ι →₀ 𝕜))
        (⋃ (s : Finset (ι →₀ 𝕜)),
          ⋃ (_ :
            Membership.mem (γ := Set (Finset (ι →₀ 𝕜)))
              (PreAbstractSimplicialComplex.faces (abstract.map fun (i : ι) ↦ Finsupp.single i 1)) s),
            (↑s : Set (ι →₀ 𝕜)))
        x })
    (Subtype.val (p := fun (x : ι →₀ 𝕜) ↦
      Membership.mem (γ := Set (ι →₀ 𝕜))
        (⋃ (s : Finset (ι →₀ 𝕜)),
          ⋃ (_ :
            Membership.mem (γ := Set (Finset (ι →₀ 𝕜)))
              (PreAbstractSimplicialComplex.faces (abstract.map fun (i : ι) ↦ Finsupp.single i 1)) s),
            (↑s : Set (ι →₀ 𝕜)))
        x))
have refine : ∀ (x : ι →₀ 𝕜)
  (hx :
    Membership.mem (γ := Set (ι →₀ 𝕜))
      (⋃ (s : Finset (ι →₀ 𝕜)),
        ⋃ (_ :
          Membership.mem (γ := Set (Finset (ι →₀ 𝕜)))
            (PreAbstractSimplicialComplex.faces (abstract.map fun (i : ι) ↦ Finsupp.single i 1)) s),
          (↑s : Set (ι →₀ 𝕜)))
      x),
  Membership.mem (γ := Set (ι →₀ 𝕜)) (Set.range fun (i : ι) ↦ Finsupp.single i 1) x
Tactic: refine (Finsupp.linearIndependent_single_one 𝕜 ι).affineIndependent.range.mono fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (hypothesis)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : DecidableEq 𝕜
inst_2 : Field 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : IsStrictOrderedRing 𝕜
abstract : PreAbstractSimplicialComplex ι
x : ι →₀ 𝕜
hx :
  Membership.mem (γ := Set (ι →₀ 𝕜))
    (⋃ (s : Finset (ι →₀ 𝕜)),
      ⋃ (_ :
        Membership.mem (γ := Set (Finset (ι →₀ 𝕜)))
          (PreAbstractSimplicialComplex.faces (abstract.map fun (i : ι) ↦ Finsupp.single i 1)) s),
        (↑s : Set (ι →₀ 𝕜)))
    x
⊢ Membership.mem (γ := Set (ι →₀ 𝕜)) (Set.range fun (i : ι) ↦ Finsupp.single i 1) x
have hx₁ : ∃ (i : Finset (ι →₀ 𝕜)) (_ :
  Membership.mem (γ := Set (Finset (ι →₀ 𝕜)))
    (PreAbstractSimplicialComplex.faces (abstract.map fun (i : ι) ↦ Finsupp.single i 1)) i),
  x ∈ i
Tactic: simp only [Set.mem_iUnion, Finset.mem_coe] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : DecidableEq 𝕜
inst_2 : Field 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : IsStrictOrderedRing 𝕜
abstract : PreAbstractSimplicialComplex ι
x : ι →₀ 𝕜
hx :
  ∃ (i : Finset (ι →₀ 𝕜)) (_ :
    Membership.mem (γ := Set (Finset (ι →₀ 𝕜)))
      (PreAbstractSimplicialComplex.faces (abstract.map fun (i : ι) ↦ Finsupp.single i 1)) i),
    x ∈ i
⊢ Membership.mem (γ := Set (ι →₀ 𝕜)) (Set.range fun (i : ι) ↦ Finsupp.single i 1) x
have obtain : ∀ w ∈ abstract.faces,
  ∀
    (hx :
      Membership.mem (γ := Finset (ι →₀ 𝕜))
        ((fun (s : Finset ι) ↦ (Finset.image (fun (i : ι) ↦ Finsupp.single i 1) s : Finset (ι →₀ 𝕜))) w) x),
    Membership.mem (γ := Set (ι →₀ 𝕜)) (Set.range fun (i : ι) ↦ Finsupp.single i 1) x
Tactic: obtain ⟨_, ⟨_, _, rfl⟩, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
⊢ (convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ⊆ K.space
have h : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
  ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
Tactic: convert! subset_biUnion_of_mem hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
⊢ Disjoint (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) ∨
    ∃ u ∈ K.faces,
      Eq (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)
have by_contra! : ∀
  (h :
    ¬Disjoint (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
          ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) ∧
      ∀ (u : Finset E) (_ : u ∈ K.faces),
        Ne (α := Set E)
          ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) :
            Set E)
          ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)),
  False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) ∧
    ∀ (u : Finset E) (_ : u ∈ K.faces),
      Ne (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)
⊢ False
have h₁ : Set.Nonempty.{u_2} (α := E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) ∧
  ∀ (u : Finset E) (_ : u ∈ K.faces),
    Ne (α := Set E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)
Tactic: rw [not_disjoint_iff_nonempty_inter] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  Set.Nonempty.{u_2} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) ∧
    ∀ (u : Finset E) (_ : u ∈ K.faces),
      Ne (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)
⊢ False
have refine_1 : (s ∩ t).Nonempty
Tactic: refine h.2 (s ∩ t) (K.down_closed hs inter_subset_left ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  Set.Nonempty.{u_2} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) ∧
    ∀ (u : Finset E) (_ : u ∈ K.faces),
      Ne (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)
refine_1 : (s ∩ t).Nonempty
⊢ False
have refine_2 : Eq (α := Set E)
  ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
  ((convexHull 𝕜 : (a : Set E) → Set E) (↑(s ∩ t) : Set E) : Set E)
Tactic: refine h.2 (s ∩ t) (K.down_closed hs inter_subset_left ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  Set.Nonempty.{u_2} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) ∧
    ∀ (u : Finset E) (_ : u ∈ K.faces),
      Ne (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)
⊢ Eq (α := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑(s ∩ t) : Set E) : Set E)
have refine_2 : Eq (α := Set E)
  ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
  ((convexHull 𝕜 : (a : Set E) → Set E) ((↑s : Set E) ∩ (↑t : Set E)) : Set E)
Tactic: rw [coe_inter, convexHull_inter_convexHull hs ht]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  Set.Nonempty.{u_2} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) ∧
    ∀ (u : Finset E) (_ : u ∈ K.faces),
      Ne (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)
refine_2 :
  Eq (α := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) ((↑s : Set E) ∩ (↑t : Set E)) : Set E)
⊢ Eq (α := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑(s ∩ t) : Set E) : Set E)
have refine_2₁ : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑s : Set E) ∩ (↑t : Set E)) : Set E)
  ((convexHull 𝕜 : (a : Set E) → Set E) ((↑s : Set E) ∩ (↑t : Set E)) : Set E)
Tactic: rw [coe_inter, convexHull_inter_convexHull hs ht]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
⊢ Disjoint (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) ∨
    ∃ u ∈ K.faces,
      Eq (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)
have by_contra! : ¬(Disjoint (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) ∨
      ∃ u ∈ K.faces,
        Eq (α := Set E)
          ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) :
            Set E)
          ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)) →
  False
Tactic: classical
  by_contra! h
  rw [not_disjoint_iff_nonempty_inter] at h
  refine h.2 (s ∩ t) (K.down_closed hs inter_subset_left ?_) ?_
  · simpa [← coe_inter] using convexHull_nonempty_iff.1 (h.1.mono (K.inter_subset_convexHull hs ht))
  · rw [coe_inter, convexHull_inter_convexHull hs ht]