awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst_2 : Group D₁
inst_3 : Group Q₁
inst_4 : Group D₂
inst_5 : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₁ ≀ᵣ Q₁
x_1 : Q₁
⊢ left
      ((fun (x : D₂ ≀ᵣ Q₂) ↦
          ({ left := ((⇑f.symm : (a : D₂) → D₁) ∘ x.left) ∘ (⇑g : (a : Q₁) → Q₂),
              right := (g.symm : (a : Q₂) → Q₁) x.right } :
            D₁ ≀ᵣ Q₁))
        ((fun (x : D₁ ≀ᵣ Q₁) ↦
            ({ left := (⇑f : (a : D₁) → D₂) ∘ x.left ∘ (⇑g.symm : (a : Q₂) → Q₁),
                right := (g : (a : Q₁) → Q₂) x.right } :
              D₂ ≀ᵣ Q₂))
          x))
      x_1 =
    x.left x_1

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst_2 : Group D₁
inst_3 : Group Q₁
inst_4 : Group D₂
inst_5 : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₁ ≀ᵣ Q₁
⊢ right.{u_3, u_4} (D := D₁)
      ((fun (x : D₂ ≀ᵣ Q₂) ↦
          ({ left := ((⇑f.symm : (a : D₂) → D₁) ∘ x.left) ∘ (⇑g : (a : Q₁) → Q₂),
              right := (g.symm : (a : Q₂) → Q₁) x.right } :
            D₁ ≀ᵣ Q₁))
        ((fun (x : D₁ ≀ᵣ Q₁) ↦
            ({ left := (⇑f : (a : D₁) → D₂) ∘ x.left ∘ (⇑g.symm : (a : Q₂) → Q₁),
                right := (g : (a : Q₁) → Q₂) x.right } :
              D₂ ≀ᵣ Q₂))
          x)) =
    x.right

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst_2 : Group D₁
inst_3 : Group Q₁
inst_4 : Group D₂
inst_5 : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₂ ≀ᵣ Q₂
left :
  ∀ (x_1 : Q₂),
    RegularWreathProduct.left
        ((fun (x : D₁ ≀ᵣ Q₁) ↦
            ({ left := (⇑f : (a : D₁) → D₂) ∘ x.left ∘ (⇑g.symm : (a : Q₂) → Q₁),
                right := (g : (a : Q₁) → Q₂) x.right } :
              D₂ ≀ᵣ Q₂))
          ((fun (x : D₂ ≀ᵣ Q₂) ↦
              ({ left := ((⇑f.symm : (a : D₂) → D₁) ∘ x.left) ∘ (⇑g : (a : Q₁) → Q₂),
                  right := (g.symm : (a : Q₂) → Q₁) x.right } :
                D₁ ≀ᵣ Q₁))
            x))
        x_1 =
      x.left x_1
right :
  RegularWreathProduct.right.{u_5, u_6} (D := D₂)
      ((fun (x : D₁ ≀ᵣ Q₁) ↦
          ({ left := (⇑f : (a : D₁) → D₂) ∘ x.left ∘ (⇑g.symm : (a : Q₂) → Q₁), right := (g : (a : Q₁) → Q₂) x.right } :
            D₂ ≀ᵣ Q₂))
        ((fun (x : D₂ ≀ᵣ Q₂) ↦
            ({ left := ((⇑f.symm : (a : D₂) → D₁) ∘ x.left) ∘ (⇑g : (a : Q₁) → Q₂),
                right := (g.symm : (a : Q₂) → Q₁) x.right } :
              D₁ ≀ᵣ Q₁))
          x)) =
    x.right
