mathlib-initiative/mathlib-tactics huggingface dataset:
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
r : S
x : S ⊗[R] M
⊢ (↑(IsTensorProduct.equiv h)).toFun (r • x) = (RingHom.id S) r • (↑(IsTensorProduct.equiv h)).toFun x

Tactic:
by
      change h.equiv (r • x) = r • h.equiv x
      refine TensorProduct.induction_on x ?_ ?_ ?_
      · rw [smul_zero, map_zero, smul_zero]
      · intro x y
        simp [smul_tmul', Algebra.linearMap_apply, smul_comm r x]
      · intro x y hx hy
        rw [map_add, smul_add, map_add, smul_add, hx, hy]

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

Goal state before:
pp: α : Type u_1
m : Multiset α
xs : List α
⊢ Multiset.sym2 ⟦xs⟧ = 0 ↔ ⟦xs⟧ = 0

Tactic:
simp

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

Goal state before:
pp: case cons.inr.inl
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
c : α
hc : c ∈ xs
h : a = x ∧ b = c ∨ a = c ∧ b = x
⊢ a = x ∨ a ∈ xs

Tactic:
obtain (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) := h

Goal state after:
case cons.inr.inl.inl
α : Type u_1
a b : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
hc : b ∈ xs
⊢ a = a ∨ a ∈ xs

case cons.inr.inl.inr
α : Type u_1
a b : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
hc : a ∈ xs
⊢ a = b ∨ a ∈ xs
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
m : Finset α
z : Sym2 α
a b : α
⊢ s(a, b) ∈ ↑m.sym2 ↔ s(a, b) ∈ (↑m).sym2

Tactic:
simp

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
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
e : M ≃ₗ[R] P
f : P →ₗ[R] N
isb : IsBaseChange S f
y : M
⊢ (f ∘ₗ ↑e) y = (↑(LinearEquiv.restrictScalars R (LinearEquiv.refl S N)) ∘ₗ f ∘ₗ ↑e) y

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case zero
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
P : Type u_2
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
A : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra S A
inst✝⁵ : IsScalarTower R S A
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module A N
inst✝¹ : IsScalarTower S A N
inst✝ : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] N ⊗[R] P :=
  (AlgebraTensorModule.assoc R S A A M P).symm ≪≫ₗ AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P)
⊢ e (1 ⊗ₜ[S] 0) = (AlgebraTensorModule.map f LinearMap.id) 0

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
x : α
h : x ∈ []
⊢ map (fun y ↦ s(x, y)) [] <+ [].sym2

Tactic:
simp

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

Goal state before:
pp: case mk
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a✝ : Sym2 α
a b : α
⊢ Quot.mk (Sym2.Rel α) (a, b) ∈ s.sym2 ↔ Quot.mk (Sym2.Rel α) (a, b) ∈ image (Function.uncurry Sym2.mk) (s ×ˢ s)

Tactic:
simp

Goal state after:
case mk
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a✝ : Sym2 α
a b : α
⊢ a ∈ s ∧ b ∈ s ↔ ∃ a_1 b_1, (a_1 ∈ s ∧ b_1 ∈ s) ∧ (a_1 = a ∧ b_1 = b ∨ a_1 = b ∧ b_1 = a)
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case nil
α : Type u_1
x : α
h : x ∉ []
⊢ (map (fun y ↦ s(x, y)) []).Disjoint [].sym2

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ ∀ x ∈ s, x ^ Multiset.count x ↑k = x ^ Multiset.count x ↑k

Tactic:
simp

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : Lattice α
x✝ y✝ : α
⊢ s(x✝, y✝).inf ≤ s(x✝, y✝).sup

Tactic:
simp

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

