awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Finset G
hS1 : S.card = rank G
hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤
⊢ rank H ≤ rank G
have trans : rank H ≤ Finset.card.{u_2} (α := H) (Finset.image (⇑f : (a : G) → H) S)
Tactic: trans (S.image f).card
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Finset G
hS1 : S.card = rank G
hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤
trans : rank H ≤ Finset.card.{u_2} (α := H) (Finset.image (⇑f : (a : G) → H) S)
⊢ rank H ≤ rank G
have trans₁ : Finset.card.{u_2} (α := H) (Finset.image (⇑f : (a : G) → H) S) ≤ rank G
Tactic: trans (S.image f).card
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Finset G
hS1 : S.card = rank G
hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤
⊢ rank H ≤ Finset.card.{u_2} (α := H) (Finset.image (⇑f : (a : G) → H) S)
have hS : Eq (α := Subgroup H) (Subgroup.closure (↑(Finset.image (⇑f : (a : G) → H) S) : Set H)) ⊤
Tactic: apply rank_le
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Finset G
hS1 : S.card = rank G
hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤
⊢ Eq (α := Subgroup H) (Subgroup.closure (↑(Finset.image (⇑f : (a : G) → H) S) : Set H)) ⊤
have hS : Eq.{u_2 + 1} (α := Subgroup H) (Subgroup.closure ((⇑f : (a : G) → H) '' (↑S : Set G))) ⊤
Tactic: rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Finset G
hS1 : S.card = rank G
hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤
hS : Eq.{u_2 + 1} (α := Subgroup H) (Subgroup.closure ((⇑f : (a : G) → H) '' (↑S : Set G))) ⊤
⊢ Eq (α := Subgroup H) (Subgroup.closure (↑(Finset.image (⇑f : (a : G) → H) S) : Set H)) ⊤
have hS₁ : Subgroup.map f (Subgroup.closure (↑S : Set G)) = ⊤
Tactic: rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Finset G
hS1 : S.card = rank G
hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤
hS : Eq.{u_2 + 1} (α := Subgroup H) (Subgroup.closure ((⇑f : (a : G) → H) '' (↑S : Set G))) ⊤
hS₁ : Subgroup.map f (Subgroup.closure (↑S : Set G)) = ⊤
⊢ Eq (α := Subgroup H) (Subgroup.closure (↑(Finset.image (⇑f : (a : G) → H) S) : Set H)) ⊤
have hS₂ : Subgroup.map f ⊤ = ⊤
Tactic: rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Finset G
hS1 : S.card = rank G
hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤
hS : Eq.{u_2 + 1} (α := Subgroup H) (Subgroup.closure ((⇑f : (a : G) → H) '' (↑S : Set G))) ⊤
hS₁ : Subgroup.map f (Subgroup.closure (↑S : Set G)) = ⊤
hS₂ : Subgroup.map f ⊤ = ⊤
⊢ Eq (α := Subgroup H) (Subgroup.closure (↑(Finset.image (⇑f : (a : G) → H) S) : Set H)) ⊤
have hS₃ : Eq.{u_2 + 1} (α := Subgroup H) ⊤ ⊤
Tactic: rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
⊢ rank H ≤ rank G
have obtain : ∀ (S : Finset G) (hS1 : S.card = rank G) (hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤), rank H ≤ rank G
Tactic: classical
  obtain ⟨S, hS1, hS2⟩ := rank_spec G
  trans (S.image f).card
  · apply rank_le
    rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
  · exact Finset.card_image_le.trans_eq hS1
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
obtain :
  ∀ (S : Finset G) (hS1 : S.card = rank G) (hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤),
    rank H ≤ rank G
⊢ rank H ≤ rank G
have obtain₁ : ∀ (S : Finset G) (hS1 : S.card = rank G) (hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤),
  rank H ≤ Finset.card.{u_2} (α := H) (Finset.image (⇑f : (a : G) → H) S)
Tactic: classical
  obtain ⟨S, hS1, hS2⟩ := rank_spec G
  trans (S.image f).card
  · apply rank_le
    rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
  · exact Finset.card_image_le.trans_eq hS1
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
obtain :
  ∀ (S : Finset G) (hS1 : S.card = rank G) (hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤),
    rank H ≤ rank G
