Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_bijective (Jordan/MultipleTransitivity.lean)

State before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
⊢ Function.Bijective ⇑(embeddingOfEquivariantMap ⋯ ι)
Tactic:
constructor
State after:
case left
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
⊢ Function.Injective ⇑(embeddingOfEquivariantMap ⋯ ι)

case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
⊢ Function.Surjective ⇑(embeddingOfEquivariantMap ⋯ ι)

State before:
case left
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
⊢ Function.Injective ⇑(embeddingOfEquivariantMap ⋯ ι)

case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
⊢ Function.Surjective ⇑(embeddingOfEquivariantMap ⋯ ι)
Tactic:
exact EquivariantMap.embeddingOfEquivariantMap_is_injective hf.injective
State after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
⊢ Function.Surjective ⇑(embeddingOfEquivariantMap ⋯ ι)

State before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
⊢ Function.Surjective ⇑(embeddingOfEquivariantMap ⋯ ι)
Tactic:
intro y
State after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
⊢ ∃ a, (embeddingOfEquivariantMap ⋯ ι) a = y

State before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
⊢ ∃ a, (embeddingOfEquivariantMap ⋯ ι) a = y
Tactic:
obtain ⟨g, _, hfg⟩ := Function.bijective_iff_has_inverse.mp hf
State after:
case right.intro.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
⊢ ∃ a, (embeddingOfEquivariantMap ⋯ ι) a = y

State before:
case right.intro.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
⊢ ∃ a, (embeddingOfEquivariantMap ⋯ ι) a = y
Tactic:
use ⟨g ∘ y, Function.Injective.comp hfg.injective (EmbeddingLike.injective y)⟩
State after:
case h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
⊢ (embeddingOfEquivariantMap ⋯ ι) { toFun := g ∘ ⇑y, inj' := ⋯ } = y

State before:
case h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
⊢ (embeddingOfEquivariantMap ⋯ ι) { toFun := g ∘ ⇑y, inj' := ⋯ } = y
Tactic:
ext i
State after:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
i : ι
⊢ ((embeddingOfEquivariantMap ⋯ ι) { toFun := g ∘ ⇑y, inj' := ⋯ }) i = y i

State before:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
i : ι
⊢ ((embeddingOfEquivariantMap ⋯ ι) { toFun := g ∘ ⇑y, inj' := ⋯ }) i = y i
Tactic:
rw [EquivariantMap.embeddingOfEquivariantMap_apply]
State after:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
i : ι
⊢ f ({ toFun := g ∘ ⇑y, inj' := ⋯ } i) = y i

State before:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
i : ι
⊢ f ({ toFun := g ∘ ⇑y, inj' := ⋯ } i) = y i
Tactic:
simp only [coeFn_mk, Function.comp_apply]
State after:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
i : ι
⊢ f (g (y i)) = y i

State before:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
i : ι
⊢ f (g (y i)) = y i
Tactic:
rw [hfg]
State after:
no goals