mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
hy : [].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨[], hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨[], hy⟩)

pp: case cons.cons.nil.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝² head✝¹ : α
hx : [head✝², head✝¹].length = 2
head✝ : α
y : List α
hy : (head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝², head✝¹], hx⟩ ⟨head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝², head✝¹], hx⟩) (fromVector ⟨head✝ :: y, hy⟩)

Tactic:
·

Goal state after:
case cons.cons.nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
hy : [].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨[], hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨[], hy⟩)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.nil.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝² head✝¹ : α
hx : [head✝², head✝¹].length = 2
head✝ : α
hy : [head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝², head✝¹], hx⟩ ⟨[head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝², head✝¹], hx⟩) (fromVector ⟨[head✝], hy⟩)

pp: case cons.cons.nil.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝³ head✝² : α
hx : [head✝³, head✝²].length = 2
head✝¹ head✝ : α
y : List α
hy : (head✝¹ :: head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝³, head✝²], hx⟩ ⟨head✝¹ :: head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝³, head✝²], hx⟩) (fromVector ⟨head✝¹ :: head✝ :: y, hy⟩)

Tactic:
·

Goal state after:
case cons.cons.nil.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝² head✝¹ : α
hx : [head✝², head✝¹].length = 2
head✝ : α
hy : [head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝², head✝¹], hx⟩ ⟨[head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝², head✝¹], hx⟩) (fromVector ⟨[head✝], hy⟩)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.nil.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝⁴ head✝³ : α
hx : [head✝⁴, head✝³].length = 2
head✝² head✝¹ head✝ : α
y : List α
hy : (head✝² :: head✝¹ :: head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝⁴, head✝³], hx⟩ ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝⁴, head✝³], hx⟩) (fromVector ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩)

pp: case cons.cons.nil.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝³ head✝² : α
hx : [head✝³, head✝²].length = 2
head✝¹ head✝ : α
hy : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝³, head✝²], hx⟩ ⟨[head✝¹, head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝³, head✝²], hx⟩) (fromVector ⟨[head✝¹, head✝], hy⟩)

Tactic:
·

Goal state after:
case cons.cons.nil.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝⁴ head✝³ : α
hx : [head✝⁴, head✝³].length = 2
head✝² head✝¹ head✝ : α
y : List α
hy : (head✝² :: head✝¹ :: head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝⁴, head✝³], hx⟩ ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝⁴, head✝³], hx⟩) (fromVector ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.nil.cons.cons.nil.inl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝¹ head✝ : α
hx hy : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨[head✝¹, head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨[head✝¹, head✝], hy⟩)

pp: case cons.cons.nil.cons.cons.nil.inr
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
hy : [head✝, head✝¹].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨[head✝, head✝¹], hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨[head✝, head✝¹], hy⟩)

Tactic:
·

Goal state after:
case cons.cons.nil.cons.cons.nil.inl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝¹ head✝ : α
hx hy : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨[head✝¹, head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨[head✝¹, head✝], hy⟩)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
hx : [].length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨[], hx⟩⟧) = ⟦⟨[], hx⟩⟧

pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
head✝ : α
x : List α
hx : (head✝ :: x).length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨head✝ :: x, hx⟩⟧) = ⟦⟨head✝ :: x, hx⟩⟧

Tactic:
·

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
hx : [].length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨[], hx⟩⟧) = ⟦⟨[], hx⟩⟧
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
head✝ : α
hx : [head✝].length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨[head✝], hx⟩⟧) = ⟦⟨[head✝], hx⟩⟧

pp: case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
head✝¹ head✝ : α
x : List α
hx : (head✝¹ :: head✝ :: x).length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨head✝¹ :: head✝ :: x, hx⟩⟧) =
    ⟦⟨head✝¹ :: head✝ :: x, hx⟩⟧

Tactic:
·

Goal state after:
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
head✝ : α
hx : [head✝].length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨[head✝], hx⟩⟧) = ⟦⟨[head✝], hx⟩⟧
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
head✝² head✝¹ head✝ : α
x : List α
hx : (head✝² :: head✝¹ :: head✝ :: x).length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩⟧) =
    ⟦⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩⟧

pp: case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨[head✝¹, head✝], hx⟩⟧) = ⟦⟨[head✝¹, head✝], hx⟩⟧

Tactic:
·

Goal state after:
case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
head✝² head✝¹ head✝ : α
x : List α
hx : (head✝² :: head✝¹ :: head✝ :: x).length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩⟧) =
    ⟦⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩⟧
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_1
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'
⊢ f 0 = g 0