obtain₁ :
  ∀ (S : Finset G) (hS1 : S.card = rank G) (hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤),
    rank H ≤ Finset.card.{u_2} (α := H) (Finset.image (⇑f : (a : G) → H) S)
⊢ rank H ≤ rank G
have obtain₂ : ∀ (S : Finset G) (hS1 : S.card = rank G) (hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤),
  Finset.card.{u_2} (α := H) (Finset.image (⇑f : (a : G) → H) S) ≤ rank G
Tactic: classical
  obtain ⟨S, hS1, hS2⟩ := rank_spec G
  trans (S.image f).card
  · apply rank_le
    rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
  · exact Finset.card_image_le.trans_eq hS1
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : Group.FG.{u_1} ↥H
inst_2 : Group.FG.{u_1} ↥K
h : H = K
⊢ rank.{u_1} ↥H = rank.{u_1} ↥K
have subst : ∀ [inst_3 : Group.FG.{u_1} ↥H], rank.{u_1} ↥H = rank.{u_1} ↥H
Tactic: subst h
Cleared hypotheses: K, inst_2, h
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
inst : Group G
s : Finset G
t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯
⊢ Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤
have rw : Eq (α := Subgroup ↥(closure (↑s : Set G)))
  (closure
    (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x) ⁻¹' (↑s : Set G)))
  ⊤
Tactic: rw [Finset.coe_preimage]
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (hypothesis)
Goal:
G : Type u_1
inst : Group G
s : Finset G
t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯
⊢ rank.{u_1} ↥(closure (↑s : Set G)) ≤ s.card
have ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤
Tactic: have ht : closure (t : Set (closure (s : Set G))) = ⊤ := by
    rw [Finset.coe_preimage]
    exact closure_preimage_eq_top (s : Set G)
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
inst : Group G
s : Finset G
t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯
ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤
⊢ rank.{u_1} ↥(closure (↑s : Set G)) ≤ s.card
have apply : t.card ≤ s.card
Tactic: apply (rank_le ht).trans
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
inst : Group G
s : Finset G
t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯
ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤
H :
  Set.InjOn (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x))
    (↑t : Set ↥(closure (↑s : Set G)))
⊢ t.card ≤ s.card
have rw : {x ∈ s |
      Membership.mem (γ := Set G)
        (Set.range (ι := ↥(closure (↑s : Set G)))
          (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)))
        x}.card ≤
  s.card
Tactic: rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
inst : Group G
s : Finset G
t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯
ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤
⊢ t.card ≤ s.card
have suffices : Set.InjOn (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x))
  (↑t : Set ↥(closure (↑s : Set G)))
Tactic: suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G))) by
    rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
    apply Finset.card_filter_le
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
inst : Group G
s : Finset G
let let₁ let₂ : rank.{u_1} ↥(closure (↑s : Set G)) ≤ s.card
⊢ rank.{u_1} ↥(closure (↑s : Set G)) ≤ s.card
have let₃ : let t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) sorry;
∀ (ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤),
  rank.{u_1} ↥(closure (↑s : Set G)) ≤ s.card
Tactic: classical
  let t : Finset (closure (s : Set G)) := s.preimage Subtype.val Subtype.coe_injective.injOn
  have ht : closure (t : Set (closure (s : Set G))) = ⊤ := by
    rw [Finset.coe_preimage]
    exact closure_preimage_eq_top (s : Set G)
  apply (rank_le ht).trans
  suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G))) by
    rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
    apply Finset.card_filter_le
  apply Subtype.coe_injective.injOn
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
inst : Group G
s : Finset G
let let₁ let₂ : rank.{u_1} ↥(closure (↑s : Set G)) ≤ s.card
let₃ :
  let t : Finset ↥(closure (↑s : Set G)) :=
    s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯;
  ∀ (ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤),
    rank.{u_1} ↥(closure (↑s : Set G)) ≤ s.card
