Theorem: MulAction.orbit.isPretransitive_iff (Jordan/Mathlib/Pretransitive.lean)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ orbit G a = ⊤ ↔ IsPretransitive G X
Tactic:
rw [IsPretransitive.mk_base_iff a]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ orbit G a = ⊤ ↔ ∀ (x : X), ∃ g, g • a = x

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ orbit G a = ⊤ ↔ ∀ (x : X), ∃ g, g • a = x
Tactic:
rw [Set.ext_iff]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (∀ (x : X), x ∈ orbit G a ↔ x ∈ ⊤) ↔ ∀ (x : X), ∃ g, g • a = x

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (∀ (x : X), x ∈ orbit G a ↔ x ∈ ⊤) ↔ ∀ (x : X), ∃ g, g • a = x
Tactic:
apply forall_congr'
State after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∀ (a_1 : X), (a_1 ∈ orbit G a ↔ a_1 ∈ ⊤) ↔ ∃ g, g • a = a_1

State before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∀ (a_1 : X), (a_1 ∈ orbit G a ↔ a_1 ∈ ⊤) ↔ ∃ g, g • a = a_1
Tactic:
intro x
State after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a x : X
⊢ (x ∈ orbit G a ↔ x ∈ ⊤) ↔ ∃ g, g • a = x

State before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a x : X
⊢ (x ∈ orbit G a ↔ x ∈ ⊤) ↔ ∃ g, g • a = x
Tactic:
simp_rw [Set.top_eq_univ, Set.mem_univ, iff_true_iff]
State after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a x : X
⊢ x ∈ orbit G a ↔ ∃ g, g • a = x

State before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a x : X
⊢ x ∈ orbit G a ↔ ∃ g, g • a = x
Tactic:
rw [mem_orbit_iff]
State after:
no goals