mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout R S R' S'
x✝ : R'
x : R' ⊗[R] S
⊢ ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun (x✝ • 0) =
    (RingHom.id R') x✝ • ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h = Mem.other' h

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout R S R' S'
x✝² : R'
x : R' ⊗[R] S
x✝¹ : R'
x✝ : S
⊢ ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun (x✝² • x✝¹ ⊗ₜ[R] x✝) =
    (RingHom.id R') x✝² •
      ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun (x✝¹ ⊗ₜ[R] x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other' h ∈ z

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb = a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout R S R' S'
x✝ : R'
x : R' ⊗[R] S
⊢ ∀ (x y : R' ⊗[R] S),
    ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun (x✝ • x) =
        (RingHom.id R') x✝ • ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun x →
      ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun (x✝ • y) =
          (RingHom.id R') x✝ • ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun y →
        ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun (x✝ • (x + y)) =
          (RingHom.id R') x✝ • ((TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv).toFun (x + y)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
⊢ Mem.other hb = a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout R S R' S'
x✝ : S
⊢ (let __spread.0 := (TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv;
      { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
        right_inv := ⋯ })
      (1 ⊗ₜ[R] x✝) =
    (toAlgHom R S S').toLinearMap x✝

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Reassoc

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
w : f = g
Z : C
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ {x ∈ image (uncurry Sym2.mk) (s ×ˢ s) | x.IsDiag} = image (uncurry Sym2.mk) s.diag

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ {x ∈ image (uncurry Sym2.mk) (s ×ˢ s) | ¬x.IsDiag} = image (uncurry Sym2.mk) s.offDiag

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : CommSemiring R
inst✝³⁰ : CommSemiring S
inst✝²⁹ : Algebra R S
inst✝²⁸ : Module R M
inst✝²⁷ : Module R N
inst✝²⁶ : Module S N
inst✝²⁵ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝²⁴ : AddCommMonoid P
inst✝²³ : Module R P
inst✝²² : AddCommMonoid Q
inst✝²¹ : Module S Q
inst✝²⁰ : Module R Q
inst✝¹⁹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝¹⁸ : CommSemiring T
inst✝¹⁷ : Algebra R T
inst✝¹⁶ : Algebra S T
inst✝¹⁵ : IsScalarTower R S T
inst✝¹⁴ : AddCommMonoid O
inst✝¹³ : Module R O
inst✝¹² : Module S O
inst✝¹¹ : Module T O
inst✝¹⁰ : IsScalarTower S T O
inst✝⁹ : IsScalarTower R S O
inst✝⁸ : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
x✝ : S
⊢ (TensorProduct.lid R S) (1 ⊗ₜ[R] x✝) = (toAlgHom R S S).toLinearMap x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α✝
f✝ : α✝ → β
α : Type ?u.43
R : Type ?u.14
N : Type ?u.13
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x✝¹ x✝ : α
⊢ (↑f • ↑g) x✝¹ x✝ = (↑f • ↑g) x✝ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_4
R : Type u_5
N : Type u_6
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
⊢ lift f • lift g = lift ⟨↑f • ↑g, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
s : Set α
z : Sym2 α
⊢ z ∈ s.sym2 ↔ ↑z ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.sym2 = uncurry Sym2.mk '' s ×ˢ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
⊢ ∅.sym2 = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
⊢ univ.sym2 = univ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra R S
x✝¹ : Algebra (A ⊗[R] S) (B ⊗[R] S)
x✝ : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H : (algebraMap (A ⊗[R] S) (B ⊗[R] S)).comp TensorProduct.includeRight.toRingHom = TensorProduct.includeRight.toRingHom
⊢ IsPushout A B (A ⊗[R] S) (B ⊗[R] S)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a : α
⊢ {a}.sym2 = {s(a, a)}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a : α
s : Set α
⊢ (insert a s).sym2 = (fun b ↦ s(a, b)) '' insert a s ∪ s.sym2

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.NatTrans

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α β : NatTrans F G
h : α = β
X : C
⊢ α.app X = β.app X

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring S
inst✝¹¹ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝¹⁰ : CommSemiring R'
inst✝⁹ : CommSemiring S'
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra R' S'
inst✝⁵ : Algebra R S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsScalarTower R S S'
inst✝² : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : S →ₐ[R] A
g : R' →ₐ[R] A
H : ∀ (x : S) (y : R'), f x * g y = g y * f x
x : S
⊢ (pushoutDesc S' f g H) ((algebraMap S S') x) = f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ (f ⁻¹' s).sym2 = Sym2.map f ⁻¹' s.sym2

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v_1, u₁} C
D : Type u₂
inst✝ : Category.{v_2, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : D
h : F.obj Z ⟶ W
⊢ F.map (f ≫ g) ≫ h = F.map f ≫ F.map g ≫ h

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (f '' s).sym2 = Sym2.map f '' s.sym2

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring S
inst✝¹¹ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝¹⁰ : CommSemiring R'
inst✝⁹ : CommSemiring S'
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra R' S'
inst✝⁵ : Algebra R S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsScalarTower R S S'
inst✝² : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : S →ₐ[R] A
g : R' →ₐ[R] A
H : ∀ (x : S) (y : R'), f x * g y = g y * f x
x : R'
⊢ (pushoutDesc S' f g H) ((algebraMap R' S') x) = g x

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
P : Prop
inst✝ : Decidable P
f : P → (X ⟶ Y)
g : ¬P → (X ⟶ Y)
⊢ F.map (if h : P then f h else g h) = if h : P then F.map (f h) else F.map (g h)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.NatTrans

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : NatTrans F G
X Y U V : C
f : X ⟶ Y
g : Y ⟶ U
h : U ⟶ V
⊢ α.app X ≫ G.map f ≫ G.map g ≫ G.map h = F.map f ≫ F.map g ≫ F.map h ≫ α.app V

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → Set α
⊢ (⋂ i, f i).sym2 = ⋂ i, (f i).sym2

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id✝¹ : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
map' : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id✝ : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g
h :
  { obj := obj, map := map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.toPrefunctor =
    { obj := obj, map := map', map_id := map_id✝, map_comp := map_comp✝ }.toPrefunctor
⊢ map = map'

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h : F.toPrefunctor = G.toPrefunctor
⊢ F = G

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst✝²⁰ : CommSemiring R'
inst✝¹⁹ : CommSemiring S'
inst✝¹⁸ : Algebra R R'
inst✝¹⁷ : Algebra S S'
inst✝¹⁶ : Algebra R' S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
inst✝¹³ : IsScalarTower R S S'
T' : Type u_8
inst✝¹² : CommSemiring T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
f : R' →ₗ[R] S' := (toAlgHom R R' S').toLinearMap
x : R
⊢ (algebraMap R T') x = (algebraMap S T') ((algebraMap R S) x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst✝²⁰ : CommSemiring R'
inst✝¹⁹ : CommSemiring S'
inst✝¹⁸ : Algebra R R'
inst✝¹⁷ : Algebra S S'
inst✝¹⁶ : Algebra R' S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
inst✝¹³ : IsScalarTower R S S'
T' : Type u_8
inst✝¹² : CommSemiring T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
f : R' →ₗ[R] S' := (toAlgHom R R' S').toLinearMap
this : IsScalarTower R S T'
⊢ ↑R (toAlgHom S S' T').toLinearMap ∘ₗ f = (toAlgHom R R' T').toLinearMap

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst✝²⁰ : CommSemiring R'
inst✝¹⁹ : CommSemiring S'
inst✝¹⁸ : Algebra R R'
inst✝¹⁷ : Algebra S S'
inst✝¹⁶ : Algebra R' S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
inst✝¹³ : IsScalarTower R S S'
T' : Type u_8
inst✝¹² : CommSemiring T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
⊢ IsPushout R T R' T' ↔ IsPushout S T S' T'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : CommSemiring S
inst✝¹⁴ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝¹³ : CommSemiring R'
inst✝¹² : CommSemiring S'
inst✝¹¹ : Algebra R R'
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra R' S'
inst✝⁸ : Algebra R S'
inst✝⁷ : IsScalarTower R R' S'
inst✝⁶ : IsScalarTower R S S'
h : IsPushout R R' S S'
T : Type u_8
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R' T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : IsScalarTower R R' T
e : S' ≃ₐ[R'] T
he : e.toRingEquiv.toRingHom.comp (algebraMap S S') = algebraMap S T
⊢ IsPushout R R' S T

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : Algebra R S
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra S B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsScalarTower R S B
inst✝⁴ : IsPushout R S A B
M : Type u_10
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : S
m : M
⊢ (cancelBaseChangeAux R S A B M).symm (s ⊗ₜ[R] m) = (algebraMap S B) s ⊗ₜ[A] m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M✝ : Type v₁
N : Type v₂
S : Type v₃
inst✝⁴⁶ : AddCommMonoid M✝
inst✝⁴⁵ : AddCommMonoid N
inst✝⁴⁴ : CommSemiring R
inst✝⁴³ : CommSemiring S
inst✝⁴² : Algebra R S
inst✝⁴¹ : Module R M✝
inst✝⁴⁰ : Module R N
inst✝³⁹ : Module S N
inst✝³⁸ : IsScalarTower R S N
f : M✝ →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝³⁷ : AddCommMonoid P
inst✝³⁶ : Module R P
inst✝³⁵ : AddCommMonoid Q
inst✝³⁴ : Module S Q
inst✝³³ : Module R Q
inst✝³² : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝³¹ : CommSemiring T
inst✝³⁰ : Algebra R T
inst✝²⁹ : Algebra S T
inst✝²⁸ : IsScalarTower R S T
inst✝²⁷ : AddCommMonoid O
inst✝²⁶ : Module R O
inst✝²⁵ : Module S O
inst✝²⁴ : Module T O
inst✝²³ : IsScalarTower S T O
inst✝²² : IsScalarTower R S O
inst✝²¹ : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst✝²⁰ : CommSemiring R'
inst✝¹⁹ : CommSemiring S'
inst✝¹⁸ : Algebra R R'
inst✝¹⁷ : Algebra S S'
inst✝¹⁶ : Algebra R' S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
inst✝¹³ : IsScalarTower R S S'
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra S B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsScalarTower R S B
inst✝⁴ : IsPushout R S A B
M : Type u_10
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
⊢ ∀ (c : S) (x : S ⊗[R] M), ↑(cancelBaseChangeAux R S A B M).symm (c • x) = c • ↑(cancelBaseChangeAux R S A B M).symm x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : Algebra R S
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra S B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsScalarTower R S B
inst✝⁴ : IsPushout R S A B
M : Type u_10
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (cancelBaseChange R S A B M) (1 ⊗ₜ[A] m) = 1 ⊗ₜ[R] m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M✝ : Type v₁
N : Type v₂
S : Type v₃
inst✝⁵⁰ : AddCommMonoid M✝
inst✝⁴⁹ : AddCommMonoid N
inst✝⁴⁸ : CommSemiring R
inst✝⁴⁷ : CommSemiring S
inst✝⁴⁶ : Algebra R S
inst✝⁴⁵ : Module R M✝
inst✝⁴⁴ : Module R N
inst✝⁴³ : Module S N
inst✝⁴² : IsScalarTower R S N
f : M✝ →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝⁴¹ : AddCommMonoid P
inst✝⁴⁰ : Module R P
inst✝³⁹ : AddCommMonoid Q
inst✝³⁸ : Module S Q
inst✝³⁷ : Module R Q
inst✝³⁶ : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝³⁵ : CommSemiring T
inst✝³⁴ : Algebra R T
inst✝³³ : Algebra S T
inst✝³² : IsScalarTower R S T
inst✝³¹ : AddCommMonoid O
inst✝³⁰ : Module R O
inst✝²⁹ : Module S O
inst✝²⁸ : Module T O
inst✝²⁷ : IsScalarTower S T O
inst✝²⁶ : IsScalarTower R S O
inst✝²⁵ : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst✝²⁴ : CommSemiring R'
inst✝²³ : CommSemiring S'
inst✝²² : Algebra R R'
inst✝²¹ : Algebra S S'
inst✝²⁰ : Algebra R' S'
inst✝¹⁹ : Algebra R S'
inst✝¹⁸ : IsScalarTower R R' S'
inst✝¹⁷ : IsScalarTower R S S'
A : Type u_8
B : Type u_9
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra S B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : IsScalarTower R S B
inst✝⁸ : IsPushout R S A B
M : Type u_10
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
C : Type u_11
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower R A C
⊢ B ⊗[A] C ≃ₐ[S] S ⊗[R] C

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : Algebra R S
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra S B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsScalarTower R S B
inst✝⁴ : IsPushout R S A B
C : Type u_11
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower R A C
⊢ ↑(cancelBaseChangeAlg R S A B C) = cancelBaseChange R S A B C

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : Algebra R S
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra S B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsScalarTower R S B
inst✝⁴ : IsPushout R S A B
C : Type u_11
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower R A C
c : C
⊢ (cancelBaseChangeAlg R S A B C) (1 ⊗ₜ[A] c) = 1 ⊗ₜ[R] c

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : Algebra R S
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra S B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsScalarTower R S B
inst✝⁴ : IsPushout R S A B
C : Type u_11
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower R A C
s : S
c : C
⊢ (cancelBaseChangeAlg R S A B C).symm (s ⊗ₜ[R] c) = (algebraMap S B) s ⊗ₜ[A] c

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_8
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
C : Type u_11
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra A C
inst✝² : IsScalarTower R A C
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (↑(cancelBaseChangeAlg R S A (S ⊗[R] A) C).symm).comp (TensorProduct.lTensor S (toAlgHom R A C)) =
    TensorProduct.includeLeft

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α β : X ≅ Y
w : α.hom = β.hom
⊢ α.inv = α.inv ≫ β.hom ≫ β.inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α β : X ≅ Y
w : α.hom = β.hom
⊢ α.inv ≫ β.hom ≫ β.inv = β.inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α β : X ≅ Y
w : α.hom = β.hom
this : α.inv = β.inv
⊢ α = β

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z Z' : C
α : X ≅ Y
β : Y ≅ Z
γ : Z ≅ Z'
⊢ (α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ refl X ≪≫ α = α

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ α ≪≫ refl Y = α

Tactic:
by

Goal state after: