Theorem: MulAction.finOneToMap_bijective (Jordan/MultipleTransitivity.lean)

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ Function.Bijective ⇑(finOneToMap M α)
Tactic:
constructor
State after:
case left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ Function.Injective ⇑(finOneToMap M α)

case right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ Function.Surjective ⇑(finOneToMap M α)

State before:
case left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ Function.Injective ⇑(finOneToMap M α)
Tactic:
intro x y hxy
State after:
case left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 1 ↪ α
hxy : (finOneToMap M α) x = (finOneToMap M α) y
⊢ x = y

State before:
case left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 1 ↪ α
hxy : (finOneToMap M α) x = (finOneToMap M α) y
⊢ x = y
Tactic:
ext i
State after:
case left.h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 1 ↪ α
hxy : (finOneToMap M α) x = (finOneToMap M α) y
i : Fin 1
⊢ x i = y i

State before:
case left.h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 1 ↪ α
hxy : (finOneToMap M α) x = (finOneToMap M α) y
i : Fin 1
⊢ x i = y i
Tactic:
rw [Fin.eq_zero i]
State after:
case left.h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 1 ↪ α
hxy : (finOneToMap M α) x = (finOneToMap M α) y
i : Fin 1
⊢ x 0 = y 0

State before:
case left.h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 1 ↪ α
hxy : (finOneToMap M α) x = (finOneToMap M α) y
i : Fin 1
⊢ x 0 = y 0
Tactic:
exact hxy
State after:
no goals

State before:
case right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ Function.Surjective ⇑(finOneToMap M α)
Tactic:
intro a
State after:
case right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ ∃ a_1, (finOneToMap M α) a_1 = a

State before:
case right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ ∃ a_1, (finOneToMap M α) a_1 = a
Tactic:
use {
  toFun := fun _ => a
  inj' := fun i j _ => by
    rw [Fin.eq_zero i, Fin.eq_zero j] }
State after:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ (finOneToMap M α) { toFun := fun x => a, inj' := ⋯ } = a

State before:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ (finOneToMap M α) { toFun := fun x => a, inj' := ⋯ } = a
Tactic:
rfl
State after:
no goals

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
i j : Fin 1
x✝ : (fun x => a) i = (fun x => a) j
⊢ i = j
Tactic:
rw [Fin.eq_zero i, Fin.eq_zero j]
State after:
no goals