Theorem: IsPreprimitive.on_subsingleton (Jordan/Primitive.lean)

State before:
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
⊢ IsPreprimitive G X
Tactic:
have : IsPretransitive G X := by
  apply IsPretransitive.mk
  intro x y
  use Classical.arbitrary G
  rw [eq_iff_true_of_subsingleton]
  trivial
State after:
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
⊢ IsPreprimitive G X

State before:
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
⊢ IsPreprimitive G X
Tactic:
apply IsPreprimitive.mk
State after:
case has_trivial_blocks'
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
⊢ ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B

State before:
case has_trivial_blocks'
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
⊢ ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
Tactic:
intro B _
State after:
case has_trivial_blocks'
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
B : Set X
a✝ : IsBlock G B
⊢ IsTrivialBlock B

State before:
case has_trivial_blocks'
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
B : Set X
a✝ : IsBlock G B
⊢ IsTrivialBlock B
Tactic:
left
State after:
case has_trivial_blocks'.h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
B : Set X
a✝ : IsBlock G B
⊢ Set.Subsingleton B

State before:
case has_trivial_blocks'.h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
B : Set X
a✝ : IsBlock G B
⊢ Set.Subsingleton B
Tactic:
exact Set.subsingleton_of_subsingleton
State after:
no goals

State before:
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
⊢ IsPretransitive G X
Tactic:
apply IsPretransitive.mk
State after:
case exists_smul_eq
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
⊢ ∀ (x y : X), ∃ g, g • x = y

State before:
case exists_smul_eq
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
⊢ ∀ (x y : X), ∃ g, g • x = y
Tactic:
intro x y
State after:
case exists_smul_eq
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ ∃ g, g • x = y
Tactic:
use Classical.arbitrary G
State after:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ Classical.arbitrary G • x = y

State before:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ Classical.arbitrary G • x = y
Tactic:
rw [eq_iff_true_of_subsingleton]
State after:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ True

State before:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ True
Tactic:
trivial
State after:
no goals