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
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
i : ι
⊢ (f : (a : A) → B)
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) x :
                DirectSum.{u_1, u_2} ι fun (i : ι) ↦ ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A) =
    (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) ((f : (a : A) → B) x) :
              DirectSum.{u_1, u_3} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          i) :
      B)

Tactic:
simp [DirectSum.decompose_map 𝒜]

Premises used: DirectSum.decompose_map
-- 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 : 𝒜 →+*ᵍ ℬ
x : A
i : ι
⊢ (f : (a : A) → B)
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) x :
                DirectSum.{u_1, u_2} ι fun (i : ι) ↦ ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A) =
    (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) ((f : (a : A) → B) x) :
              DirectSum.{u_1, u_3} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          i) :
      B)

Tactic:
_root_.map_directSumDecompose ..

Premises used: map_directSumDecompose
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : Semiring A
inst_6 : Algebra R A
𝒜 : ι → Submodule R A
inst_7 : GradedAlgebra 𝒜
i j : ι
suffices :
  LE.le (α := Submodule S (S ⊗[R] A))
    (Submodule.map₂ (M := S ⊗[R] A) (N := S ⊗[R] A)
      (↑(Algebra.lmul S (S ⊗[R] A)) :
        [inst_8 : FunLike (S ⊗[R] A →ₐ[S] Module.End S (S ⊗[R] A)) (S ⊗[R] A) (Module.End S (S ⊗[R] A))] →
          [SemilinearMapClass (S ⊗[R] A →ₐ[S] Module.End S (S ⊗[R] A)) (RingHom.id S) (S ⊗[R] A)
                (Module.End S (S ⊗[R] A))] →
            S ⊗[R] A →ₗ[S] Module.End S (S ⊗[R] A))
      (Submodule.baseChange S (𝒜 i)) (Submodule.baseChange S (𝒜 j)))
    (Submodule.baseChange S (𝒜 (i + j)))
⊢ ∀ {gi gj : S ⊗[R] A},
    Membership.mem (γ := Submodule S (S ⊗[R] A)) (Submodule.baseChange S (𝒜 i)) gi →
      Membership.mem (γ := Submodule S (S ⊗[R] A)) (Submodule.baseChange S (𝒜 j)) gj →
        Membership.mem (γ := Submodule S (S ⊗[R] A)) (Submodule.baseChange S (𝒜 (i + j))) (gi * gj)

Tactic:
suffices h : ((𝒜 i).baseChange S).map₂ (Algebra.lmul S (S ⊗[R] A)) ((𝒜 j).baseChange S) ≤
      (𝒜 (i + j)).baseChange S from fun xi xj ↦ (h <| apply_mem_map₂ _ · ·)
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : Semiring A
inst_6 : Algebra R A
𝒜 : ι → Submodule R A
inst_7 : GradedAlgebra 𝒜
i j : ι
simp_rw :
  ∀
    x ∈
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R S A : (a : S) → A →ₗ[R] S ⊗[R] A) 1) (𝒜 i)) :
        Set (S ⊗[R] A)),
    ∀
      y ∈
        (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R S A : (a : S) → A →ₗ[R] S ⊗[R] A) 1) (𝒜 j)) :
          Set (S ⊗[R] A)),
      Membership.mem (α := S ⊗[R] A)
        (↑(span S
              (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R S A : (a : S) → A →ₗ[R] S ⊗[R] A) 1)
                    (𝒜 (i + j))) :
                Set (S ⊗[R] A))) :
          Set (S ⊗[R] A))
        (((((↑(Algebra.lmul S (S ⊗[R] A)) :
                      [inst_8 : FunLike (S ⊗[R] A →ₐ[S] Module.End S (S ⊗[R] A)) (S ⊗[R] A) (Module.End S (S ⊗[R] A))] →
                        [SemilinearMapClass (S ⊗[R] A →ₐ[S] Module.End S (S ⊗[R] A)) (RingHom.id S) (S ⊗[R] A)
                              (Module.End S (S ⊗[R] A))] →
                          S ⊗[R] A →ₗ[S] Module.End S (S ⊗[R] A)) :
                    (a : S ⊗[R] A) → S ⊗[R] A →ₗ[S] S ⊗[R] A)
                  x :
                S ⊗[R] A →ₗ[S] S ⊗[R] A) :
              (a : S ⊗[R] A) → S ⊗[R] A)
            y :
          S ⊗[R] A)