pp: case refine_2
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'
⊢ ∀ (m : R'), f ((toAlgHom R R' S').toLinearMap m) = g ((toAlgHom R R' S').toLinearMap m)

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) (n : S'), f n = g n → f (s • n) = g (s • n)

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

Goal state after:
case refine_1
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'
⊢ f 0 = g 0
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_2
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'
⊢ ∀ (m : R'), f ((toAlgHom R R' S').toLinearMap m) = g ((toAlgHom R R' S').toLinearMap m)

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) (n : S'), f n = g n → f (s • n) = g (s • n)

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

Goal state after:
case refine_2
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'
⊢ ∀ (m : R'), f ((toAlgHom R R' S').toLinearMap m) = g ((toAlgHom R R' S').toLinearMap m)
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) (n : S'), f n = g n → f (s • n) = g (s • n)

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

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) (n : S'), f n = g n → f (s • n) = g (s • n)
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:
·

Goal state after:
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₂)
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
⊢ f = g

Tactic:
apply (cancel_epi (inv f)).1

Goal state after:
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
⊢ inv f ≫ f = inv f ≫ g
Module: Mathlib.CategoryTheory.Iso

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 : X ⟶ Y
inst✝ : IsIso f
⊢ F.map (inv f) = inv (F.map f)

Tactic:
apply eq_inv_of_hom_inv_id

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

Goal state before:
pp: case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
Y : C
⊢ ofObj X Y → ∃ i, X i = Y

pp: case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
Y : C
⊢ (∃ i, X i = Y) → ofObj X Y

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
Y : C
⊢ ofObj X Y → ∃ i, X i = Y
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
Y : C
⊢ (∃ i, X i = Y) → ofObj X Y

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
Y : C
⊢ (∃ i, X i = Y) → ofObj X Y
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ pair X Y Z → X = Z ∨ Y = Z

pp: case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ X = Z ∨ Y = Z → pair X Y Z

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ pair X Y Z → X = Z ∨ Y = Z
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ X = Z ∨ Y = Z → pair X Y Z

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ X = Z ∨ Y = Z → pair X Y Z
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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ E
inst✝¹ : F.Faithful
G : D ⥤ E
inst✝ : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
⊢ Faithful.div F G obj h_obj map h_map ⋙ G = F

Tactic:
obtain ⟨F_obj, _, _, _⟩ := F

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : G.Faithful
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_obj : C → E
map✝ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
inst✝ : { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.Faithful
h_obj : ∀ (X : C), G.obj (obj X) = { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
⊢ Faithful.div { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } G obj h_obj map h_map ⋙ G =
    { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X : V), (of σ ⋙q lift σ φ τ h).obj X = φ.obj X

pp: case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of σ ⋙q lift σ φ τ h).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
·

Goal state after:
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X : V), (of σ ⋙q lift σ φ τ h).obj X = φ.obj X
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of σ ⋙q lift σ φ τ h).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
·

Goal state after:
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of σ ⋙q lift σ φ τ h).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X : Push σ),
    Φ.obj X =
      { obj := τ, map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x ↦ τ X ⟶ τ Y) fun X Y f ↦ ⋯.mpr (⋯.mpr (φ.map f)) }.obj
        X

pp: case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X Y : Push σ) (f : X ⟶ Y),
    Φ.map f =
      Eq.recOn ⋯
        (Eq.recOn ⋯
          ({ obj := τ,
                map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x ↦ τ X ⟶ τ Y) fun X Y f ↦ ⋯.mpr (⋯.mpr (φ.map f)) }.map
            f))

Tactic:
·

Goal state after:
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X : Push σ),
    Φ.obj X =
      { obj := τ, map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x ↦ τ X ⟶ τ Y) fun X Y f ↦ ⋯.mpr (⋯.mpr (φ.map f)) }.obj
        X
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case nil
V : Type u
inst✝ : Quiver V
a : V
hzero : nil.length = 0
⊢ a = a

pp: case cons
V : Type u
inst✝ : Quiver V
a b b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ b
hzero : (a✝¹.cons a✝).length = 0
⊢ a = b

Tactic:
·

Goal state after:
case nil
V : Type u
inst✝ : Quiver V
a : V
hzero : nil.length = 0
⊢ a = a
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons
V : Type u
inst✝ : Quiver V
a b b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ b
hzero : (a✝¹.cons a✝).length = 0
⊢ a = b

Tactic:
·

Goal state after:
case cons
V : Type u
inst✝ : Quiver V
a b b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ b
hzero : (a✝¹.cons a✝).length = 0
⊢ a = b
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X Y : Push σ) (f : X ⟶ Y),
    Φ.map f =
      Eq.recOn ⋯
        (Eq.recOn ⋯
          ({ obj := τ,
                map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x ↦ τ X ⟶ τ Y) fun X Y f ↦ ⋯.mpr (⋯.mpr (φ.map f)) }.map
            f))

Tactic:
·

Goal state after:
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X Y : Push σ) (f : X ⟶ Y),
    Φ.map f =
      Eq.recOn ⋯
        (Eq.recOn ⋯
          ({ obj := τ,
                map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x ↦ τ X ⟶ τ Y) fun X Y f ↦ ⋯.mpr (⋯.mpr (φ.map f)) }.map
            f))
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case nil
V : Type u
inst✝ : Quiver V
a : V
hzero : nil.length = 0
⊢ nil = nil

pp: case cons
V : Type u
inst✝ : Quiver V
a b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ a
hzero : (a✝¹.cons a✝).length = 0
⊢ a✝¹.cons a✝ = nil

Tactic:
·

Goal state after:
case nil
V : Type u
inst✝ : Quiver V
a : V
hzero : nil.length = 0
⊢ nil = nil