Theorem: isPretransitive.of_surjective_map (Jordan/EquivariantMap.lean)

State before:
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
⊢ IsPretransitive N β
Tactic:
apply MulAction.IsPretransitive.mk
State after:
case exists_smul_eq
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
⊢ ∀ (x y : β), ∃ g, g • x = y

State before:
case exists_smul_eq
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
⊢ ∀ (x y : β), ∃ g, g • x = y
Tactic:
intro x y
State after:
case exists_smul_eq
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
x y : β
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
x y : β
⊢ ∃ g, g • x = y
Tactic:
let h_eq := h.exists_smul_eq
State after:
case exists_smul_eq
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
x y : β
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
x y : β
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨x', rfl⟩ := hf x
State after:
case exists_smul_eq.intro
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
y : β
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : α
⊢ ∃ g, g • f x' = y

State before:
case exists_smul_eq.intro
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
y : β
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : α
⊢ ∃ g, g • f x' = y
Tactic:
obtain ⟨y', rfl⟩ := hf y
State after:
case exists_smul_eq.intro.intro
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' y' : α
⊢ ∃ g, g • f x' = f y'

State before:
case exists_smul_eq.intro.intro
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' y' : α
⊢ ∃ g, g • f x' = f y'
Tactic:
obtain ⟨g, rfl⟩ := h_eq x' y'
State after:
case exists_smul_eq.intro.intro.intro
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : α
g : M
⊢ ∃ g_1, g_1 • f x' = f (g • x')

State before:
case exists_smul_eq.intro.intro.intro
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : α
g : M
⊢ ∃ g_1, g_1 • f x' = f (g • x')
Tactic:
use φ g
State after:
case h
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : α
g : M
⊢ φ g • f x' = f (g • x')

State before:
case h
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : α
g : M
⊢ φ g • f x' = f (g • x')
Tactic:
simp only [map_smulₛₗ]
State after:
no goals