Goal state before:
pp: case inl.inl
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
xs : List α
z : Sym α n
hz : z ∈ List.sym n (a :: xs)
⊢ a ∈ a :: xs

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z z' : Sym α n
⊢ (fun p ↦ x ::ₛ p) z = (fun p ↦ x ::ₛ p) z' → z = z'

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
x y z w : α
⊢ Rel α (x, y) (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
x y z w : α
⊢ s(x, y) = s(z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
p q : α × α
⊢ s(p.1, p.2) = s(q.1, q.2) ↔ p = q ∨ p = q.swap

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ : Module R Q
g : M →ₗ[R] Q
I₄ : IsScalarTower R R Q
x✝ : M
⊢ (↑R (g ∘ₗ ↑e.symm) ∘ₗ ↑e) x✝ = g x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
⊢ ∑ i ∈ s, f i ≠ ⊤ ↔ ∀ i ∈ s, f i ≠ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refl
R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ : Module R Q
I₄ : IsScalarTower R R Q
y : N →ₗ[R] Q
x✝ : N
⊢ y x✝ = ((↑R y ∘ₗ ↑e) ∘ₗ ↑e.symm) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
h : ∏ j ∈ s, f j = ⊤
⊢ f i ≠ 0

Tactic:
by_contra! h0

Goal state after:
ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
h : ∏ j ∈ s, f j = ⊤
h0 : f i = 0
⊢ False
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
p : α → Prop
a b : α
⊢ (∀ c ∈ s(a, b), p c) ↔ p a ∧ p b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
x y z : α
⊢ z ∈ ↑s(x, y) ↔ z ∈ {x, y}

Tactic:
simp

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

Goal state before:
pp: case mpr
α : Type u_1
x y : α
hne : x ≠ y
⊢ x ∈ s(x, y) ∧ y ∈ s(x, y)

Tactic:
simp

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

Goal state before:
pp: case f
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := fun p H ↦ s(f p.1 ⋯, f p.2 ⋯)
p : α × α
Hp : ∀ a ∈ s(p.1, p.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun s ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp
hpq✝ : Rel α p p
hpq : p = p ∨ p = p.swap
Hq : ∀ a ∈ Quot.mk (Rel α) p, P a
⊢ f p.1 ⋯ = f p.1 ⋯ ∧ f p.2 ⋯ = f p.2 ⋯

Tactic:
simp

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

Goal state before:
pp: case g
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := fun p H ↦ s(f p.1 ⋯, f p.2 ⋯)
q : α × α
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
hpq✝ : Rel α q.swap q
hpq : q.swap = q ∨ q.swap = q.swap
Hp : ∀ a ∈ s(q.swap.1, q.swap.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(q.swap.1, q.swap.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun s ↦ (∀ a ∈ s, P a) → Sym2 β) (g q.swap) e H = g q.swap Hp
⊢ (f q.swap.1 ⋯, f q.swap.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y : V
f g : X ⟶ Y
⊢ homOfEq f ⋯ ⋯ = g ↔ f = homOfEq g ⋯ ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X' Y' : V
g f : X' ⟶ Y'
⊢ f = homOfEq g ⋯ ⋯ ↔ homOfEq f ⋯ ⋯ = g

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : { a // a.IsDiag }
x✝ : α
⊢ x✝ ∈ ↑((fun a ↦ ⟨diag a, ⋯⟩) ((fun x ↦ (↑x).diagElem ⋯) x)) ↔ x✝ ∈ ↑x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
x✝ : Sym2 α
⊢ x✝ ∈ diagSet ↔ x✝ ∈ Set.univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, a) = z
⊢ s(a, a).IsDiag

Tactic:
simp

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
r : β → β → Prop
sym : Std.Symm r
f : α → β
x✝ y✝ : α
⊢ s(x✝, y✝) ∈ fromRel ⋯ ↔ map f s(x✝, y✝) ∈ fromRel sym

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (x y : α), s(x, y) ∉ fromRel ⋯

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (x y : α), s(x, y) ∈ fromRel ⋯

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
z : Sym2 α
⊢ ∀ (x y : α), s(x, y) ∈ fromRel ⋯ ↔ s(x, y) ∈ {z | ¬z.IsDiag}

Tactic:
simp

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

Goal state before:
pp: case mk
α : Type u_1
x✝ : Sym2 α
a b : α
⊢ Quot.mk (Rel α) (a, b) ∈ diagSet ↔ Quot.mk (Rel α) (a, b) ∈ fromRel ⋯

Tactic:
simp

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

Goal state before:
pp: case mk
α : Type u_1
x✝ : Sym2 α
a b : α
⊢ Quot.mk (Rel α) (a, b) ∈ diagSetᶜ ↔ Quot.mk (Rel α) (a, b) ∈ fromRel ⋯

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ 𝟙 X ≫ f = f

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = f

Tactic:
simp

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

Goal state before:
pp: case e'_2
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ f = f ≫ 𝟙 Y

Tactic:
simp

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

Goal state before:
pp: case e'_3
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ g = g ≫ 𝟙 Y

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f = f ≫ 𝟙 X

Tactic:
simp

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

Goal state before:
pp: case e'_1.e'_3
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : Y ⟶ Y
⊢ f = f ≫ 𝟙 Y

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f : X ⟶ Y
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = F.map f

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f : X ⟶ Y
⊢ F.map (Quiver.homOfEq f ⋯ ⋯) = Quiver.homOfEq (F.map f) ⋯ ⋯

Tactic:
simp

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
hf : IsBaseChange S f
x : R
y : N
⊢ (IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M) x)) 0 =
    (↑R ((LinearMap.lsmul S N) ((algebraMap R S) x))) 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case zero
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'
h : IsPushout R S R' S'
y : S ⊗[R] R'
⊢ ⋯.equiv (0 * y) = ⋯.equiv 0 * ⋯.equiv y

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case tmul.zero
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'
h : IsPushout R S R' S'
a : S
b : R'
⊢ ⋯.equiv (a ⊗ₜ[R] b * 0) = ⋯.equiv (a ⊗ₜ[R] b) * ⋯.equiv 0

Tactic:
simp

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
⊢ ((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:
simp

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:
simp

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

Goal state before:
pp: case mk
α : Type u_1
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ ∅.sym2 ↔ Quot.mk (Rel α) (x, y) ∈ ∅

Tactic:
simp

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

Goal state before:
pp: case mk
α : Type u_1
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ univ.sym2 ↔ Quot.mk (Rel α) (x, y) ∈ univ

Tactic:
simp

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

Goal state before:
pp: case mk
α : Type u_1
a : α
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ {a}.sym2 ↔ Quot.mk (Rel α) (x, y) ∈ {s(a, a)}

Tactic:
simp

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
f : α → β
s : Set β
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ (f ⁻¹' s).sym2 ↔ Quot.mk (Rel α) (x, y) ∈ Sym2.map f ⁻¹' s.sym2

Tactic:
simp

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:
let f : R' →ₗ[R] S' := (IsScalarTower.toAlgHom R R' S').toLinearMap

Goal state after:
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
⊢ IsPushout R T R' T' ↔ IsPushout S T S' T'
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case zero
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
s : S
⊢ ↑(cancelBaseChangeAux R S A B M).symm (s • 0) = s • ↑(cancelBaseChangeAux R S A B M).symm 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_2
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
⊢ ∀ (a₁ a₂ : S) (b₁ b₂ : C),
    ↑(cancelBaseChange R S A B C).symm ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      ↑(cancelBaseChange R S A B C).symm (a₁ ⊗ₜ[R] b₁) * ↑(cancelBaseChange R S A B C).symm (a₂ ⊗ₜ[R] b₂)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z X : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X ∧ 𝟙 X ≫ 𝟙 X = 𝟙 X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso h
⊢ (f ≫ h) ≫ inv h ≫ inv f = 𝟙 X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ inv f ≫ f = 𝟙 Y

Tactic:
simp

Goal state after: