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

State before:
M : Type ?u.67011
α : Type ?u.67014
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x✝ : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x y : ↥(SubMulAction.ofStabilizer M a)
hxy : (fun u => id ↑u) x = (fun u => id ↑u) y
⊢ x = y
Tactic:
simpa using hxy
State after:
no goals

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
⊢ let j := { toFun := fun u => id ↑u, inj' := ⋯ };
  ∃ x',
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x j ∧
      x' { val := n, isLt := ⋯ } = a
Tactic:
intro _
State after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
⊢ ∃ x',
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x j✝ ∧
      x' { val := n, isLt := ⋯ } = a

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
⊢ ∃ x',
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x j✝ ∧
      x' { val := n, isLt := ⋯ } = a
Tactic:
refine' may_extend_with (x.trans (subtype _)) a _
State after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
⊢ a ∉ Set.range (Function.Embedding.trans x (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)).toFun

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
⊢ a ∉ Set.range (Function.Embedding.trans x (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)).toFun
Tactic:
rintro ⟨u, hu⟩
State after:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : (Function.Embedding.trans x (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)).toFun u = a
⊢ False

State before:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : (Function.Embedding.trans x (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)).toFun u = a
⊢ False
Tactic:
simp only [toFun_eq_coe, trans_apply, Function.Embedding.coe_subtype] at hu
State after:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : ↑(x u) = a
⊢ False

State before:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : ↑(x u) = a
⊢ False
Tactic:
apply SubMulAction.neq_of_mem_ofStabilizer M a
State after:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : ↑(x u) = a
⊢ ↑?m.69556 = a

M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : ↑(x u) = a
⊢ ↥(SubMulAction.ofStabilizer M a)

State before:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : ↑(x u) = a
⊢ ↑?m.69556 = a

M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : ↑(x u) = a
⊢ ↥(SubMulAction.ofStabilizer M a)
Tactic:
exact hu
State after:
no goals