⊢ LE.le (α := Submodule S (S ⊗[R] A))
    (Submodule.map₂ (M := S ⊗[R] A) (N := S ⊗[R] A)
      (↑(Algebra.lmul S (S ⊗[R] A)) :
        [inst_8 : FunLike (S ⊗[R] A →ₐ[S] Module.End S (S ⊗[R] A)) (S ⊗[R] A) (Module.End S (S ⊗[R] A))] →
          [SemilinearMapClass (S ⊗[R] A →ₐ[S] Module.End S (S ⊗[R] A)) (RingHom.id S) (S ⊗[R] A)
                (Module.End S (S ⊗[R] A))] →
            S ⊗[R] A →ₗ[S] Module.End S (S ⊗[R] A))
      (Submodule.baseChange S (𝒜 i)) (Submodule.baseChange S (𝒜 j)))
    (Submodule.baseChange S (𝒜 (i + j)))

Tactic:
simp_rw [baseChange_eq_span, map₂_span_span, span_le, Set.image2_subset_iff]

Premises used: Submodule.baseChange_eq_span, Submodule.map₂_span_span, Set.image2_subset_iff, Submodule.span_le
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : Semiring A
inst_6 : Algebra R A
𝒜 : ι → Submodule R A
inst_7 : GradedAlgebra 𝒜
i j : ι
x : A
hx : x ∈ (↑(𝒜 i) : Set A)
y : A
hy : y ∈ (↑(𝒜 j) : Set A)
⊢ Membership.mem (α := S ⊗[R] A)
    (↑(span S
          (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R S A : (a : S) → A →ₗ[R] S ⊗[R] A) 1)
                (𝒜 (i + j))) :
            Set (S ⊗[R] A))) :
      Set (S ⊗[R] A))
    (((((↑(Algebra.lmul S (S ⊗[R] A)) :
                  [inst_8 : FunLike (S ⊗[R] A →ₐ[S] Module.End S (S ⊗[R] A)) (S ⊗[R] A) (Module.End S (S ⊗[R] A))] →
                    [SemilinearMapClass (S ⊗[R] A →ₐ[S] Module.End S (S ⊗[R] A)) (RingHom.id S) (S ⊗[R] A)
                          (Module.End S (S ⊗[R] A))] →
                      S ⊗[R] A →ₗ[S] Module.End S (S ⊗[R] A)) :
                (a : S ⊗[R] A) → S ⊗[R] A →ₗ[S] S ⊗[R] A)
              (((TensorProduct.mk R S A : (a : S) → A →ₗ[R] S ⊗[R] A) 1 : (a : A) → S ⊗[R] A) x) :
            S ⊗[R] A →ₗ[S] S ⊗[R] A) :
          (a : S ⊗[R] A) → S ⊗[R] A)
        (((TensorProduct.mk R S A : (a : S) → A →ₗ[R] S ⊗[R] A) 1 : (a : A) → S ⊗[R] A) y) :
      S ⊗[R] A)

Tactic:
simpa using subset_span <| Set.mem_image_of_mem _ <| mul_mem_graded hx hy

Premises used: SetLike.mul_mem_graded, Set.mem_image_of_mem, Submodule.subset_span
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : Semiring A
inst_6 : Algebra R A
𝒜 : ι → Submodule R A
inst_7 : GradedAlgebra 𝒜
s : S
⊢ Eq (α := S ⊗[R] A)
    (↑((algebraMap S ↥(Submodule.baseChange S (𝒜 0)) : (a : S) → ↥(Submodule.baseChange S (𝒜 0))) s) : S ⊗[R] A)
    (s ⊗ₜ[R] 1)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq ι
