awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Frattini
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)) ⊤
⊢ (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
-- Module: Mathlib.GroupTheory.Frattini
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_normal_in_G : (map (Subgroup.subtype (frattini G)) (↑P : Subgroup ↥(frattini G))).Normal
⊢ (↑P : Subgroup ↥(frattini G)).Normal

Tactic:
P_normal_in_G.of_map_subtype

Premises used: Subgroup.Normal.of_map_subtype
-- Module: Mathlib.GroupTheory.Frattini
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_normal_in_G : (map (Subgroup.subtype (frattini G)) (↑P : Subgroup ↥(frattini G))).Normal
⊢ (↑P : Subgroup ↥(frattini G)).Normal

Tactic:
exact P_normal_in_G.of_map_subtype

Premises used: Subgroup.Normal.of_map_subtype
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
f : α → β
x : α
⊢ Eq.{v + 1} (α := Multiplicative β)
    ((((Abelianization.lift : (a : FreeGroup α →* Multiplicative β) → Abelianization (FreeGroup α) →* Multiplicative β)
              ((FreeGroup.lift : (a : α → Multiplicative β) → FreeGroup α →* Multiplicative β) f) :
            MonoidHom.{u, v} (Abelianization (FreeGroup α)) (Multiplicative β)) :
          (a : Abelianization (FreeGroup α)) → Multiplicative β)
        ((Abelianization.of : (a : FreeGroup α) → Abelianization (FreeGroup α)) (FreeGroup.of x)) :
      Multiplicative β)
    ((((FreeGroup.lift : (a : α → Multiplicative β) → FreeGroup α →* Multiplicative β) f :
            MonoidHom.{u, v} (FreeGroup α) (Multiplicative β)) :
          (a : FreeGroup α) → Multiplicative β)
        (FreeGroup.of x) :
      Multiplicative β)

Tactic:
Abelianization.lift_apply_of (FreeGroup.lift f (β := Multiplicative β)) (FreeGroup.of x)

Premises used: FreeGroup.of, Abelianization.lift_apply_of, FreeGroup.lift, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
f : α → β
x : α
h :
  β = Multiplicative β →
    f x =
      (((FreeGroup.lift : (a : α → Multiplicative β) → FreeGroup α →* Multiplicative β) f :
            MonoidHom.{u, v} (FreeGroup α) (Multiplicative β)) :
          (a : FreeGroup α) → Multiplicative β)
        (FreeGroup.of x)
⊢ (((lift : (a : α → β) → FreeAbelianGroup α →+ β) f : AddMonoidHom.{u, v} (FreeAbelianGroup α) β) :
        (a : FreeAbelianGroup α) → β)
      (of x) =
    f x

Tactic:
convert! Abelianization.lift_apply_of (FreeGroup.lift f (β := Multiplicative β)) (FreeGroup.of x)

Premises used: FreeGroup.of, Abelianization.lift_apply_of, FreeGroup.lift, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
f : α → β
x : α
e_1 : β = Multiplicative β
⊢ f x =
    (((FreeGroup.lift : (a : α → Multiplicative β) → FreeGroup α →* Multiplicative β) f :
          MonoidHom.{u, v} (FreeGroup α) (Multiplicative β)) :
        (a : FreeGroup α) → Multiplicative β)
      (FreeGroup.of x)

Tactic:
(FreeGroup.lift_apply_of (β := Multiplicative β)).symm

Premises used: FreeGroup.lift_apply_of, Multiplicative, Eq.symm
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
f : α → β
x : α
e_1 : β = Multiplicative β
⊢ f x =
    (((FreeGroup.lift : (a : α → Multiplicative β) → FreeGroup α →* Multiplicative β) f :
          MonoidHom.{u, v} (FreeGroup α) (Multiplicative β)) :
        (a : FreeGroup α) → Multiplicative β)
      (FreeGroup.of x)

Tactic:
exact (FreeGroup.lift_apply_of (β := Multiplicative β)).symm

Premises used: FreeGroup.lift_apply_of, Eq.symm
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
f : α → β
g : AddMonoidHom.{u, v} (FreeAbelianGroup α) β
hg : ∀ (x : α), (g : (a : FreeAbelianGroup α) → β) (of x) = f x
x : FreeAbelianGroup α
⊢ Eq.{v + 1} (α := β) ((g : (a : FreeAbelianGroup α) → β) x : β)
    ((((lift : (a : α → β) → FreeAbelianGroup α →+ β) f : AddMonoidHom.{u, v} (FreeAbelianGroup α) β) :
          (a : FreeAbelianGroup α) → β)
        x :
      β)

Tactic:
DFunLike.congr_fun (lift.symm_apply_eq.mp (funext hg : g ∘ of = f)) _

Premises used: DFunLike.congr_fun, Equiv.symm_apply_eq, funext, FreeAbelianGroup.lift, Iff.mp
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
g h : AddMonoidHom.{u, v} (FreeAbelianGroup α) β
H :
  ∀ (x : α),
    Eq.{v + 1} (α := β) ((g : (a : FreeAbelianGroup α) → β) (of x) : β) ((h : (a : FreeAbelianGroup α) → β) (of x) : β)
⊢ g = h

Tactic:
lift.symm.injective <| funext H

Premises used: funext, FreeAbelianGroup.lift, Equiv.injective, Equiv.symm
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : AddCommGroup β
inst_1 : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
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 : γ)
⊢ 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 :
          β) :
      γ)

