mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : ModuleCat R
f : X ⟶ Y
this✝ : TopologicalSpace ↑X := ⊤
this : TopologicalSpace ↑Y := ⊤
⊢ Continuous (ModuleCat.Hom.hom f).toFun

Tactic:
rw [continuous_iff_coinduced_le]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : ModuleCat R
f : X ⟶ Y
this✝ : TopologicalSpace ↑X := ⊤
this : TopologicalSpace ↑Y := ⊤
⊢ TopologicalSpace.coinduced (ModuleCat.Hom.hom f).toFun (of R ↑X).topologicalSpace ≤ (of R ↑Y).topologicalSpace
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ Continuous LinearMap.id.toFun

Tactic:
rw [continuous_iff_coinduced_le]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ TopologicalSpace.coinduced LinearMap.id.toFun ((𝟭 (TopModuleCat R)).obj X).topologicalSpace ≤
    ((forget₂ (TopModuleCat R) (ModuleCat R) ⋙ indiscrete R).obj X).topologicalSpace
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
⊢ Continuous (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun

Tactic:
rw [continuous_iff_coinduced_le]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
⊢ TopologicalSpace.coinduced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun (freeObj R X).topologicalSpace ≤
    (freeObj R Y).topologicalSpace
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst✝ : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w✝¹ : Fact κF.IsRegular
h✝¹ : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w✝ : Fact κG.IsRegular
h✝ : G.IsCardinalAccessible κG
this : Fact (max κF κG).IsRegular
⊢ κF ≤ max κF κG

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst✝ : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w✝¹ : Fact κF.IsRegular
h✝¹ : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w✝ : Fact κG.IsRegular
h✝ : G.IsCardinalAccessible κG
this✝ : Fact (max κF κG).IsRegular
this : F.IsCardinalAccessible (max κF κG)
⊢ κG ≤ max κF κG

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopModuleCat R
f : X ⟶ Y
a : ↑((forget₂ (TopModuleCat R) TopCat).obj X)
⊢ ((Finsupp.mapDomain (⇑(Hom.hom f)) (Finsupp.single a 1)).sum fun x r ↦ r • x) =
    (Hom.hom f) ((Finsupp.single a 1).sum fun x r ↦ r • x)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Small

Goal state before:
pp: P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → ↑↑(R i)) → CommRingCat := fun S ↦ of ↥S.snd.snd
S : CommRingCat
hS : P S
s : Set ↑S
hs : Ideal.span s = ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
hs' : s.Finite
S' : ↑s → CommRingCat
hS' : ∀ (f : ↑s), Q' (S' f)
e : ∀ (f : ↑s), Nonempty (of (Localization.Away ↑f) ≅ S' f)
φ : ↑S →+* (i : Fin (Nat.card ↑s)) → ↑(S' ((Finite.equivFin ↑s).symm i)) :=
  ((RingEquiv.piCongrRight fun i ↦ ⋯.some.commRingCatIsoToRingEquiv).trans
          (RingEquiv.piCongrLeft (fun x ↦ ↑(S' x)) (Finite.equivFin ↑s).symm).symm).toRingHom.comp
    (algebraMap (↑S) ((i : ↑s) → ↑(of (Localization.Away ↑i))))
⊢ (ObjectProperty.ofObj f).isoClosure S

Tactic:
have hφ : Function.Injective φ := by
    dsimp only [RingHom.coe_comp, φ]
    refine (RingEquiv.injective _).comp (Localization.algebraMap_injective_of_span_eq_top _ hs)

Goal state after:
P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → ↑↑(R i)) → CommRingCat := fun S ↦ of ↥S.snd.snd
S : CommRingCat
hS : P S
s : Set ↑S
hs : Ideal.span s = ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
hs' : s.Finite
S' : ↑s → CommRingCat
hS' : ∀ (f : ↑s), Q' (S' f)
e : ∀ (f : ↑s), Nonempty (of (Localization.Away ↑f) ≅ S' f)
φ : ↑S →+* (i : Fin (Nat.card ↑s)) → ↑(S' ((Finite.equivFin ↑s).symm i)) :=
  ((RingEquiv.piCongrRight fun i ↦ ⋯.some.commRingCatIsoToRingEquiv).trans
          (RingEquiv.piCongrLeft (fun x ↦ ↑(S' x)) (Finite.equivFin ↑s).symm).symm).toRingHom.comp
    (algebraMap (↑S) ((i : ↑s) → ↑(of (Localization.Away ↑i))))
hφ : Function.Injective ⇑φ
⊢ (ObjectProperty.ofObj f).isoClosure S
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
x✝³ x✝² : N
x✝¹ : (i : ι) → M i
x✝ : ι
⊢ (pi fun i ↦ (mk R N (M i)) (x✝³ + x✝²) ∘ₗ proj i) x✝¹ x✝ =
    ((pi fun i ↦ (mk R N (M i)) x✝³ ∘ₗ proj i) + pi fun i ↦ (mk R N (M i)) x✝² ∘ₗ proj i) x✝¹ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: case e_n
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
m : (i : ι) → M i
j : ι
⊢ (∑ a, Pi.single a (m a)) j = m j

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
this : Pi.single i (x ⊗ₜ[R] m) = fun j ↦ x ⊗ₜ[R] Pi.single i m j
⊢ ((piRightInv R S N M) fun j ↦ x ⊗ₜ[R] Pi.single i m j) = x ⊗ₜ[R] Pi.single i m

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
j : ι
m : M j
⊢ ((AlgebraTensorModule.curry (piRightInv R S N M ∘ₗ piRightHom R S N M)) x ∘ₗ single R M j) m =
    ((AlgebraTensorModule.curry LinearMap.id) x ∘ₗ single R M j) m

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R A B C : CommRingCat
inst✝ : TopologicalSpace ↑R
f : A ≅ B
x✝ : B ⟶ R
⊢ (fun φ ↦ f.inv ≫ φ) ((fun φ ↦ f.hom ≫ φ) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R A B C : CommRingCat
inst✝ : TopologicalSpace ↑R
f : A ≅ B
x✝ : A ⟶ R
⊢ (fun φ ↦ f.hom ≫ φ) ((fun φ ↦ f.inv ≫ φ) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
x y : N
i : ι → R
j : ι
⊢ ((toSpanSingleton R N (x + y)).compLeft ι) i j =
    ((toSpanSingleton R N x).compLeft ι + (toSpanSingleton R N y).compLeft ι) i j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : IsEmpty ι
j' : J₁
a : j ⟶ F.obj j'
k' : J₁
b : k ⟶ F.obj k'
⊢ ∀ (i : ι), f i ≫ b ≫ F.map (IsFiltered.rightToMax j' k') = a ≫ F.map (IsFiltered.leftToMax j' k')

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: case hC
R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
f : of (MvPolynomial σ ↑A) ⟶ R
x✝ : ↑A
⊢ ((Hom.hom
            ((fun fx ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
              ((fun f ↦ (ofHom MvPolynomial.C ≫ f, fun i ↦ (ConcreteCategory.hom f) (MvPolynomial.X i))) f))).comp
        MvPolynomial.C)
      x✝ =
    ((Hom.hom f).comp MvPolynomial.C) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: case hX
R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
f : of (MvPolynomial σ ↑A) ⟶ R
i✝ : σ
⊢ (Hom.hom
        ((fun fx ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
          ((fun f ↦ (ofHom MvPolynomial.C ≫ f, fun i ↦ (ConcreteCategory.hom f) (MvPolynomial.X i))) f)))
      (MvPolynomial.X i✝) =
    (Hom.hom f) (MvPolynomial.X i✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: case fst
R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
fx : (A ⟶ R) × (σ → ↑R)
x✝ : ↑A
⊢ (Hom.hom
        ((fun f ↦ (ofHom MvPolynomial.C ≫ f, fun i ↦ (ConcreteCategory.hom f) (MvPolynomial.X i)))
            ((fun fx ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2)) fx)).1)
      x✝ =
    (Hom.hom fx.1) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: case snd
R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
fx : (A ⟶ R) × (σ → ↑R)
x✝ : σ
⊢ ((fun f ↦ (ofHom MvPolynomial.C ≫ f, fun i ↦ (ConcreteCategory.hom f) (MvPolynomial.X i)))
          ((fun fx ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2)) fx)).2
      x✝ =
    fx.2 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
s : S
x : N
i : ι → R
j : ι
⊢ s • (algebraMap R S) (i j) • x = (s • (toSpanSingleton R N x).compLeft ι) i j

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Pi

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
y : A ⊗[R] ((i : ι) → B i)
⊢ (piRightHom R S A B) (0 * y) = (piRightHom R S A B) 0 * (piRightHom R S A B) y

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Pi

Goal state before:
pp: case tmul.zero
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝ : A
y✝ : (i : ι) → B i
⊢ (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝ * 0) = (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝) * (piRightHom R S A B) 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Pi

Goal state before:
pp: case tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ : A
y✝ : (i : ι) → B i
j : ι
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝ ⊗ₜ[R] y✝) j =
    ((piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝)) j

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
⊢ (_root_.TensorProduct.piRightHom R S A B) 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
⊢ ∀ (x y : A ⊗[R] ((i : ι) → B i)),
    (_root_.TensorProduct.piRightHom R S A B) (x * y) =
      (_root_.TensorProduct.piRightHom R S A B) x * (_root_.TensorProduct.piRightHom R S A B) y

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝³ : (i : ι) → Semiring (B i)
inst✝² : (i : ι) → Algebra R (B i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ (_root_.TensorProduct.piRight R S A B) 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝³ : (i : ι) → Semiring (B i)
inst✝² : (i : ι) → Algebra R (B i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ∀ (x y : A ⊗[R] ((i : ι) → B i)),
    (_root_.TensorProduct.piRight R S A B) (x * y) =
      (_root_.TensorProduct.piRight R S A B) x * (_root_.TensorProduct.piRight R S A B) y

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
ι : Type u_4
B✝ : ι → Type u_5
inst✝⁷ : (i : ι) → Semiring (B✝ i)
inst✝⁶ : (i : ι) → Algebra R (B✝ i)
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
B : Type u_6
C : Type u_7
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra R B
inst✝ : Algebra R C
x✝³ x✝² : A
x✝¹ x✝ : B × C
⊢ ↑(_root_.TensorProduct.prodRight R S A B C) ((x✝³ * x✝²) ⊗ₜ[R] (x✝¹ * x✝)) =
    ↑(_root_.TensorProduct.prodRight R S A B C) (x✝³ ⊗ₜ[R] x✝¹) *
      ↑(_root_.TensorProduct.prodRight R S A B C) (x✝² ⊗ₜ[R] x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
hz₁ : g₁ z₁ = i₂ y₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
this : f₂ (y₁ - y₂) = 0
⊢ π₁ z₁ = π₁ z₂

Tactic:
hf

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
hz₁ : g₁ z₁ = i₂ y₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
this : y₁ - y₂ ∈ Set.range ⇑f₁
⊢ π₁ z₁ = π₁ z₂
Module: Mathlib.LinearAlgebra.TensorProduct.Prod

Goal state before:
pp: case hl.fst
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M₁
inst✝³ : Module S M₁
inst✝² : IsScalarTower R S M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝¹ : M₁
x✝ : M₂
⊢ (((AlgebraTensorModule.curry
            ((AlgebraTensorModule.lift
                  (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                    (AlgebraTensorModule.mk R S M₁ M₂).prod (AlgebraTensorModule.mk R S M₁ M₃)) ∘ₗ
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                  ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃))) ∘ₗ
              LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)))
          x✝¹)
        x✝).1 =
    (((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃))) x✝¹) x✝).1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Prod

Goal state before:
pp: case hl.snd
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M₁
inst✝³ : Module S M₁
inst✝² : IsScalarTower R S M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝¹ : M₁
x✝ : M₂
⊢ (((AlgebraTensorModule.curry
            ((AlgebraTensorModule.lift
                  (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                    (AlgebraTensorModule.mk R S M₁ M₂).prod (AlgebraTensorModule.mk R S M₁ M₃)) ∘ₗ
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                  ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃))) ∘ₗ
              LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)))
          x✝¹)
        x✝).2 =
    (((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃))) x✝¹) x✝).2

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Prod

Goal state before:
pp: case hr.fst
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M₁
inst✝³ : Module S M₁
inst✝² : IsScalarTower R S M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝¹ : M₁
x✝ : M₃
⊢ (((AlgebraTensorModule.curry
            ((AlgebraTensorModule.lift
                  (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                    (AlgebraTensorModule.mk R S M₁ M₂).prod (AlgebraTensorModule.mk R S M₁ M₃)) ∘ₗ
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                  ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃))) ∘ₗ
              LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)))
          x✝¹)
        x✝).1 =
    (((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃))) x✝¹) x✝).1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Prod

Goal state before:
pp: case hr.snd
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M₁
inst✝³ : Module S M₁
inst✝² : IsScalarTower R S M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝¹ : M₁
x✝ : M₃
⊢ (((AlgebraTensorModule.curry
            ((AlgebraTensorModule.lift
                  (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                    (AlgebraTensorModule.mk R S M₁ M₂).prod (AlgebraTensorModule.mk R S M₁ M₃)) ∘ₗ
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                  ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃))) ∘ₗ
              LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)))
          x✝¹)
        x✝).2 =
    (((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃))) x✝¹) x✝).2

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Prod

Goal state before:
pp: case hl
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M₁
inst✝³ : Module S M₁
inst✝² : IsScalarTower R S M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝¹ : M₁
x✝ : M₂
⊢ ((AlgebraTensorModule.curry
            (((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃)) ∘ₗ
              AlgebraTensorModule.lift
                (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                  (AlgebraTensorModule.mk R S M₁ M₂).prod (AlgebraTensorModule.mk R S M₁ M₃))))
          x✝¹ ∘ₗ
        LinearMap.inl R M₂ M₃)
      x✝ =
    ((AlgebraTensorModule.curry LinearMap.id) x✝¹ ∘ₗ LinearMap.inl R M₂ M₃) x✝

Tactic:
simp

Goal state after: