Theorem: Partition.top_eq_indiscrete (Matroid/ForMathlib/SetPartition.lean)

State before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
hs : s ≠ ⊥
⊢ ⊤ = indiscrete s hs
Tactic:
ext a
State after:
case hP
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
hs : s ≠ ⊥
a : α✝
⊢ a ∈ ⊤ ↔ a ∈ indiscrete s hs

State before:
case hP
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
hs : s ≠ ⊥
a : α✝
⊢ a ∈ ⊤ ↔ a ∈ indiscrete s hs
Tactic:
rw [mem_top_iff, mem_indiscrete_iff, and_iff_left_iff_imp]
State after:
case hP
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
hs : s ≠ ⊥
a : α✝
⊢ a = s → a ≠ ⊥

State before:
case hP
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
hs : s ≠ ⊥
a : α✝
⊢ a = s → a ≠ ⊥
Tactic:
rintro rfl
State after:
case hP
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a : α✝
hs : a ≠ ⊥
⊢ a ≠ ⊥

State before:
case hP
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a : α✝
hs : a ≠ ⊥
⊢ a ≠ ⊥
Tactic:
assumption
State after:
no goals