awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
b a₁ a₂ : B
ha₂ : Membership.mem (γ := Submodule B B) (Submodule.span B ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A))) a₂
ih :
  ∀ (i : ι),
    Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
      (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₂ :
                DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
              (a : ι) → ↥(ℬ a))
            i) :
        B)
i : ι
⊢ Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
    (∑
      ij ∈
        SProd.sprod (α := Finset ι) (β := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(ℬ i))
            ((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₁))
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(ℬ i))
            ((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₂)) with
      ij.1 + ij.2 = i,
      (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₁ :
                  DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
                (a : ι) → ↥(ℬ a))
              ij.1) :
          B) *
        (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₂ :
                  DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
                (a : ι) → ↥(ℬ a))
              ij.2) :
          B))

Tactic:
exact sum_mem fun ij hij ↦ Ideal.mul_mem_left _ _ <| ih _

Premises used: Ideal.map, Ideal.mul_mem_left, HomogeneousIdeal.toIdeal, sum_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal ℬ
n : ι
a : A
ha : Membership.mem (γ := Submodule A A) (Ideal.comap f I.toIdeal) a
rw :
  (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) ((f : (a : A) → B) a) :
              DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          n) :
      B) ∈
    I
⊢ Membership.mem (γ := Submodule A A) (Ideal.comap f I.toIdeal)
    (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) a :
              DirectSum.{u_7, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          n) :
      A)

Tactic:
rw [Ideal.mem_comap, HomogeneousIdeal.mem_iff, f.map_directSumDecompose]

Premises used: GradedRingHom.map_directSumDecompose, Ideal.mem_comap, HomogeneousIdeal.mem_iff
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal ℬ
n : ι
a : A
ha : Membership.mem (γ := Submodule A A) (Ideal.comap f I.toIdeal) a
⊢ (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) ((f : (a : A) → B) a) :
              DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          n) :
      B) ∈
    I

Tactic:
I.2 _ ha

Premises used: Set.Mem, HomogeneousSubmodule.is_homogeneous'
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal ℬ
n : ι
a : A
ha : Membership.mem (γ := Submodule A A) (Ideal.comap f I.toIdeal) a
⊢ (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) ((f : (a : A) → B) a) :
              DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          n) :
      B) ∈
    I

Tactic:
exact I.2 _ ha

Premises used: HomogeneousSubmodule.is_homogeneous'
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
σ : Type u_4
τ : Type u_5
ι : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : SetLike σ A
inst_3 : SetLike τ B
inst_4 : AddSubmonoidClass σ A
inst_5 : AddSubmonoidClass τ B
inst_6 : DecidableEq ι
inst_7 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
inst_8 : GradedRing 𝒜
inst_9 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
I : HomogeneousIdeal 𝒜
J : HomogeneousIdeal ℬ
⊢ map f I ≤ J ↔ I ≤ comap f J

Tactic:
Ideal.map_le_iff_le_comap

Premises used: Set.Mem, Ideal.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
σ : Type u_4
τ : Type u_5
ι : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : SetLike σ A
inst_3 : SetLike τ B
inst_4 : AddSubmonoidClass σ A
inst_5 : AddSubmonoidClass τ B
inst_6 : DecidableEq ι
inst_7 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
inst_8 : GradedRing 𝒜
inst_9 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
⊢ GaloisConnection (α := HomogeneousIdeal 𝒜) (β := HomogeneousIdeal ℬ) (map f) (comap f)

Tactic:
fun _ _ ↦
  map_le_iff_le_comap f

Premises used: HomogeneousIdeal.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
σ : Type u_4
τ : Type u_5
ι : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : SetLike σ A
inst_3 : SetLike τ B
inst_4 : AddSubmonoidClass σ A
inst_5 : AddSubmonoidClass τ B
inst_6 : DecidableEq ι
inst_7 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
inst_8 : GradedRing 𝒜
inst_9 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
⊢ Monotone (α := HomogeneousIdeal 𝒜) (β := HomogeneousIdeal ℬ) (map f)

Tactic:
(gc_map_comap f).monotone_l

Premises used: HomogeneousIdeal.gc_map_comap, GaloisConnection.monotone_l
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
σ : Type u_4
τ : Type u_5
ι : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : SetLike σ A
inst_3 : SetLike τ B
inst_4 : AddSubmonoidClass σ A
inst_5 : AddSubmonoidClass τ B
inst_6 : DecidableEq ι
inst_7 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
inst_8 : GradedRing 𝒜
inst_9 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
⊢ Monotone (α := HomogeneousIdeal ℬ) (β := HomogeneousIdeal 𝒜) (comap f)

