Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_injective (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.Injective ⇑f
ι : Type u_5
⊢ Function.Injective ⇑(embeddingOfEquivariantMap hf ι)
Tactic:
intro x y hxy
State after:
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.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
⊢ x = y

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.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
⊢ x = y
Tactic:
ext i
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.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
i : ι
⊢ x i = y i

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.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
i : ι
⊢ x i = y i
Tactic:
apply hf
State after:
case h.a
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.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
i : ι
⊢ f (x i) = f (y i)

State before:
case h.a
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.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
i : ι
⊢ f (x i) = f (y i)
Tactic:
simp only [← EquivariantMap.embeddingOfEquivariantMap_apply hf]
State after:
case h.a
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.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
i : ι
⊢ ((embeddingOfEquivariantMap hf ι) x) i = ((embeddingOfEquivariantMap hf ι) y) i

State before:
case h.a
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.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
i : ι
⊢ ((embeddingOfEquivariantMap hf ι) x) i = ((embeddingOfEquivariantMap hf ι) y) i
Tactic:
rw [hxy]
State after:
no goals