awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
by_contra! by_contra!₁ by_contra!₂ 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
⊢ 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 : 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: 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]
-- 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
by_contra! by_contra!₁ by_contra!₂ 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
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ 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
⊢ 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 :
    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
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]
-- 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
by_contra! by_contra!₁ by_contra!₂ 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
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ 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
by_contra!₁₁ :
  ∀
    (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
⊢ 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 refine_1 : ∀
  (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)),
  (s ∩ t).Nonempty
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]
-- 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
x : E
faces : Set (Finset E)
indep : ∀ s ∈ faces, AffineIndependent 𝕜 (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
down_closed : IsLowerSet faces
inter_subset_convexHull :
  ∀ s ∈ faces,
    ∀ t ∈ 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)
⊢ IsRelLowerSet (faces \ {∅}) Finset.Nonempty
have this : faces \ {∅} = {f : Finset E | f ∈ faces ∧ f.Nonempty}
Tactic: have : faces \ {∅} = {f ∈ faces | f.Nonempty} := by grind
-- 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
⊢ K.vertices = ⋃ k ∈ K.faces, (↑k : Set E)
have h : ∀ (x : E), x ∈ K.vertices ↔ Membership.mem (γ := Set E) (⋃ k ∈ K.faces, (↑k : Set E)) x
Tactic: ext x
-- 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
x : E
⊢ x ∈ K.vertices ↔ Membership.mem (γ := Set E) (⋃ k ∈ K.faces, (↑k : Set E)) x
have h : ∀ (h : Membership.mem (γ := Set E) (⋃ k ∈ K.faces, (↑k : Set E)) x), x ∈ K.vertices
Tactic: refine ⟨fun h => mem_biUnion h <| mem_coe.2 <| mem_singleton_self x, fun 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
x : E
h : Membership.mem (γ := Set E) (⋃ k ∈ K.faces, (↑k : Set E)) x
⊢ x ∈ K.vertices
have h₁ : ∀ (s : Finset E) (hs : s ∈ K.faces) (hx : x ∈ (↑s : Set E)), x ∈ K.vertices
Tactic: obtain ⟨s, hs, hx⟩ := mem_iUnion₂.1 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 : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x ↔ x ∈ s
have refine : ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x), x ∈ s
Tactic: refine ⟨fun h => ?_, fun h => subset_convexHull 𝕜 _ 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 : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x
⊢ x ∈ s
have h₁ : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑{x} : Set E) ∩ (↑s : Set E)) : Set E) x
Tactic: have h := K.inter_subset_convexHull hx hs ⟨by simp, 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 : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h_1 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x
h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑{x} : Set E) ∩ (↑s : Set E)) : Set E) x
⊢ x ∈ s
have by_contra : ∀ (H : ¬x ∈ s), False
Tactic: by_contra 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 : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h_1 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x
h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑{x} : Set E) ∩ (↑s : Set E)) : Set E) x
H : ¬x ∈ s
⊢ False
have rwa : ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑({x} ∩ s) : Set E) : Set E) x) (H : ¬x ∈ s),
  False
Tactic: rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm,
    coe_empty, convexHull_empty] at h
Cleared hypotheses: h, 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 : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h_1 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x
h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑{x} : Set E) ∩ (↑s : Set E)) : Set E) x
H : ¬x ∈ s
rwa :
  ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑({x} ∩ s) : Set E) : Set E) x)
    (H : ¬x ∈ s), False
⊢ False
have rwa₁ : ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑∅ : Set E) : Set E) x) (H : ¬x ∈ s), False
Tactic: rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm,
    coe_empty, convexHull_empty] at h
Cleared hypotheses: h, 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 : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h_1 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x
h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑{x} : Set E) ∩ (↑s : Set E)) : Set E) x
H : ¬x ∈ s
rwa :
  ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑({x} ∩ s) : Set E) : Set E) x)
    (H : ¬x ∈ s), False
rwa₁ :
  ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑∅ : Set E) : Set E) x) (H : ¬x ∈ s), False
⊢ False
have rwa₂ : ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ∅ : Set E) x) (H : ¬x ∈ s), False
Tactic: rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm,
    coe_empty, convexHull_empty] at h
Cleared hypotheses: h, 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 : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h_1 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x
h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑{x} : Set E) ∩ (↑s : Set E)) : Set E) x
H : ¬x ∈ s
rwa :
  ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑({x} ∩ s) : Set E) : Set E) x)
    (H : ¬x ∈ s), False
rwa₁ :
  ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑∅ : Set E) : Set E) x) (H : ¬x ∈ s), False
rwa₂ : ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ∅ : Set E) x) (H : ¬x ∈ s), False
⊢ False
have rwa₃ : ∀ (h : Membership.mem (γ := Set E) ∅ x) (H : ¬x ∈ s), False
Tactic: rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm,
    coe_empty, convexHull_empty] at h
Cleared hypotheses: h, 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 : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x
⊢ x ∈ s
have have : ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑{x} : Set E) ∩ (↑s : Set E)) : Set E) x),
  x ∈ s
Tactic: classical
  have h := K.inter_subset_convexHull hx hs ⟨by simp, h⟩
  by_contra H
  rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm,
    coe_empty, convexHull_empty] at 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 : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x
