mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ z.IsDiag

Tactic:
]

Goal state after:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, a) = z
⊢ z.IsDiag
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:
]

Goal state after:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, a) = z
⊢ s(a, a).IsDiag
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r₁ r₂ : α → α → Prop
sym₁ : Std.Symm r₁
sym₂ : Std.Symm r₂
⊢ fromRel sym₁ = fromRel sym₂ ↔ (fromRelOrderIso α) ⟨r₁, sym₁⟩ = (fromRelOrderIso α) ⟨r₂, sym₂⟩

Tactic:
]

Goal state after:
α : Type u_1
r₁ r₂ : α → α → Prop
sym₁ : Std.Symm r₁
sym₂ : Std.Symm r₂
⊢ fromRel sym₁ = fromRel sym₂ ↔ (fromRelOrderIso α) ⟨r₁, sym₁⟩ = (fromRelOrderIso α) ⟨r₂, sym₂⟩
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
z : Sym2 α
⊢ x ∈ z.toMultiset ↔ x ∈ z.toMultiset

Tactic:
]

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
x✝ y✝ : α
h : x✝ = y✝
⊢ #s(x✝, y✝).toFinset = 1

Tactic:
]

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
x✝ y✝ : α
h : x✝ = y✝
⊢ #s(x✝, y✝).toFinset = 1
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
x✝ y✝ : α
h : ¬x✝ = y✝
⊢ #s(x✝, y✝).toFinset = 2

Tactic:
]

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
x✝ y✝ : α
h : ¬x✝ = y✝
⊢ #s(x✝, y✝).toFinset = 2
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = a₂
h₂ : b₁ = b₂
⊢ [a₂, b₂].Perm [a₂, b₂]

Tactic:
]

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

Goal state before:
pp: α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂].Perm [a₂, b₂]

Tactic:
]

Goal state after:
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂].Perm [a₂, b₂]
Module: Mathlib.CategoryTheory.Category.Basic

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

Tactic:
]

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 g : X ⟶ Y
h : f = g
⊢ F.map g = F.map g

Tactic:
]

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
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
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝¹ : Module R Q := Module.restrictScalars R S Q
this✝ : IsScalarTower R S Q
this : IsScalarTower R T Q
r' : M →ₗ[R] Q := ↑R r ∘ₗ f
q : O →ₗ[T] Q := hc.lift r'
q' : O →ₗ[T] Q
hq' : ↑R (↑S q' ∘ₗ h) = ↑R r
⊢ (↑R q' ∘ₗ ↑R h) ∘ₗ f = ↑R q ∘ₗ ↑R h ∘ₗ f

Tactic:
]

Goal state after:
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
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
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝¹ : Module R Q := Module.restrictScalars R S Q
this✝ : IsScalarTower R S Q
this : IsScalarTower R T Q
r' : M →ₗ[R] Q := ↑R r ∘ₗ f
q : O →ₗ[T] Q := hc.lift r'
q' : O →ₗ[T] Q
hq' : ↑R (↑S q' ∘ₗ h) = ↑R r
⊢ (↑R q' ∘ₗ ↑R h) ∘ₗ f = ↑R q ∘ₗ ↑R h ∘ₗ f
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
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
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝¹ : Module R Q := Module.restrictScalars R S Q
this✝ : IsScalarTower R S Q
this : IsScalarTower R T Q
r' : M →ₗ[R] Q := ↑R r ∘ₗ f
q : O →ₗ[T] Q := hc.lift r'
q' : O →ₗ[T] Q
hq' : ↑R (↑S q' ∘ₗ h) = ↑R r
⊢ ↑R r ∘ₗ f = r'

Tactic:
]

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
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
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝¹ : Module R Q := Module.restrictScalars R S Q
this✝ : IsScalarTower R S Q
this : IsScalarTower R T Q
r' : M →ₗ[R] Q := ↑R r ∘ₗ f
q : O →ₗ[T] Q := hc.lift r'
⊢ ∀ (y : O →ₗ[T] Q), (fun g' ↦ ↑S g' ∘ₗ h = r) y → y = q

Tactic:
intro q' hq'
    apply hc.algHom_ext'
    apply_fun LinearMap.restrictScalars R at hq'
    rw [← LinearMap.comp_assoc]
    rw [show q'.restrictScalars R ∘ₗ h.restrictScalars R = _ from hq', hc.lift_comp]

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
s : S
m : M
⊢ ((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) (LinearMap.id s)) (((LinearMap.lsmul R M) x) m) =
    (↑R ((LinearMap.lsmul S N) ((algebraMap R S) x)))
      (((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) s) m)

Tactic:
]

Goal state after:
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
s : S
m : M
⊢ ((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) (LinearMap.id s)) (((LinearMap.lsmul R M) x) m) =
    (↑R ((LinearMap.lsmul S N) ((algebraMap R S) x)))
      (((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) s) m)
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 : S
⊢ (algebraMap S S') a = (algebraMap S S') a

