awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ Eq.{u_3 + 1} (α := Ideal A) (InfSet.sInf {J : Ideal A | I ≤ J ∧ J.IsPrime})
    (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
have a : LE.le.{u_3} (α := Ideal A) (InfSet.sInf {J : Ideal A | I ≤ J ∧ J.IsPrime})
  (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
a :
  LE.le.{u_3} (α := Ideal A) (InfSet.sInf {J : Ideal A | I ≤ J ∧ J.IsPrime})
    (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
⊢ Eq.{u_3 + 1} (α := Ideal A) (InfSet.sInf {J : Ideal A | I ≤ J ∧ J.IsPrime})
    (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
have a₁ : LE.le.{u_3} (α := Ideal A) (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
  (InfSet.sInf {J : Ideal A | I ≤ J ∧ J.IsPrime})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ LE.le.{u_3} (α := Ideal A) (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
    (InfSet.sInf {J : Ideal A | I ≤ J ∧ J.IsPrime})
have a : IsCoinitialFor.{u_3} (α := Ideal A) {J : Ideal A | I ≤ J ∧ J.IsPrime}
  {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}
Tactic: refine sInf_le_sInf_of_isCoinitialFor ?_
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
⊢ ∃ (b : Ideal A), Membership.mem (γ := Set (Ideal A)) {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime} b ∧ b ≤ J
have a : Membership.mem (γ := Set (Ideal A)) {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}
  (HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 J))
Tactic: refine ⟨(J.homogeneousCore 𝒜).toIdeal, ?_, J.toIdeal_homogeneousCore_le _⟩
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
⊢ Membership.mem (γ := Set (Ideal A)) {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}
    (HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 J))
have a : I ≤ HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 J)
Tactic: refine ⟨HomogeneousIdeal.isHomogeneous _, ?_, HJ₂.homogeneousCore⟩
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 I.radical
have rw : IsHomogeneous 𝒜 (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
Tactic: rw [h.radical_eq]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.RingHom (goal)
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Semiring D
inst_4 : SetLike σ A
inst_5 : SetLike τ B
inst_6 : SetLike ψ C
inst_7 : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
f g : 𝒜 →+*ᵍ ℬ
h :
  Eq (α := (a : A) → B) ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) f)
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) g)
⊢ f = g
have mk : ∀ (toRingHom : A →+* B)
  (map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom : (a : A) → B) x : B))
  (h :
    Eq (α := (a : A) → B)
      ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
        { toRingHom := toRingHom, map_mem := @map_mem })
      ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) g)),
  { toRingHom := toRingHom, map_mem := @map_mem : 𝒜 →+*ᵍ ℬ } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.RingHom (goal)
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Semiring D
inst_4 : SetLike σ A
inst_5 : SetLike τ B
inst_6 : SetLike ψ C
inst_7 : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
g : 𝒜 →+*ᵍ ℬ
toRingHom : A →+* B
map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom : (a : A) → B) x : B)
h :
  Eq (α := (a : A) → B)
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toRingHom := toRingHom, map_mem := @map_mem })
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) g)
⊢ { toRingHom := toRingHom, map_mem := @map_mem : 𝒜 →+*ᵍ ℬ } = g
have mk : ∀ (toRingHom_1 : A →+* B)
  (map_mem_1 :
    ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom_1 : (a : A) → B) x : B))
  (h :
    Eq (α := (a : A) → B)
      ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
        { toRingHom := toRingHom, map_mem := @map_mem })
      ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
        { toRingHom := toRingHom_1, map_mem := @map_mem_1 })),
  { toRingHom := toRingHom, map_mem := @map_mem : 𝒜 →+*ᵍ ℬ } = { toRingHom := toRingHom_1, map_mem := @map_mem_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.RingHom (goal)
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Semiring D
inst_4 : SetLike σ A
inst_5 : SetLike τ B
inst_6 : SetLike ψ C
inst_7 : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
toRingHom : A →+* B
map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom : (a : A) → B) x : B)
toRingHom_1 : A →+* B
map_mem_1 : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom_1 : (a : A) → B) x : B)
h :
  Eq (α := (a : A) → B)
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toRingHom := toRingHom, map_mem := @map_mem })
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toRingHom := toRingHom_1, map_mem := @map_mem_1 })
⊢ { toRingHom := toRingHom, map_mem := @map_mem : 𝒜 →+*ᵍ ℬ } = { toRingHom := toRingHom_1, map_mem := @map_mem_1 }
have mk : toRingHom = toRingHom_1
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.RingHom (goal)
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Semiring D
inst_4 : SetLike σ A
inst_5 : SetLike τ B
inst_6 : SetLike ψ C
inst_7 : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
toRingHom : A →+* B
map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom : (a : A) → B) x : B)
toRingHom_1 : A →+* B
map_mem_1 : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom_1 : (a : A) → B) x : B)
h :
  Eq (α := (a : A) → B)
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toRingHom := toRingHom, map_mem := @map_mem })
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toRingHom := toRingHom_1, map_mem := @map_mem_1 })
⊢ toRingHom = toRingHom_1
have mk : Eq (α := (a : A) → B) (⇑toRingHom : (a : A) → B) (⇑toRingHom_1 : (a : A) → B)
Tactic: apply DFunLike.coe_injective'
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.RingHom (goal)
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Semiring D
inst_4 : SetLike σ A
inst_5 : SetLike τ B
inst_6 : SetLike ψ C
inst_7 : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
n : ℕ
f : 𝒜 →+*ᵍ 𝒜
⊢ Eq (α := A → A) (⇑f : (a : A) → A)^[n] (⇑(npowRec n f) : (a : A) → A)
have zero : Eq (α := A → A) (⇑f : (a : A) → A)^[0] (⇑(npowRec 0 f) : (a : A) → A)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.RingHom (goal)
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Semiring D
inst_4 : SetLike σ A
inst_5 : SetLike τ B
inst_6 : SetLike ψ C
inst_7 : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
n : ℕ
f : 𝒜 →+*ᵍ 𝒜
zero : Eq (α := A → A) (⇑f : (a : A) → A)^[0] (⇑(npowRec 0 f) : (a : A) → A)
⊢ Eq (α := A → A) (⇑f : (a : A) → A)^[n] (⇑(npowRec n f) : (a : A) → A)
have succ : ∀ (n : ℕ),
  Eq (α := A → A) (⇑f : (a : A) → A)^[n] (⇑(npowRec n f) : (a : A) → A) →
    Eq (α := A → A) (⇑f : (a : A) → A)^[n + 1] (⇑(npowRec (n + 1) f) : (a : A) → A)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.RingHom (goal)
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
σ : Type u_6
τ : Type u_7
ψ : Type u_8
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ψ C
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
g : ℬ →+*ᵍ 𝒞
f₁ f₂ : 𝒜 →+*ᵍ ℬ
hg : Function.Injective.{u_3 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
h : g.comp f₁ = g.comp f₂
x : A
⊢ Eq.{u_4 + 1} (α := C) ((g : (a : B) → C) ((f₁ : (a : A) → B) x : B) : C)
    ((g : (a : B) → C) ((f₂ : (a : A) → B) x : B) : C)
have rw : Eq.{u_4 + 1} (α := C) ((g.comp f₁ : (a : A) → C) x : C) ((g : (a : B) → C) ((f₂ : (a : A) → B) x : B) : C)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.RingHom (goal)
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
σ : Type u_6
τ : Type u_7
ψ : Type u_8
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ψ C
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
g : ℬ →+*ᵍ 𝒞
f₁ f₂ : 𝒜 →+*ᵍ ℬ
hg : Function.Injective.{u_3 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
h : g.comp f₁ = g.comp f₂
x : A
rw : Eq.{u_4 + 1} (α := C) ((g.comp f₁ : (a : A) → C) x : C) ((g : (a : B) → C) ((f₂ : (a : A) → B) x : B) : C)
⊢ Eq.{u_4 + 1} (α := C) ((g : (a : B) → C) ((f₁ : (a : A) → B) x : B) : C)
    ((g : (a : B) → C) ((f₂ : (a : A) → B) x : B) : C)
have rw₁ : Eq.{u_4 + 1} (α := C) ((g.comp f₂ : (a : A) → C) x : C) ((g : (a : B) → C) ((f₂ : (a : A) → B) x : B) : C)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.RingHom (goal)
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
σ : Type u_6
τ : Type u_7
ψ : Type u_8
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ψ C
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
g : ℬ →+*ᵍ 𝒞
f₁ f₂ : 𝒜 →+*ᵍ ℬ
hg : Function.Injective.{u_3 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
h : g.comp f₁ = g.comp f₂
x : A
rw : Eq.{u_4 + 1} (α := C) ((g.comp f₁ : (a : A) → C) x : C) ((g : (a : B) → C) ((f₂ : (a : A) → B) x : B) : C)
rw₁ : Eq.{u_4 + 1} (α := C) ((g.comp f₂ : (a : A) → C) x : C) ((g : (a : B) → C) ((f₂ : (a : A) → B) x : B) : C)
⊢ Eq.{u_4 + 1} (α := C) ((g : (a : B) → C) ((f₁ : (a : A) → B) x : B) : C)
    ((g : (a : B) → C) ((f₂ : (a : A) → B) x : B) : C)
have rw₂ : Eq.{u_4 + 1} (α := C) ((g : (a : B) → C) ((f₂ : (a : A) → B) x : B) : C)
  ((g : (a : B) → C) ((f₂ : (a : A) → B) x : B) : C)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.RingHom (goal)
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Semiring D
inst_4 : SetLike σ A
inst_5 : SetLike τ B
inst_6 : SetLike ψ C
inst_7 : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
inst_8 : AddSubmonoidClass σ A
inst_9 : AddSubmonoidClass τ B
f : 𝒜 →+*ᵍ ℬ
i : ι
⊢ Eq.{u_3 + 1} (α := ↥(ℬ i)) (Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ i) ((f : (a : A) → B) (↑0 : A)) ⋯ : ↥(ℬ i))
    (0 : ↥(ℬ i))
have a : Eq.{u_3 + 1} (α := B) ((↑(Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ i) ((f : (a : A) → B) (↑0 : A)) sorry) : B) : B)
  ((↑0 : B) : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.RingHom (goal)
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Semiring D
inst_4 : SetLike σ A
inst_5 : SetLike τ B
inst_6 : SetLike ψ C
inst_7 : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
inst_8 : AddSubmonoidClass σ A
inst_9 : AddSubmonoidClass τ B
f : 𝒜 →+*ᵍ ℬ
i : ι
x y : ↥(𝒜 i)
⊢ Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ i) ((f : (a : A) → B) (↑(x + y) : A)) ⋯ =
    HAdd.hAdd (α := ↥(ℬ i)) (β := ↥(ℬ i))
      (Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ i) ((f : (a : A) → B) (↑x : A)) ⋯ : ↥(ℬ i))
      (Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ i) ((f : (a : A) → B) (↑y : A)) ⋯ : ↥(ℬ i))