inst_4 : AddCommMonoid ι
inst_5 : CommSemiring A
inst_6 : Algebra R A
𝒜 : ι → Submodule R A
inst_7 : GradedAlgebra 𝒜
x : ↥(Submodule.baseChange S (𝒜 0))
⊢ (algebraMap (↥(Submodule.baseChange S (𝒜 0))) (S ⊗[R] A) : (a : ↥(Submodule.baseChange S (𝒜 0))) → S ⊗[R] A) x =
    (↑x : S ⊗[R] A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Semiring A
inst_5 : Semiring B
inst_6 : Algebra R A
inst_7 : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst_8 : GradedAlgebra 𝒜
inst_9 : GradedAlgebra ℬ
inst_10 : Algebra R S
inst_11 : Algebra R B
inst_12 : IsScalarTower R S B
f : GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)
i : ι
x : S ⊗[R] A
hx : Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i)) x
obtain :
  ∀ (x : TensorProduct.{u_2, u_3, u_4} R S ↥(𝒜 i))
    (hx :
      Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
        (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) x) : S ⊗[R] A)),
    Membership.mem (α := B) (ℬ i)
      ((AlgHom.toRingHom (R := S) ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
            (a : S ⊗[R] A) → B)
          (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) x) : S ⊗[R] A) :
        B)
⊢ Membership.mem (α := B) (ℬ i)
    ((AlgHom.toRingHom (R := S) ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
          (a : S ⊗[R] A) → B)
        x :
      B)

Tactic:
obtain ⟨x, rfl⟩ := toBaseChange_surjective' _ _ hx

Premises used: Submodule.toBaseChange_surjective', rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Semiring A
inst_5 : Semiring B
inst_6 : Algebra R A
inst_7 : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst_8 : GradedAlgebra 𝒜
inst_9 : GradedAlgebra ℬ
inst_10 : Algebra R S
inst_11 : Algebra R B
inst_12 : IsScalarTower R S B
f : GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)
i : ι
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
    (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) 0) : S ⊗[R] A)
⊢ Membership.mem (α := B) (ℬ i)
    ((AlgHom.toRingHom (R := S) ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
          (a : S ⊗[R] A) → B)
        (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) 0) : S ⊗[R] A) :
      B)

Tactic:
simp
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Semiring A
inst_5 : Semiring B
inst_6 : Algebra R A
inst_7 : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst_8 : GradedAlgebra 𝒜
inst_9 : GradedAlgebra ℬ
inst_10 : Algebra R S
inst_11 : Algebra R B
inst_12 : IsScalarTower R S B
f : GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)
i : ι
x y : TensorProduct.{u_2, u_3, u_4} R S ↥(𝒜 i)
h :
  ∀
    (hx :
      Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
        (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) x) : S ⊗[R] A)),
    Membership.mem (α := B) (ℬ i)
      ((AlgHom.toRingHom (R := S) ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
            (a : S ⊗[R] A) → B)
          (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) x) : S ⊗[R] A) :
        B)
h_1 :
  ∀
    (hx :
      Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
        (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) y) : S ⊗[R] A)),
    Membership.mem (α := B) (ℬ i)
      ((AlgHom.toRingHom (R := S) ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
            (a : S ⊗[R] A) → B)
          (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) y) : S ⊗[R] A) :
        B)
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
    (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) (x + y)) : S ⊗[R] A)
⊢ Membership.mem (α := B) (ℬ i)
    ((AlgHom.toRingHom (R := S) ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
          (a : S ⊗[R] A) → B)
        (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) (x + y)) : S ⊗[R] A) :
      B)

Tactic:
simp_all [add_mem]

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Semiring A
inst_5 : Semiring B
inst_6 : Algebra R A
inst_7 : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst_8 : GradedAlgebra 𝒜
inst_9 : GradedAlgebra ℬ
inst_10 : Algebra R S
inst_11 : Algebra R B
inst_12 : IsScalarTower R S B
f : GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)
i : ι
r : S
x : ↥(𝒜 i)
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
    (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) (r ⊗ₜ[R] x)) : S ⊗[R] A)
⊢ Membership.mem (α := B) (ℬ i) ((f : (a : A) → B) (↑x : A) : B)

Tactic:
f.map_mem x.2

Premises used: Set.Mem, GradedAlgHom.map_mem, Subtype.property
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Semiring A
inst_5 : Semiring B
inst_6 : Algebra R A
inst_7 : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst_8 : GradedAlgebra 𝒜
inst_9 : GradedAlgebra ℬ
inst_10 : Algebra R S
inst_11 : Algebra R B
inst_12 : IsScalarTower R S B
f : GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)
i : ι
r : S
x : ↥(𝒜 i)
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
    (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) (r ⊗ₜ[R] x)) : S ⊗[R] A)
⊢ Membership.mem (α := B) (ℬ i) ((f : (a : A) → B) (↑x : A) : B)

