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

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsMultiplyPretransitive M α 0
Tactic:
apply IsPretransitive.mk
State after:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ ∀ (x y : Fin 0 ↪ α), ∃ g, g • x = y

State before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ ∀ (x y : Fin 0 ↪ α), ∃ g, g • x = y
Tactic:
intro x y
State after:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
⊢ ∃ g, g • x = y
Tactic:
use 1
State after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
⊢ 1 • x = y

State before:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
⊢ 1 • x = y
Tactic:
rw [one_smul]
State after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
⊢ x = y

State before:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
⊢ x = y
Tactic:
ext i
State after:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
i : Fin 0
⊢ x i = y i

State before:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
i : Fin 0
⊢ x i = y i
Tactic:
exfalso
State after:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
i : Fin 0
⊢ False

State before:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
i : Fin 0
⊢ False
Tactic:
exact IsEmpty.false i
State after:
no goals