have a : (↑(Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ i) ((f : (a : A) → B) (↑(x + y) : A)) sorry) : B) =
  (↑(HAdd.hAdd (α := ↥(ℬ i)) (β := ↥(ℬ i))
        (Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ i) ((f : (a : A) → B) (↑x : A)) sorry : ↥(ℬ i))
        (Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ i) ((f : (a : A) → B) (↑y : A)) sorry : ↥(ℬ i))) :
    B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.RingHom (goal)
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_6
τ : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : SetLike σ A
inst_3 : SetLike τ B
inst_4 : DecidableEq ι
inst_5 : AddMonoid ι
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_8 : GradedRing 𝒜
inst_9 : GradedRing ℬ
F : Type u_10
inst_10 : FunLike F A B
inst_11 : GradedFunLike F 𝒜 ℬ
inst_12 : RingHomClass F A B
f : F
x : A
⊢ Eq (α := ⨁ (i : ι), ↥(ℬ i)) ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) ((f : (a : A) → B) x) : ⨁ (i : ι), ↥(ℬ i))
    ((map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
          (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
        ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) :
      ⨁ (i : ι), ↥(ℬ i))
have rw : Eq (α := ⨁ (i : ι), ↥(ℬ i))
  (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
    (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i))
      ((f : (a : A) → B)
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)))
  (∑ x_1 ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
    (map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
        (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
      ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x_1) : A)))