Tactic:
exact f.map_mem x.2

Premises used: GradedAlgHom.map_mem, Subtype.property
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Semiring A
inst_5 : Semiring B
inst_6 : Algebra R A
inst_7 : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst_8 : GradedAlgebra 𝒜
inst_9 : GradedAlgebra ℬ
inst_10 : Algebra R S
inst_11 : Algebra R B
inst_12 : IsScalarTower R S B
f : GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)
i : ι
r : S
x : ↥(𝒜 i)
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
    (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) (r ⊗ₜ[R] x)) : S ⊗[R] A)
⊢ Membership.mem (α := B) (ℬ i)
    ((AlgHom.toRingHom (R := S) ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
          (a : S ⊗[R] A) → B)
        (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) (r ⊗ₜ[R] x)) : S ⊗[R] A) :
      B)

Tactic:
simpa using smul_mem _ _ <| by exact f.map_mem x.2

Premises used: Submodule.smul_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Semiring A
inst_5 : Semiring B
inst_6 : Algebra R A
inst_7 : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst_8 : GradedAlgebra 𝒜
inst_9 : GradedAlgebra ℬ
inst_10 : Algebra R S
inst_11 : Algebra R B
inst_12 : IsScalarTower R S B
f : GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)
⊢ (↑((fun (f : GradedAlgHom S (A := S ⊗[R] A) (fun (x : ι) ↦ baseChange S (𝒜 x)) ℬ) ↦
            let __src : A →ₐ[R] B :=
              (Equiv.symm (AlgHom.liftEquiv R S A B) : (a : S ⊗[R] A →ₐ[S] B) → A →ₐ[R] B) (↑f : S ⊗[R] A →ₐ[S] B);
            ({ toAlgHom := __src, map_mem := ⋯ } :
              GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)))
          ((fun (f : GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)) ↦
              let __src : S ⊗[R] A →ₐ[S] B :=
                (AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B);
              ({ toAlgHom := __src, map_mem := ⋯ } :
                GradedAlgHom S (A := S ⊗[R] A) (fun (x : ι) ↦ baseChange S (𝒜 x)) ℬ))
            f)) :
      A →ₐ[R] B) =
    (↑f : A →ₐ[R] B)

Tactic:
simp
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Semiring A
inst_5 : Semiring B
inst_6 : Algebra R A
inst_7 : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst_8 : GradedAlgebra 𝒜
inst_9 : GradedAlgebra ℬ
inst_10 : Algebra R S
inst_11 : Algebra R B
inst_12 : IsScalarTower R S B
f : GradedAlgHom S (A := S ⊗[R] A) (fun (x : ι) ↦ baseChange S (𝒜 x)) ℬ
⊢ (↑((fun (f : GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)) ↦
            let __src : S ⊗[R] A →ₐ[S] B :=
              (AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B);
            ({ toAlgHom := __src, map_mem := ⋯ } : GradedAlgHom S (A := S ⊗[R] A) (fun (x : ι) ↦ baseChange S (𝒜 x)) ℬ))
          ((fun (f : GradedAlgHom S (A := S ⊗[R] A) (fun (x : ι) ↦ baseChange S (𝒜 x)) ℬ) ↦
              let __src : A →ₐ[R] B :=
                (Equiv.symm (AlgHom.liftEquiv R S A B) : (a : S ⊗[R] A →ₐ[S] B) → A →ₐ[R] B) (↑f : S ⊗[R] A →ₐ[S] B);
              ({ toAlgHom := __src, map_mem := ⋯ } :
                GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)))
            f)) :
      S ⊗[R] A →ₐ[S] B) =
    (↑f : S ⊗[R] A →ₐ[S] B)

Tactic:
simp
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Semiring A
inst_5 : Semiring B
inst_6 : Algebra R A
inst_7 : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst_8 : GradedAlgebra 𝒜
inst_9 : GradedAlgebra ℬ
inst_10 : Algebra R S
inst_11 : Algebra R B
inst_12 : IsScalarTower R S B
f : GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)
r : S
x : A
⊢ (((liftEquiv 𝒜 ℬ :
              (a : 𝒜 →ₐᵍ[R] fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)) →
                (fun (x : ι) ↦ baseChange S (𝒜 x)) →ₐᵍ[S] ℬ)
            f :
          GradedAlgHom S (A := S ⊗[R] A) (fun (x : ι) ↦ baseChange S (𝒜 x)) ℬ) :
        (a : S ⊗[R] A) → B)
      (r ⊗ₜ[R] x) =
    HSMul.hSMul (β := B) r ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Semiring A
