awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type u
f : FreeAbelianGroup (α → β)
x y : FreeAbelianGroup α
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 β)
⊢ (fun (x : FreeAbelianGroup α) ↦ f <*> x) (x + y) =
    HAdd.hAdd (α := FreeAbelianGroup β) ((fun (x : FreeAbelianGroup α) ↦ f <*> x) x)
      ((fun (x : FreeAbelianGroup α) ↦ f <*> x) y)

Tactic:
change lift (· <$> (x + y)) _ = lift (· <$> x) _ + lift (· <$> y) _

Premises used: FreeAbelianGroup.lift, HAdd.hAdd, DFunLike.coe, Functor.map
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type u
f : FreeAbelianGroup (α → β)
x y : FreeAbelianGroup α
⊢ ((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:
simp [← Pi.add_def]

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

Tactic:
(seqAddGroupHom f).map_zero

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

Tactic:
(seqAddGroupHom f).map_add x y

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

Tactic:
(seqAddGroupHom f).map_neg x

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

Tactic:
(seqAddGroupHom f).map_sub x y

Premises used: AddMonoidHom.map_sub, FreeAbelianGroup.seqAddGroupHom
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
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)
rw₁ rw₂ : Eq (α := FreeAbelianGroup α_1) (-pure x) (-pure x)
⊢ Eq (α := FreeAbelianGroup α_1) (id <$> (-pure x)) (-pure x)

Tactic:
rw [FreeAbelianGroup.map_neg, ih]

Premises used: FreeAbelianGroup.map_neg
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
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
rw₂ rw₃ : x + y = x + y
⊢ id <$> (x + y) = x + y

Tactic:
rw [FreeAbelianGroup.map_add, ihx, ihy]

Premises used: FreeAbelianGroup.map_add
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
rw rw₁ : Eq.{u + 1} (α := FreeAbelianGroup γ) 0 0
⊢ Eq.{u + 1} (α := FreeAbelianGroup γ) 0 (0 >>= fun (x : α_1) ↦ f x >>= g)

Tactic:
rw [zero_bind]

Premises used: FreeAbelianGroup.zero_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
iterate iterate₁ iterate₂ iterate₃ : 0 >>= g = 0 >>= fun (x : α_1) ↦ f x >>= g
⊢ 0 >>= f >>= g = 0 >>= fun (x : α_1) ↦ f x >>= g

Tactic:
iterate 3 rw [zero_bind]

Premises used: FreeAbelianGroup.zero_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
rw : f x >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
⊢ pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g

Tactic:
rw [pure_bind]

Premises used: FreeAbelianGroup.pure_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
rw rw₁ : f x >>= g = f x >>= g
⊢ f x >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g

Tactic:
rw [pure_bind]

Premises used: FreeAbelianGroup.pure_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
iterate iterate₁ iterate₂ iterate₃ : f x >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
⊢ pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g

Tactic:
iterate 2 rw [pure_bind]

Premises used: FreeAbelianGroup.pure_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
ih : pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
rw : -(pure x >>= f) >>= g = -pure x >>= fun (x : α_1) ↦ f x >>= g
⊢ -pure x >>= f >>= g = -pure x >>= fun (x : α_1) ↦ f x >>= g

Tactic:
rw [neg_bind]

Premises used: FreeAbelianGroup.neg_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
ih : pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
rw : -(pure x >>= f >>= g) = -pure x >>= fun (x : α_1) ↦ f x >>= g
⊢ -(pure x >>= f) >>= g = -pure x >>= fun (x : α_1) ↦ f x >>= g

Tactic:
rw [neg_bind]

Premises used: FreeAbelianGroup.neg_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
ih : pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
rw : Eq (α := FreeAbelianGroup γ) (-(pure x >>= fun (x : α_1) ↦ f x >>= g)) (-pure x >>= fun (x : α_1) ↦ f x >>= g)
⊢ -(pure x >>= f >>= g) = -pure x >>= fun (x : α_1) ↦ f x >>= g

Tactic:
rw [ih]
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
ih : pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
try : Eq (α := FreeAbelianGroup γ) (-(pure x >>= fun (x : α_1) ↦ f x >>= g)) (-pure x >>= fun (x : α_1) ↦ f x >>= g)
⊢ -(pure x >>= f >>= g) = -pure x >>= fun (x : α_1) ↦ f x >>= g

Tactic:
try rw [ih]
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
ih : pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
rw rw₁ :
  Eq (α := FreeAbelianGroup γ) (-(pure x >>= fun (x : α_1) ↦ f x >>= g)) (-(pure x >>= fun (x : α_1) ↦ f x >>= g))
⊢ Eq (α := FreeAbelianGroup γ) (-(pure x >>= fun (x : α_1) ↦ f x >>= g)) (-pure x >>= fun (x : α_1) ↦ f x >>= g)

Tactic:
rw [neg_bind]

Premises used: FreeAbelianGroup.neg_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
ih : pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
iterate iterate₁ iterate₂ iterate₃ iterate₄ iterate₅ iterate₆ iterate₇ :
  -(pure x >>= f) >>= g = -pure x >>= fun (x : α_1) ↦ f x >>= g
⊢ -pure x >>= f >>= g = -pure x >>= fun (x : α_1) ↦ f x >>= g

Tactic:
iterate 3 rw [neg_bind] <;> try rw [ih]

Premises used: FreeAbelianGroup.neg_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x y : FreeAbelianGroup α_1
ihx : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
rw : (x >>= f) + (y >>= f) >>= g = x + y >>= fun (x : α_1) ↦ f x >>= g
⊢ x + y >>= f >>= g = x + y >>= fun (x : α_1) ↦ f x >>= g

Tactic:
rw [add_bind]

Premises used: FreeAbelianGroup.add_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x y : FreeAbelianGroup α_1
ihx : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
rw : (x >>= f >>= g) + (y >>= f >>= g) = x + y >>= fun (x : α_1) ↦ f x >>= g
⊢ (x >>= f) + (y >>= f) >>= g = x + y >>= fun (x : α_1) ↦ f x >>= g

Tactic:
rw [add_bind]

Premises used: FreeAbelianGroup.add_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x y : FreeAbelianGroup α_1
ihx : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
rw :
  HAdd.hAdd (α := FreeAbelianGroup γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g) =
    x + y >>= fun (x : α_1) ↦ f x >>= g
⊢ (x >>= f >>= g) + (y >>= f >>= g) = x + y >>= fun (x : α_1) ↦ f x >>= g

Tactic:
rw [ihx, ihy]
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x y : FreeAbelianGroup α_1
ihx : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
try :
  HAdd.hAdd (α := FreeAbelianGroup γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g) =
    x + y >>= fun (x : α_1) ↦ f x >>= g
⊢ (x >>= f >>= g) + (y >>= f >>= g) = x + y >>= fun (x : α_1) ↦ f x >>= g

Tactic:
try rw [ihx, ihy]
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x y : FreeAbelianGroup α_1
ihx : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
rw rw₁ :
  HAdd.hAdd (α := FreeAbelianGroup γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g) =
    HAdd.hAdd (α := FreeAbelianGroup γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g)
⊢ HAdd.hAdd (α := FreeAbelianGroup γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g) =
    x + y >>= fun (x : α_1) ↦ f x >>= g

Tactic:
rw [add_bind]

Premises used: FreeAbelianGroup.add_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x y : FreeAbelianGroup α_1
ihx : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
iterate iterate₁ iterate₂ iterate₃ iterate₄ iterate₅ iterate₆ iterate₇ :
  (x >>= f) + (y >>= f) >>= g = x + y >>= fun (x : α_1) ↦ f x >>= g
⊢ x + y >>= f >>= g = x + y >>= fun (x : α_1) ↦ f x >>= g

Tactic:
iterate 3 rw [add_bind] <;> try rw [ihx, ihy]

Premises used: FreeAbelianGroup.add_bind
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
y : FreeAbelianGroup β_1
zero : Eq (α := FreeAbelianGroup (α_1 × β_1)) (0 <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)
zero₁ : Eq (α := FreeAbelianGroup (α_1 × β_1)) 0 ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)
zero₂ zero₃ : Eq.{u + 1} (α := FreeAbelianGroup (α_1 × β_1)) 0 0
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> 0 <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)

Tactic:
rw [FreeAbelianGroup.map_zero, zero_seq, seq_zero]

Premises used: FreeAbelianGroup.seq_zero, FreeAbelianGroup.map_zero, FreeAbelianGroup.zero_seq
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
y : FreeAbelianGroup β_1
p : α_1
pure : Prod.mk p <$> y = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> Pure.pure p
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> Pure.pure p <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> Pure.pure p)

Tactic:
rw [map_pure, pure_seq]

Premises used: FreeAbelianGroup.pure_seq, FreeAbelianGroup.map_pure
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
pure : Eq.{u + 1} (α := FreeAbelianGroup (α_1 × β_1)) 0 ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> 0 <*> Pure.pure p)
pure₁ : Eq.{u + 1} (α := FreeAbelianGroup (α_1 × β_1)) 0 (0 <*> Pure.pure p)
pure₂ pure₃ : Eq.{u + 1} (α := FreeAbelianGroup (α_1 × β_1)) 0 0
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> 0) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> 0 <*> Pure.pure p)

Tactic:
rw [FreeAbelianGroup.map_zero, FreeAbelianGroup.map_zero, zero_seq]

Premises used: FreeAbelianGroup.map_zero, FreeAbelianGroup.zero_seq
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
q : β_1
pure :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Pure.pure (p, q))
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
pure₁ : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Pure.pure (p, q)) ((Pure.pure fun (a : α_1) ↦ (a, q)) <*> Pure.pure p)
pure₂ : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Pure.pure (p, q)) ((fun (a : α_1) ↦ (a, q)) <$> Pure.pure p)
pure₃ pure₄ : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Pure.pure (p, q)) (Pure.pure (p, q))
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> Pure.pure q)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)

Tactic:
rw [map_pure, map_pure, pure_seq, map_pure]

