Theorem: foo_mul (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
a b : RingQuot rel
i j : ι
ha : a ∈ quotSubmodule R 𝒜 rel i
hb : b ∈ quotSubmodule R 𝒜 rel j
⊢ a * b ∈ quotSubmodule R 𝒜 rel (i + j)
Tactic:
obtain ⟨a, ha, rfl⟩ := ha
State after:
case intro.intro
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
b : RingQuot rel
i j : ι
hb : b ∈ quotSubmodule R 𝒜 rel j
a : A
ha : a ∈ ↑(𝒜 i)
⊢ (RingQuot.mkAlgHom R rel) a * b ∈ quotSubmodule R 𝒜 rel (i + j)

State before:
case intro.intro
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
b : RingQuot rel
i j : ι
hb : b ∈ quotSubmodule R 𝒜 rel j
a : A
ha : a ∈ ↑(𝒜 i)
⊢ (RingQuot.mkAlgHom R rel) a * b ∈ quotSubmodule R 𝒜 rel (i + j)
Tactic:
obtain ⟨b, hb, rfl⟩ := hb
State after:
case intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
i j : ι
a : A
ha : a ∈ ↑(𝒜 i)
b : A
hb : b ∈ ↑(𝒜 j)
⊢ (RingQuot.mkAlgHom R rel) a * (RingQuot.mkAlgHom R rel) b ∈ quotSubmodule R 𝒜 rel (i + j)

State before:
case intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
i j : ι
a : A
ha : a ∈ ↑(𝒜 i)
b : A
hb : b ∈ ↑(𝒜 j)
⊢ (RingQuot.mkAlgHom R rel) a * (RingQuot.mkAlgHom R rel) b ∈ quotSubmodule R 𝒜 rel (i + j)
Tactic:
rw [← map_mul]
State after:
case intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
i j : ι
a : A
ha : a ∈ ↑(𝒜 i)
b : A
hb : b ∈ ↑(𝒜 j)
⊢ (RingQuot.mkAlgHom R rel) (a * b) ∈ quotSubmodule R 𝒜 rel (i + j)

State before:
case intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
i j : ι
a : A
ha : a ∈ ↑(𝒜 i)
b : A
hb : b ∈ ↑(𝒜 j)
⊢ (RingQuot.mkAlgHom R rel) (a * b) ∈ quotSubmodule R 𝒜 rel (i + j)
Tactic:
exact ⟨a * b, h𝒜.mul_mem ha hb, rfl⟩
State after:
no goals