internlm/Lean-Github huggingface dataset:
Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_injective
Proof state before:
case h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
i : ι
⊢ x i = y i
Tactic:
apply hf
Proof state after:
case h.a
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
i : ι
⊢ f (x i) = f (y i)
Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_injective
Proof state before:
case h.a
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
i : ι
⊢ f (x i) = f (y i)
Tactic:
simp only [← EquivariantMap.embeddingOfEquivariantMap_apply hf]
Proof state after:
case h.a
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
i : ι
⊢ ((embeddingOfEquivariantMap hf ι) x) i = ((embeddingOfEquivariantMap hf ι) y) i
Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_injective
Proof state before:
case h.a
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
i : ι
⊢ ((embeddingOfEquivariantMap hf ι) x) i = ((embeddingOfEquivariantMap hf ι) y) i
Tactic:
rw [hxy]
Proof state after:
no goals
Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_bijective
Proof state before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
⊢ Function.Bijective ⇑(embeddingOfEquivariantMap ⋯ ι)
Tactic:
constructor
Proof state after:
case left
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
⊢ Function.Injective ⇑(embeddingOfEquivariantMap ⋯ ι)

case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
⊢ Function.Surjective ⇑(embeddingOfEquivariantMap ⋯ ι)
Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_bijective
Proof state before:
case left
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
⊢ Function.Injective ⇑(embeddingOfEquivariantMap ⋯ ι)