Tactic:
rw [← AddMonoidHom.comp_apply g (lift f)]

Premises used: FreeAbelianGroup.lift, AddMonoidHom.comp_apply, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
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 : γ)

Tactic:
(lift_unique _ _ ?_).symm

Premises used: FreeAbelianGroup.lift_unique, Eq.symm
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : AddCommGroup β
inst_1 : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
refine :
  ∀ (x : α),
    Eq.{u_4 + 1} (α := γ)
      ((g.comp ((lift : (a : α → β) → FreeAbelianGroup α →+ β) f) : (a : FreeAbelianGroup α) → γ) (of x) : γ)
      (((⇑g : (a : β) → γ) ∘ f) x : γ)
⊢ 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:
refine (lift_unique _ _ ?_).symm

Premises used: FreeAbelianGroup.lift_unique, Eq.symm
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : AddCommGroup β
inst_1 : AddCommGroup γ
a_1 : FreeAbelianGroup α
f : α → β
g : β →+ γ
a : α
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) : γ)
⊢ Eq.{u_4 + 1} (α := γ)
    ((g.comp ((lift : (a : α → β) → FreeAbelianGroup α →+ β) f) : (a : FreeAbelianGroup α) → γ) (of a) : γ)
    (((⇑g : (a : β) → γ) ∘ f) a : γ)

Tactic:
change g ((lift f) (of a)) = g (f a)

Premises used: FreeAbelianGroup.lift, FreeAbelianGroup.of, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
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 : (a : β) → γ)
        ((((lift : (a : α → β) → FreeAbelianGroup α →+ β) f : AddMonoidHom.{u_2, u_3} (FreeAbelianGroup α) β) :
              (a : FreeAbelianGroup α) → β)
            (of a) :
          β) :
      γ)
    ((g : (a : β) → γ) (f a) : γ)

Tactic:
simp only [lift_apply_of]

Premises used: FreeAbelianGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
⊢ Function.Injective.{u + 1, u + 1} (α := α) of

Tactic:
fun x y hoxy ↦ Classical.by_contradiction fun hxy : x ≠ y ↦
    let f : FreeAbelianGroup α →+ ℤ := lift fun z ↦ if x = z then (1 : ℤ) else 0
    have hfx1 : f (of x) = 1 := (lift_apply_of _ _).trans <| if_pos rfl
    have hfy1 : f (of y) = 1 := hoxy ▸ hfx1
    have hfy0 : f (of y) = 0 := (lift_apply_of _ _).trans <| if_neg hxy
    one_ne_zero <| hfy1.symm.trans hfy0

Premises used: Classical.by_contradiction, Eq.rec, if_pos, FreeAbelianGroup.lift, Function.Injective, FreeAbelianGroup.lift_apply_of, one_ne_zero, OfNat.ofNat, Eq.symm, Eq, if_neg, DFunLike.coe, rfl, Eq.trans, ite
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := (lift : (a : α → ℤ) → FreeAbelianGroup α →+ ℤ) 1
⊢ Eq (α := ℤ) ((f : (a : FreeAbelianGroup α) → ℤ) (of x) : ℤ) (1 : ℤ)

Tactic:
have hfx : f (of x) = 1 := lift_apply_of _ _
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
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 : ℤ)
rw₁ rw₂ : Eq (α := ℤ) 0 0
⊢ Eq (α := ℤ) ((f : (a : FreeAbelianGroup α) → ℤ) (of x) : ℤ) (0 : ℤ)

Tactic:
rw [h, map_zero]

Premises used: map_zero
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
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 : ℤ)

Tactic:
have hf0 : f (of x) = 0 := by rw [h, map_zero]
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := (lift : (a : α → ℤ) → FreeAbelianGroup α →+ ℤ) 1
hfx : Eq (α := ℤ) ((f : (a : FreeAbelianGroup α) → ℤ) (of x) : ℤ) (1 : ℤ)
hf0 : Eq (α := ℤ) ((f : (a : FreeAbelianGroup α) → ℤ) (of x) : ℤ) (0 : ℤ)
⊢ False

Tactic:
one_ne_zero <| hfx.symm.trans hf0

Premises used: one_ne_zero, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := (lift : (a : α → ℤ) → FreeAbelianGroup α →+ ℤ) 1
hfx : Eq (α := ℤ) ((f : (a : FreeAbelianGroup α) → ℤ) (of x) : ℤ) (1 : ℤ)
hf0 : Eq (α := ℤ) ((f : (a : FreeAbelianGroup α) → ℤ) (of x) : ℤ) (0 : ℤ)
⊢ False

Tactic:
exact one_ne_zero <| hfx.symm.trans hf0

Premises used: one_ne_zero, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
x : α
⊢ 0 ≠ of x

Tactic:
of_ne_zero _ |>.symm

Premises used: FreeAbelianGroup.of_ne_zero, Ne.symm
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
motive : FreeAbelianGroup α → Prop
z : FreeAbelianGroup α
zero : motive 0
of : ∀ (x : α), motive (FreeAbelianGroup.of x)
neg : ∀ (x : α), motive (FreeAbelianGroup.of x) → motive (-FreeAbelianGroup.of x)
add : ∀ (x y : FreeAbelianGroup α), motive x → motive y → motive (x + y)
⊢ motive z

Tactic:
Quotient.inductionOn' z fun x ↦ Quot.inductionOn x fun L ↦
    List.recOn L zero fun ⟨x, b⟩ _ ih ↦ Bool.recOn b (add _ _ (neg _ (of x)) ih) (add _ _ (of x) ih)

Premises used: Quotient.inductionOn'
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
inst : AddCommGroup G
f g : α → G
⊢ (((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:
simp only [(lift _).map_zero, zero_add]

Premises used: AddMonoidHom.map_zero, zero_add, FreeAbelianGroup.lift, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
inst : AddCommGroup G
f g : α → G
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:
simp only [lift_apply_of, Pi.add_apply]

Premises used: Pi.add_apply, FreeAbelianGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
inst : AddCommGroup G
f g : α → G
x : α
h :
  (((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)
⊢ (((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:
simp only [map_neg, lift_apply_of, Pi.add_apply, neg_add]

Premises used: neg_add, map_neg, Pi.add_apply, FreeAbelianGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
inst : AddCommGroup G
f g : α → G
x y : FreeAbelianGroup α
hx :
  (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
        (a : FreeAbelianGroup α) → G)
      x =
    HAdd.hAdd (α := G) (β := G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          x :
        G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          x :
        G)
hy :
  (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
        (a : FreeAbelianGroup α) → G)
      y =
    HAdd.hAdd (α := G) (β := G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          y :
        G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          y :
        G)
⊢ (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
        (a : FreeAbelianGroup α) → G)
      (x + y) =
    HAdd.hAdd (α := G) (β := G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          (x + y) :
        G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          (x + y) :
        G)

Tactic:
simp only [(lift _).map_add, hx, hy, add_add_add_comm]

Premises used: FreeAbelianGroup.lift, add_add_add_comm, AddMonoidHom.map_add, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
inst : AddCommGroup G
f g : α → G
⊢ (lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) =
    HAdd.hAdd (α := AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) (β := AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G)
      ((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G)
      ((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G)

Tactic:
AddMonoidHom.ext <| lift_add_apply _ _

Premises used: AddMonoidHom.ext, FreeAbelianGroup.lift_add_apply
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
inst : AddCommGroup G
f : α → G
⊢ Eq (α := AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G)
    ((lift : (a : α → G) → FreeAbelianGroup α →+ G) (-f) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G)
    (-(lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G)

Tactic:
liftAddEquiv.map_neg f

Premises used: AddEquiv.map_neg
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
inst : AddCommGroup G
f : α → G
a : FreeAbelianGroup α
⊢ Eq.{u_1 + 1} (α := G)
    ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) (-f) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
          (a : FreeAbelianGroup α) → G)
        a :
      G)
    (-(((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          a :
      G)

Tactic:
congr($(lift_neg f) a)

Premises used: congrArg, id, FreeAbelianGroup.lift_neg, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
motive : FreeAbelianGroup α → Prop
z : FreeAbelianGroup α
zero : motive 0
pure : ∀ (x : α), motive (Pure.pure x)
neg : ∀ (x : α), motive (Pure.pure x) → motive (-Pure.pure x)
add : ∀ (x y : FreeAbelianGroup α), motive x → motive y → motive (x + y)
⊢ motive z

Tactic:
FreeAbelianGroup.induction_on z zero pure neg add

Premises used: FreeAbelianGroup.induction_on
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
f : α → β
x : α
⊢ Eq (α := FreeAbelianGroup β) (f <$> pure x) (pure (f x))

Tactic:
rfl

Premises used: FreeGroup.of, Quotient.liftOn', FreeGroup.Lift.aux, Quotient.map₂, List.append, Con.liftOn, FreeAbelianGroup.of, FreeGroup.mk, List.foldr, rfl, List.prod
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
f : α → β
⊢ Eq (α := FreeAbelianGroup β) (f <$> 0) 0

Tactic:
(lift (of ∘ f)).map_zero

Premises used: AddMonoidHom.map_zero, Function.comp, FreeAbelianGroup.lift, FreeAbelianGroup.of, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
f : α → β
x y : FreeAbelianGroup α
⊢ f <$> (x + y) = f <$> x + f <$> y

Tactic:
(lift _).map_add _ _

Premises used: FreeAbelianGroup.lift, AddMonoidHom.map_add, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
f : α → β
x : FreeAbelianGroup α
⊢ f <$> (-x) = -f <$> x

Tactic:
map_neg (lift <| of ∘ f) _

Premises used: Function.comp, map_neg, FreeAbelianGroup.lift, FreeAbelianGroup.of, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
f : α → β
x y : FreeAbelianGroup α
⊢ f <$> (x - y) = f <$> x - f <$> y

Tactic:
map_sub (lift <| of ∘ f) _ _

Premises used: map_sub, Function.comp, FreeAbelianGroup.lift, FreeAbelianGroup.of, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
f : α → β
y : α
⊢ f <$> of y = of (f y)

Tactic:
rfl

Premises used: FreeGroup.of, Quotient.liftOn', FreeGroup.Lift.aux, Quotient.map₂, List.append, Con.liftOn, FreeAbelianGroup.of, FreeGroup.mk, List.foldr, rfl, List.prod
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
f : α → FreeAbelianGroup β
x : α
⊢ pure x >>= f = f x

Tactic:
lift_apply_of _ _

Premises used: FreeAbelianGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
f : α → FreeAbelianGroup β
⊢ 0 >>= f = 0

Tactic:
(lift f).map_zero

Premises used: AddMonoidHom.map_zero, FreeAbelianGroup.lift, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
f : α → FreeAbelianGroup β
x y : FreeAbelianGroup α
⊢ x + y >>= f = (x >>= f) + (y >>= f)

Tactic:
(lift _).map_add _ _

Premises used: FreeAbelianGroup.lift, AddMonoidHom.map_add, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
f : α → FreeAbelianGroup β
x : FreeAbelianGroup α
⊢ -x >>= f = -(x >>= f)

Tactic:
map_neg (lift f) _

Premises used: map_neg, FreeAbelianGroup.lift, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
f : α → FreeAbelianGroup β
x y : FreeAbelianGroup α
⊢ x - y >>= f = (x >>= f) - (y >>= f)

Tactic:
map_sub (lift f) _ _

Premises used: map_sub, FreeAbelianGroup.lift, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
f : α → β
x : FreeAbelianGroup α
⊢ pure f <*> x = f <$> x

Tactic:
pure_bind _ _

Premises used: FreeAbelianGroup.pure_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
x : FreeAbelianGroup α
⊢ Eq.{u + 1} (α := FreeAbelianGroup β) (0 <*> x) 0

Tactic:
zero_bind _

Premises used: FreeAbelianGroup.zero_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
f g : FreeAbelianGroup (α → β)
x : FreeAbelianGroup α
⊢ f + g <*> x = (f <*> x) + (g <*> x)

Tactic:
add_bind _ _ _

Premises used: FreeAbelianGroup.add_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
f : FreeAbelianGroup (α → β)
x : FreeAbelianGroup α
⊢ -f <*> x = -(f <*> x)

Tactic:
neg_bind _ _

Premises used: FreeAbelianGroup.neg_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α β : Type u
f g : FreeAbelianGroup (α → β)
x : FreeAbelianGroup α
⊢ f - g <*> x = (f <*> x) - (g <*> x)

Tactic:
sub_bind _ _ _

Premises used: FreeAbelianGroup.sub_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type u
f : FreeAbelianGroup (α → β)
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)
⊢ FreeAbelianGroup α →+ FreeAbelianGroup β

Tactic:
refine .mk' (f <*> ·) fun x y ↦ ?_