inst_5 : Semiring B
inst_6 : Algebra R A
inst_7 : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst_8 : GradedAlgebra 𝒜
inst_9 : GradedAlgebra ℬ
inst_10 : Algebra R S
inst_11 : Algebra R B
inst_12 : IsScalarTower R S B
f : GradedAlgHom S (A := S ⊗[R] A) (fun (x : ι) ↦ baseChange S (𝒜 x)) ℬ
x : A
⊢ Eq.{u_5 + 1} (α := B)
    ((((Equiv.symm (liftEquiv 𝒜 ℬ) :
                (a : (fun (x : ι) ↦ baseChange S (𝒜 x)) →ₐᵍ[S] ℬ) →
                  𝒜 →ₐᵍ[R] fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x))
              f :
            GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)) :
          (a : A) → B)
        x :
      B)
    ((f : (a : S ⊗[R] A) → B) (1 ⊗ₜ[R] x) : B)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Semiring A
inst_5 : Algebra R A
𝒜 : ι → Submodule R A
inst_6 : GradedAlgebra 𝒜
inst_7 : Algebra R S
x : A
⊢ Eq (α := S ⊗[R] A) ((includeRight S 𝒜 : (a : A) → S ⊗[R] A) x : S ⊗[R] A) (1 ⊗ₜ[R] x : S ⊗[R] A)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Grassmannian
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
N₁ N₂ : G(k, M; R)
h : N₁.toSubmodule = N₂.toSubmodule
mk :
  ∀ (toSubmodule : Submodule R M) (finite_quotient : Module.Finite.{u, v} R (M ⧸ toSubmodule))
    (projective_quotient : Projective.{u, v} R (M ⧸ toSubmodule))
    (rankAtStalk_eq : ∀ (p : PrimeSpectrum R), rankAtStalk.{u, v} (M ⧸ toSubmodule) p = k)
    (h :
      { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
            rankAtStalk_eq := rankAtStalk_eq : G(k, M; R) }.toSubmodule =
        N₂.toSubmodule),
    { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
        rankAtStalk_eq := rankAtStalk_eq : G(k, M; R) } =
      N₂
⊢ N₁ = N₂

Tactic:
cases N₁
-- Module: Mathlib.RingTheory.Grassmannian
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
N₂ : G(k, M; R)
toSubmodule : Submodule R M
finite_quotient : Module.Finite.{u, v} R (M ⧸ toSubmodule)
projective_quotient : Projective.{u, v} R (M ⧸ toSubmodule)
rankAtStalk_eq : ∀ (p : PrimeSpectrum R), rankAtStalk.{u, v} (M ⧸ toSubmodule) p = k
h :
  { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
        rankAtStalk_eq := rankAtStalk_eq : G(k, M; R) }.toSubmodule =
    N₂.toSubmodule
mk :
  ∀ (toSubmodule_1 : Submodule R M) (finite_quotient_1 : Module.Finite.{u, v} R (M ⧸ toSubmodule_1))
    (projective_quotient_1 : Projective.{u, v} R (M ⧸ toSubmodule_1))
    (rankAtStalk_eq_1 : ∀ (p : PrimeSpectrum R), rankAtStalk.{u, v} (M ⧸ toSubmodule_1) p = k)
    (h :
      { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
            rankAtStalk_eq := rankAtStalk_eq : G(k, M; R) }.toSubmodule =
        { toSubmodule := toSubmodule_1, finite_quotient := finite_quotient_1,
            projective_quotient := projective_quotient_1, rankAtStalk_eq := rankAtStalk_eq_1 :
            G(k, M; R) }.toSubmodule),
    { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
        rankAtStalk_eq := rankAtStalk_eq : G(k, M; R) } =
      { toSubmodule := toSubmodule_1, finite_quotient := finite_quotient_1,
        projective_quotient := projective_quotient_1, rankAtStalk_eq := rankAtStalk_eq_1 }
⊢ { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
      rankAtStalk_eq := rankAtStalk_eq : G(k, M; R) } =
    N₂

Tactic:
cases N₂