awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
V : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
𝒞 : ι → Submodule R C
𝒟 : ι → Submodule R D
inst_11 : GradedAlgebra 𝒜
inst_12 : GradedAlgebra ℬ
inst_13 : GradedAlgebra 𝒞
inst_14 : GradedAlgebra 𝒟
f g : 𝒜 →ₐᵍ[R] ℬ
h :
  Eq (α := (a : A) → B) ((fun (f : 𝒜 →ₐᵍ[R] ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) f)
    ((fun (f : 𝒜 →ₐᵍ[R] ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) g)
rcases :
  ∀ (toFun : A → B) (map_one' : toFun 1 = 1)
    (map_mul' :
      ∀ (x y : A),
        { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun (x * y) =
          { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun x *
            { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun y)
    (map_zero' : (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun 0 = 0)
    (map_add' :
      ∀ (x y : A),
        (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun (x + y) =
          (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun x +
            (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun y)
    (commutes' :
      ∀ (r : R),
        (↑(↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add' :
                        A →+* B } :
                    A →* B) :
                OneHom A B).toFun
            ((algebraMap R A : (a : R) → A) r) =
          (algebraMap R B : (a : R) → B) r)
    (map_mem :
      ∀ {i : ι} {x : A},
        x ∈ 𝒜 i →
          Membership.mem (α := B) (ℬ i)
            (({ toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero',
                      map_add' := map_add', commutes' := commutes' : A →ₐ[R] B }.toRingHom :
                  (a : A) → B)
                x :
              B))
    (h :
      Eq (α := (a : A) → B)
        ((fun (f : 𝒜 →ₐᵍ[R] ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
          { toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
            commutes' := commutes', map_mem := @map_mem })
        ((fun (f : 𝒜 →ₐᵍ[R] ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) g)),
    { toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
        commutes' := commutes', map_mem := @map_mem } =
      g
⊢ f = g

Tactic:
rcases f with ⟨⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩, _⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
F : Type u_11
inst_9 : FunLike F A B
inst_10 : GradedFunLike F 𝒜 ℬ
inst_11 : AlgHomClass F R A B
f : F
⊢ (↑(ofClass f) : A →ₐ[R] B) = (↑f : A →ₐ[R] B)

Tactic:
rfl

Premises used: AlgHomClass.toAlgHom, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
F : Type u_11
inst_9 : FunLike F A B
inst_10 : GradedFunLike F 𝒜 ℬ
inst_11 : AlgHomClass F R A B
f : F
⊢ toGradedRingHom (ofClass f) = (↑f : 𝒜 →+*ᵍ ℬ)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, GradedRingHom.ofClass, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
F : Type u_11
inst_9 : FunLike F A B
inst_10 : GradedFunLike F 𝒜 ℬ
inst_11 : AlgHomClass F R A B
f : F
⊢ Eq (α := (a : A) → B) (⇑(ofClass f) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
f : 𝒜 →ₐᵍ[R] ℬ
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →ₐ[R] B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
f : A →ₐ[R] B
h : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem (α := B) (ℬ i) ((f.toRingHom : (a : A) → B) x : B)
⊢ Eq (α := (a : A) → B) (⇑{ toAlgHom := f, map_mem := @h } : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
f : A → B
h₁ : f 1 = 1
h₂ :
  ∀ (x y : A),
    { toFun := f, map_one' := h₁ : OneHom A B }.toFun (x * y) =
      { toFun := f, map_one' := h₁ : OneHom A B }.toFun x * { toFun := f, map_one' := h₁ : OneHom A B }.toFun y
h₃ : (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun 0 = 0
h₄ :
  ∀ (x y : A),
    (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun (x + y) =
      (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun x +
        (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun y
h₅ :
  ∀ (r : R),
    (↑(↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ : A →+* B } : A →* B) :
            OneHom A B).toFun
        ((algebraMap R A : (a : R) → A) r) =
      (algebraMap R B : (a : R) → B) r
h₆ :
  ∀ {i : ι} {x : A},
    x ∈ 𝒜 i →
      Membership.mem (α := B) (ℬ i)
        (({ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ :
                  A →ₐ[R] B }.toRingHom :
              (a : A) → B)
            x :
          B)
⊢ (⇑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_mem := @h₆ } :
      (a : A) → B) =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
f : A →ₐ[R] B
h : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem (α := B) (ℬ i) ((f.toRingHom : (a : A) → B) x : B)
⊢ (↑{ toAlgHom := f, map_mem := @h : 𝒜 →ₐᵍ[R] ℬ } : A →ₐ[R] B) = f

Tactic:
dsimp only
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
⊢ Function.Injective (α := 𝒜 →ₐᵍ[R] ℬ) (β := (a : A) → B) (DFunLike.coe (β := fun (x : A) ↦ B))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
f₁ f₂ : 𝒜 →ₐᵍ[R] ℬ
⊢ Eq (α := (a : A) → B) (⇑f₁ : (a : A) → B) (⇑f₂ : (a : A) → B) ↔ f₁ = f₂

Tactic:
DFunLike.coe_fn_eq

Premises used: DFunLike.coe_fn_eq
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
⊢ Function.Injective (α := 𝒜 →ₐᵍ[R] ℬ) toAlgHom

Tactic:
fun _ _ h ↦ coe_fn_injective congr($h)

Premises used: congrArg, id, Function.Injective, DFunLike.coe, GradedAlgHom.coe_fn_injective
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
⊢ Function.Injective (α := 𝒜 →ₐᵍ[R] ℬ) toGradedRingHom

Tactic:
fun _ _ h ↦ coe_fn_injective congr($h)

Premises used: congrArg, id, Function.Injective, DFunLike.coe, GradedAlgHom.coe_fn_injective
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
⊢ Function.Injective (β := A →ₗ[R] B) fun (x : 𝒜 →ₐᵍ[R] ℬ) ↦
    (↑x : [inst_9 : FunLike (𝒜 →ₐᵍ[R] ℬ) A B] → [SemilinearMapClass (𝒜 →ₐᵍ[R] ℬ) (RingHom.id R) A B] → A →ₗ[R] B)

Tactic:
AlgHom.toLinearMap_injective.comp coe_algHom_injective

Premises used: AlgHom.toLinearMap, GradedAlgHom.coe_algHom_injective, AlgHom.toLinearMap_injective, SemilinearMapClass.semilinearMap, Function.Injective.comp
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
⊢ Function.Injective (α := 𝒜 →ₐᵍ[R] ℬ) (β := A →+* B) RingHomClass.toRingHom

Tactic:
AlgHom.coe_ringHom_injective.comp coe_algHom_injective

Premises used: AlgHom.coe_ringHom_injective, GradedAlgHom.coe_algHom_injective, MonoidHomClass.toMonoidHom, Function.Injective.comp, RingHomClass.toRingHom
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
⊢ Function.Injective (α := 𝒜 →ₐᵍ[R] ℬ) (β := A →* B) MonoidHomClass.toMonoidHom

Tactic:
AlgHom.coe_monoidHom_injective.comp coe_algHom_injective

Premises used: GradedAlgHom.coe_algHom_injective, MonoidHomClass.toMonoidHom, Function.Injective.comp, AlgHom.coe_monoidHom_injective
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
⊢ Function.Injective (α := 𝒜 →ₐᵍ[R] ℬ) (β := A →+ B) AddMonoidHomClass.toAddMonoidHom

Tactic:
AlgHom.coe_addMonoidHom_injective.comp coe_algHom_injective

Premises used: AlgHom.coe_addMonoidHom_injective, AddMonoidHomClass.toAddMonoidHom, GradedAlgHom.coe_algHom_injective, Function.Injective.comp
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
f₁ f₂ : 𝒜 →ₐᵍ[R] ℬ
H : f₁ = f₂
x : A
⊢ Eq.{u_7 + 1} (α := B) ((f₁ : (a : A) → B) x : B) ((f₂ : (a : A) → B) x : B)

Tactic:
DFunLike.congr_fun H x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
f : 𝒜 →ₐᵍ[R] ℬ
x y : A
h : x = y
⊢ Eq.{u_7 + 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.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
f₁ f₂ : 𝒜 →ₐᵍ[R] ℬ
H : ∀ (x : A), Eq.{u_7 + 1} (α := B) ((f₁ : (a : A) → B) x : B) ((f₂ : (a : A) → B) x : B)
⊢ f₁ = f₂

Tactic:
DFunLike.ext _ _ H

Premises used: DFunLike.ext
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
f : 𝒜 →ₐᵍ[R] ℬ
h₁ : Eq.{u_7 + 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₅ :
  ∀ (r : R),
    (↑(↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ : A →+* B } :
                A →* B) :
            OneHom A B).toFun
        ((algebraMap R A : (a : R) → A) r) =
      (algebraMap R B : (a : R) → B) r
h₆ :
  ∀ {i : ι} {x : A},
    x ∈ 𝒜 i →
      Membership.mem (α := B) (ℬ i)
        (({ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                  commutes' := h₅ : A →ₐ[R] B }.toRingHom :
              (a : A) → B)
            x :
          B)
⊢ { toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅,
      map_mem := @h₆ } =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
f : 𝒜 →ₐᵍ[R] ℬ
r : R
⊢ Eq.{u_7 + 1} (α := B) ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
    ((algebraMap R B : (a : R) → B) r : B)

Tactic:
f.commutes' r

Premises used: AlgHom.commutes', GradedAlgHom.toAlgHom
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
f : 𝒜 →ₐᵍ[R] ℬ
⊢ (↑f : A →ₐ[R] B).comp (Algebra.ofId R A) = Algebra.ofId R B

Tactic:
AlgHom.ext f.commutes

Premises used: GradedAlgHom.commutes, AlgHom.ext
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
f : 𝒜 →+*ᵍ ℬ
h : ∀ (c : R) (x : A), (f : (a : A) → B) (c • x) = HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B)
⊢ Eq (α := (a : A) → B) (⇑(mk' f h) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
⊢ Eq (α := (a : A) → A) (⇑(GradedAlgHom.id R 𝒜) : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
⊢ (↑(GradedAlgHom.id R 𝒜) : A →ₐ[R] A) = AlgHom.id R A

Tactic:
rfl

Premises used: AlgHom.id, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
C : Type u_8
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
inst_7 : DecidableEq ι
inst_8 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_9 : GradedAlgebra 𝒜
inst_10 : GradedAlgebra ℬ
g : B →ₐ[R] C
f : 𝒜 →ₐᵍ[R] ℬ
⊢ Eq (α := (a : A) → C) (⇑(g.comp (↑f : A →ₐ[R] B)) : (a : A) → C)
    (Function.comp.{u_6 + 1, u_7 + 1, u_8 + 1} (β := B) (⇑g : (a : B) → C) (⇑f : (a : A) → B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
C : Type u_8
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
inst_7 : DecidableEq ι
inst_8 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
𝒞 : ι → Submodule R C
inst_9 : GradedAlgebra 𝒜
inst_10 : GradedAlgebra ℬ
inst_11 : GradedAlgebra 𝒞
g : ℬ →ₐᵍ[R] 𝒞
f : 𝒜 →ₐᵍ[R] ℬ
⊢ (g.comp f).toGradedRingHom = g.toGradedRingHom.comp f.toGradedRingHom

Tactic:
rfl

Premises used: GradedRingHom.comp, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
C : Type u_8
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
inst_7 : DecidableEq ι
inst_8 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
𝒞 : ι → Submodule R C
inst_9 : GradedAlgebra 𝒜
inst_10 : GradedAlgebra ℬ
inst_11 : GradedAlgebra 𝒞
g : ℬ →ₐᵍ[R] 𝒞
f : 𝒜 →ₐᵍ[R] ℬ
⊢ (↑(g.comp f) : A →ₐ[R] C) = (↑g : B →ₐ[R] C).comp (↑f : A →ₐ[R] B)

Tactic:
rfl

Premises used: AlgHom.comp, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
f : 𝒜 →ₐᵍ[R] ℬ
⊢ f.comp (GradedAlgHom.id R 𝒜) = f

Tactic:
rfl

Premises used: AlgHom.comp, GradedAlgHom.comp, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
f : 𝒜 →ₐᵍ[R] ℬ
⊢ comp (GradedAlgHom.id R ℬ) f = f

Tactic:
rfl

Premises used: AlgHom.comp, GradedAlgHom.comp, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
𝒞 : ι → Submodule R C
𝒟 : ι → Submodule R D
inst_11 : GradedAlgebra 𝒜
inst_12 : GradedAlgebra ℬ
inst_13 : GradedAlgebra 𝒞
inst_14 : GradedAlgebra 𝒟
fCD : 𝒞 →ₐᵍ[R] 𝒟
fBC : ℬ →ₐᵍ[R] 𝒞
fAB : 𝒜 →ₐᵍ[R] ℬ
⊢ (fCD.comp fBC).comp fAB = fCD.comp (fBC.comp fAB)

Tactic:
rfl

Premises used: AlgHom.comp, GradedAlgHom.comp, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
⊢ Eq.{u_6 + 1} (α := (a : A) → A) (⇑1 : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
f g : 𝒜 →ₐᵍ[R] 𝒜
⊢ 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.AlgHom
Goal:
R : Type u_1
A : Type u_6
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
f : 𝒜 →ₐᵍ[R] 𝒜
n : ℕ
h : ∀ (x : A), (f ^ Nat.zero : (a : A) → A) x = (⇑f : (a : A) → A)^[Nat.zero] x
⊢ Eq (α := (a : A) → A) (⇑(f ^ Nat.zero) : (a : A) → A) (⇑f : (a : A) → A)^[Nat.zero]

Tactic:
ext
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
f : 𝒜 →ₐᵍ[R] 𝒜
n : ℕ
x : A
⊢ (f ^ Nat.zero : (a : A) → A) x = (⇑f : (a : A) → A)^[Nat.zero] x

Tactic:
simp
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
f : 𝒜 →ₐᵍ[R] 𝒜
n x : ℕ
ih : Eq (α := (a : A) → A) (⇑(f ^ x) : (a : A) → A) (⇑f : (a : A) → A)^[x]
h : ∀ (x_1 : A), (f ^ x.succ : (a : A) → A) x_1 = (⇑f : (a : A) → A)^[x.succ] x_1
⊢ Eq (α := (a : A) → A) (⇑(f ^ x.succ) : (a : A) → A) (⇑f : (a : A) → A)^[x.succ]

Tactic:
ext