Tactic:
]

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 : R'
⊢ (algebraMap R' S') a = (algebraMap R' S') a

Tactic:
]

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

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

Tactic:
]

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

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z
Module: Mathlib.Data.Sym.Sym2

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

Tactic:
]

Goal state after:
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb✝ = a
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
⊢ g ≫ h = g ≫ h

Tactic:
]

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 x✝ x✝¹ • ↑g x✝ x✝¹ = ↑f x✝ x✝¹ • ↑g x✝ x✝¹

Tactic:
]

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:
constructor
  convert! isBaseChange_tensorProduct_map (R := R) (P := S) _ (IsBaseChange.linearMap A B)
  ext s
  simpa using congr($H s)

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 g = F.map g

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_3
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')
x : S'
s : S
s' : S'
e : f s' = g s'
⊢ f ((algebraMap S S') s) * g s' = g ((algebraMap S S') s) * g s'

Tactic:
]

Goal state after:
case refine_3
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')
x : S'
s : S
s' : S'
e : f s' = g s'
⊢ f ((algebraMap S S') s) * g s' = g ((algebraMap S S') s) * g s'
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_4
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')
x s₁ s₂ : S'
e₁ : f s₁ = g s₁
e₂ : f s₂ = g s₂
⊢ g s₁ + g s₂ = g s₁ + g s₂

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_4
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')
x : S'
⊢ ∀ (n₁ n₂ : S'), f n₁ = g n₁ → f n₂ = g n₂ → f (n₁ + n₂) = g (n₁ + n₂)

Tactic:
intro s₁ s₂ e₁ e₂
    rw [map_add, map_add, e₁, e₂]

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 S T') ((algebraMap R S) x) = (algebraMap S T') ((algebraMap R S) x)

Tactic:
]

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'
heq : ↑R (toAlgHom S S' T').toLinearMap ∘ₗ f = (toAlgHom R R' T').toLinearMap
⊢ IsBaseChange T (toAlgHom S S' T').toLinearMap ↔ IsBaseChange T (toAlgHom S S' T').toLinearMap

pp: case hf
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'
heq : ↑R (toAlgHom S S' T').toLinearMap ∘ₗ f = (toAlgHom R R' T').toLinearMap
⊢ IsBaseChange S f

Tactic:
]

Goal state after:
case hf
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'
heq : ↑R (toAlgHom S S' T').toLinearMap ∘ₗ f = (toAlgHom R R' T').toLinearMap
⊢ IsBaseChange S f
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 : IsBaseChange R' (toAlgHom R S S').toLinearMap
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
⊢ IsBaseChange R' (toAlgHom R S T).toLinearMap

Tactic:
]

Goal state after:
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 : IsBaseChange R' (toAlgHom R S S').toLinearMap
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
⊢ IsBaseChange R' (toAlgHom R S T).toLinearMap
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f✝ g✝ : X ≅ Y
X✝ Y✝ : C
f g : X✝ ≅ Y✝
h : f.hom = g.hom
⊢ g.inv = g.inv

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Y ⟶ X
⊢ f = α.inv ↔ f = α.inv

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ β.hom = α.symm.hom ↔ β.hom = α.inv
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
]

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
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso (f ≫ g)
⊢ IsIso (inv f ≫ f ≫ g)

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso (f ≫ g)
⊢ IsIso (inv f ≫ f ≫ g)
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso f
hh : IsIso (f ≫ g)
w : f ≫ g = h
⊢ IsIso g
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : g ≫ f = 𝟙 X
⊢ IsIso (inv g)
Module: Mathlib.CategoryTheory.Functor.Category

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
f : X ⟶ Y
inst✝¹ : IsIso (α.app X)
inst✝ : IsIso (α.app Y)
⊢ F.map f ≫ α.app Y = α.app X ≫ G.map f

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
f : X ⟶ Y
inst✝¹ : IsIso (α.app X)
inst✝ : IsIso (α.app Y)
⊢ F.map f ≫ α.app Y = α.app X ≫ G.map f
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P Q : ObjectProperty C
⊢ ¬P ≤ Q ↔ ∃ X, P X ∧ ¬Q X

Tactic:
by
  simp [le_def]

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

Goal state before:
pp: C : Type u
inst✝¹ : CategoryStruct.{v, u} C
P : ObjectProperty C
X : C
inst✝ : P.Is X
⊢ P.Is X

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : CategoryStruct.{v, u} C
P : ObjectProperty C
X : C
inst✝ : P.Is X
⊢ P.Is X
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty C
X : C
hX : P X
⊢ P X

Tactic:
]

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty C
X : C
hX : P X
⊢ P X