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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ map (fun p ↦ f x ::ₛ p) (map (Sym.map f) (List.sym n (x :: xs))) ++ map (Sym.map f) (List.sym (n + 1) xs) =
    map (Sym.map f) (List.sym (n + 1) (x :: xs))

Tactic:
simp only [map_map, List.sym, map_append, append_cancel_right_eq]

Goal state after:
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ map ((fun p ↦ f x ::ₛ p) ∘ Sym.map f) (List.sym n (x :: xs)) =
    map (Sym.map f ∘ fun p ↦ x ::ₛ p) (List.sym n (x :: xs))
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
Q : Type (max v₁ v₂ v₃)
⊢ ∀ [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q] [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q),
    ∃! g', ↑R g' ∘ₗ f = g

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
h : IsBaseChange S f
Q : Type (max v₁ v₂ v₃)
inst✝ : AddCommMonoid Q
⊢ ∀ [inst : Module R Q] [inst_1 : Module S Q] [inst_2 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
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
Q : Type (max v₁ v₂ v₃)
inst✝ : AddCommMonoid Q
⊢ ∀ [inst : Module R Q] [inst_1 : Module S Q] [inst_2 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g

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
h : IsBaseChange S f
Q : Type (max v₁ v₂ v₃)
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
⊢ ∀ [inst : Module S Q] [inst_1 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
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
Q : Type (max v₁ v₂ v₃)
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
⊢ ∀ [inst : Module S Q] [inst_1 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g

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
h : IsBaseChange S f
Q : Type (max v₁ v₂ v₃)
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
inst✝ : Module S Q
⊢ ∀ [inst : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
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
Q : Type (max v₁ v₂ v₃)
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
inst✝ : Module S Q
⊢ ∀ [inst : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g

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
h : IsBaseChange S f
Q : Type (max v₁ v₂ v₃)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module S Q
inst✝ : IsScalarTower R S Q
⊢ ∀ (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a✝ : α × α
⊢ ∀ ⦃b : α × α⦄, Rel α a✝ b → Rel β (Prod.map f f a✝) (Prod.map f f b)

Tactic:
_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a✝ b✝ : α × α
⊢ Rel α a✝ b✝ → Rel β (Prod.map f f a✝) (Prod.map f f b✝)
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
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
⊢ ∏ j ∈ s, f j = ⊤

Tactic:
classical rw [← prod_erase_mul _ _ hi]
  refine WithTop.mul_eq_top_iff.mpr (Or.inl ⟨?_, hi'⟩)
  refine prod_ne_zero_iff.mpr ?_
  intros
  simp_all only [ne_eq, mem_erase, not_false_eq_true]

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
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
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
⊢ ∀ [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module T Q] [inst_3 : IsScalarTower R T Q]
    (g_1 : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = g_1

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
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
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝ : AddCommMonoid Q
⊢ ∀ [inst : Module R Q] [inst_1 : Module T Q] [inst_2 : IsScalarTower R T Q] (g_1 : M →ₗ[R] Q),
    ∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = g_1
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
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
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝ : AddCommMonoid Q
⊢ ∀ [inst : Module R Q] [inst_1 : Module T Q] [inst_2 : IsScalarTower R T Q] (g_1 : M →ₗ[R] Q),
    ∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = g_1

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
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
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
⊢ ∀ [inst : Module T Q] [inst_1 : IsScalarTower R T Q] (g_1 : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = g_1
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
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
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
⊢ ∀ [inst : Module T Q] [inst_1 : IsScalarTower R T Q] (g_1 : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = g_1

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
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
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
inst✝ : Module T Q
⊢ ∀ [inst : IsScalarTower R T Q] (g_1 : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = g_1
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
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
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
inst✝ : Module T Q
⊢ ∀ [inst : IsScalarTower R T Q] (g_1 : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = g_1

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
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
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower R T Q
⊢ ∀ (g_1 : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = g_1
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
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_1 : Module S Q] [inst_2 : Module T Q] [inst_3 : IsScalarTower S T Q] (g : N →ₗ[S] Q),
    ∃! g', ↑S g' ∘ₗ h = g

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
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_1 : Module T Q] [inst_2 : IsScalarTower S T Q] (g : N →ₗ[S] Q), ∃! g', ↑S g' ∘ₗ h = g
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
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_1 : Module T Q] [inst_2 : IsScalarTower S T Q] (g : N →ₗ[S] Q), ∃! g', ↑S g' ∘ₗ h = g

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
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_1 : IsScalarTower S T Q] (g : N →ₗ[S] Q), ∃! g', ↑S g' ∘ₗ h = g
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
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_1 : IsScalarTower S T Q] (g : N →ₗ[S] Q), ∃! g', ↑S g' ∘ₗ h = g

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
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] (g : N →ₗ[S] Q), ∃! g', ↑S g' ∘ₗ h = g
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
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] (g : N →ₗ[S] Q), ∃! g', ↑S g' ∘ₗ h = g

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
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
⊢ ∀ (g : N →ₗ[S] Q), ∃! g', ↑S g' ∘ₗ h = g
Module: Mathlib.RingTheory.IsTensorProduct

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

Tactic:
| tmul x y =>

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

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
⊢ P.strictMap F ≤ P.map F

Tactic:
by
  rintro _ ⟨X, hX⟩
  exact ⟨X, hX, ⟨Iso.refl _⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : CategoryStruct.{v₁, u₁} C
X Y : C
p : X = Y
⊢ Y ⟶ Y

Tactic:
exact 𝟙 _

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

Goal state before:
pp: α : Type u₁
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
I : Type u_1
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
inst✝ : ∀ (i : Discrete I), IsIso (f i)
⊢ IsIso (natTrans f)

Tactic:
change IsIso (Discrete.natIso (fun i => asIso (f i))).hom
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : Cᵒᵖ ≌ Dᵒᵖ
X : C
⊢ e.functor.unop.map ((NatIso.unop e.unitIso).symm.hom.app X) ≫
      (NatIso.unop e.counitIso).symm.hom.app (e.functor.unop.obj X) =
    𝟙 (e.functor.unop.obj X)

Tactic:
by
    apply Quiver.Hom.op_inj
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

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 : F ⟶ G),
    (𝟭 (Cᵒᵖ ⥤ D)ᵒᵖ).map f ≫ (unop G).rightOpLeftOpIso.op.hom =
      (unop F).rightOpLeftOpIso.op.hom ≫
        ({ obj := fun F ↦ (unop F).rightOp, map := fun {X Y} η ↦ NatTrans.rightOp η.unop, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun F ↦ op F.leftOp, map := fun {X Y} η ↦ (NatTrans.leftOp η).op, map_id := ⋯,
                map_comp := ⋯ }).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
⊢ (𝟭 (Cᵒᵖ ⥤ D)ᵒᵖ).map η ≫ (unop G).rightOpLeftOpIso.op.hom =
    (unop F).rightOpLeftOpIso.op.hom ≫
      ({ obj := fun F ↦ (unop F).rightOp, map := fun {X Y} η ↦ NatTrans.rightOp η.unop, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun F ↦ op F.leftOp, map := fun {X Y} η ↦ (NatTrans.leftOp η).op, map_id := ⋯, map_comp := ⋯ }).map
        η
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsGroupoid C
⊢ ⊤ ≤ isomorphisms C

Tactic:
_

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsGroupoid C
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), ⊤ f → isomorphisms C f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
P Q : MorphismProperty C
h : P ≤ Q
⊢ (fun x ↦ x.map F) P ≤ (fun x ↦ x.map F) Q

Tactic:
X

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
P Q : MorphismProperty C
h : P ≤ Q
X : D
⊢ ∀ ⦃Y : D⦄ (f : X ⟶ Y), (fun x ↦ x.map F) P f → (fun x ↦ x.map F) Q f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X Y : D
f : X ⟶ Y
⊢ ⊤ f → ⊤.map F f

Tactic:
_

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X Y : D
f : X ⟶ Y
a✝ : ⊤ f
⊢ ⊤.map F f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
h : P ≤ Q
⊢ P.isoClosure ≤ Q.isoClosure

Tactic:
X

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
h : P ≤ Q
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P.isoClosure f → Q.isoClosure f