Tactic:
(gc_map_comap f).monotone_u

Premises used: GaloisConnection.monotone_u, HomogeneousIdeal.gc_map_comap
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
σ : Type u_4
τ : Type u_5
ι : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : SetLike σ A
inst_3 : SetLike τ B
inst_4 : AddSubmonoidClass σ A
inst_5 : AddSubmonoidClass τ B
inst_6 : DecidableEq ι
inst_7 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
inst_8 : GradedRing 𝒜
inst_9 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
J : HomogeneousIdeal ℬ
⊢ toIdeal (comap f J) = Ideal.comap f J.toIdeal

Tactic:
rfl

Premises used: Ideal.comap, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
σ : Type u_4
τ : Type u_5
ι : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : SetLike σ A
inst_3 : SetLike τ B
inst_4 : AddSubmonoidClass σ A
inst_5 : AddSubmonoidClass τ B
inst_6 : DecidableEq ι
inst_7 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
inst_8 : GradedRing 𝒜
inst_9 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
J : HomogeneousIdeal ℬ
⊢ (↑(comap f J) : Set A) = (⇑f : (a : A) → B) ⁻¹' (↑J : Set B)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
σ : Type u_4
τ : Type u_5
ι : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : SetLike σ A
inst_3 : SetLike τ B
inst_4 : AddSubmonoidClass σ A
inst_5 : AddSubmonoidClass τ B
inst_6 : DecidableEq ι
inst_7 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
inst_8 : GradedRing 𝒜
inst_9 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
I : HomogeneousIdeal 𝒜
⊢ toIdeal (map f I) = Ideal.map f I.toIdeal

Tactic:
rfl

Premises used: Ideal.map, Submodule.span, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I I₁ I₂ I₃ : HomogeneousIdeal 𝒜
J J₁ J₂ J₃ : HomogeneousIdeal ℬ
K : HomogeneousIdeal 𝒞
inst_14 : J.toIdeal.IsPrime
⊢ (toIdeal (comap f J)).IsPrime

Tactic:
inferInstanceAs (J.toIdeal.comap f).IsPrime

Premises used: _private.0.HomogeneousIdeal.isPrime_comap._proof_1
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
σ : Type u_4
ι : Type u_7
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
⊢ map (GradedRingHom.id 𝒜) I = I

Tactic:
ext <| Ideal.map_id _

Premises used: Ideal.map_id, HomogeneousIdeal.ext
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
⊢ Eq (α := HomogeneousIdeal 𝒞) (map g (map f I)) (map (g.comp f) I)

Tactic:
ext <| Ideal.map_map _ _

Premises used: Ideal.map_map, HomogeneousIdeal.ext
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
⊢ Eq (α := HomogeneousIdeal 𝒞) (map (g.comp f) I) (map g (map f I))

Tactic:
(map_map f g).symm

Premises used: HomogeneousIdeal.map_map, Eq.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
σ : Type u_4
ι : Type u_7
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
⊢ comap (GradedRingHom.id 𝒜) I = I

Tactic:
rfl

Premises used: Set.Mem, setOf, HomogeneousIdeal.comap, Set.preimage, Ideal.comap, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
K : HomogeneousIdeal 𝒞
⊢ Eq (α := HomogeneousIdeal 𝒜) (comap f (comap g K)) (comap (g.comp f) K)

Tactic:
rfl

Premises used: Set.Mem, setOf, HomogeneousIdeal.comap, GradedRingHom.comp, Set.preimage, Ideal.comap, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddCommMonoid ι
inst_11 : PartialOrder ι
inst_12 : CanonicallyOrderedAdd ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_13 : GradedRing 𝒜
inst_14 : GradedRing ℬ
inst_15 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (map g (ℬ₊))
rw : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (map g (map f (𝒜₊)))
⊢ LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (map (g.comp f) (𝒜₊))

Tactic:
rw [map_comp]

Premises used: HomogeneousIdeal.map_comp
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddCommMonoid ι
inst_11 : PartialOrder ι
inst_12 : CanonicallyOrderedAdd ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_13 : GradedRing 𝒜
inst_14 : GradedRing ℬ
inst_15 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (map g (ℬ₊))
⊢ LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (map g (map f (𝒜₊)))

Tactic:
hg.trans <| map_mono _ hf