⊢ (fun (x : D₁ ≀ᵣ Q₁) ↦
        ({ left := (⇑f : (a : D₁) → D₂) ∘ x.left ∘ (⇑g.symm : (a : Q₂) → Q₁), right := (g : (a : Q₁) → Q₂) x.right } :
          D₂ ≀ᵣ Q₂))
      ((fun (x : D₂ ≀ᵣ Q₂) ↦
          ({ left := ((⇑f.symm : (a : D₂) → D₁) ∘ x.left) ∘ (⇑g : (a : Q₁) → Q₂),
              right := (g.symm : (a : Q₂) → Q₁) x.right } :
            D₁ ≀ᵣ Q₁))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst_2 : Group D₁
inst_3 : Group Q₁
inst_4 : Group D₂
inst_5 : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₂ ≀ᵣ Q₂
x_1 : Q₂
⊢ left
      ((fun (x : D₁ ≀ᵣ Q₁) ↦
          ({ left := (⇑f : (a : D₁) → D₂) ∘ x.left ∘ (⇑g.symm : (a : Q₂) → Q₁), right := (g : (a : Q₁) → Q₂) x.right } :
            D₂ ≀ᵣ Q₂))
        ((fun (x : D₂ ≀ᵣ Q₂) ↦
            ({ left := ((⇑f.symm : (a : D₂) → D₁) ∘ x.left) ∘ (⇑g : (a : Q₁) → Q₂),
                right := (g.symm : (a : Q₂) → Q₁) x.right } :
              D₁ ≀ᵣ Q₁))
          x))
      x_1 =
    x.left x_1

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst_2 : Group D₁
inst_3 : Group Q₁
inst_4 : Group D₂
inst_5 : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₂ ≀ᵣ Q₂
⊢ right.{u_5, u_6} (D := D₂)
      ((fun (x : D₁ ≀ᵣ Q₁) ↦
          ({ left := (⇑f : (a : D₁) → D₂) ∘ x.left ∘ (⇑g.symm : (a : Q₂) → Q₁), right := (g : (a : Q₁) → Q₂) x.right } :
            D₂ ≀ᵣ Q₂))
        ((fun (x : D₂ ≀ᵣ Q₂) ↦
            ({ left := ((⇑f.symm : (a : D₂) → D₁) ∘ x.left) ∘ (⇑g : (a : Q₁) → Q₂),
                right := (g.symm : (a : Q₂) → Q₁) x.right } :
              D₁ ≀ᵣ Q₁))
          x)) =
    x.right

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst_2 : Group D₁
inst_3 : Group Q₁
inst_4 : Group D₂
inst_5 : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x y : D₁ ≀ᵣ Q₁
left :
  ∀ (x_1 : Q₂),
    RegularWreathProduct.left
        { left := (⇑f : (a : D₁) → D₂) ∘ (x * y).left ∘ (⇑g.symm : (a : Q₂) → Q₁),
          right := (g : (a : Q₁) → Q₂) (x * y).right }
        x_1 =
      (HMul.hMul (α := D₂ ≀ᵣ Q₂) (β := D₂ ≀ᵣ Q₂)
            ({ left := (⇑f : (a : D₁) → D₂) ∘ x.left ∘ (⇑g.symm : (a : Q₂) → Q₁),
                right := (g : (a : Q₁) → Q₂) x.right } :
              D₂ ≀ᵣ Q₂)
            ({ left := (⇑f : (a : D₁) → D₂) ∘ y.left ∘ (⇑g.symm : (a : Q₂) → Q₁),
                right := (g : (a : Q₁) → Q₂) y.right } :
              D₂ ≀ᵣ Q₂)).left
        x_1
right :
  RegularWreathProduct.right.{u_5, u_6} (D := D₂)
      { left := (⇑f : (a : D₁) → D₂) ∘ (x * y).left ∘ (⇑g.symm : (a : Q₂) → Q₁),
        right := (g : (a : Q₁) → Q₂) (x * y).right } =
    (HMul.hMul (α := D₂ ≀ᵣ Q₂) (β := D₂ ≀ᵣ Q₂)
        ({ left := (⇑f : (a : D₁) → D₂) ∘ x.left ∘ (⇑g.symm : (a : Q₂) → Q₁), right := (g : (a : Q₁) → Q₂) x.right } :
          D₂ ≀ᵣ Q₂)
        ({ left := (⇑f : (a : D₁) → D₂) ∘ y.left ∘ (⇑g.symm : (a : Q₂) → Q₁), right := (g : (a : Q₁) → Q₂) y.right } :
          D₂ ≀ᵣ Q₂)).right
⊢ { left := (⇑f : (a : D₁) → D₂) ∘ (x * y).left ∘ (⇑g.symm : (a : Q₂) → Q₁),
      right := (g : (a : Q₁) → Q₂) (x * y).right } =
    HMul.hMul (α := D₂ ≀ᵣ Q₂) (β := D₂ ≀ᵣ Q₂)
      ({ left := (⇑f : (a : D₁) → D₂) ∘ x.left ∘ (⇑g.symm : (a : Q₂) → Q₁), right := (g : (a : Q₁) → Q₂) x.right } :
        D₂ ≀ᵣ Q₂)
      ({ left := (⇑f : (a : D₁) → D₂) ∘ y.left ∘ (⇑g.symm : (a : Q₂) → Q₁), right := (g : (a : Q₁) → Q₂) y.right } :
        D₂ ≀ᵣ Q₂)

Tactic:
ext
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst_2 : Group D₁
inst_3 : Group Q₁
inst_4 : Group D₂
inst_5 : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x y : D₁ ≀ᵣ Q₁
x_1 : Q₂
⊢ left
      { left := (⇑f : (a : D₁) → D₂) ∘ (x * y).left ∘ (⇑g.symm : (a : Q₂) → Q₁),
        right := (g : (a : Q₁) → Q₂) (x * y).right }
      x_1 =
    (HMul.hMul (α := D₂ ≀ᵣ Q₂) (β := D₂ ≀ᵣ Q₂)
          ({ left := (⇑f : (a : D₁) → D₂) ∘ x.left ∘ (⇑g.symm : (a : Q₂) → Q₁), right := (g : (a : Q₁) → Q₂) x.right } :
            D₂ ≀ᵣ Q₂)
          ({ left := (⇑f : (a : D₁) → D₂) ∘ y.left ∘ (⇑g.symm : (a : Q₂) → Q₁), right := (g : (a : Q₁) → Q₂) y.right } :
            D₂ ≀ᵣ Q₂)).left
      x_1

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst_2 : Group D₁
inst_3 : Group Q₁
inst_4 : Group D₂
inst_5 : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x y : D₁ ≀ᵣ Q₁
⊢ right.{u_5, u_6} (D := D₂)
      { left := (⇑f : (a : D₁) → D₂) ∘ (x * y).left ∘ (⇑g.symm : (a : Q₂) → Q₁),
        right := (g : (a : Q₁) → Q₂) (x * y).right } =
    (HMul.hMul (α := D₂ ≀ᵣ Q₂) (β := D₂ ≀ᵣ Q₂)
        ({ left := (⇑f : (a : D₁) → D₂) ∘ x.left ∘ (⇑g.symm : (a : Q₂) → Q₁), right := (g : (a : Q₁) → Q₂) x.right } :
          D₂ ≀ᵣ Q₂)
        ({ left := (⇑f : (a : D₁) → D₂) ∘ y.left ∘ (⇑g.symm : (a : Q₂) → Q₁), right := (g : (a : Q₁) → Q₂) y.right } :
          D₂ ≀ᵣ Q₂)).right

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
Λ : Type u_3
inst_2 : MulAction D Λ
w : D ≀ᵣ Q
p : Λ × Q
⊢ w • p = (w.left (w.right * p.2) • p.1, w.right * p.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
Λ : Type u_3
inst_2 : MulAction D Λ
⊢ ∀ (x y : D ≀ᵣ Q) (b : Λ × Q), (x * y) • b = x • y • b

Tactic:
simp [smul_smul, mul_assoc]

Premises used: mul_assoc, smul_smul
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
Λ : Type u_3
inst_2 : MulAction D Λ
⊢ ∀ (b : Λ × Q), HSMul.hSMul (α := D ≀ᵣ Q) 1 b = b

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
Λ : Type u_3
inst_2 : MulAction D Λ
inst_3 : FaithfulSMul D Λ
inst_4 : Nonempty Q
inst_5 : Nonempty Λ
simp :
  ∀ {m₁ m₂ : D ≀ᵣ Q},
    (∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right) → m₁ = m₂
⊢ ∀ {m₁ m₂ : D ≀ᵣ Q}, (∀ (a : Λ × Q), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
simp only [smul_def, Prod.mk.injEq, mul_left_inj, Prod.forall]

Premises used: RegularWreathProduct.smul_def, mul_left_inj, Prod.mk.injEq, Prod.forall
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
Λ : Type u_3
inst_2 : MulAction D Λ
inst_3 : FaithfulSMul D Λ
inst_4 : Nonempty Q
inst_5 : Nonempty Λ
m₁ m₂ : D ≀ᵣ Q
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
let : ∀ (a : Λ), m₁ = m₂
⊢ m₁ = m₂

Tactic:
let ⟨a⟩ := ‹Nonempty Λ›
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
Λ : Type u_3
inst_2 : MulAction D Λ
inst_3 : FaithfulSMul D Λ
inst_4 : Nonempty Q
inst_5 : Nonempty Λ
m₁ m₂ : D ≀ᵣ Q
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
let : ∀ (b : Q), m₁ = m₂
⊢ m₁ = m₂

Tactic:
let ⟨b⟩ := ‹Nonempty Q›
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
Λ : Type u_3
inst_2 : MulAction D Λ
inst_3 : FaithfulSMul D Λ
inst_4 : Nonempty Q
inst_5 : Nonempty Λ
m₁ m₂ : D ≀ᵣ Q
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
b : Q
left : ∀ (q : Q), m₁.left q = m₂.left q
right : m₁.right = m₂.right
⊢ m₁ = m₂

Tactic:
ext q
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
Λ : Type u_3
inst_2 : MulAction D Λ
inst_3 : FaithfulSMul D Λ
inst_4 : Nonempty Q
inst_5 : Nonempty Λ
m₁ m₂ : D ≀ᵣ Q
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
b q : Q
⊢ ∀ (a : Λ), m₁.left (m₁.right * (m₁.right⁻¹ * q)) • a = m₂.left (m₂.right * (m₁.right⁻¹ * q)) • a

Tactic:
have hh := fun a => (h a (m₁.right⁻¹ * q)).1
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
Λ : Type u_3
inst_2 : MulAction D Λ
inst_3 : FaithfulSMul D Λ
inst_4 : Nonempty Q
inst_5 : Nonempty Λ
m₁ m₂ : D ≀ᵣ Q
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
b q : Q
hh : ∀ (a : Λ), m₁.left (m₁.right * (m₁.right⁻¹ * q)) • a = m₂.left (m₂.right * (m₁.right⁻¹ * q)) • a
⊢ ∀ (a : Λ), m₁.left (m₁.right * (m₁.right⁻¹ * q)) • a = m₂.left (m₁.right * (m₁.right⁻¹ * q)) • a

Tactic:
rw [← (h a b).2] at hh

Premises used: And.right
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
Λ : Type u_3
inst_2 : MulAction D Λ
inst_3 : FaithfulSMul D Λ
inst_4 : Nonempty Q
inst_5 : Nonempty Λ
m₁ m₂ : D ≀ᵣ Q
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
b q : Q
hh : ∀ (a : Λ), m₁.left (m₁.right * (m₁.right⁻¹ * q)) • a = m₂.left (m₁.right * (m₁.right⁻¹ * q)) • a
⊢ ∀ (a : Λ), m₁.left q • a = m₂.left q • a

Tactic:
group at hh
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
Λ : Type u_3
inst_2 : MulAction D Λ
inst_3 : FaithfulSMul D Λ
inst_4 : Nonempty Q
inst_5 : Nonempty Λ
m₁ m₂ : D ≀ᵣ Q
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
b q : Q
hh : ∀ (a : Λ), m₁.left q • a = m₂.left q • a
⊢ m₁.left q = m₂.left q

Tactic:
FaithfulSMul.eq_of_smul_eq_smul hh

Premises used: FaithfulSMul.eq_of_smul_eq_smul
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
Λ : Type u_3
inst_2 : MulAction D Λ
inst_3 : FaithfulSMul D Λ
inst_4 : Nonempty Q
inst_5 : Nonempty Λ
m₁ m₂ : D ≀ᵣ Q
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
b q : Q
hh : ∀ (a : Λ), m₁.left q • a = m₂.left q • a
⊢ m₁.left q = m₂.left q

Tactic:
exact FaithfulSMul.eq_of_smul_eq_smul hh

Premises used: FaithfulSMul.eq_of_smul_eq_smul
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
Λ : Type u_3
inst_2 : MulAction D Λ
inst_3 : FaithfulSMul D Λ
inst_4 : Nonempty Q
inst_5 : Nonempty Λ
m₁ m₂ : D ≀ᵣ Q
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
b : Q
⊢ m₁.right = m₂.right

Tactic:
(h a b).2

Premises used: And.right
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
Λ : Type u_3
inst_2 : MulAction D Λ
inst_3 : FaithfulSMul D Λ
inst_4 : Nonempty Q
inst_5 : Nonempty Λ
m₁ m₂ : D ≀ᵣ Q
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
b : Q
⊢ m₁.right = m₂.right

Tactic:
exact (h a b).2

Premises used: And.right
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
Λ : Type u_3
inst_2 : MulAction D Λ
inst_3 : FaithfulSMul D Λ
inst_4 : Nonempty Λ
⊢ Function.Injective (α := D ≀ᵣ Q) (β := Equiv.Perm (Λ × Q)) (⇑(toPerm D Q Λ) : (a : D ≀ᵣ Q) → Equiv.Perm (Λ × Q))

Tactic:
MulAction.toPerm_injective

Premises used: MulAction.toPerm, MulAction.toPerm_injective
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
G : Type u
⊢ IteratedWreathProduct G 0 = PUnit.{u + 1}

Tactic:
rfl

Premises used: rfl, IteratedWreathProduct
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
G : Type u
n : ℕ
⊢ IteratedWreathProduct G (n + 1) = IteratedWreathProduct G n ≀ᵣ G

Tactic:
rfl

Premises used: rfl, IteratedWreathProduct
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
G : Type u
n : ℕ
inst_2 : Finite G
⊢ Finite PUnit.{u + 1}

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
G : Type u
n_1 : ℕ
inst_2 : Finite G
n : ℕ
h : Finite.{u + 1} (IteratedWreathProduct G n)
⊢ Finite.{u + 1} (IteratedWreathProduct G n ≀ᵣ G)

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
G : Type u
n : ℕ
inst_2 : Finite G
zero : Finite.{u + 1} (IteratedWreathProduct G 0)
succ : ∀ (n : ℕ) (h : Finite.{u + 1} (IteratedWreathProduct G n)), Finite.{u + 1} (IteratedWreathProduct G (n + 1))
⊢ Finite.{u + 1} (IteratedWreathProduct G n)

Tactic:
induction n with
  | zero => rw [IteratedWreathProduct_zero]; infer_instance
  | succ n h => rw [IteratedWreathProduct_succ]; infer_instance

Premises used: IteratedWreathProduct_succ, IteratedWreathProduct_zero
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
G : Type u
n : ℕ
inst : Finite G
⊢ Nat.card.{u} (IteratedWreathProduct G 0) = HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range 0, Nat.card G ^ i)

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
G : Type u
n_1 : ℕ
inst : Finite G
n : ℕ
h : Nat.card.{u} (IteratedWreathProduct G n) = HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range n, Nat.card G ^ i)
succ :
  Nat.card.{u} (IteratedWreathProduct G n ≀ᵣ G) =
    HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range (n + 1), Nat.card G ^ i)
succ₁ :
  Nat.card.{u} (IteratedWreathProduct G n) ^ Nat.card G * Nat.card G =
    HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range (n + 1), Nat.card G ^ i)
succ₂ :
  HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range n, Nat.card G ^ i) ^ Nat.card G * Nat.card G =
    HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range (n + 1), Nat.card G ^ i)
succ₃ :
  HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range n, Nat.card G ^ i) ^ Nat.card G * Nat.card G =
    Nat.card G ^ (Nat.card G * ∑ i ∈ Finset.range n, Nat.card G ^ i + 1)
succ₄ :
  HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range n, Nat.card G ^ i) ^ Nat.card G * Nat.card G =
    Nat.card G ^ (Nat.card G * ∑ i ∈ Finset.range n, Nat.card G ^ i) * Nat.card G
succ₅ succ₆ :
  HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range n, Nat.card G ^ i) ^ Nat.card G * Nat.card G =
    HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range n, Nat.card G ^ i) ^ Nat.card G * Nat.card G
⊢ Nat.card.{u} (IteratedWreathProduct G (n + 1)) =
    HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range (n + 1), Nat.card G ^ i)

Tactic:
rw [IteratedWreathProduct_succ, RegularWreathProduct.card,
      h, geom_sum_succ, pow_succ, pow_mul']

Premises used: RegularWreathProduct.card, pow_succ, geom_sum_succ, IteratedWreathProduct_succ, pow_mul'
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
G : Type u
n : ℕ
inst : Finite G
zero : Nat.card.{u} (IteratedWreathProduct G 0) = HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range 0, Nat.card G ^ i)
succ :
  ∀ (n : ℕ)
    (h :
      Nat.card.{u} (IteratedWreathProduct G n) =
        HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range n, Nat.card G ^ i)),
    Nat.card.{u} (IteratedWreathProduct G (n + 1)) =
      HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range (n + 1), Nat.card G ^ i)