⊢ rank.{u_1} ↥(closure (↑s : Set G)) ≤ s.card
have let₄ : let t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) sorry;
∀ (ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤), t.card ≤ s.card
Tactic: classical
  let t : Finset (closure (s : Set G)) := s.preimage Subtype.val Subtype.coe_injective.injOn
  have ht : closure (t : Set (closure (s : Set G))) = ⊤ := by
    rw [Finset.coe_preimage]
    exact closure_preimage_eq_top (s : Set G)
  apply (rank_le ht).trans
  suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G))) by
    rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
    apply Finset.card_filter_le
  apply Subtype.coe_injective.injOn
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
inst : Group G
s : Finset G
let let₁ let₂ : rank.{u_1} ↥(closure (↑s : Set G)) ≤ s.card
let₃ :
  let t : Finset ↥(closure (↑s : Set G)) :=
    s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯;
  ∀ (ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤),
    rank.{u_1} ↥(closure (↑s : Set G)) ≤ s.card
let₄ :
  let t : Finset ↥(closure (↑s : Set G)) :=
    s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯;
  ∀ (ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤), t.card ≤ s.card
⊢ rank.{u_1} ↥(closure (↑s : Set G)) ≤ s.card
have let₅ : let t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) sorry;
∀ (ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤),
  Set.InjOn (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x))
    (↑t : Set ↥(closure (↑s : Set G)))
Tactic: classical
  let t : Finset (closure (s : Set G)) := s.preimage Subtype.val Subtype.coe_injective.injOn
  have ht : closure (t : Set (closure (s : Set G))) = ⊤ := by
    rw [Finset.coe_preimage]
    exact closure_preimage_eq_top (s : Set G)
  apply (rank_le ht).trans
  suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G))) by
    rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
    apply Finset.card_filter_le
  apply Subtype.coe_injective.injOn
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ rank.{u_1} ↥(closure s) ≤ Nat.card.{u_1} (↑s : Type u_1)
have haveI : ∀ (this : Fintype (↑s : Type u_1)), rank.{u_1} ↥(closure s) ≤ Nat.card.{u_1} (↑s : Type u_1)
Tactic: haveI := Fintype.ofFinite s
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
this : Fintype (↑s : Type u_1)
⊢ rank.{u_1} ↥(closure s) ≤ Nat.card.{u_1} (↑s : Type u_1)
have rw : rank.{u_1} ↥(closure (↑s.toFinset : Set G)) ≤ s.toFinset.card
Tactic: rw [Nat.card_eq_fintype_card, ← s.toFinset_card, ← rank_congr (congr_arg _ s.coe_toFinset)]
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
inst : Group G
g : G
⊢ Nat.card.{u_1} ↥(centralizer {g}) = Nat.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
have rw : Nat.card.{u_1} ↥(comap (MulEquiv.toMonoidHom ConjAct.toConjAct) (MulAction.stabilizer (ConjAct G) g)) =
  Nat.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
Tactic: rw [centralizer_eq_comap_stabilizer]
-- 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
a b c : D ≀ᵣ Q
⊢ a * b * c = a * (b * c)
have left : ∀ (x : Q), (a * b * c).left x = (a * (b * c)).left x
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
a b c : D ≀ᵣ Q
left : ∀ (x : Q), (a * b * c).left x = (a * (b * c)).left x
⊢ a * b * c = a * (b * c)
have right : (a * b * c).right = (a * (b * c)).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
a : D ≀ᵣ Q
⊢ 1 * a = a
have left : ∀ (x : Q), (1 * a).left x = a.left x
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
a : D ≀ᵣ Q
left : ∀ (x : Q), (1 * a).left x = a.left x
⊢ 1 * a = a
have right : (1 * a).right = a.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
a : D ≀ᵣ Q
⊢ a * 1 = a
have left : ∀ (x : Q), (a * 1).left x = a.left x
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
a : D ≀ᵣ Q
left : ∀ (x : Q), (a * 1).left x = a.left x
⊢ a * 1 = a
have right : (a * 1).right = a.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
a : D ≀ᵣ Q
⊢ a⁻¹ * a = 1
have left : ∀ (x : Q), (a⁻¹ * a).left x = left 1 x
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
a : D ≀ᵣ Q
left : ∀ (x : Q), (a⁻¹ * a).left x = RegularWreathProduct.left 1 x
⊢ a⁻¹ * a = 1
have right : (a⁻¹ * a).right = right.{u_1, u_2} (D := D) 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
x x_1 : Q
⊢ { left := 1, right := x * x_1 } =
    HMul.hMul (α := D ≀ᵣ Q) { left := 1, right := x : D ≀ᵣ Q } { left := 1, right := x_1 : D ≀ᵣ Q }
