internlm/Lean-Github huggingface dataset:
Theorem: isPretransitive.of_surjective_map
Proof 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
Proof 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
Theorem: isPretransitive.of_surjective_map
Proof 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
Proof 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
Theorem: isPretransitive.of_surjective_map
Proof 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
Proof 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'
Theorem: isPretransitive.of_surjective_map
Proof 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'
Proof 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')
Theorem: isPretransitive.of_surjective_map
Proof 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
Proof 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')
Theorem: isPretransitive.of_surjective_map
Proof 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ₛₗ]
Proof state after:
no goals
Theorem: isPretransitive.of_bijective_map_iff
Proof 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
Proof 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 α
Theorem: isPretransitive.of_bijective_map_iff
Proof 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
Proof 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 α
Theorem: isPretransitive.of_bijective_map_iff
Proof 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
Proof 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 α
Theorem: isPretransitive.of_bijective_map_iff
Proof 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
Proof 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
Theorem: isPretransitive.of_bijective_map_iff
Proof 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
Proof 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
Theorem: isPretransitive.of_bijective_map_iff
Proof 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)
Proof 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
Theorem: isPretransitive.of_bijective_map_iff
Proof 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
Proof 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
Theorem: isPretransitive.of_bijective_map_iff
Proof 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
Proof 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
Theorem: isPretransitive.of_bijective_map_iff
Proof 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
Proof 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
Theorem: isPretransitive.of_bijective_map_iff
Proof 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ₛₗ]
Proof state after:
no goals
Theorem: MulAction.isMultiplyPreprimitive_zero
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsMultiplyPreprimitive M α 0
Tactic:
constructor
Proof state after:
case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsMultiplyPretransitive M α 0

case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑0 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Theorem: MulAction.isMultiplyPreprimitive_zero
Proof state before:
case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsMultiplyPretransitive M α 0
Tactic:
apply MulAction.is_zero_pretransitive
Proof state after:
no goals
Theorem: MulAction.isMultiplyPreprimitive_zero
Proof state before:
case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑0 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
intro s
Proof state after:
case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
⊢ Set.encard s + 1 = ↑0 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Theorem: MulAction.isMultiplyPreprimitive_zero
Proof state before:
case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
⊢ Set.encard s + 1 = ↑0 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
simp
Proof state after:
no goals
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsPreprimitive M α ↔ IsMultiplyPreprimitive M α 1
Tactic:
constructor
Proof state after:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsPreprimitive M α → IsMultiplyPreprimitive M α 1

case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsMultiplyPreprimitive M α 1 → IsPreprimitive M α
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsPreprimitive M α → IsMultiplyPreprimitive M α 1
Tactic:
intro h
Proof state after:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ IsMultiplyPreprimitive M α 1
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ IsMultiplyPreprimitive M α 1
Tactic:
constructor
Proof state after:
case mp.left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ IsMultiplyPretransitive M α 1

case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
case mp.left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ IsMultiplyPretransitive M α 1
Tactic:
rw [← isPretransitive_iff_is_one_pretransitive]
Proof state after:
case mp.left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ IsPretransitive M α
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
case mp.left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ IsPretransitive M α
Tactic:
exact h.toIsPretransitive
Proof state after:
no goals
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
intro s hs
Proof state after:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = ↑1
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = ↑1
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
simp only [Nat.cast_one] at hs
Proof state after:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
suffices s = ∅ by
  rw [this]
  rw [isPreprimitive_of_bijective_map_iff
    (SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective M α)
    (SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective M α)]
  exact h
Proof state after:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
⊢ s = ∅
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
⊢ s = ∅
Tactic:
rw [← Set.encard_eq_zero, ← Nat.cast_zero, ← WithTop.add_one_eq_coe_succ_iff]
Proof state after:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
⊢ Set.encard s + 1 = ↑(Nat.succ 0)
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
⊢ Set.encard s + 1 = ↑(Nat.succ 0)
Tactic:
exact hs
Proof state after:
no goals
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
this : s = ∅
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
rw [this]
Proof state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
this : s = ∅
⊢ IsPreprimitive ↥(fixingSubgroup M ∅) ↥(SubMulAction.ofFixingSubgroup M ∅)
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
this : s = ∅
⊢ IsPreprimitive ↥(fixingSubgroup M ∅) ↥(SubMulAction.ofFixingSubgroup M ∅)
Tactic:
rw [isPreprimitive_of_bijective_map_iff
  (SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective M α)
  (SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective M α)]
Proof state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
this : s = ∅
⊢ IsPreprimitive M α
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
this : s = ∅
⊢ IsPreprimitive M α
Tactic:
exact h
Proof state after:
no goals
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsMultiplyPreprimitive M α 1 → IsPreprimitive M α
Tactic:
rintro ⟨_, h1'⟩
Proof state after:
case mpr.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
left✝ : IsMultiplyPretransitive M α 1
h1' : ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
⊢ IsPreprimitive M α