Premises used: HomogeneousIdeal.map_mono, LE.le.trans
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddCommMonoid ι
inst_11 : PartialOrder ι
inst_12 : CanonicallyOrderedAdd ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_13 : GradedRing 𝒜
inst_14 : GradedRing ℬ
inst_15 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (map g (ℬ₊))
⊢ LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (map g (map f (𝒜₊)))

Tactic:
exact hg.trans <| map_mono _ hf

Premises used: HomogeneousIdeal.map_mono, LE.le.trans
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
Goal:
ιM : Type u_2
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
p : Submodule A M
ℳ : ιM → σM
inst_3 : DecidableEq ιM
inst_4 : SetLike σM M
inst_5 : AddSubmonoidClass σM M
inst_6 : Decomposition ℳ
hp : p.IsHomogeneous ℳ
x : M
⊢ x ∈ p ↔
    ∀ (i : ιM),
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) i) : M) ∈ p

Tactic:
AddSubmonoidClass.IsHomogeneous.mem_iff ℳ _ hp

Premises used: DirectSum.AddSubmonoidClass.IsHomogeneous.mem_iff
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
Goal:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst_3 : DecidableEq ιA
inst_4 : AddMonoid ιA
inst_5 : SetLike σA A
inst_6 : AddSubmonoidClass σA A
inst_7 : GradedRing 𝒜
inst_8 : DecidableEq ιM
inst_9 : SetLike σM M
inst_10 : AddSubmonoidClass σM M
inst_11 : Decomposition ℳ
inst_12 : VAdd ιA ιM
inst_13 : GradedSMul 𝒜 ℳ
p : Submodule A M
hp : p.IsHomogeneous ℳ
q : Submodule A M
hq : q.IsHomogeneous ℳ
h : (↑p : Set M) = (↑q : Set M)
⊢ Eq (α := HomogeneousSubmodule 𝒜 ℳ) { toSubmodule := p, is_homogeneous' := hp }
    { toSubmodule := q, is_homogeneous' := hq }

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
Goal:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst_3 : DecidableEq ιA
inst_4 : AddMonoid ιA
inst_5 : SetLike σA A
inst_6 : AddSubmonoidClass σA A
inst_7 : GradedRing 𝒜
inst_8 : DecidableEq ιM
inst_9 : SetLike σM M
inst_10 : AddSubmonoidClass σM M
inst_11 : Decomposition ℳ
inst_12 : VAdd ιA ιM
inst_13 : GradedSMul 𝒜 ℳ
x : HomogeneousSubmodule 𝒜 ℳ
r : A
m : M
hm : m ∈ x
⊢ r • m ∈ x

Tactic:
Submodule.smul_mem x.toSubmodule r hm

Premises used: Set.Mem, Submodule.smul_mem, HomogeneousSubmodule.toSubmodule
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
Goal:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst_3 : DecidableEq ιA
inst_4 : AddMonoid ιA
inst_5 : SetLike σA A
inst_6 : AddSubmonoidClass σA A
inst_7 : GradedRing 𝒜
inst_8 : DecidableEq ιM
inst_9 : SetLike σM M
inst_10 : AddSubmonoidClass σM M
inst_11 : Decomposition ℳ
inst_12 : VAdd ιA ιM
inst_13 : GradedSMul 𝒜 ℳ
x : HomogeneousSubmodule 𝒜 ℳ
r : A
m : M
hm : m ∈ x
⊢ r • m ∈ x

Tactic:
exact Submodule.smul_mem x.toSubmodule r hm

Premises used: Submodule.smul_mem, HomogeneousSubmodule.toSubmodule
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
Goal:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst_3 : DecidableEq ιA
inst_4 : AddMonoid ιA
inst_5 : SetLike σA A
inst_6 : AddSubmonoidClass σA A
inst_7 : GradedRing 𝒜
inst_8 : DecidableEq ιM
inst_9 : SetLike σM M
inst_10 : AddSubmonoidClass σM M
inst_11 : Decomposition ℳ
inst_12 : VAdd ιA ιM
inst_13 : GradedSMul 𝒜 ℳ
p : HomogeneousSubmodule 𝒜 ℳ
⊢ p.IsHomogeneous ℳ

Tactic:
p.is_homogeneous'

Premises used: HomogeneousSubmodule.is_homogeneous'
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
Goal:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst_3 : DecidableEq ιA
inst_4 : AddMonoid ιA
inst_5 : SetLike σA A
inst_6 : AddSubmonoidClass σA A
inst_7 : GradedRing 𝒜
inst_8 : DecidableEq ιM
inst_9 : SetLike σM M
inst_10 : AddSubmonoidClass σM M
inst_11 : Decomposition ℳ
inst_12 : VAdd ιA ιM
inst_13 : GradedSMul 𝒜 ℳ
x_1 x_2 : HomogeneousSubmodule 𝒜 ℳ
x : Submodule A M
hx : x.IsHomogeneous ℳ
y : Submodule A M
hy : y.IsHomogeneous ℳ
h : x = y
⊢ Eq (α := HomogeneousSubmodule 𝒜 ℳ) { toSubmodule := x, is_homogeneous' := hx }
    { toSubmodule := y, is_homogeneous' := hy }

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
Goal:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst_3 : DecidableEq ιA
inst_4 : AddMonoid ιA
inst_5 : SetLike σA A
inst_6 : AddSubmonoidClass σA A
inst_7 : GradedRing 𝒜
inst_8 : DecidableEq ιM
inst_9 : SetLike σM M
inst_10 : AddSubmonoidClass σM M
inst_11 : Decomposition ℳ
inst_12 : VAdd ιA ιM
inst_13 : GradedSMul 𝒜 ℳ
I J : HomogeneousSubmodule 𝒜 ℳ
h : I.toSubmodule = J.toSubmodule
⊢ I = J

Tactic:
HomogeneousSubmodule.toSubmodule_injective _ _ h

Premises used: HomogeneousSubmodule.toSubmodule_injective
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
Goal:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst_3 : DecidableEq ιA
inst_4 : AddMonoid ιA
inst_5 : SetLike σA A
inst_6 : AddSubmonoidClass σA A
inst_7 : GradedRing 𝒜
inst_8 : DecidableEq ιM
inst_9 : SetLike σM M
inst_10 : AddSubmonoidClass σM M
inst_11 : Decomposition ℳ
inst_12 : VAdd ιA ιM
inst_13 : GradedSMul 𝒜 ℳ
I J : HomogeneousSubmodule 𝒜 ℳ
h : ∀ (i : ιM), ∀ x ∈ ℳ i, x ∈ I ↔ x ∈ J
h₁ : ∀ (x : M), x ∈ I.toSubmodule ↔ x ∈ J.toSubmodule
⊢ I = J

Tactic:
ext
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
Goal:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst_3 : DecidableEq ιA
inst_4 : AddMonoid ιA
inst_5 : SetLike σA A
inst_6 : AddSubmonoidClass σA A
inst_7 : GradedRing 𝒜
inst_8 : DecidableEq ιM
inst_9 : SetLike σM M
inst_10 : AddSubmonoidClass σM M
inst_11 : Decomposition ℳ
inst_12 : VAdd ιA ιM
inst_13 : GradedSMul 𝒜 ℳ
I J : HomogeneousSubmodule 𝒜 ℳ
h : ∀ (i : ιM), ∀ x ∈ ℳ i, x ∈ I ↔ x ∈ J
x : M
h₁ :
  (∀ (i : ιM),
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) i) : M) ∈
        I.toSubmodule) ↔
    ∀ (i : ιM),
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) i) : M) ∈
        J.toSubmodule
