Theorem: Geometry.SimplicialComplex.mem_ofSimplex (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 : ℕ
hs : AffineIndependent 𝕜 Subtype.val
⊢ t ∈ ofSimplex hs ↔ t.Nonempty ∧ t ⊆ s
Tactic:
refine' ⟨_, fun h => ⟨h.1, s, rfl, h.2⟩⟩
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 : ℕ
hs : AffineIndependent 𝕜 Subtype.val
⊢ t ∈ ofSimplex hs → t.Nonempty ∧ t ⊆ s

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 : ℕ
hs : AffineIndependent 𝕜 Subtype.val
⊢ t ∈ ofSimplex hs → t.Nonempty ∧ t ⊆ s
Tactic:
rintro ⟨ht, u, rfl : u = s, hts⟩
State after:
case 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
t : Finset E
A : Set (Finset E)
m n : ℕ
ht : t.Nonempty
u : Finset E
hts : t ⊆ u
hs : AffineIndependent 𝕜 Subtype.val
⊢ t.Nonempty ∧ t ⊆ u

State before:
case 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
t : Finset E
A : Set (Finset E)
m n : ℕ
ht : t.Nonempty
u : Finset E
hts : t ⊆ u
hs : AffineIndependent 𝕜 Subtype.val
⊢ t.Nonempty ∧ t ⊆ u
Tactic:
exact ⟨ht, hts⟩
State after:
no goals