awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
x : ↥H
this : Fintype (Quotient (α := G ⧸ H) (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)))
⊢ Eq.{u_1 + 1} (α := ↥H ⧸ H.focalSubgroupOf)
    (∏ q : Quotient (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)),
      (QuotientGroup.mk' H.focalSubgroupOf : (a : ↥H) → ↥H ⧸ H.focalSubgroupOf)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          ((Quotient.out q.out)⁻¹ * (↑x : G) ^ minimalPeriod (fun (x_1 : G ⧸ H) ↦ (↑x : G) • x_1) q.out *
            Quotient.out q.out)
          ⋯))
    (∏ i : Quotient (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)),
      HPow.hPow (α := ↥H ⧸ H.focalSubgroupOf) (↑x : ↥H ⧸ H.focalSubgroupOf)
        (minimalPeriod (fun (x_1 : G ⧸ H) ↦ (↑x : G) • x_1) i.out))
have apply : ∀ (x_1 : Quotient (α := G ⧸ H) (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H))),
  Membership.mem (γ := Finset (Quotient (α := G ⧸ H) (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)))) Finset.univ
      x_1 →
    (QuotientGroup.mk' H.focalSubgroupOf : (a : ↥H) → ↥H ⧸ H.focalSubgroupOf)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          ((Quotient.out x_1.out)⁻¹ * (↑x : G) ^ minimalPeriod (fun (x_2 : G ⧸ H) ↦ (↑x : G) • x_2) x_1.out *
            Quotient.out x_1.out)
          sorry) =
      HPow.hPow (α := ↥H ⧸ H.focalSubgroupOf) (↑x : ↥H ⧸ H.focalSubgroupOf)
        (minimalPeriod (fun (x_2 : G ⧸ H) ↦ (↑x : G) • x_2) x_1.out)