Tactic: rw [← DirectSum.sum_support_decompose 𝒜 x, map_sum, DirectSum.decompose_sum,
    DirectSum.decompose_sum, map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.RingHom (goal)
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_6
τ : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : SetLike σ A
inst_3 : SetLike τ B
inst_4 : DecidableEq ι
inst_5 : AddMonoid ι
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_8 : GradedRing 𝒜
inst_9 : GradedRing ℬ
F : Type u_10
inst_10 : FunLike F A B
inst_11 : GradedFunLike F 𝒜 ℬ
inst_12 : RingHomClass F A B
f : F
x : A
⊢ Eq (α := ⨁ (i : ι), ↥(ℬ i))
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
      (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i))
        ((f : (a : A) → B)
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)))
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
      (map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
          (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
        ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x_1) : A)))
have e_f : Eq (α := ι → ⨁ (i : ι), ↥(ℬ i))
  (fun (i : ι) ↦
    (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i))
      ((f : (a : A) → B)
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)))
  fun (x_1 : ι) ↦
  (map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
      (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
    ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x_1) : A))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.RingHom (goal)
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_6
τ : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : SetLike σ A
inst_3 : SetLike τ B
inst_4 : DecidableEq ι
inst_5 : AddMonoid ι
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_8 : GradedRing 𝒜
inst_9 : GradedRing ℬ
F : Type u_10
inst_10 : FunLike F A B
inst_11 : GradedFunLike F 𝒜 ℬ
inst_12 : RingHomClass F A B
f : F
x : A
⊢ Eq (α := ⨁ (i : ι), ↥(ℬ i)) ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) ((f : (a : A) → B) x) : ⨁ (i : ι), ↥(ℬ i))
    ((map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
          (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
        ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) :
      ⨁ (i : ι), ↥(ℬ i))
have rw : Eq (α := ⨁ (i : ι), ↥(ℬ i))
  ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i))
      ((f : (a : A) → B)
        (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A))) :
    ⨁ (i : ι), ↥(ℬ i))
  ((map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
        (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
      ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
        (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A))) :
    ⨁ (i : ι), ↥(ℬ i))
