Theorem: MulAction.IsPretransitive.mk_base_iff (Jordan/Mathlib/Pretransitive.lean)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ IsPretransitive G X ↔ ∀ (x : X), ∃ g, g • a = x
Tactic:
constructor
State after:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ IsPretransitive G X → ∀ (x : X), ∃ g, g • a = x

case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (∀ (x : X), ∃ g, g • a = x) → IsPretransitive G X

State before:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ IsPretransitive G X → ∀ (x : X), ∃ g, g • a = x
Tactic:
intro hG x
State after:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : IsPretransitive G X
x : X
⊢ ∃ g, g • a = x

State before:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : IsPretransitive G X
x : X
⊢ ∃ g, g • a = x
Tactic:
let hG_eq := hG.exists_smul_eq
State after:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : IsPretransitive G X
x : X
hG_eq : ∀ (x y : X), ∃ g, g • x = y := exists_smul_eq
⊢ ∃ g, g • a = x

State before:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : IsPretransitive G X
x : X
hG_eq : ∀ (x y : X), ∃ g, g • x = y := exists_smul_eq
⊢ ∃ g, g • a = x
Tactic:
exact hG_eq a x
State after:
no goals

State before:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (∀ (x : X), ∃ g, g • a = x) → IsPretransitive G X
Tactic:
intro hG
State after:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
⊢ IsPretransitive G X

State before:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
⊢ IsPretransitive G X
Tactic:
apply IsPretransitive.mk
State after:
case mpr.exists_smul_eq
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
⊢ ∀ (x y : X), ∃ g, g • x = y

State before:
case mpr.exists_smul_eq
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
⊢ ∀ (x y : X), ∃ g, g • x = y
Tactic:
intro x y
State after:
case mpr.exists_smul_eq
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
⊢ ∃ g, g • x = y

State before:
case mpr.exists_smul_eq
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨g, hx⟩ := hG x
State after:
case mpr.exists_smul_eq.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
⊢ ∃ g, g • x = y

State before:
case mpr.exists_smul_eq.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨h, hy⟩ := hG y
State after:
case mpr.exists_smul_eq.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ ∃ g, g • x = y

State before:
case mpr.exists_smul_eq.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ ∃ g, g • x = y
Tactic:
use h * g⁻¹
State after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹) • x = y

State before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹) • x = y
Tactic:
rw [← hx]
State after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹) • g • a = y

State before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹) • g • a = y
Tactic:
rw [smul_smul, inv_mul_cancel_right]
State after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ h • a = y

State before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ h • a = y
Tactic:
exact hy
State after:
no goals