Theorem: isPretransitive.of_bijective_map_iff (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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPretransitive M α ↔ IsPretransitive N β
Tactic:
constructor
State after:
case mp
α✝ : 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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPretransitive M α → IsPretransitive N β

case mpr
α✝ : 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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPretransitive N β → IsPretransitive M α

State before:
case mp
α✝ : 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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPretransitive M α → IsPretransitive N β

case mpr
α✝ : 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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPretransitive N β → IsPretransitive M α
Tactic:
apply isPretransitive.of_surjective_map hf.surjective
State after:
case mpr
α✝ : 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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPretransitive N β → IsPretransitive M α

State before:
case mpr
α✝ : 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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPretransitive N β → IsPretransitive M α
Tactic:
intro hN
State after:
case mpr
α✝ : 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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
⊢ IsPretransitive M α

State before:
case mpr
α✝ : 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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
⊢ IsPretransitive M α
Tactic:
apply IsPretransitive.mk
State after:
case mpr.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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
⊢ ∀ (x y : α), ∃ g, g • x = y

State before:
case mpr.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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
⊢ ∀ (x y : α), ∃ g, g • x = y
Tactic:
intro x y
State after:
case mpr.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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
x y : α
⊢ ∃ g, g • x = y

State before:
case mpr.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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
x y : α
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨k, hk⟩ := exists_smul_eq N (f x) (f y)
State after:
case mpr.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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
x y : α
k : N
hk : k • f x = f y
⊢ ∃ g, g • x = y

State before:
case mpr.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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
x y : α
k : N
hk : k • f x = f y
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨g, rfl⟩ := hφ k
State after:
case mpr.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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
x y : α
g : M
hk : φ g • f x = f y
⊢ ∃ g, g • x = y

State before:
case mpr.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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
x y : α
g : M
hk : φ g • f x = f y
⊢ ∃ g, g • x = y
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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
x y : α
g : M
hk : φ g • f x = f y
⊢ g • x = y

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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
x y : α
g : M
hk : φ g • f x = f y
⊢ g • x = y
Tactic:
apply hf.injective
State after:
case h.a
α✝ : 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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
x y : α
g : M
hk : φ g • f x = f y
⊢ f (g • x) = f y

State before:
case h.a
α✝ : 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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
x y : α
g : M
hk : φ g • f x = f y
⊢ f (g • x) = f y
Tactic:
simp only [hk, map_smulₛₗ]
State after:
no goals