Tactic: classical
  rw [← DirectSum.sum_support_decompose 𝒜 x, map_sum, DirectSum.decompose_sum,
    DirectSum.decompose_sum, map_sum]
  congr 1
  simp [DirectSum.decompose_of_mem _ (map_mem f (Subtype.prop _)),
    DirectSum.decompose_of_mem _ (Subtype.prop _), DirectSum.map_of, GradedRingHom.gradedAddHom]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.RingHom (goal)
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_6
τ : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : SetLike σ A
inst_3 : SetLike τ B
inst_4 : DecidableEq ι
inst_5 : AddMonoid ι
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_8 : GradedRing 𝒜
inst_9 : GradedRing ℬ
F : Type u_10
inst_10 : FunLike F A B
inst_11 : GradedFunLike F 𝒜 ℬ
inst_12 : RingHomClass F A B
f : F
x : A
rw :
  Eq (α := ⨁ (i : ι), ↥(ℬ i))
    ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i))
        ((f : (a : A) → B)
          (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A))) :
      ⨁ (i : ι), ↥(ℬ i))
    ((map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
          (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
        ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
          (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A))) :
      ⨁ (i : ι), ↥(ℬ i))
⊢ Eq (α := ⨁ (i : ι), ↥(ℬ i)) ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) ((f : (a : A) → B) x) : ⨁ (i : ι), ↥(ℬ i))
    ((map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
          (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
        ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) :
      ⨁ (i : ι), ↥(ℬ i))
have rw₁ : Eq (α := ⨁ (i : ι), ↥(ℬ i))
  ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i))
      (∑ x_1 ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
        (f : (a : A) → B)
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x_1) : A)) :
    ⨁ (i : ι), ↥(ℬ i))
  ((map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
        (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
      ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
        (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A))) :
    ⨁ (i : ι), ↥(ℬ i))
Tactic: classical
  rw [← DirectSum.sum_support_decompose 𝒜 x, map_sum, DirectSum.decompose_sum,
    DirectSum.decompose_sum, map_sum]
  congr 1
  simp [DirectSum.decompose_of_mem _ (map_mem f (Subtype.prop _)),
    DirectSum.decompose_of_mem _ (Subtype.prop _), DirectSum.map_of, GradedRingHom.gradedAddHom]