awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ψ = toAddMonoid (β := β) fun (i : ι) ↦ ψ.comp (of β i)
have e_a : ∀ (x : ι),
  ψ.comp (DFinsupp.singleAddHom (fun (i : ι) ↦ β i) x) =
    AddMonoidHom.comp (toAddMonoid (β := β) fun (i : ι) ↦ ψ.comp (of β i)) (DFinsupp.singleAddHom (fun (i : ι) ↦ β i) x)
Tactic: apply DFinsupp.addHom_ext'
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
x : ι
⊢ ψ.comp (DFinsupp.singleAddHom (fun (i : ι) ↦ β i) x) =
    AddMonoidHom.comp (toAddMonoid (β := β) fun (i : ι) ↦ ψ.comp (of β i)) (DFinsupp.singleAddHom (fun (i : ι) ↦ β i) x)
have e_a : ψ.comp (DFinsupp.singleAddHom (fun (i : ι) ↦ β i) x) = ψ.comp (of β x)
Tactic: simp [toAddMonoid]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
i : ι
f : AddMonoidHom.{u₁, w} γ (β i)
⊢ (fromAddMonoid (β := β) : (a : ⨁ (i : ι), γ →+ β i) → γ →+ ⨁ (i : ι), β i)
      (((of (fun (i : ι) ↦ AddMonoidHom.{u₁, w} γ (β i)) i :
            AddMonoidHom.{u₁, w} γ (β i) →+ ⨁ (i : ι), AddMonoidHom.{u₁, w} γ (β i)) :
          (a : γ →+ β i) → ⨁ (i : ι), γ →+ β i)
        f) =
    AddMonoidHom.comp (of β i) f
have rw : (((AddMonoidHom.compHom : (a : β i →+ ⨁ (i : ι), β i) → (γ →+ β i) →+ γ →+ ⨁ (i : ι), β i) (of β i) :
        AddMonoidHom.{u₁, w} γ (β i) →+ γ →+ ⨁ (i : ι), β i) :
      (a : γ →+ β i) → γ →+ ⨁ (i : ι), β i)
    f =
  AddMonoidHom.comp (of β i) f
Tactic: rw [fromAddMonoid, toAddMonoid_of]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
i : ι
f : AddMonoidHom.{u₁, w} γ (β i)
x : γ
⊢ Eq (α := ⨁ (i : ι), β i)
    ((((fromAddMonoid (β := β) : (a : ⨁ (i : ι), γ →+ β i) → γ →+ ⨁ (i : ι), β i)
              (((of (fun (i : ι) ↦ AddMonoidHom.{u₁, w} γ (β i)) i :
                    AddMonoidHom.{u₁, w} γ (β i) →+ ⨁ (i : ι), AddMonoidHom.{u₁, w} γ (β i)) :
                  (a : γ →+ β i) → ⨁ (i : ι), γ →+ β i)
                f) :
            γ →+ ⨁ (i : ι), β i) :
          (a : γ) → ⨁ (i : ι), β i)
        x :
      ⨁ (i : ι), β i)
    ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f : (a : γ) → β i) x) : ⨁ (i : ι), β i)
have rw : Eq (α := ⨁ (i : ι), β i) ((AddMonoidHom.comp (of β i) f : (a : γ) → ⨁ (i : ι), β i) x : ⨁ (i : ι), β i)
  ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f : (a : γ) → β i) x) : ⨁ (i : ι), β i)
Tactic: rw [fromAddMonoid_of, AddMonoidHom.coe_comp, Function.comp]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
i : ι
f : AddMonoidHom.{u₁, w} γ (β i)
x : γ
rw :
  Eq (α := ⨁ (i : ι), β i) ((AddMonoidHom.comp (of β i) f : (a : γ) → ⨁ (i : ι), β i) x : ⨁ (i : ι), β i)
    ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f : (a : γ) → β i) x) : ⨁ (i : ι), β i)
⊢ Eq (α := ⨁ (i : ι), β i)
    ((((fromAddMonoid (β := β) : (a : ⨁ (i : ι), γ →+ β i) → γ →+ ⨁ (i : ι), β i)
              (((of (fun (i : ι) ↦ AddMonoidHom.{u₁, w} γ (β i)) i :
                    AddMonoidHom.{u₁, w} γ (β i) →+ ⨁ (i : ι), AddMonoidHom.{u₁, w} γ (β i)) :
                  (a : γ →+ β i) → ⨁ (i : ι), γ →+ β i)
                f) :
            γ →+ ⨁ (i : ι), β i) :
          (a : γ) → ⨁ (i : ι), β i)
        x :
      ⨁ (i : ι), β i)
    ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f : (a : γ) → β i) x) : ⨁ (i : ι), β i)
