Theorem: isTrivialBlock_of_surjective_map (Jordan/Primitive.lean)

State before:
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : IsTrivialBlock B
⊢ IsTrivialBlock (⇑f '' B)
Tactic:
cases' hB with hB hB
State after:
case inl
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : Set.Subsingleton B
⊢ IsTrivialBlock (⇑f '' B)

case inr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ IsTrivialBlock (⇑f '' B)

State before:
case inl
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : Set.Subsingleton B
⊢ IsTrivialBlock (⇑f '' B)
Tactic:
apply Or.intro_left
State after:
case inl.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : Set.Subsingleton B
⊢ Set.Subsingleton (⇑f '' B)

State before:
case inl.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : Set.Subsingleton B
⊢ Set.Subsingleton (⇑f '' B)
Tactic:
apply Set.Subsingleton.image hB
State after:
no goals

State before:
case inr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ IsTrivialBlock (⇑f '' B)
Tactic:
apply Or.intro_right
State after:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ ⇑f '' B = ⊤

State before:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ ⇑f '' B = ⊤
Tactic:
rw [hB]
State after:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ ⇑f '' ⊤ = ⊤

State before:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ ⇑f '' ⊤ = ⊤
Tactic:
simp only [Set.top_eq_univ, Set.image_univ, Set.range_iff_surjective]
State after:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ Function.Surjective ⇑f

State before:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ Function.Surjective ⇑f
Tactic:
exact hf
State after:
no goals