case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
⊢ Function.Surjective ⇑(embeddingOfEquivariantMap ⋯ ι)
Tactic:
exact EquivariantMap.embeddingOfEquivariantMap_is_injective hf.injective
Proof state after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
⊢ Function.Surjective ⇑(embeddingOfEquivariantMap ⋯ ι)
Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_bijective
Proof state before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
⊢ Function.Surjective ⇑(embeddingOfEquivariantMap ⋯ ι)
Tactic:
intro y
Proof state after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
⊢ ∃ a, (embeddingOfEquivariantMap ⋯ ι) a = y
Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_bijective
Proof state before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
⊢ ∃ a, (embeddingOfEquivariantMap ⋯ ι) a = y
Tactic:
obtain ⟨g, _, hfg⟩ := Function.bijective_iff_has_inverse.mp hf
Proof state after:
case right.intro.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
⊢ ∃ a, (embeddingOfEquivariantMap ⋯ ι) a = y
Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_bijective
Proof state before:
case right.intro.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
⊢ ∃ a, (embeddingOfEquivariantMap ⋯ ι) a = y
Tactic:
use ⟨g ∘ y, Function.Injective.comp hfg.injective (EmbeddingLike.injective y)⟩
Proof state after:
case h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
⊢ (embeddingOfEquivariantMap ⋯ ι) { toFun := g ∘ ⇑y, inj' := ⋯ } = y
Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_bijective
Proof state before:
case h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
⊢ (embeddingOfEquivariantMap ⋯ ι) { toFun := g ∘ ⇑y, inj' := ⋯ } = y
Tactic:
ext i
Proof state after:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
i : ι
⊢ ((embeddingOfEquivariantMap ⋯ ι) { toFun := g ∘ ⇑y, inj' := ⋯ }) i = y i
Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_bijective
Proof state before:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
i : ι
⊢ ((embeddingOfEquivariantMap ⋯ ι) { toFun := g ∘ ⇑y, inj' := ⋯ }) i = y i
Tactic:
rw [EquivariantMap.embeddingOfEquivariantMap_apply]
Proof state after:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
i : ι
⊢ f ({ toFun := g ∘ ⇑y, inj' := ⋯ } i) = y i
Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_bijective
Proof state before:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
i : ι
⊢ f ({ toFun := g ∘ ⇑y, inj' := ⋯ } i) = y i
Tactic:
simp only [coeFn_mk, Function.comp_apply]
Proof state after:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
i : ι
⊢ f (g (y i)) = y i
Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_bijective
Proof state before:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
σ : M → N
f : α →ₑ[σ] β
hf : Function.Bijective ⇑f
ι : Type u_5
y : ι ↪ β
g : β → α
left✝ : Function.LeftInverse g ⇑f
hfg : Function.RightInverse g ⇑f
i : ι
⊢ f (g (y i)) = y i
Tactic:
rw [hfg]
Proof state after:
no goals
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
⊢ IsMultiplyPretransitive N β n
Tactic:
let h_eq := h.exists_smul_eq
Proof state after:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsMultiplyPretransitive N β n
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsMultiplyPretransitive N β n
Tactic:
apply IsPretransitive.mk
Proof state after:
case exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : Fin n ↪ β), ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
case exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : Fin n ↪ β), ∃ g, g • x = y
Tactic:
let aux : (Fin n ↪ β) → (Fin n ↪ α) := fun x =>
  { toFun := (Function.surjInv hf) ∘ x.toFun
    inj' := fun u v huv => by
      let huv' :=congr_arg f huv
      simp only [Function.comp_apply, Function.surjInv_eq] at huv'
      exact x.inj' huv' }
Proof state after:
case exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
⊢ ∀ (x y : Fin n ↪ β), ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
case exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
⊢ ∀ (x y : Fin n ↪ β), ∃ g, g • x = y
Tactic:
have aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun (aux x i) = x i := fun x i => by
  simp only [toFun_eq_coe, coeFn_mk, Function.comp_apply, aux]
  apply Function.surjInv_eq
Proof state after:
case exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
⊢ ∀ (x y : Fin n ↪ β), ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
case exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
⊢ ∀ (x y : Fin n ↪ β), ∃ g, g • x = y
Tactic:
intro x y
Proof state after:
case exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
⊢ ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
case exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨g, hg⟩ := h_eq (aux x) (aux y)
Proof state after:
case exists_smul_eq.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : g • aux x = aux y
⊢ ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
case exists_smul_eq.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : g • aux x = aux y
⊢ ∃ g, g • x = y
Tactic:
use σ g
Proof state after:
case h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : g • aux x = aux y
⊢ σ g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
case h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : g • aux x = aux y
⊢ σ g • x = y
Tactic:
ext i
Proof state after:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : g • aux x = aux y
i : Fin n
⊢ (σ g • x) i = y i
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : g • aux x = aux y
i : Fin n
⊢ (σ g • x) i = y i
Tactic:
rw [DFunLike.ext_iff] at hg
Proof state after:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : ∀ (x_1 : Fin n), (g • aux x) x_1 = (aux y) x_1
i : Fin n
⊢ (σ g • x) i = y i
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : ∀ (x_1 : Fin n), (g • aux x) x_1 = (aux y) x_1
i : Fin n
⊢ (σ g • x) i = y i
Tactic:
simp only [smul_apply]
Proof state after:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : ∀ (x_1 : Fin n), (g • aux x) x_1 = (aux y) x_1
i : Fin n
⊢ σ g • x i = y i
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : ∀ (x_1 : Fin n), (g • aux x) x_1 = (aux y) x_1
i : Fin n
⊢ σ g • x i = y i
Tactic:
simp only [← aux_apply, ← hg, smul_apply, MulActionHom.map_smul']
Proof state after:
no goals
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x : Fin n ↪ β
u v : Fin n
huv : (Function.surjInv hf ∘ x.toFun) u = (Function.surjInv hf ∘ x.toFun) v
⊢ u = v
Tactic:
let huv' :=congr_arg f huv
Proof state after:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x : Fin n ↪ β
u v : Fin n
huv : (Function.surjInv hf ∘ x.toFun) u = (Function.surjInv hf ∘ x.toFun) v
huv' : f ((Function.surjInv hf ∘ x.toFun) u) = f ((Function.surjInv hf ∘ x.toFun) v) := congr_arg (⇑f) huv
⊢ u = v
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x : Fin n ↪ β
u v : Fin n
huv : (Function.surjInv hf ∘ x.toFun) u = (Function.surjInv hf ∘ x.toFun) v
huv' : f ((Function.surjInv hf ∘ x.toFun) u) = f ((Function.surjInv hf ∘ x.toFun) v) := congr_arg (⇑f) huv
⊢ u = v
Tactic:
simp only [Function.comp_apply, Function.surjInv_eq] at huv'
Proof state after:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x : Fin n ↪ β
u v : Fin n
huv : (Function.surjInv hf ∘ x.toFun) u = (Function.surjInv hf ∘ x.toFun) v
huv' : x.toFun u = x.toFun v
⊢ u = v
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x : Fin n ↪ β
u v : Fin n
huv : (Function.surjInv hf ∘ x.toFun) u = (Function.surjInv hf ∘ x.toFun) v
huv' : x.toFun u = x.toFun v
⊢ u = v
Tactic:
exact x.inj' huv'
Proof state after:
no goals