Theorem: isPreprimitive_iff_isSimpleOrder_blocks (Jordan/Primitive.lean)

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsPreprimitive G X ↔ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
Tactic:
haveI : Nontrivial { B : Set X // a ∈ B ∧ IsBlock G B } :=
  Block.mem_is_nontrivial_order_of_nontrivial G a
State after:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
⊢ IsPreprimitive G X ↔ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
⊢ IsPreprimitive G X ↔ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
Tactic:
constructor
State after:
case mp
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
⊢ IsPreprimitive G X → IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }

case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
⊢ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B } → IsPreprimitive G X

State before:
case mp
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
⊢ IsPreprimitive G X → IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
Tactic:
intro hGX'
State after:
case mp
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
⊢ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }

State before:
case mp
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
⊢ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
Tactic:
apply IsSimpleOrder.mk
State after:
case mp.eq_bot_or_eq_top
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
⊢ ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤

State before:
case mp.eq_bot_or_eq_top
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
⊢ ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤
Tactic:
rintro ⟨B, haB, hB⟩
State after:
case mp.eq_bot_or_eq_top.mk.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ { val := B, property := ⋯ } = ⊥ ∨ { val := B, property := ⋯ } = ⊤

State before:
case mp.eq_bot_or_eq_top.mk.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ { val := B, property := ⋯ } = ⊥ ∨ { val := B, property := ⋯ } = ⊤
Tactic:
simp only [← Subtype.coe_inj, Subtype.coe_mk]
State after:
case mp.eq_bot_or_eq_top.mk.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ B = ↑⊥ ∨ B = ↑⊤

State before:
case mp.eq_bot_or_eq_top.mk.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ B = ↑⊥ ∨ B = ↑⊤
Tactic:
cases hGX'.has_trivial_blocks hB with
| inl h =>
  apply Or.intro_left
  change B = ↑(Block.boundedOrderOfMem G a).bot
  rw [Block.boundedOrderOfMem.bot_eq]
  exact Set.Subsingleton.eq_singleton_of_mem h haB
| inr h =>
  apply Or.intro_right
  change B = ↑(Block.boundedOrderOfMem G a).top
  exact h
State after:
no goals

State before:
case mp.eq_bot_or_eq_top.mk.intro.inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : Set.Subsingleton B
⊢ B = ↑⊥ ∨ B = ↑⊤
Tactic:
apply Or.intro_left
State after:
case mp.eq_bot_or_eq_top.mk.intro.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : Set.Subsingleton B
⊢ B = ↑⊥

State before:
case mp.eq_bot_or_eq_top.mk.intro.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : Set.Subsingleton B
⊢ B = ↑⊥
Tactic:
rw [Block.boundedOrderOfMem.bot_eq]
State after:
case mp.eq_bot_or_eq_top.mk.intro.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : Set.Subsingleton B
⊢ B = {a}

State before:
case mp.eq_bot_or_eq_top.mk.intro.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : Set.Subsingleton B
⊢ B = {a}
Tactic:
exact Set.Subsingleton.eq_singleton_of_mem h haB
State after:
no goals

State before:
case mp.eq_bot_or_eq_top.mk.intro.inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : B = ⊤
⊢ B = ↑⊥ ∨ B = ↑⊤
Tactic:
apply Or.intro_right
State after:
case mp.eq_bot_or_eq_top.mk.intro.inr.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : B = ⊤
⊢ B = ↑⊤

State before:
case mp.eq_bot_or_eq_top.mk.intro.inr.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : B = ⊤
⊢ B = ↑⊤
Tactic:
exact h
State after:
no goals

State before:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
⊢ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B } → IsPreprimitive G X
Tactic:
intro h
State after:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
⊢ IsPreprimitive G X

State before:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
⊢ IsPreprimitive G X
Tactic:
let h_bot_or_top := h.eq_bot_or_eq_top
State after:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
⊢ IsPreprimitive G X

State before:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
⊢ IsPreprimitive G X
Tactic:
apply IsPreprimitive.mk_mem a
State after:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
⊢ ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B

State before:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
⊢ ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
Tactic:
intro B haB hB
State after:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ IsTrivialBlock B

State before:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ IsTrivialBlock B
Tactic:
cases' h_bot_or_top ⟨B, haB, hB⟩ with hB' hB' <;>
  simp only [← Subtype.coe_inj, Subtype.coe_mk] at hB'
State after:
case mpr.inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊥
⊢ IsTrivialBlock B

case mpr.inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊤
⊢ IsTrivialBlock B

State before:
case mpr.inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊥
⊢ IsTrivialBlock B
Tactic:
left
State after:
case mpr.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊥
⊢ Set.Subsingleton B

State before:
case mpr.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊥
⊢ Set.Subsingleton B
Tactic:
rw [hB']
State after:
case mpr.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊥
⊢ Set.Subsingleton ↑⊥

State before:
case mpr.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊥
⊢ Set.Subsingleton ↑⊥
Tactic:
exact Set.subsingleton_singleton
State after:
no goals

State before:
case mpr.inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊤
⊢ IsTrivialBlock B
Tactic:
right
State after:
case mpr.inr.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊤
⊢ B = ⊤

State before:
case mpr.inr.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊤
⊢ B = ⊤
Tactic:
rw [hB']
State after:
case mpr.inr.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊤
⊢ ↑⊤ = ⊤

State before:
case mpr.inr.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊤
⊢ ↑⊤ = ⊤
Tactic:
rfl
State after:
no goals