internlm/Lean-Github huggingface dataset:
Theorem: Finset.mul_kneser'
Proof state before:
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ s t : Finset α
hs : s.Nonempty
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty
Proof state after:
case inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t s : Finset α
hs : s.Nonempty
⊢ (s * (s * ∅).mulStab).card + (∅ * (s * ∅).mulStab).card ≤ (s * ∅).card + (s * ∅).mulStab.card

case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Theorem: Finset.mul_kneser'
Proof state before:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
refine'
  (le_card_mul_add_card_mulStab_mul (hs.mul (hs.mul ht).mulStab) $
        ht.mul (hs.mul ht).mulStab).trans_eq
    _
Proof state after:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ (s * (s * t).mulStab * (t * (s * t).mulStab)).card + (s * (s * t).mulStab * (t * (s * t).mulStab)).mulStab.card =
    (s * t).card + (s * t).mulStab.card
Theorem: Finset.mul_kneser'
Proof state before:
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ (s * (s * t).mulStab * (t * (s * t).mulStab)).card + (s * (s * t).mulStab * (t * (s * t).mulStab)).mulStab.card =
    (s * t).card + (s * t).mulStab.card
Tactic:
rw [mul_mulStab_mul_mul_mul_mulStab_mul]
Proof state after:
no goals
Theorem: Finset.mul_kneser'
Proof state before:
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t✝ t : Finset α
⊢ (∅ * (∅ * t).mulStab).card + (t * (∅ * t).mulStab).card ≤ (∅ * t).card + (∅ * t).mulStab.card
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.mul_kneser'
Proof state before:
case inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t s : Finset α
hs : s.Nonempty
⊢ (s * (s * ∅).mulStab).card + (∅ * (s * ∅).mulStab).card ≤ (s * ∅).card + (s * ∅).mulStab.card
Tactic:
simp
Proof state after:
no goals
Theorem: IsExposed.span_lt
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hst : IsExposed ℝ s t
hts : ¬s ⊆ t
⊢ affineSpan ℝ t < affineSpan ℝ s
Tactic:
apply (affineSpan_mono _ hst.subset).lt_of_ne
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hst : IsExposed ℝ s t
hts : ¬s ⊆ t
⊢ affineSpan ℝ t ≠ affineSpan ℝ s
Theorem: IsExposed.span_lt
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hst : IsExposed ℝ s t
hts : ¬s ⊆ t
⊢ affineSpan ℝ t ≠ affineSpan ℝ s
Tactic:
rintro h
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hst : IsExposed ℝ s t
hts : ¬s ⊆ t
h : affineSpan ℝ t = affineSpan ℝ s
⊢ False
Theorem: IsExposed.span_lt
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hst : IsExposed ℝ s t
hts : ¬s ⊆ t
h : affineSpan ℝ t = affineSpan ℝ s
⊢ False
Tactic:
sorry
Proof state after:
no goals
Theorem: mem_exposed_set_iff_mem_frontier
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
⊢ (∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t) ↔ x ∈ s ∧ x ∈ frontier s
Tactic:
use fun ⟨t, hst, hts, hxt⟩ => ⟨hst.subset hxt, hst.subset_frontier hts hxt⟩
Proof state after:
case mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
⊢ x ∈ s ∧ x ∈ frontier s → ∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Theorem: mem_exposed_set_iff_mem_frontier
Proof state before:
case mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
⊢ x ∈ s ∧ x ∈ frontier s → ∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Tactic:
rintro ⟨hxA, hxfA⟩
Proof state after:
case mpr.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
⊢ ∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Theorem: mem_exposed_set_iff_mem_frontier
Proof state before:
case mpr.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
⊢ ∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Tactic:
obtain ⟨y, hyA⟩ := id hs₂
Proof state after:
case mpr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
⊢ ∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Theorem: mem_exposed_set_iff_mem_frontier
Proof state before:
case mpr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
⊢ ∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Tactic:
obtain ⟨l, hl⟩ := geometric_hahn_banach_open_point (Convex.interior hs₁) isOpen_interior hxfA.2
Proof state after:
case mpr.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l✝ : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
⊢ ∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Theorem: mem_exposed_set_iff_mem_frontier
Proof state before:
case mpr.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l✝ : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
⊢ ∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Tactic:
refine'
  ⟨{x ∈ s | ∀ y ∈ s, l y ≤ l x}, fun _ => ⟨l, rfl⟩, fun h =>
    not_le.2 (hl y hyA) ((h (interior_subset hyA)).2 x hxA), hxA, fun z hzA => _⟩
