Theorem: Geometry.SimplicialComplex.subfacet (LeanCamCombi/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
⊢ ∃ t ∈ K.facets, s ⊆ t
Tactic:
have := id hs
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs this : s ∈ K
⊢ ∃ t ∈ K.facets, s ⊆ t

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs this : s ∈ K
⊢ ∃ t ∈ K.facets, s ⊆ t
Tactic:
revert this
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
⊢ s ∈ K → ∃ t ∈ K.facets, s ⊆ t

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
⊢ s ∈ K → ∃ t ∈ K.facets, s ⊆ t
Tactic:
refine strongDownwardInductionOn s ?_ (face_dimension_le_space_dimension hs)
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
⊢ ∀ (t₁ : Finset E),
    (∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t₁ ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t) →
      t₁.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t₁ ∈ K → ∃ t ∈ K.facets, t₁ ⊆ t

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
⊢ ∀ (t₁ : Finset E),
    (∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t₁ ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t) →
      t₁.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t₁ ∈ K → ∃ t ∈ K.facets, t₁ ⊆ t
Tactic:
rintro t h - ht
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1
Tactic:
by_cases htfacet : t ∈ K.facets
State after:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∈ K.facets
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1

case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∉ K.facets
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1

State before:
case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∉ K.facets
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1
Tactic:
obtain ⟨u, hu, htu⟩ := (not_facet_iff_subface ht).mp htfacet
State after:
case neg.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∉ K.facets
u : Finset E
hu : u ∈ K.faces
htu : t ⊂ u
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1

State before:
case neg.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∉ K.facets
u : Finset E
hu : u ∈ K.faces
htu : t ⊂ u
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1
Tactic:
obtain ⟨v, hv⟩ := h (face_dimension_le_space_dimension hu) htu hu
State after:
case neg.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∉ K.facets
u : Finset E
hu : u ∈ K.faces
htu : t ⊂ u
v : Finset E
hv : v ∈ K.facets ∧ u ⊆ v
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1

State before:
case neg.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∉ K.facets
u : Finset E
hu : u ∈ K.faces
htu : t ⊂ u
v : Finset E
hv : v ∈ K.facets ∧ u ⊆ v
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1
Tactic:
exact ⟨v, hv.1, htu.1.trans hv.2⟩
State after:
no goals

State before:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∈ K.facets
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1
Tactic:
exact ⟨t, htfacet, Subset.rfl⟩
State after:
no goals