internlm/Lean-Github huggingface dataset:
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
hf' : Function.Surjective ⇑f'
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)
Tactic:
refine isPreprimitive_of_surjective_map hf' (h.right s ?_)
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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
hf' : Function.Surjective ⇑f'
⊢ Set.encard s + 1 = ↑n
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
hf' : Function.Surjective ⇑f'
⊢ Set.encard s + 1 = ↑n
Tactic:
rw [← ht, ← hs', hf.injective.encard_image]
Proof state after:
no goals
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_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 β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
⊢ φ m • ↑{ val := y, property := hy } = ↑{ val := y, property := hy }
Tactic:
rw [← hs', Set.mem_image_iff_bex] at hy
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 β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy✝ : y ∈ t
hy : ∃ x, ∃ (_ : x ∈ s), f x = y
⊢ φ m • ↑{ val := y, property := hy✝ } = ↑{ val := y, property := hy✝ }
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_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 β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy✝ : y ∈ t
hy : ∃ x, ∃ (_ : x ∈ s), f x = y
⊢ φ m • ↑{ val := y, property := hy✝ } = ↑{ val := y, property := hy✝ }
Tactic:
obtain ⟨x, hx, hx'⟩ := hy
Proof state after:
case 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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ φ m • ↑{ val := y, property := hy } = ↑{ val := y, property := hy }
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case 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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ φ m • ↑{ val := y, property := hy } = ↑{ val := y, property := hy }
Tactic:
simp only [Subtype.coe_mk]
Proof state after:
case 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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ φ m • y = y
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case 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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ φ m • y = y
Tactic:
rw [← hx', ← map_smulₛₗ]
Proof state after:
case 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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ f (m • x) = f x
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case 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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ f (m • x) = f x
Tactic:
apply congr_arg
Proof state after:
case intro.intro.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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ m • x = x
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case intro.intro.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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ m • x = x
Tactic:
rw [mem_fixingSubgroup_iff] at hm
Proof state after:
case intro.intro.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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : ∀ y ∈ s, m • y = y
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ m • x = x
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case intro.intro.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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : ∀ y ∈ s, m • y = y
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ m • x = x
Tactic:
exact hm x hx
Proof state after:
no goals
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_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 β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
x✝¹ : ↥(fixingSubgroup M s)
x✝ : ↥(SubMulAction.ofFixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup M s
⊢ (fun x =>
        match x with
        | { val := x, property := hx } => { val := f.toFun x, property := ⋯ })
      ({ val := m, property := hm } • { val := x, property := hx }) =
    φ' { val := m, property := hm } •
      (fun x =>
          match x with
          | { val := x, property := hx } => { val := f.toFun x, property := ⋯ })
        { val := x, property := hx }
Tactic:
rw [← SetLike.coe_eq_coe]
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 β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
x✝¹ : ↥(fixingSubgroup M s)
x✝ : ↥(SubMulAction.ofFixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup M s
⊢ ↑((fun x =>
          match x with
          | { val := x, property := hx } => { val := f.toFun x, property := ⋯ })
        ({ val := m, property := hm } • { val := x, property := hx })) =
    ↑(φ' { val := m, property := hm } •
        (fun x =>
            match x with
            | { val := x, property := hx } => { val := f.toFun x, property := ⋯ })
          { val := x, property := hx })
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_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 β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
x✝¹ : ↥(fixingSubgroup M s)
x✝ : ↥(SubMulAction.ofFixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup M s
⊢ ↑((fun x =>
          match x with
          | { val := x, property := hx } => { val := f.toFun x, property := ⋯ })
        ({ val := m, property := hm } • { val := x, property := hx })) =
    ↑(φ' { val := m, property := hm } •
        (fun x =>
            match x with
            | { val := x, property := hx } => { val := f.toFun x, property := ⋯ })
          { val := x, property := hx })
Tactic:
exact f.map_smul' m x
Proof state after:
no goals
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_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 β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
⊢ Function.Surjective ⇑f'
Tactic:
rintro ⟨y, hy⟩
Proof state after:
case mk
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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
⊢ ∃ a, f' a = { val := y, property := hy }
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case mk
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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
⊢ ∃ a, f' a = { val := y, property := hy }
Tactic:
obtain ⟨x, hx⟩ := hf.right y
Proof state after:
case mk.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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ ∃ a, f' a = { val := y, property := hy }
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case mk.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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ ∃ a, f' a = { val := y, property := hy }
Tactic:
use ⟨x, ?_⟩
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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ f' { val := x, property := ?w } = { val := y, property := hy }

case w
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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ x ∈ SubMulAction.ofFixingSubgroup M s
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_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 β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ f' { val := x, property := ?w } = { val := y, property := hy }
Tactic:
simp only [f']
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
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ { toFun := fun x => { val := f.toFun ↑x, property := ⋯ }, map_smul' := ⋯ } { val := x, property := ?w } =
    { val := y, property := hy }
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_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 β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ { toFun := fun x => { val := f.toFun ↑x, property := ⋯ }, map_smul' := ⋯ } { val := x, property := ?w } =
    { val := y, property := hy }
Tactic:
apply Subtype.coe_injective
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.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ (fun a => ↑a)
      ({ toFun := fun x => { val := f.toFun ↑x, property := ⋯ }, map_smul' := ⋯ } { val := x, property := ?w }) =
    (fun a => ↑a) { val := y, property := hy }
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
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.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ (fun a => ↑a)
      ({ toFun := fun x => { val := f.toFun ↑x, property := ⋯ }, map_smul' := ⋯ } { val := x, property := ?w }) =
    (fun a => ↑a) { val := y, property := hy }
Tactic:
exact hx
Proof state after:
no goals