Tactic: apply Finset.prod_congr rfl
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
x : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf
⊢ ∃ (a : G), ((↑P : Subgroup G).transferFocal : (a : G) → ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) a = x
have obtain : ∀ (x : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf),
  ∃ (a : G),
    Eq (α := ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
      (((↑P : Subgroup G).transferFocal : (a : G) → ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) a :
        ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
      ((fun (y : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) ↦ y ^ (↑P : Subgroup G).index) x :
        ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
Tactic: obtain ⟨x, rfl⟩ := focalSubgroupOf.pow_index_surjective P x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
x : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf
⊢ ∃ (a : G),
    Eq (α := ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
      (((↑P : Subgroup G).transferFocal : (a : G) → ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) a :
        ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
      ((fun (y : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) ↦ y ^ (↑P : Subgroup G).index) x :
        ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
have obtain : ∀ (x : ↥(↑P : Subgroup G)),
  ∃ (a : G),
    Eq (α := ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
      (((↑P : Subgroup G).transferFocal : (a : G) → ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) a :
        ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
      ((fun (y : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) ↦ y ^ (↑P : Subgroup G).index)
          ((QuotientGroup.mk' (↑P : Subgroup G).focalSubgroupOf :
              (a : ↥(↑P : Subgroup G)) → ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
            x) :
        ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
Tactic: obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective _ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
⊢ MonoidHom.ker ((↑P : Subgroup G).transferFocal.restrict P) = (↑P : Subgroup G).focalSubgroupOf
have h : ∀ (g : ↥P),
  Membership.mem (γ := Subgroup ↥P) (MonoidHom.ker ((↑P : Subgroup G).transferFocal.restrict P)) g ↔
    g ∈ (↑P : Subgroup G).focalSubgroupOf
Tactic: ext g
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (hypothesis)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
g : ↥P
⊢ Membership.mem (γ := Subgroup ↥P) (MonoidHom.ker ((↑P : Subgroup G).transferFocal.restrict P)) g ↔
    g ∈ (↑P : Subgroup G).focalSubgroupOf
have hQ : IsPGroup.{u_1} p (↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
Tactic: have hQ : IsPGroup p (P ⧸ P.focalSubgroupOf) := P.2.to_quotient P.focalSubgroupOf
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
g : ↥P
hQ : IsPGroup.{u_1} p (↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
⊢ Membership.mem (γ := Subgroup ↥P) (MonoidHom.ker ((↑P : Subgroup G).transferFocal.restrict P)) g ↔
    g ∈ (↑P : Subgroup G).focalSubgroupOf
have h : HPow.hPow (α := ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
      (↑g : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) (↑P : Subgroup G).index =
    1 ↔
  g ∈ (↑P : Subgroup G).focalSubgroupOf
Tactic: rw [MonoidHom.mem_ker, MonoidHom.restrict_apply, transferFocal_eq_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
⊢ (↑P : Subgroup G).transferFocal.ker ⊓ (↑P : Subgroup G) = (↑P : Subgroup G).focalSubgroup
have rw : map (↑P : Subgroup G).subtype (MonoidHom.ker ((↑P : Subgroup G).transferFocal.restrict (↑P : Subgroup G))) =
  map (↑P : Subgroup G).subtype (↑P : Subgroup G).focalSubgroupOf
Tactic: rw [← subgroupOf_map_subtype, ← MonoidHom.ker_restrict, ← map_focalSubgroupOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
⊢ _root_.commutator G ⊓ (↑P : Subgroup G) = (↑P : Subgroup G).focalSubgroup
have a : _root_.commutator G ⊓ (↑P : Subgroup G) ≤ (↑P : Subgroup G).focalSubgroup
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
a : _root_.commutator G ⊓ (↑P : Subgroup G) ≤ (↑P : Subgroup G).focalSubgroup
⊢ _root_.commutator G ⊓ (↑P : Subgroup G) = (↑P : Subgroup G).focalSubgroup
have a₁ : (↑P : Subgroup G).focalSubgroup ≤ _root_.commutator G ⊓ (↑P : Subgroup G)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
⊢ _root_.commutator G ⊓ (↑P : Subgroup G) ≤ (↑P : Subgroup G).focalSubgroup
have apply : _root_.commutator G ⊓ (↑P : Subgroup G) ≤ (↑P : Subgroup G).transferFocal.ker ⊓ (↑P : Subgroup G)
Tactic: apply le_trans ?_ (ker_transferFocal_inf_eq_focalSubgroup P).le
-- Lean 4 proof step from Mathlib.GroupTheory.Frattini (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
⊢ frattini G ≤ comap φ (frattini H)
have simp_rw : ∀ (i : Subgroup H) (i_1 : Membership.mem (γ := Set (Subgroup H)) {H_1 : Subgroup H | IsCoatom H_1} i),
  ⨅ (a : Subgroup G), ⨅ (_ : Membership.mem (γ := Set (Subgroup G)) {H : Subgroup G | IsCoatom H} a), a ≤ comap φ i
Tactic: simp_rw [frattini, Order.radical, comap_iInf, le_iInf_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Frattini (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM : Membership.mem (γ := Set (Subgroup H)) {H_1 : Subgroup H | IsCoatom H_1} M
⊢ ⨅ (a : Subgroup G), ⨅ (_ : Membership.mem (γ := Set (Subgroup G)) {H : Subgroup G | IsCoatom H} a), a ≤ comap φ M
have hi : Membership.mem (γ := Set (Subgroup G)) {H : Subgroup G | IsCoatom H} (comap φ M)
Tactic: apply biInf_le
-- Lean 4 proof step from Mathlib.GroupTheory.Frattini (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
φ : G →* H
⊢ Characteristic (frattini G)
have rw : ∀ (ϕ : G ≃* G), comap ϕ.toMonoidHom (frattini G) = frattini G
Tactic: rw [characteristic_iff_comap_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Frattini (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
⊢ Group.IsNilpotent.{u_1} ↥(frattini G)
have q : Group.IsNilpotent.{u_1} ↥(frattini G) ↔
  ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p ↥(frattini G)), (↑P : Subgroup ↥(frattini G)).Normal
Tactic: have q := (Group.isNilpotent_of_finite_tfae (G := frattini G)).out 0 3
-- Lean 4 proof step from Mathlib.GroupTheory.Frattini (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
q :
  Group.IsNilpotent.{u_1} ↥(frattini G) ↔
    ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p ↥(frattini G)), (↑P : Subgroup ↥(frattini G)).Normal
⊢ Group.IsNilpotent.{u_1} ↥(frattini G)
have rw : ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p ↥(frattini G)), (↑P : Subgroup ↥(frattini G)).Normal
Tactic: rw [q]
-- Lean 4 proof step from Mathlib.GroupTheory.Frattini (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
⊢ (↑P : Subgroup ↥(frattini G)).Normal
have frattini_argument : Eq (α := Subgroup G)
  (normalizer (↑(map (Subgroup.subtype (frattini G)) (↑P : Subgroup ↥(frattini G))) : Set G) ⊔ frattini G) ⊤
Tactic: have frattini_argument := Sylow.normalizer_sup_eq_top P
-- Lean 4 proof step from Mathlib.GroupTheory.Frattini (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
frattini_argument :
  Eq (α := Subgroup G)
    (normalizer (↑(map (Subgroup.subtype (frattini G)) (↑P : Subgroup ↥(frattini G))) : Set G) ⊔ frattini G) ⊤
⊢ (↑P : Subgroup ↥(frattini G)).Normal
have normalizer_P : Eq (α := Subgroup G) (normalizer (↑(map (Subgroup.subtype (frattini G)) (↑P : Subgroup ↥(frattini G))) : Set G)) ⊤
Tactic: have normalizer_P := frattini_nongenerating frattini_argument
-- Lean 4 proof step from Mathlib.GroupTheory.Frattini (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
frattini_argument :
  Eq (α := Subgroup G)
    (normalizer (↑(map (Subgroup.subtype (frattini G)) (↑P : Subgroup ↥(frattini G))) : Set G) ⊔ frattini G) ⊤
normalizer_P :
  Eq (α := Subgroup G) (normalizer (↑(map (Subgroup.subtype (frattini G)) (↑P : Subgroup ↥(frattini G))) : Set G)) ⊤
⊢ (↑P : Subgroup ↥(frattini G)).Normal
have P_normal_in_G : (map (Subgroup.subtype (frattini G)) (↑P : Subgroup ↥(frattini G))).Normal
Tactic: have P_normal_in_G : (map (frattini G).subtype P).Normal := normalizer_eq_top_iff.mp normalizer_P
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
f : α → β
x : α
⊢ (((lift : (a : α → β) → FreeAbelianGroup α →+ β) f : AddMonoidHom.{u, v} (FreeAbelianGroup α) β) :
        (a : FreeAbelianGroup α) → β)
      (of x) =
    f x
have h : β = Multiplicative β →
  f x =
    (((FreeGroup.lift : (a : α → Multiplicative β) → FreeGroup α →* Multiplicative β) f :
          MonoidHom.{u, v} (FreeGroup α) (Multiplicative β)) :
        (a : FreeGroup α) → Multiplicative β)
      (FreeGroup.of x)
Tactic: convert! Abelianization.lift_apply_of (FreeGroup.lift f (β := Multiplicative β)) (FreeGroup.of x)
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : AddCommGroup β
inst_1 : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) ((⇑g : (a : β) → γ) ∘ f) :
            AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        a :
      γ)
    ((g : (a : β) → γ)
        ((((lift : (a : α → β) → FreeAbelianGroup α →+ β) f : AddMonoidHom.{u_2, u_3} (FreeAbelianGroup α) β) :
              (a : FreeAbelianGroup α) → β)
            a :
          β) :
      γ)
have rw : Eq.{u_4 + 1} (α := γ)
  ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) ((⇑g : (a : β) → γ) ∘ f) :
          AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
        (a : FreeAbelianGroup α) → γ)
      a :
    γ)
  ((g.comp ((lift : (a : α → β) → FreeAbelianGroup α →+ β) f) : (a : FreeAbelianGroup α) → γ) a : γ)
Tactic: rw [← AddMonoidHom.comp_apply g (lift f)]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : AddCommGroup β
inst_1 : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) ((⇑g : (a : β) → γ) ∘ f) :
            AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        a :
      γ)
    ((g.comp ((lift : (a : α → β) → FreeAbelianGroup α →+ β) f) : (a : FreeAbelianGroup α) → γ) a : γ)
have refine : ∀ (x : α),
  Eq.{u_4 + 1} (α := γ)
    ((g.comp ((lift : (a : α → β) → FreeAbelianGroup α →+ β) f) : (a : FreeAbelianGroup α) → γ) (of x) : γ)
    (((⇑g : (a : β) → γ) ∘ f) x : γ)
Tactic: refine (lift_unique _ _ ?_).symm
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : AddCommGroup β
inst_1 : AddCommGroup γ
a_1 : FreeAbelianGroup α
f : α → β
g : β →+ γ
a : α
⊢ Eq.{u_4 + 1} (α := γ)
    ((g.comp ((lift : (a : α → β) → FreeAbelianGroup α →+ β) f) : (a : FreeAbelianGroup α) → γ) (of a) : γ)
    (((⇑g : (a : β) → γ) ∘ f) a : γ)
have change : Eq.{u_4 + 1} (α := γ)
  ((g : (a : β) → γ)
      ((((lift : (a : α → β) → FreeAbelianGroup α →+ β) f : AddMonoidHom.{u_2, u_3} (FreeAbelianGroup α) β) :
            (a : FreeAbelianGroup α) → β)
          (of a) :
        β) :
    γ)
  ((g : (a : β) → γ) (f a) : γ)
Tactic: change g ((lift f) (of a)) = g (f a)
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (hypothesis)
Goal:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := (lift : (a : α → ℤ) → FreeAbelianGroup α →+ ℤ) 1
⊢ False
have hfx : Eq (α := ℤ) ((f : (a : FreeAbelianGroup α) → ℤ) (of x) : ℤ) (1 : ℤ)
Tactic: have hfx : f (of x) = 1 := lift_apply_of _ _
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := (lift : (a : α → ℤ) → FreeAbelianGroup α →+ ℤ) 1
hfx : Eq (α := ℤ) ((f : (a : FreeAbelianGroup α) → ℤ) (of x) : ℤ) (1 : ℤ)
⊢ Eq (α := ℤ) ((f : (a : FreeAbelianGroup α) → ℤ) (of x) : ℤ) (0 : ℤ)
have rw : Eq (α := ℤ) ((f : (a : FreeAbelianGroup α) → ℤ) 0 : ℤ) (0 : ℤ)
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := (lift : (a : α → ℤ) → FreeAbelianGroup α →+ ℤ) 1
hfx : Eq (α := ℤ) ((f : (a : FreeAbelianGroup α) → ℤ) (of x) : ℤ) (1 : ℤ)
rw : Eq (α := ℤ) ((f : (a : FreeAbelianGroup α) → ℤ) 0 : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((f : (a : FreeAbelianGroup α) → ℤ) (of x) : ℤ) (0 : ℤ)
have rw₁ : Eq (α := ℤ) 0 0
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (hypothesis)
Goal:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := (lift : (a : α → ℤ) → FreeAbelianGroup α →+ ℤ) 1
hfx : Eq (α := ℤ) ((f : (a : FreeAbelianGroup α) → ℤ) (of x) : ℤ) (1 : ℤ)
⊢ False
have hf0 : Eq (α := ℤ) ((f : (a : FreeAbelianGroup α) → ℤ) (of x) : ℤ) (0 : ℤ)
Tactic: have hf0 : f (of x) = 0 := by rw [h, map_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
inst : AddCommGroup G
f g : α → G
a : FreeAbelianGroup α
⊢ (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
        (a : FreeAbelianGroup α) → G)
      a =
    HAdd.hAdd (α := G) (β := G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          a :
        G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          a :
        G)
have zero : (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
      (a : FreeAbelianGroup α) → G)
    0 =
  HAdd.hAdd (α := G) (β := G)
    ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
          (a : FreeAbelianGroup α) → G)
        0 :
      G)
    ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
          (a : FreeAbelianGroup α) → G)
        0 :
      G)
Tactic: induction a using FreeAbelianGroup.induction_on with
  | zero => simp only [(lift _).map_zero, zero_add]
  | of x => simp only [lift_apply_of, Pi.add_apply]
  | neg x => simp only [map_neg, lift_apply_of, Pi.add_apply, neg_add]
  | add x y hx hy => simp only [(lift _).map_add, hx, hy, add_add_add_comm]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
inst : AddCommGroup G
f g : α → G
a : FreeAbelianGroup α
zero :
  (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
        (a : FreeAbelianGroup α) → G)
      0 =
    HAdd.hAdd (α := G) (β := G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          0 :
        G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          0 :
        G)
⊢ (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
        (a : FreeAbelianGroup α) → G)
      a =
    HAdd.hAdd (α := G) (β := G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          a :
        G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          a :
        G)
have of : ∀ (x : α),
  (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
        (a : FreeAbelianGroup α) → G)
      (of x) =
    HAdd.hAdd (α := G) (β := G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          (of x) :
        G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          (of x) :
        G)
Tactic: induction a using FreeAbelianGroup.induction_on with
  | zero => simp only [(lift _).map_zero, zero_add]
  | of x => simp only [lift_apply_of, Pi.add_apply]
  | neg x => simp only [map_neg, lift_apply_of, Pi.add_apply, neg_add]
  | add x y hx hy => simp only [(lift _).map_add, hx, hy, add_add_add_comm]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type u
f : FreeAbelianGroup (α → β)
⊢ FreeAbelianGroup α →+ FreeAbelianGroup β
have refine : ∀ (x y : FreeAbelianGroup α),
  (fun (x : FreeAbelianGroup α) ↦ f <*> x) (x + y) =
    HAdd.hAdd (α := FreeAbelianGroup β) ((fun (x : FreeAbelianGroup α) ↦ f <*> x) x)
      ((fun (x : FreeAbelianGroup α) ↦ f <*> x) y)
Tactic: refine .mk' (f <*> ·) fun x y ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type u
f : FreeAbelianGroup (α → β)
x y : FreeAbelianGroup α
⊢ (fun (x : FreeAbelianGroup α) ↦ f <*> x) (x + y) =
    HAdd.hAdd (α := FreeAbelianGroup β) ((fun (x : FreeAbelianGroup α) ↦ f <*> x) x)
      ((fun (x : FreeAbelianGroup α) ↦ f <*> x) y)
have change : ((lift : (a : (α → β) → FreeAbelianGroup β) → FreeAbelianGroup (α → β) →+ FreeAbelianGroup β) fun (x_1 : α → β) ↦
        x_1 <$> (x + y) :
      (a : FreeAbelianGroup (α → β)) → FreeAbelianGroup β)
    f =
  HAdd.hAdd (α := FreeAbelianGroup β) (β := FreeAbelianGroup β)
    (((lift : (a : (α → β) → FreeAbelianGroup β) → FreeAbelianGroup (α → β) →+ FreeAbelianGroup β) fun (x_1 : α → β) ↦
            x_1 <$> x :
          (a : FreeAbelianGroup (α → β)) → FreeAbelianGroup β)
        f :
      FreeAbelianGroup β)
    (((lift : (a : (α → β) → FreeAbelianGroup β) → FreeAbelianGroup (α → β) →+ FreeAbelianGroup β) fun (x : α → β) ↦
            x <$> y :
          (a : FreeAbelianGroup (α → β)) → FreeAbelianGroup β)
        f :
      FreeAbelianGroup β)
Tactic: change lift (· <$> (x + y)) _ = lift (· <$> x) _ + lift (· <$> y) _
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 : Type u
x_1 : FreeAbelianGroup α_1
x : α_1
ih : Eq (α := FreeAbelianGroup α_1) (id <$> pure x) (pure x)
⊢ Eq (α := FreeAbelianGroup α_1) (id <$> (-pure x)) (-pure x)
have rw : Eq (α := FreeAbelianGroup α_1) (-id <$> pure x) (-pure x)
Tactic: rw [FreeAbelianGroup.map_neg, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 : Type u
x_1 : FreeAbelianGroup α_1
x : α_1
ih : Eq (α := FreeAbelianGroup α_1) (id <$> pure x) (pure x)
rw : Eq (α := FreeAbelianGroup α_1) (-id <$> pure x) (-pure x)
⊢ Eq (α := FreeAbelianGroup α_1) (id <$> (-pure x)) (-pure x)
have rw₁ : Eq (α := FreeAbelianGroup α_1) (-pure x) (-pure x)
Tactic: rw [FreeAbelianGroup.map_neg, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 : Type u
x_1 x y : FreeAbelianGroup α_1
ihx : id <$> x = x
ihy : id <$> y = y
⊢ id <$> (x + y) = x + y
have rw : id <$> x + id <$> y = x + y
Tactic: rw [FreeAbelianGroup.map_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 : Type u
x_1 x y : FreeAbelianGroup α_1
ihx : id <$> x = x
ihy : id <$> y = y
rw : id <$> x + id <$> y = x + y
⊢ id <$> (x + y) = x + y
have rw₁ : x + id <$> y = x + y
Tactic: rw [FreeAbelianGroup.map_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 : Type u
x_1 x y : FreeAbelianGroup α_1
ihx : id <$> x = x
ihy : id <$> y = y
rw : id <$> x + id <$> y = x + y
rw₁ : x + id <$> y = x + y
⊢ id <$> (x + y) = x + y
have rw₂ : x + y = x + y
Tactic: rw [FreeAbelianGroup.map_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
⊢ Eq.{u + 1} (α := FreeAbelianGroup γ) 0 (0 >>= fun (x : α_1) ↦ f x >>= g)
have rw : Eq.{u + 1} (α := FreeAbelianGroup γ) 0 0
Tactic: rw [zero_bind]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
⊢ 0 >>= f >>= g = 0 >>= fun (x : α_1) ↦ f x >>= g
have iterate : 0 >>= g = 0 >>= fun (x : α_1) ↦ f x >>= g
Tactic: iterate 3 rw [zero_bind]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
⊢ pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
have rw : f x >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
Tactic: rw [pure_bind]