Theorem: isTrivialBlock_of_injective_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.Injective ⇑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.Injective ⇑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.Injective ⇑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.Injective ⇑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.Injective ⇑f
B : Set β
hB : 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.Injective ⇑f
B : Set β
hB : Set.Subsingleton B
⊢ Set.Subsingleton (⇑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.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ IsTrivialBlock (⇑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.Injective ⇑f
B : Set β
hB : Set.Subsingleton B
⊢ Set.Subsingleton (⇑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.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ IsTrivialBlock (⇑f ⁻¹' B)
Tactic:
exact Set.Subsingleton.preimage hB hf
State after:
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.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ IsTrivialBlock (⇑f ⁻¹' B)

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.Injective ⇑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.Injective ⇑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.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ ⇑f ⁻¹' B = ⊤
Tactic:
simp only [hB, Set.top_eq_univ]
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.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ ⇑f ⁻¹' Set.univ = Set.univ

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.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ ⇑f ⁻¹' Set.univ = Set.univ
Tactic:
apply Set.preimage_univ
State after:
no goals