Proof state after:
case mpr.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l✝ : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
⊢ l z ≤ l x
Theorem: mem_exposed_set_iff_mem_frontier
Proof state before:
case mpr.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l✝ : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
⊢ l z ≤ l x
Tactic:
suffices h : l '' closure (interior s) ⊆ closure (Iio (l x)) by
  rw [closure_Iio, ← closure_eq_closure_interior hs₁ hs₂] at h
  exact h ⟨z, subset_closure hzA, rfl⟩
Proof state after:
case mpr.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l✝ : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
⊢ ⇑l '' closure (interior s) ⊆ closure (Iio (l x))
Theorem: mem_exposed_set_iff_mem_frontier
Proof state before:
case mpr.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l✝ : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
⊢ ⇑l '' closure (interior s) ⊆ closure (Iio (l x))
Tactic:
refine' (image_closure_subset_closure_image l.continuous).trans $ closure_mono _
Proof state after:
case mpr.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l✝ : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
⊢ ⇑l '' interior s ⊆ Iio (l x)
Theorem: mem_exposed_set_iff_mem_frontier
Proof state before:
case mpr.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l✝ : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
⊢ ⇑l '' interior s ⊆ Iio (l x)
Tactic:
rintro _ ⟨w, hw, rfl⟩
Proof state after:
case mpr.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l✝ : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
w : E
hw : w ∈ interior s
⊢ l w ∈ Iio (l x)
Theorem: mem_exposed_set_iff_mem_frontier
Proof state before:
case mpr.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l✝ : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
w : E
hw : w ∈ interior s
⊢ l w ∈ Iio (l x)
Tactic:
exact hl w hw
Proof state after:
no goals
Theorem: mem_exposed_set_iff_mem_frontier
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l✝ : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
h : ⇑l '' closure (interior s) ⊆ closure (Iio (l x))
⊢ l z ≤ l x
Tactic:
rw [closure_Iio, ← closure_eq_closure_interior hs₁ hs₂] at h
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l✝ : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
h : ⇑l '' closure s ⊆ Iic (l x)
⊢ l z ≤ l x
Theorem: mem_exposed_set_iff_mem_frontier
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l✝ : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
h : ⇑l '' closure s ⊆ Iic (l x)
⊢ l z ≤ l x
Tactic:
exact h ⟨z, subset_closure hzA, rfl⟩
Proof state after:
no goals
Theorem: mem_extreme_set_iff_mem_frontier
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
⊢ (∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t) ↔ x ∈ s ∧ x ∈ frontier s
Tactic:
use fun ⟨t, hst, hts, hxt⟩ => ⟨hst.1 hxt, hst.subset_frontier hts hxt⟩
Proof state after:
case mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
⊢ x ∈ s ∧ x ∈ frontier s → ∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Theorem: mem_extreme_set_iff_mem_frontier
Proof state before:
case mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
⊢ x ∈ s ∧ x ∈ frontier s → ∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Tactic:
rintro h
Proof state after:
case mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
h : x ∈ s ∧ x ∈ frontier s
⊢ ∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Theorem: mem_extreme_set_iff_mem_frontier
Proof state before:
case mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
h : x ∈ s ∧ x ∈ frontier s
⊢ ∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Tactic:
obtain ⟨t, hst, hts, hxt⟩ := (mem_exposed_set_iff_mem_frontier hs₁ hs₂).2 h
Proof state after:
case mpr.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t✝ C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
h : x ∈ s ∧ x ∈ frontier s
t : Set E
hst : IsExposed ℝ s t
hts : ¬s ⊆ t
hxt : x ∈ t
⊢ ∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Theorem: mem_extreme_set_iff_mem_frontier
Proof state before:
case mpr.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t✝ C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
h : x ∈ s ∧ x ∈ frontier s
t : Set E
hst : IsExposed ℝ s t
hts : ¬s ⊆ t
hxt : x ∈ t
⊢ ∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Tactic:
exact ⟨t, hst.isExtreme, hts, hxt⟩
Proof state after:
no goals
Theorem: extremePoints_subset_closure_exposedPoints
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ extremePoints ℝ s ⊆ closure (exposedPoints ℝ s)
Tactic:
sorry
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.Pure.exists_facet
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s : Finset E
hK : K.Pure n
hs : s ∈ K
⊢ ∃ t ∈ K.facets, s ⊆ t
Tactic:
sorry
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.Pure.exists_face_of_card_le
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s : Finset E
hK : K.Pure n
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k
Tactic:
by_cases H : s ∈ K.facets
Proof state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s : Finset E
hK : K.Pure n
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∈ K.facets
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s : Finset E
hK : K.Pure n
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∉ K.facets
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k
Theorem: Geometry.SimplicialComplex.Pure.exists_face_of_card_le
Proof state before:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s : Finset E
hK : K.Pure n
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∈ K.facets
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k
Tactic:
exact ⟨s, hs, Subset.rfl, hcard.antisymm <| h.trans (hK.2 H).ge⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.Pure.exists_face_of_card_le
Proof state before:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s : Finset E
hK : K.Pure n
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∉ K.facets
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k
Tactic:
unfold facets at H
Proof state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s : Finset E
hK : K.Pure n
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∉ {s | s ∈ K.faces ∧ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t}
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k
Theorem: Geometry.SimplicialComplex.Pure.exists_face_of_card_le
Proof state before:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s : Finset E
hK : K.Pure n
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∉ {s | s ∈ K.faces ∧ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t}
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k
Tactic:
simp at H
Proof state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s : Finset E
hK : K.Pure n
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∈ K → ∃ x ∈ K, s ⊆ x ∧ ¬s = x
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k
Theorem: Geometry.SimplicialComplex.Pure.exists_face_of_card_le
Proof state before:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s : Finset E
hK : K.Pure n
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∈ K → ∃ x ∈ K, s ⊆ x ∧ ¬s = x
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k
Tactic:
sorry
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.pure_unique
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s : Finset E
hK : K.faces.Nonempty
ha : K.Pure a
hb : K.Pure b
⊢ a = b
Tactic:
obtain ⟨s, hs⟩ := hK
Proof state after:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
ha : K.Pure a
hb : K.Pure b
s : Finset E
hs : s ∈ K.faces
⊢ a = b
Theorem: Geometry.SimplicialComplex.pure_unique
Proof state before:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
ha : K.Pure a
hb : K.Pure b
s : Finset E
hs : s ∈ K.faces
⊢ a = b
Tactic:
obtain ⟨t, ht, -⟩ := ha.exists_facet hs
Proof state after:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
ha : K.Pure a
hb : K.Pure b
s : Finset E
hs : s ∈ K.faces
t : Finset E
ht : t ∈ K.facets
⊢ a = b
Theorem: Geometry.SimplicialComplex.pure_unique
Proof state before:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
ha : K.Pure a
hb : K.Pure b
s : Finset E
hs : s ∈ K.faces
t : Finset E
ht : t ∈ K.facets
⊢ a = b
Tactic:
exact add_right_cancel ((ha.2 ht).symm.trans <| hb.2 ht)
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.pure_iff
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s : Finset E
⊢ K.Pure n ↔ ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
Tactic:
refine' ⟨fun hK s hs => _, fun hK => ⟨fun s hs => _, fun s hs => _⟩⟩
Proof state after:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
hK : K.Pure n
s : Finset E
hs : s ∈ K
⊢ ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t