have have₁ have₂ :
  ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑{x} : Set E) ∩ (↑s : Set E)) : Set E) x),
    x ∈ s
⊢ x ∈ s
have have₃ : ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑{x} : Set E) ∩ (↑s : Set E)) : Set E) x)
  (H : ¬x ∈ s), False
Tactic: classical
  have h := K.inter_subset_convexHull hx hs ⟨by simp, h⟩
  by_contra H
  rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm,
    coe_empty, convexHull_empty] at 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 : Finset E
hs : s ∈ K.faces
⊢ s ∉ K.facets ↔ ∃ t ∈ K.faces, s ⊂ t
have refine_1 : ∀ (hs' : ¬(s ∈ K.faces ∧ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t)), ∃ t ∈ K.faces, s ⊂ t
Tactic: refine ⟨fun 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 : Finset E
hs : s ∈ K.faces
refine_1 : ∀ (hs' : ¬(s ∈ K.faces ∧ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t)), ∃ t ∈ K.faces, s ⊂ t
⊢ s ∉ K.facets ↔ ∃ t ∈ K.faces, s ⊂ t
have refine_2 : (∃ t ∈ K.faces, s ⊂ t) → s ∉ K.facets
Tactic: refine ⟨fun hs' : ¬(_ ∧ _) => ?_, ?_⟩
-- 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 : Finset E
hs : s ∈ K.faces
hs' : ¬(s ∈ K.faces ∧ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t)
⊢ ∃ t ∈ K.faces, s ⊂ t
have hs'₁ : ∀ (_ : s ∈ K.faces), ∃ t ∈ K.faces, s ⊆ t ∧ s ≠ t
Tactic: push Not at hs'
Cleared hypotheses: 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 : Finset E
hs : s ∈ K.faces
hs' : ∀ (_ : s ∈ K.faces), ∃ t ∈ K.faces, s ⊆ t ∧ s ≠ t
⊢ ∃ t ∈ K.faces, s ⊂ t
have refine_1 : ∀ (t : Finset E) (ht : t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t), ∃ t ∈ K.faces, s ⊂ t
Tactic: obtain ⟨t, ht⟩ := hs' hs
-- 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 : Finset E
hs_1 : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ s ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
⊢ False
have this : s = t
Tactic: have := hs' ht.1 ht.2.1
-- 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 : Finset E
hs_1 : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ s ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
this : s = t
⊢ False
have ht₁ : t ∈ K.faces ∧ t ⊂ t
Tactic: rw [this] at ht
Cleared hypotheses: ht, hs, hs', this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have hxz : x < z
Tactic: have hxz := hxy.trans hyz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxz : x < z
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have hxy₁ : 0 < y - x
Tactic: rw [← sub_pos] at hxy hxz hyz
Cleared hypotheses: hxy, hyz, hxz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxz : x < z
hxy₁ : 0 < y - x
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have hyz₁ : 0 < z - y
Tactic: rw [← sub_pos] at hxy hxz hyz
Cleared hypotheses: hxy, hyz, hxz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxz : x < z
hxy₁ : 0 < y - x
hyz₁ : 0 < z - y
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have hxz₁ : 0 < z - x
Tactic: rw [← sub_pos] at hxy hxz hyz
Cleared hypotheses: hxy, hyz, hxz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have ha : 0 ≤ (z - y) / (z - x)
Tactic: have ha : 0 ≤ (z - y) / (z - x) := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have hb : 0 ≤ (y - x) / (z - x)
Tactic: have hb : 0 ≤ (y - x) / (z - x) := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have key : f (((z - y) / (z - x)) • x + ((y - x) / (z - x)) • z) ≤ ((z - y) / (z - x)) • f x + ((y - x) / (z - x)) • f z
Tactic: have key := hf.2 hx hz ha hb (by field)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
key : f ((z - y) / (z - x) * x + (y - x) / (z - x) * z) ≤ (z - y) / (z - x) * f x + (y - x) / (z - x) * f z
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have key₁ : f (z * y * (z - x)⁻¹ - y * x * (z - x)⁻¹) ≤
  z * (z - x)⁻¹ * f x - y * (z - x)⁻¹ * f x + y * (z - x)⁻¹ * f z - x * (z - x)⁻¹ * f z
Tactic: ring_nf at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
key :
  f (z * y * (z - x)⁻¹ - y * x * (z - x)⁻¹) ≤
    z * (z - x)⁻¹ * f x - y * (z - x)⁻¹ * f x + y * (z - x)⁻¹ * f z - x * (z - x)⁻¹ * f z
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have field_simp : ∀ (key : (z - x) * f y ≤ f x * (z - y) + y * f z - x * f z), (z - y) * (f y - f x) ≤ (y - x) * (f z - f y)
Tactic: field_simp at key ⊢
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
key : (z - x) * f y ≤ f x * (z - y) + y * f z - x * f z
⊢ (z - y) * (f y - f x) ≤ (y - x) * (f z - f y)
have linarith : (y - x) * (f z - f y) < (z - y) * (f y - f x) →
  (z - x) * f y - (f x * (z - y) + y * f z - x * f z) + ((y - x) * (f z - f y) - (z - y) * (f y - f x)) = 0
Tactic: linarith