awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
f : 𝒜 →+*ᵍ ℬ
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →+* B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
f : A →+* B
h : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((f : (a : A) → B) x : B)
⊢ Eq (α := (a : A) → B) (⇑{ toRingHom := f, map_mem := @h : 𝒜 →+*ᵍ ℬ } : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
F : Type u_10
inst_4 : FunLike F A B
inst_5 : GradedFunLike F 𝒜 ℬ
inst_6 : RingHomClass F A B
f : F
⊢ Eq (α := (a : A) → B) (⇑(↑f : 𝒜 →+*ᵍ ℬ) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
f : 𝒜 →+*ᵍ ℬ
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ (⇑(f.copy f' h) : (a : A) → B) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
f : 𝒜 →+*ᵍ ℬ
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
f g : 𝒜 →+*ᵍ ℬ
h : f = g
x : A
⊢ Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) x : B) ((g : (a : A) → B) x : B)

Tactic:
DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
f : 𝒜 →+*ᵍ ℬ
x y : A
h : x = y
⊢ Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)

Tactic:
DFunLike.congr_arg f h

Premises used: DFunLike.congr_arg
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
f g : 𝒜 →+*ᵍ ℬ
h : Eq (α := (a : A) → B) (⇑f : (a : A) → B) (⇑g : (a : A) → B)
⊢ f = g

Tactic:
DFunLike.coe_injective h

Premises used: DFunLike.coe_injective
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
f g : 𝒜 →+*ᵍ ℬ
⊢ (∀ (x : A), Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) x : B) ((g : (a : A) → B) x : B)) → f = g

Tactic:
DFunLike.ext _ _

Premises used: DFunLike.ext
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
f : 𝒜 →+*ᵍ ℬ
h₁ : Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
h₂ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_one' := h₁ : OneHom A B }.toFun (x * y) =
      { toFun := (⇑f : (a : A) → B), map_one' := h₁ : OneHom A B }.toFun x *
        { toFun := (⇑f : (a : A) → B), map_one' := h₁ : OneHom A B }.toFun y
h₃ : (↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun 0 = 0
h₄ :
  ∀ (x y : A),
    (↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun (x + y) =
      (↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun x +
        (↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun y
h₅ :
  ∀ {i : ι} {x : A},
    x ∈ 𝒜 i →
      Membership.mem.{u_3, u_7} (α := B) (ℬ i)
        (({ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ : A →+* B } :
              (a : A) → B)
            x :
          B)
⊢ { toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, map_mem := @h₅ :
      𝒜 →+*ᵍ ℬ } =
    f

Tactic:
ext fun _ => rfl

Premises used: GradedRingHom.ext, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
⊢ Function.Injective (β := A →+* B) fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑f : A →+* B)

Tactic:
fun _ _ h =>
  ext <| DFunLike.congr_fun (F := A →+* B) h

Premises used: DFunLike.congr_fun, GradedRingHom.ext, Function.Injective
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
f : 𝒜 →+*ᵍ ℬ
⊢ Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 0 : B) (0 : B)

Tactic:
map_zero f

Premises used: map_zero
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
f : 𝒜 →+*ᵍ ℬ
⊢ Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)

Tactic:
map_one f

Premises used: map_one
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
f : 𝒜 →+*ᵍ ℬ
a b : A
⊢ (f : (a : A) → B) (a + b) = HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)

Tactic:
map_add ..

Premises used: map_add
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
f : 𝒜 →+*ᵍ ℬ
a b : A
⊢ (f : (a : A) → B) (a * b) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)

Tactic:
map_mul ..

Premises used: map_mul
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_10
B : Type u_11
σ : Type u_12
τ : Type u_13
inst : Ring A
inst_1 : Ring B
inst_2 : SetLike σ A
inst_3 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
f : 𝒜 →+*ᵍ ℬ
x : A
⊢ Eq.{u_11 + 1} (α := B) ((f : (a : A) → B) (-x) : B) (-(f : (a : A) → B) x : B)

Tactic:
map_neg f x

Premises used: map_neg
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_10
B : Type u_11
σ : Type u_12
τ : Type u_13
inst : Ring A
inst_1 : Ring B
inst_2 : SetLike σ A
inst_3 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
f : 𝒜 →+*ᵍ ℬ
x y : A
⊢ (f : (a : A) → B) (x - y) = HSub.hSub (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)

Tactic:
map_sub f x y

Premises used: map_sub
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_6
inst : Semiring A
inst_1 : SetLike σ A
𝒜 : ι → σ
⊢ Eq (α := (a : A) → A) (⇑(id 𝒜) : (a : A) → A) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_6
inst : Semiring A
inst_1 : SetLike σ A
𝒜 : ι → σ
x : A
⊢ (id 𝒜 : (a : A) → A) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_6
inst : Semiring A
inst_1 : SetLike σ A
𝒜 : ι → σ
⊢ Eq (α := A →+* A) (↑(id 𝒜) : A →+* A) (RingHom.id A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
h : 𝒞 →+*ᵍ 𝒟
g : ℬ →+*ᵍ 𝒞
f : 𝒜 →+*ᵍ ℬ
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
rfl

Premises used: GradedRingHom.comp, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
hnp : ℬ →+*ᵍ 𝒞
hmn : 𝒜 →+*ᵍ ℬ
⊢ Eq (α := (a : A) → C) (⇑(hnp.comp hmn) : (a : A) → C)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := B) (⇑hnp : (a : B) → C) (⇑hmn : (a : A) → B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
hnp : ℬ →+*ᵍ 𝒞
hmn : 𝒜 →+*ᵍ ℬ
x : A
⊢ Eq.{u_4 + 1} (α := C) ((hnp.comp hmn : (a : A) → C) x : C) ((hnp : (a : B) → C) ((hmn : (a : A) → B) x : B) : C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
f : 𝒜 →+*ᵍ ℬ
⊢ f.comp (id 𝒜) = f

Tactic:
ext fun _ => rfl

Premises used: GradedRingHom.ext, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
𝒜 : ι → σ
ℬ : ι → τ
f : 𝒜 →+*ᵍ ℬ
⊢ comp (id ℬ) f = f

Tactic:
ext fun _ => rfl

Premises used: GradedRingHom.ext, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_6
inst : Semiring A
inst_1 : SetLike σ A
𝒜 : ι → σ
⊢ Eq (α := 𝒜 →+*ᵍ 𝒜) 1 (id 𝒜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_6
inst : Semiring A
inst_1 : SetLike σ A
𝒜 : ι → σ
f g : 𝒜 →+*ᵍ 𝒜
⊢ f * g = f.comp g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_6
inst : Semiring A
inst_1 : SetLike σ A
𝒜 : ι → σ
⊢ Eq.{u_2 + 1} (α := (a : A) → A) (⇑1 : (a : A) → A) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_6
inst : Semiring A
inst_1 : SetLike σ A
𝒜 : ι → σ
f g : 𝒜 →+*ᵍ 𝒜
⊢ Eq (α := (a : A) → A) (⇑(f * g) : (a : A) → A) (Function.comp (β := A) (⇑f : (a : A) → A) (⇑g : (a : A) → A))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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)
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)
⊢ Eq (α := A → A) (⇑f : (a : A) → A)^[n] (⇑(npowRec n f) : (a : A) → A)

Tactic:
induction n
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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 : 𝒜 →+*ᵍ 𝒜
⊢ Eq (α := A → A) (⇑f : (a : A) → A)^[0] (⇑(npowRec 0 f) : (a : A) → A)

Tactic:
simp [npowRec, *]

Premises used: npowRec
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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 : 𝒜 →+*ᵍ 𝒜
n : ℕ
h : 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:
simp [npowRec, *]

Premises used: npowRec
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_6
inst : Semiring A
inst_1 : SetLike σ A
𝒜 : ι → σ
f : 𝒜 →+*ᵍ 𝒜
n : ℕ
⊢ Eq (α := (a : A) → A) (⇑(f ^ n) : (a : A) → A) (⇑f : (a : A) → A)^[n]

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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₁ g₂ : ℬ →+*ᵍ 𝒞
f : 𝒜 →+*ᵍ ℬ
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => ext <| hf.forall.2 (GradedRingHom.ext_iff.1 h), fun h => h ▸ rfl⟩

Premises used: Iff.mpr, Function.Surjective.forall, Eq.rec, GradedRingHom.ext, Iff.intro, Iff.mp, GradedRingHom.ext_iff, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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)
rw₂ 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)
⊢ 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]