have rw₁ : Eq (α := ⨁ (i : ι), β i)
  (comp (β := β i) (⇑(of β i) : (a : β i) → ⨁ (i : ι), β i) (⇑f : (a : γ) → β i) x : ⨁ (i : ι), β i)
  ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f : (a : γ) → β i) x) : ⨁ (i : ι), β i)
Tactic: rw [fromAddMonoid_of, AddMonoidHom.coe_comp, Function.comp]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
i : ι
f : AddMonoidHom.{u₁, w} γ (β i)
x : γ
rw :
  Eq (α := ⨁ (i : ι), β i) ((AddMonoidHom.comp (of β i) f : (a : γ) → ⨁ (i : ι), β i) x : ⨁ (i : ι), β i)
    ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f : (a : γ) → β i) x) : ⨁ (i : ι), β i)
rw₁ :
  Eq (α := ⨁ (i : ι), β i)
    (comp (β := β i) (⇑(of β i) : (a : β i) → ⨁ (i : ι), β i) (⇑f : (a : γ) → β i) x : ⨁ (i : ι), β i)
    ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f : (a : γ) → β i) x) : ⨁ (i : ι), β i)
⊢ Eq (α := ⨁ (i : ι), β i)
    ((((fromAddMonoid (β := β) : (a : ⨁ (i : ι), γ →+ β i) → γ →+ ⨁ (i : ι), β i)
              (((of (fun (i : ι) ↦ AddMonoidHom.{u₁, w} γ (β i)) i :
                    AddMonoidHom.{u₁, w} γ (β i) →+ ⨁ (i : ι), AddMonoidHom.{u₁, w} γ (β i)) :
                  (a : γ →+ β i) → ⨁ (i : ι), γ →+ β i)
                f) :
            γ →+ ⨁ (i : ι), β i) :
          (a : γ) → ⨁ (i : ι), β i)
        x :
      ⨁ (i : ι), β i)
    ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f : (a : γ) → β i) x) : ⨁ (i : ι), β i)
have rw₂ : Eq (α := ⨁ (i : ι), β i) ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f : (a : γ) → β i) x) : ⨁ (i : ι), β i)
  ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f : (a : γ) → β i) x) : ⨁ (i : ι), β i)
Tactic: rw [fromAddMonoid_of, AddMonoidHom.coe_comp, Function.comp]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι_1 : Type v
β : ι_1 → Type w
inst : (i : ι_1) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Unique ι
x : ⨁ (x : ι), M
⊢ Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (x : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((toAddMonoid (β := fun (x : ι) ↦ M) fun (x : ι) ↦ AddMonoidHom.id M : (a : ⨁ (i : ι), M) → M) 0) :
      ⨁ (i : ι), M)
    (0 : ⨁ (i : ι), M)
