awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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
⊢ (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
have right : 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: ext
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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 := (⇑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₂)
have left : ∀ (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: ext
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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
⊢ { 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₂)
have right : 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: ext
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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}, (∀ (a : Λ × Q), m₁ • a = m₂ • a) → m₁ = m₂
have 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₂
Tactic: simp only [smul_def, Prod.mk.injEq, mul_left_inj, Prod.forall]
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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
⊢ m₁ = m₂
have let : ∀ (a : Λ), m₁ = m₂
Tactic: let ⟨a⟩ := ‹Nonempty Λ›
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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 : Λ
⊢ m₁ = m₂
have let : ∀ (b : Q), m₁ = m₂
Tactic: let ⟨b⟩ := ‹Nonempty Q›
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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₁ = m₂
have left : ∀ (q : Q), m₁.left q = m₂.left q
Tactic: ext q
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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
⊢ m₁ = m₂
have right : m₁.right = m₂.right
Tactic: ext q
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (hypothesis)
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
⊢ m₁.left q = m₂.left q
have hh : ∀ (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
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (hypothesis)
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
⊢ m₁.left q = m₂.left q
have hh₁ : ∀ (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
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (hypothesis)
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
⊢ m₁.left q = m₂.left q
have hh₁ : ∀ (a : Λ), m₁.left q • a = m₂.left q • a
Tactic: group at hh
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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.{u + 1} (IteratedWreathProduct G n)
have zero : Finite.{u + 1} (IteratedWreathProduct G 0)
Tactic: induction n with
  | zero => rw [IteratedWreathProduct_zero]; infer_instance
  | succ n h => rw [IteratedWreathProduct_succ]; infer_instance
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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)
⊢ Finite.{u + 1} (IteratedWreathProduct G n)
have succ : ∀ (n : ℕ) (h : Finite.{u + 1} (IteratedWreathProduct G n)), Finite.{u + 1} (IteratedWreathProduct G (n + 1))
Tactic: induction n with
  | zero => rw [IteratedWreathProduct_zero]; infer_instance
  | succ n h => rw [IteratedWreathProduct_succ]; infer_instance
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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)
⊢ Nat.card.{u} (IteratedWreathProduct G (n + 1)) =
    HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range (n + 1), Nat.card G ^ i)
have succ : Nat.card.{u} (IteratedWreathProduct G n ≀ᵣ G) =
  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']
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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)
⊢ Nat.card.{u} (IteratedWreathProduct G (n + 1)) =
    HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range (n + 1), Nat.card G ^ i)
have 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)
Tactic: rw [IteratedWreathProduct_succ, RegularWreathProduct.card,
      h, geom_sum_succ, pow_succ, pow_mul']
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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)
⊢ Nat.card.{u} (IteratedWreathProduct G (n + 1)) =
    HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range (n + 1), Nat.card G ^ i)
have 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)
Tactic: rw [IteratedWreathProduct_succ, RegularWreathProduct.card,
      h, geom_sum_succ, pow_succ, pow_mul']
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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)
⊢ Nat.card.{u} (IteratedWreathProduct G (n + 1)) =
    HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range (n + 1), Nat.card G ^ i)
have 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)
Tactic: rw [IteratedWreathProduct_succ, RegularWreathProduct.card,
      h, geom_sum_succ, pow_succ, pow_mul']
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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)
⊢ Nat.card.{u} (IteratedWreathProduct G (n + 1)) =
    HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range (n + 1), Nat.card G ^ i)
have 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
Tactic: rw [IteratedWreathProduct_succ, RegularWreathProduct.card,
      h, geom_sum_succ, pow_succ, pow_mul']
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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
⊢ Nat.card.{u} (IteratedWreathProduct G (n + 1)) =
    HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range (n + 1), Nat.card G ^ i)
have 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
Tactic: rw [IteratedWreathProduct_succ, RegularWreathProduct.card,
      h, geom_sum_succ, pow_succ, pow_mul']
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
Goal:
G : Type u
n : ℕ
inst : Finite G
⊢ Nat.card.{u} (IteratedWreathProduct G n) = HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range n, Nat.card G ^ i)
have zero : Nat.card.{u} (IteratedWreathProduct G 0) = HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range 0, 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']
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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)
⊢ Nat.card.{u} (IteratedWreathProduct G n) = HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range n, Nat.card G ^ i)
have 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)
Tactic: induction n with
  | zero => simp
  | succ n h => rw [IteratedWreathProduct_succ, RegularWreathProduct.card,
      h, geom_sum_succ, pow_succ, pow_mul']
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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 (IteratedWreathProduct G n)
have zero : Group (IteratedWreathProduct G 0)
Tactic: induction n with
 | zero => rw [IteratedWreathProduct_zero]; infer_instance
 | succ n ih => rw [IteratedWreathProduct_succ]; infer_instance
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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)
⊢ Group (IteratedWreathProduct G n)
have succ : (n : ℕ) → (ih : Group (IteratedWreathProduct G n)) → Group (IteratedWreathProduct G (n + 1))
Tactic: induction n with
 | zero => rw [IteratedWreathProduct_zero]; infer_instance
 | succ n ih => rw [IteratedWreathProduct_succ]; infer_instance
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (hypothesis)
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)
⊢ 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))
have this : 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)⟩
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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 α)
⊢ Nat.card.{u_4} (Fin n → G) = p ^ n
have rw : Nat.card G ^ Nat.card (Fin n) = p ^ n
Tactic: rw [Nat.card_fun, Nat.card_fin, hG]
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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
⊢ Nat.card.{u_4} (Fin n → G) = p ^ n
have rw₁ : Nat.card G ^ n = p ^ n
Tactic: rw [Nat.card_fun, Nat.card_fin, hG]
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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
⊢ Nat.card.{u_4} (Fin n → G) = p ^ n
have rw₂ : p ^ n = p ^ n
Tactic: rw [Nat.card_fun, Nat.card_fin, hG]
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (hypothesis)
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)
⊢ MulEquiv.{u_3, u_4} (↥(↑P : Subgroup (Equiv.Perm α))) (IteratedWreathProduct G n)
have hf : 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)
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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)
hf :
  Function.Injective.{u_4 + 1, u_3 + 1} (α := IteratedWreathProduct G n) (β := Equiv.Perm α)
    (⇑f : (a : IteratedWreathProduct G n) → Equiv.Perm α)
g : MulEquiv.{u_3, u_4} (↥f.range) (IteratedWreathProduct G n) := (MonoidHom.ofInjective hf).symm
⊢ Nat.card.{u_3} ↥f.range = HPow.hPow (β := ℕ) p (((Nat.card.{u_3} (Equiv.Perm α)).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw : Nat.card.{u_4} (IteratedWreathProduct G n) =
  HPow.hPow (β := ℕ) p (((Nat.card.{u_3} (Equiv.Perm α)).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [Nat.card_congr g.toEquiv, IteratedWreathProduct.card, hG, Nat.card_perm, hα,
        ← Nat.multiplicity_eq_factorization hp.out (p ^ n).factorial_ne_zero,
        Nat.Prime.multiplicity_factorial_pow hp.out]