Premises used: GradedRingHom.comp_apply
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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 : ι
a :
  Eq.{u_3 + 1} (α := B) ((↑(Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ i) ((f : (a : A) → B) (↑0 : A)) ⋯) : B) : B)
    ((↑0 : B) : B)
⊢ Eq.{u_3 + 1} (α := ↥(ℬ i)) (Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ i) ((f : (a : A) → B) (↑0 : A)) ⋯ : ↥(ℬ i))
    (0 : ↥(ℬ i))

Tactic:
ext
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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} (α := B) ((↑(Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ i) ((f : (a : A) → B) (↑0 : A)) ⋯) : B) : B)
    ((↑0 : B) : B)

Tactic:
simp
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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)
a :
  (↑(Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ i) ((f : (a : A) → B) (↑(x + y) : A)) ⋯) : B) =
    (↑(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))) :
      B)
⊢ 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))

Tactic:
ext
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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)) ⋯) : B) =
    (↑(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))) :
      B)

Tactic:
simp
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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))
    (∑ 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)))
⊢ 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))

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 x, map_sum, DirectSum.decompose_sum,
    DirectSum.decompose_sum, map_sum]

Premises used: map_sum, DirectSum.sum_support_decompose, DirectSum.decompose_sum
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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
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))
⊢ 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:
congr 1
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
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))
    (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:
simp [DirectSum.decompose_of_mem _ (map_mem f (Subtype.prop _)),
    DirectSum.decompose_of_mem _ (Subtype.prop _), DirectSum.map_of, GradedRingHom.gradedAddHom]

Premises used: DirectSum.decompose_of_mem, DirectSum.map_of, Graded.map_mem, Subtype.prop, GradedRingHom.gradedAddHom