have left : ∀ (x_2 : Q),
  left { left := 1, right := x * x_1 } x_2 =
    (HMul.hMul (α := D ≀ᵣ Q) { left := 1, right := x : D ≀ᵣ Q } { left := 1, right := x_1 : D ≀ᵣ Q }).left x_2
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
x x_1 : Q
left :
  ∀ (x_2 : Q),
    RegularWreathProduct.left { left := 1, right := x * x_1 } x_2 =
      (HMul.hMul (α := D ≀ᵣ Q) { left := 1, right := x : D ≀ᵣ Q } { left := 1, right := x_1 : D ≀ᵣ Q }).left x_2
⊢ { left := 1, right := x * x_1 } =
    HMul.hMul (α := D ≀ᵣ Q) { left := 1, right := x : D ≀ᵣ Q } { left := 1, right := x_1 : D ≀ᵣ Q }
have right : right.{u_1, u_2} (D := D) { left := 1, right := x * x_1 : D ≀ᵣ Q } =
  (HMul.hMul (α := D ≀ᵣ Q) { left := 1, right := x : D ≀ᵣ Q } { left := 1, right := x_1 : 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
⊢ Eq (α := Q →* Q) (MonoidHom.comp (N := D ≀ᵣ Q) rightHom inl) (MonoidHom.id Q)
have h : ∀ (x : Q),
  Eq (α := Q) ((MonoidHom.comp (N := D ≀ᵣ Q) rightHom inl : (a : Q) → Q) x : Q) ((MonoidHom.id Q : (a : Q) → Q) x : Q)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
Goal:
D : Type u_1
Q : Type u_2
inst : Finite Q
⊢ Nat.card (D ≀ᵣ Q) = Nat.card D ^ Nat.card Q * Nat.card Q
have rw : Nat.card ((Q → D) × Q) = Nat.card D ^ Nat.card Q * Nat.card Q
Tactic: rw [Nat.card_congr (equivProd D Q), Nat.card_prod (Q → D) Q, Nat.card_fun]
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
Goal:
D : Type u_1
Q : Type u_2
inst : Finite Q
rw : Nat.card ((Q → D) × Q) = Nat.card D ^ Nat.card Q * Nat.card Q
⊢ Nat.card (D ≀ᵣ Q) = Nat.card D ^ Nat.card Q * Nat.card Q
have rw₁ : Nat.card (Q → D) * Nat.card Q = Nat.card D ^ Nat.card Q * Nat.card Q
Tactic: rw [Nat.card_congr (equivProd D Q), Nat.card_prod (Q → D) Q, Nat.card_fun]
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
Goal:
D : Type u_1
Q : Type u_2
inst : Finite Q
rw : Nat.card ((Q → D) × Q) = Nat.card D ^ Nat.card Q * Nat.card Q
rw₁ : Nat.card (Q → D) * Nat.card Q = Nat.card D ^ Nat.card Q * Nat.card Q
⊢ Nat.card (D ≀ᵣ Q) = Nat.card D ^ Nat.card Q * Nat.card Q
have rw₂ : Nat.card D ^ Nat.card Q * Nat.card Q = Nat.card D ^ Nat.card Q * Nat.card Q
Tactic: rw [Nat.card_congr (equivProd D Q), Nat.card_prod (Q → D) Q, Nat.card_fun]
-- 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₁
⊢ (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
have left : ∀ (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: 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 : D₁ ≀ᵣ Q₁
left :
  ∀ (x_1 : Q₁),
    RegularWreathProduct.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
⊢ (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
have right : 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: 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 : 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₂))
      ((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 left : ∀ (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: ext