have rw : Eq (α := ⨁ (x : ι), M) (((of.{u_1, v} (fun (x : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) 0) 0
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι_1 : Type v
β : ι_1 → Type w
inst : (i : ι_1) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Unique ι
x : ⨁ (x : ι), M
rw : Eq (α := ⨁ (x : ι), M) (((of.{u_1, v} (fun (x : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) 0) 0
⊢ Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (x : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((toAddMonoid (β := fun (x : ι) ↦ M) fun (x : ι) ↦ AddMonoidHom.id M : (a : ⨁ (i : ι), M) → M) 0) :
      ⨁ (i : ι), M)
    (0 : ⨁ (i : ι), M)
have rw₁ : Eq (α := ⨁ (x : ι), M) 0 0
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι_1 : Type v
β : ι_1 → Type w
inst : (i : ι_1) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Unique ι
x_1 : ⨁ (x : ι), M
p : ι
x : M
⊢ Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (x : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((toAddMonoid (β := fun (x : ι) ↦ M) fun (x : ι) ↦ AddMonoidHom.id M : (a : ⨁ (i : ι), M) → M)
          (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)) :
      ⨁ (i : ι), M)
    (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
have rw : Eq (α := ⨁ (x : ι), M)
  (((of.{u_1, v} (fun (x : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
      ((toAddMonoid (β := fun (x : ι) ↦ M) fun (x : ι) ↦ AddMonoidHom.id M : (a : ⨁ (i : ι), M) → M)
        (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)) :
    ⨁ (i : ι), M)
  (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
Tactic: rw [Unique.default_eq p, toAddMonoid_of, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι_1 : Type v
β : ι_1 → Type w
inst : (i : ι_1) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Unique ι
x_1 : ⨁ (x : ι), M
p : ι
x : M
rw :
  Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (x : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((toAddMonoid (β := fun (x : ι) ↦ M) fun (x : ι) ↦ AddMonoidHom.id M : (a : ⨁ (i : ι), M) → M)
          (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)) :
      ⨁ (i : ι), M)
    (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
⊢ Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (x : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((toAddMonoid (β := fun (x : ι) ↦ M) fun (x : ι) ↦ AddMonoidHom.id M : (a : ⨁ (i : ι), M) → M)
          (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)) :
      ⨁ (i : ι), M)
    (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
have rw₁ : Eq (α := ⨁ (x : ι), M)
  (((of.{u_1, v} (fun (x : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
      ((AddMonoidHom.id M : (a : M) → M) x) :
    ⨁ (i : ι), M)
  (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
Tactic: rw [Unique.default_eq p, toAddMonoid_of, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι_1 : Type v
β : ι_1 → Type w
inst : (i : ι_1) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Unique ι
x_1 : ⨁ (x : ι), M
p : ι
x : M
rw :
  Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (x : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((toAddMonoid (β := fun (x : ι) ↦ M) fun (x : ι) ↦ AddMonoidHom.id M : (a : ⨁ (i : ι), M) → M)
          (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)) :
      ⨁ (i : ι), M)
    (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
rw₁ :
  Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (x : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((AddMonoidHom.id M : (a : M) → M) x) :
      ⨁ (i : ι), M)
    (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
⊢ Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (x : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((toAddMonoid (β := fun (x : ι) ↦ M) fun (x : ι) ↦ AddMonoidHom.id M : (a : ⨁ (i : ι), M) → M)
          (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)) :
      ⨁ (i : ι), M)
    (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
have rw₂ : Eq (α := ⨁ (x : ι), M)
  (((of.{u_1, v} (fun (x : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
  (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
Tactic: rw [Unique.default_eq p, toAddMonoid_of, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
M : Type v
ι : Type u_1
inst : AddCommMonoid M
inst_1 : Unique ι
x : ⨁ (x : ι), M
⊢ (DirectSum.id M ι : (a : ⨁ (x : ι), M) → M) x = (x : (a : ι) → M) default
have rw : ((of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) ((x : (a : ι) → M) default) = x
Tactic: rw [← AddEquiv.eq_symm_apply, id_symm_apply, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
M : Type v
ι : Type u_1
inst : AddCommMonoid M
inst_1 : Unique ι
x : ⨁ (x : ι), M
⊢ ((of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) ((x : (a : ι) → M) default) = x
have zero : Eq (α := ⨁ (x : ι), M)
  (((of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) ((0 : (a : ι) → M) default) :
    ⨁ (i : ι), M)
  (0 : ⨁ (i : ι), M)
Tactic: induction x using DirectSum.induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
M : Type v
ι : Type u_1
inst : AddCommMonoid M
inst_1 : Unique ι
x : ⨁ (x : ι), M
zero :
  Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((0 : (a : ι) → M) default) :
      ⨁ (i : ι), M)
    (0 : ⨁ (i : ι), M)
⊢ ((of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) ((x : (a : ι) → M) default) = x
have of : ∀ (i : ι) (x : M),
  Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        (((((of.{u_1, v} (fun (x : ι) ↦ M) i : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M) :
            (a : ι) → M)
          default) :
      ⨁ (i : ι), M)
    (((of.{u_1, v} (fun (x : ι) ↦ M) i : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
Tactic: induction x using DirectSum.induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
M : Type v
ι : Type u_1
inst : AddCommMonoid M
inst_1 : Unique ι
x : ⨁ (x : ι), M
zero :
  Eq (α := ⨁ (x : ι), M)
    (((DirectSum.of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((0 : (a : ι) → M) default) :
      ⨁ (i : ι), M)
    (0 : ⨁ (i : ι), M)
of :
  ∀ (i : ι) (x : M),
    Eq (α := ⨁ (x : ι), M)
      (((DirectSum.of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
          (((((DirectSum.of.{u_1, v} (fun (x : ι) ↦ M) i : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x :
                ⨁ (i : ι), M) :
              (a : ι) → M)
            default) :
        ⨁ (i : ι), M)
      (((DirectSum.of.{u_1, v} (fun (x : ι) ↦ M) i : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
⊢ ((DirectSum.of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
      ((x : (a : ι) → M) default) =
    x
have add : ∀ (x y : ⨁ (i : ι), M),
  ((DirectSum.of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((x : (a : ι) → M) default) =
      x →
    ((DirectSum.of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
          ((y : (a : ι) → M) default) =
        y →
      ((DirectSum.of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
          ((x + y : (a : ι) → M) default) =
        x + y
Tactic: induction x using DirectSum.induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
inst : DecidableEq ι
M : Type u_1
S : Type u_2
inst_1 : DecidableEq M
inst_2 : AddCommMonoid M
inst_3 : SetLike S M
inst_4 : AddSubmonoidClass S M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ Eq (α := M) ((DirectSum.coeAddMonoidHom A : (a : ⨁ (i : ι), ↥(A i)) → M) x : M)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) x fun (i : ι) (x : ↥(A i)) ↦ (↑x : M) : M)
have simp : Eq (α := M)
  ((DFinsupp.sumAddHom (β := fun (i : ι) ↦ ↥(A i)) fun (i : ι) ↦ AddSubmonoidClass.subtype (A i) :
        (a : ⨁ (i : ι), ↥(A i)) → M)
      x :
    M)
  (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) x fun (i : ι) (x : ↥(A i)) ↦ (↑x : M) : M)
Tactic: simp only [DirectSum.coeAddMonoidHom, toAddMonoid, DFinsupp.liftAddHom, AddEquiv.coe_mk,
    Equiv.coe_fn_mk]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
M : Type u_1
S : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike S M
inst_3 : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
⊢ (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i)) x :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          j) :
      M) =
    (↑(if i = j then x else 0) : M)
have inl : ∀ (x : ↥(A j)),
  (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) j : ↥(A j) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A j)) → ⨁ (i : ι), ↥(A i)) x :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          j) :
      M) =
    (↑(if j = j then x else 0) : M)
Tactic: obtain rfl | h := Decidable.eq_or_ne j i
Cleared hypotheses: i, x
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
M : Type u_1
S : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike S M
inst_3 : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
inl :
  ∀ (x : ↥(A j)),
    (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) j : ↥(A j) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A j)) → ⨁ (i : ι), ↥(A i)) x :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            j) :
        M) =
      (↑(if j = j then x else 0) : M)
⊢ (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i)) x :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          j) :
      M) =
    (↑(if i = j then x else 0) : M)
have inr : ∀ (h : j ≠ i),
  (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i)) x :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          j) :
      M) =
    (↑(if i = j then x else 0) : M)
Tactic: obtain rfl | h := Decidable.eq_or_ne j i
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
M : Type u_1
S : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike S M
inst_3 : AddSubmonoidClass S M
A : ι → S
j : ι
x : ↥(A j)
⊢ (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) j : ↥(A j) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A j)) → ⨁ (i : ι), ↥(A i)) x :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          j) :
      M) =
    (↑(if j = j then x else 0) : M)
have inl : (↑x : M) = (↑(if j = j then x else 0) : M)
Tactic: rw [DirectSum.of_eq_same, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
M : Type u_1
S : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike S M
inst_3 : AddSubmonoidClass S M
A : ι → S
j : ι
x : ↥(A j)
inl : (↑x : M) = (↑(if j = j then x else 0) : M)
⊢ (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) j : ↥(A j) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A j)) → ⨁ (i : ι), ↥(A i)) x :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          j) :
      M) =
    (↑(if j = j then x else 0) : M)
have inl₁ : (↑x : M) = (↑x : M)
Tactic: rw [DirectSum.of_eq_same, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
M : Type u_1
S : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike S M
inst_3 : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : j ≠ i
⊢ (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i)) x :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          j) :
      M) =
    (↑(if i = j then x else 0) : M)
have inr : (↑0 : M) = (↑(if i = j then x else 0) : M)
Tactic: rw [DirectSum.of_eq_of_ne _ _ _ h, if_neg h.symm, ZeroMemClass.coe_zero, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
M : Type u_1
S : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike S M
inst_3 : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : j ≠ i
inr : (↑0 : M) = (↑(if i = j then x else 0) : M)
⊢ (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i)) x :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          j) :
      M) =
    (↑(if i = j then x else 0) : M)
have inr₁ : Eq.{u_1 + 1} (α := M) (↑0 : M) (↑0 : M)
Tactic: rw [DirectSum.of_eq_of_ne _ _ _ h, if_neg h.symm, ZeroMemClass.coe_zero, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
M : Type u_1
S : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike S M
inst_3 : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : j ≠ i
inr : (↑0 : M) = (↑(if i = j then x else 0) : M)
inr₁ : Eq.{u_1 + 1} (α := M) (↑0 : M) (↑0 : M)
⊢ (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i)) x :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          j) :
      M) =
    (↑(if i = j then x else 0) : M)
have inr₂ : Eq.{u_1 + 1} (α := M) 0 (↑0 : M)
Tactic: rw [DirectSum.of_eq_of_ne _ _ _ h, if_neg h.symm, ZeroMemClass.coe_zero, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
M : Type u_1
S : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike S M
inst_3 : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : j ≠ i
inr : (↑0 : M) = (↑(if i = j then x else 0) : M)
inr₁ : Eq.{u_1 + 1} (α := M) (↑0 : M) (↑0 : M)
inr₂ : Eq.{u_1 + 1} (α := M) 0 (↑0 : M)
⊢ (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i)) x :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          j) :
      M) =
    (↑(if i = j then x else 0) : M)
have inr₃ : Eq.{u_1 + 1} (α := M) 0 0
Tactic: rw [DirectSum.of_eq_of_ne _ _ _ h, if_neg h.symm, ZeroMemClass.coe_zero, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
M : Type u_1
inst : DecidableEq ι
inst_1 : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ iSup A = ⊤
have rw : Surjective (α := Π₀ (i : ι), ↥(A i)) (β := M)
  (⇑(DFinsupp.sumAddHom (β := fun (i : ι) ↦ ↥(A i)) fun (i : ι) ↦ (A i).subtype) : (a : Π₀ (i : ι), ↥(A i)) → M)
Tactic: rw [AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom, AddMonoidHom.mrange_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → AddMonoidHom.{u_4, u_5} (α i) (β i)
x y : ⨁ (i : ι), α i
simp_rw simp_rw₁ :
  Eq (α := ⨁ (i : ι), β i) ((map (α := α) (β := β) f : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) x : ⨁ (i : ι), β i)
      ((map (α := α) (β := β) f : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) y : ⨁ (i : ι), β i) ↔
    ∀ (i : ι),
      Eq.{u_5 + 1} (α := β i) ((f i : (a : α i) → β i) ((x : (a : ι) → α a) i) : β i)
        ((f i : (a : α i) → β i) ((y : (a : ι) → α a) i) : β i)
⊢ Eq (α := ⨁ (i : ι), β i) ((map (α := α) (β := β) f : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) x : ⨁ (i : ι), β i)
      ((map (α := α) (β := β) f : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) y : ⨁ (i : ι), β i) ↔
    ∀ (i : ι),
      Eq.{u_5 + 1} (α := β i) ((f i : (a : α i) → β i) ((x : (a : ι) → α a) i) : β i)
        ((f i : (a : α i) → β i) ((y : (a : ι) → α a) i) : β i)
have simp_rw₂ : (∀ (i : ι),
    (((map (α := α) (β := β) f : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) x : ⨁ (i : ι), β i) : (a : ι) → β a) i =
      (((map (α := α) (β := β) f : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) y : ⨁ (i : ι), β i) : (a : ι) → β a) i) ↔
  ∀ (i : ι),
    Eq.{u_5 + 1} (α := β i) ((f i : (a : α i) → β i) ((x : (a : ι) → α a) i) : β i)
      ((f i : (a : α i) → β i) ((y : (a : ι) → α a) i) : β i)
Tactic: simp_rw [DirectSum.ext_iff, map_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
x y : Decomposition ℳ
⊢ x = y
have obtain : ∀ (decompose' : M → ⨁ (i : ι), ↥(ℳ i))
  (left_inv : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose')
  (xr : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'),
  { decompose' := decompose', left_inv := left_inv, right_inv := xr : Decomposition ℳ } = y
Tactic: obtain ⟨_, _, xr⟩ := x
Cleared hypotheses: x