⊢ x ∈ I.toSubmodule ↔ x ∈ J.toSubmodule

Tactic:
rw [I.isHomogeneous.mem_iff, J.isHomogeneous.mem_iff]

Premises used: HomogeneousSubmodule.isHomogeneous, Submodule.IsHomogeneous.mem_iff
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
Goal:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst_3 : DecidableEq ιA
inst_4 : AddMonoid ιA
inst_5 : SetLike σA A
inst_6 : AddSubmonoidClass σA A
inst_7 : GradedRing 𝒜
inst_8 : DecidableEq ιM
inst_9 : SetLike σM M
inst_10 : AddSubmonoidClass σM M
inst_11 : Decomposition ℳ
inst_12 : VAdd ιA ιM
inst_13 : GradedSMul 𝒜 ℳ
I J : HomogeneousSubmodule 𝒜 ℳ
h : ∀ (i : ιM), ∀ x ∈ ℳ i, x ∈ I ↔ x ∈ J
x : M
h₁ :
  ∀ (a : ιM),
    (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) a) : M) ∈
        I.toSubmodule ↔
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) a) : M) ∈
        J.toSubmodule
⊢ (∀ (i : ιM),
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) i) : M) ∈
        I.toSubmodule) ↔
    ∀ (i : ιM),
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) i) : M) ∈
        J.toSubmodule

Tactic:
apply forall_congr'

Premises used: forall_congr'