case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
hK : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K
⊢ s.card ≤ n + 1

case refine'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
hK : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K.facets
⊢ s.card = n + 1
Theorem: Geometry.SimplicialComplex.pure_iff
Proof state before:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
hK : K.Pure n
s : Finset E
hs : s ∈ K
⊢ ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
Tactic:
obtain ⟨t, ht, hst⟩ := hK.exists_facet hs
Proof state after:
case refine'_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
hK : K.Pure n
s : Finset E
hs : s ∈ K
t : Finset E
ht : t ∈ K.facets
hst : s ⊆ t
⊢ ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
Theorem: Geometry.SimplicialComplex.pure_iff
Proof state before:
case refine'_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
hK : K.Pure n
s : Finset E
hs : s ∈ K
t : Finset E
ht : t ∈ K.facets
hst : s ⊆ t
⊢ ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
Tactic:
exact ⟨t, ht.1, hK.2 ht, hst⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.pure_iff
Proof state before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
hK : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K
⊢ s.card ≤ n + 1
Tactic:
obtain ⟨t, _, htcard, hst⟩ := hK hs
Proof state after:
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
hK : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K
t : Finset E
left✝ : t ∈ K
htcard : t.card = n + 1
hst : s ⊆ t
⊢ s.card ≤ n + 1
Theorem: Geometry.SimplicialComplex.pure_iff
Proof state before:
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
hK : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K
t : Finset E
left✝ : t ∈ K
htcard : t.card = n + 1
hst : s ⊆ t
⊢ s.card ≤ n + 1
Tactic:
exact (Finset.card_le_card hst).trans_eq htcard
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.pure_iff
Proof state before:
case refine'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
hK : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K.facets
⊢ s.card = n + 1
Tactic:
obtain ⟨t, ht, htcard, hst⟩ := hK hs.1
Proof state after:
case refine'_3.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
hK : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K.facets
t : Finset E
ht : t ∈ K
htcard : t.card = n + 1
hst : s ⊆ t
⊢ s.card = n + 1
Theorem: Geometry.SimplicialComplex.pure_iff
Proof state before:
case refine'_3.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
hK : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K.facets
t : Finset E
ht : t ∈ K
htcard : t.card = n + 1
hst : s ⊆ t
⊢ s.card = n + 1
Tactic:
rwa [hs.2 ht hst]
Proof state after:
no goals