⊢ Nat.card.{u} (IteratedWreathProduct G n) = HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range n, Nat.card G ^ i)

Tactic:
induction n with
  | zero => simp
  | succ n h => rw [IteratedWreathProduct_succ, RegularWreathProduct.card,
      h, geom_sum_succ, pow_succ, pow_mul']

Premises used: RegularWreathProduct.card, pow_succ, geom_sum_succ, IteratedWreathProduct_succ, pow_mul'
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
G : Type u
n : ℕ
inst_2 : Group G
⊢ Group PUnit.{u + 1}

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
G : Type u
n_1 : ℕ
inst_2 : Group G
n : ℕ
ih : Group (IteratedWreathProduct G n)
⊢ Group (IteratedWreathProduct G n ≀ᵣ G)

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
G : Type u
n : ℕ
inst_2 : Group G
zero : Group (IteratedWreathProduct G 0)
succ : (n : ℕ) → (ih : Group (IteratedWreathProduct G n)) → Group (IteratedWreathProduct G (n + 1))
⊢ Group (IteratedWreathProduct G n)

Tactic:
induction n with
 | zero => rw [IteratedWreathProduct_zero]; infer_instance
 | succ n ih => rw [IteratedWreathProduct_succ]; infer_instance

Premises used: IteratedWreathProduct_succ, IteratedWreathProduct_zero
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
G_1 : Type u
n_1 : ℕ
inst_2 : Group G_1
G : Type u_3
inst_3 : Group G
n : ℕ
x : MulAction (IteratedWreathProduct G n) (Fin n → G) :=
  MulAction.compHom (M := Equiv.Perm (Fin n → G)) (Fin n → G) (iteratedWreathToPermHom G n)
⊢ IteratedWreathProduct G (n + 1) →* Equiv.Perm (Fin (n + 1) → G)

Tactic:
exact (Fin.succFunEquiv G n).symm.permCongrHom.toMonoidHom.comp
        (RegularWreathProduct.toPerm (IteratedWreathProduct G n) G (Fin n → G))

Premises used: MonoidHom.comp, MulEquiv.toMonoidHom, Equiv.permCongrHom, Fin.succFunEquiv, Equiv.symm, RegularWreathProduct.toPerm, IteratedWreathProduct
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
G : Type u_3
inst : Group G
⊢ Function.Injective (α := PUnit.{u_3 + 1}) (β := Equiv.Perm (Fin 0 → G))
    (⇑(iteratedWreathToPermHom G 0) : (a : PUnit.{u_3 + 1}) → Equiv.Perm (Fin 0 → G))

Tactic:
apply Function.injective_of_subsingleton

Premises used: Function.injective_of_subsingleton
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
G : Type u_3
inst : Group G
n : ℕ
x : MulAction (IteratedWreathProduct G n) (Fin n → G) := MulAction.compHom (Fin n → G) (iteratedWreathToPermHom G n)
⊢ FaithfulSMul.{u_3, u_3} (IteratedWreathProduct G n) (Fin n → G)

Tactic:
have : FaithfulSMul (IteratedWreathProduct G n) (Fin n → G) :=
        ⟨fun h ↦ iteratedWreathToPermHomInj G n (Equiv.ext h)⟩
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
G : Type u_3
inst : Group G
n : ℕ
x : MulAction (IteratedWreathProduct G n) (Fin n → G) := MulAction.compHom (Fin n → G) (iteratedWreathToPermHom G n)
this : FaithfulSMul.{u_3, u_3} (IteratedWreathProduct G n) (Fin n → G)
⊢ Function.Injective (α := IteratedWreathProduct G (n + 1)) (β := Equiv.Perm (Fin (n + 1) → G))
    (⇑(iteratedWreathToPermHom G (n + 1)) : (a : IteratedWreathProduct G (n + 1)) → Equiv.Perm (Fin (n + 1) → G))

Tactic:
((Fin.succFunEquiv G n).symm.permCongrHom.toEquiv.comp_injective _).mpr
        (RegularWreathProduct.toPermInj (IteratedWreathProduct G n) G (Fin n → G))

Premises used: Iff.mpr, Equiv.trans, MulEquiv.toEquiv, RegularWreathProduct.toPermInj, Equiv.permCongrHom, Fin.succFunEquiv, Equiv.comp_injective, Equiv.symm, IteratedWreathProduct
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
G : Type u_3
inst : Group G
n : ℕ
x : MulAction (IteratedWreathProduct G n) (Fin n → G) := MulAction.compHom (Fin n → G) (iteratedWreathToPermHom G n)
this : FaithfulSMul.{u_3, u_3} (IteratedWreathProduct G n) (Fin n → G)
⊢ Function.Injective (α := IteratedWreathProduct G (n + 1)) (β := Equiv.Perm (Fin (n + 1) → G))
    (⇑(iteratedWreathToPermHom G (n + 1)) : (a : IteratedWreathProduct G (n + 1)) → Equiv.Perm (Fin (n + 1) → G))

Tactic:
exact ((Fin.succFunEquiv G n).symm.permCongrHom.toEquiv.comp_injective _).mpr
        (RegularWreathProduct.toPermInj (IteratedWreathProduct G n) G (Fin n → G))

Premises used: Iff.mpr, MulEquiv.toEquiv, RegularWreathProduct.toPermInj, Equiv.permCongrHom, Fin.succFunEquiv, Equiv.comp_injective, Equiv.symm, IteratedWreathProduct
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
G_1 : Type u
n_1 : ℕ
inst_2 : Group G_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst_3 : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst_4 : Group G
inst_5 : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
rw : Nat.card G ^ Nat.card (Fin n) = p ^ n
rw₁ : Nat.card G ^ n = p ^ n
rw₂ rw₃ : p ^ n = p ^ n
⊢ Nat.card.{u_4} (Fin n → G) = p ^ n

Tactic:
rw [Nat.card_fun, Nat.card_fin, hG]

Premises used: Nat.card_fun, Nat.card_fin
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
G_1 : Type u
n_1 : ℕ
inst_2 : Group G_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst_3 : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst_4 : Group G
inst_5 : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
e1 : Equiv.{u_3 + 1, u_4 + 1} α (Fin n → G) := (Finite.equivFinOfCardEq hα).trans (Finite.equivFinOfCardEq ⋯).symm
f : MonoidHom.{u_4, u_3} (IteratedWreathProduct G n) (Equiv.Perm α) :=
  e1.symm.permCongrHom.toMonoidHom.comp (iteratedWreathToPermHom G n)
⊢ Function.Injective.{u_4 + 1, u_3 + 1} (α := IteratedWreathProduct G n) (β := Equiv.Perm α)
    (⇑f : (a : IteratedWreathProduct G n) → Equiv.Perm α)

Tactic:
have hf : Function.Injective f :=
    (e1.symm.permCongrHom.comp_injective _).mpr (iteratedWreathToPermHomInj G n)