Premises used: FreeAbelianGroup.pure_seq, FreeAbelianGroup.map_pure
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
q : β_1
ih :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> Pure.pure q)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
pure :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk p <$> Pure.pure q)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (-Pure.pure q) <*> Pure.pure p)
pure₁ :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk p <$> Pure.pure q)
    (-(fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
pure₂ :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk p <$> Pure.pure q)
    (-((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p))
pure₃ pure₄ :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p))
    (-((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p))
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> (-Pure.pure q))
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (-Pure.pure q) <*> Pure.pure p)

Tactic:
rw [FreeAbelianGroup.map_neg, FreeAbelianGroup.map_neg, neg_seq, ih]

Premises used: FreeAbelianGroup.map_neg, FreeAbelianGroup.neg_seq
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
y₁ y₂ : FreeAbelianGroup β_1
ih1 : Prod.mk p <$> y₁ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p
ih2 : Prod.mk p <$> y₂ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p
pure : Prod.mk p <$> y₁ + Prod.mk p <$> y₂ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (y₁ + y₂) <*> Pure.pure p
pure₁ :
  Prod.mk p <$> y₁ + Prod.mk p <$> y₂ =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 → α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁)
        ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂) <*>
      Pure.pure p
pure₂ :
  Prod.mk p <$> y₁ + Prod.mk p <$> y₂ =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p)
pure₃ :
  ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p) + Prod.mk p <$> y₂ =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p)
pure₄ pure₅ :
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p) =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p)
⊢ Prod.mk p <$> (y₁ + y₂) = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (y₁ + y₂) <*> Pure.pure p

Tactic:
rw [FreeAbelianGroup.map_add, FreeAbelianGroup.map_add, add_seq, ih1, ih2]

Premises used: FreeAbelianGroup.map_add, FreeAbelianGroup.add_seq
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
y : FreeAbelianGroup β_1
p : α_1
pure :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> 0) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> 0 <*> Pure.pure p)
pure₁ :
  ∀ (q : β_1),
    Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> Pure.pure q)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
pure₂ :
  ∀ (q : β_1)
    (ih :
      Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> Pure.pure q)
        ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)),
    Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> (-Pure.pure q))
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (-Pure.pure q) <*> Pure.pure p)
pure₃ :
  ∀ (y₁ y₂ : FreeAbelianGroup β_1) (ih1 : Prod.mk p <$> y₁ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p)
    (ih2 : Prod.mk p <$> y₂ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p),
    Prod.mk p <$> (y₁ + y₂) = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (y₁ + y₂) <*> Pure.pure p
⊢ Prod.mk p <$> y = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> Pure.pure p

Tactic:
induction y using FreeAbelianGroup.induction_on' with
      | zero => rw [FreeAbelianGroup.map_zero, FreeAbelianGroup.map_zero, zero_seq]
      | pure q => rw [map_pure, map_pure, pure_seq, map_pure]
      | neg q ih => rw [FreeAbelianGroup.map_neg, FreeAbelianGroup.map_neg, neg_seq, ih]
      | add y₁ y₂ ih1 ih2 =>
        rw [FreeAbelianGroup.map_add, FreeAbelianGroup.map_add, add_seq, ih1, ih2]

Premises used: Pure.pure, FreeAbelianGroup.pure_seq, FreeAbelianGroup.map_add, FreeAbelianGroup.map_neg, FreeAbelianGroup.neg_seq, FreeAbelianGroup.map_pure, FreeAbelianGroup.map_zero, FreeAbelianGroup.zero_seq, FreeAbelianGroup.add_seq
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
y : FreeAbelianGroup β_1
p : α_1
ih :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> pure p <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p)
neg :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk <$> pure p <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -pure p)
neg₁ :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-(Prod.mk <$> pure p <*> y))
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -pure p)
neg₂ :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-(Prod.mk <$> pure p <*> y))
    (-((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p))
neg₃ neg₄ :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p))
    (-((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p))
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (-pure p) <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -pure p)

Tactic:
rw [FreeAbelianGroup.map_neg, neg_seq, seq_neg, ih]

Premises used: FreeAbelianGroup.seq_neg, FreeAbelianGroup.map_neg, FreeAbelianGroup.neg_seq
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
y : FreeAbelianGroup β_1
x₁ x₂ : FreeAbelianGroup α_1
ih1 : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
ih2 : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₂ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)
add :
  HAdd.hAdd (α := FreeAbelianGroup (β_1 → α_1 × β_1)) (Prod.mk <$> x₁) (Prod.mk <$> x₂) <*> y =
    (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂
add₁ :
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) (Prod.mk <$> x₂ <*> y) =
    (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂
add₂ :
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) (Prod.mk <$> x₂ <*> y) =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)
add₃ :
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
      (Prod.mk <$> x₂ <*> y) =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)
add₄ add₅ :
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂) =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (x₁ + x₂) <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂)

Tactic:
rw [FreeAbelianGroup.map_add, add_seq, seq_add, ih1, ih2]

Premises used: FreeAbelianGroup.seq_add, FreeAbelianGroup.map_add, FreeAbelianGroup.add_seq