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

Goal state before:
pp: case refine_1
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 :
  ∀ (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
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
s : S
x : S ⊗[R] M
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, g a_2 = a
g' : { x // x ∈ d } → α :=
  fun x ↦
    match x with
    | ⟨x, hx⟩ => ⋯.choose
i : α
e : β
he : e ∈ d
hi : ⋯.choose = i
⊢ ⋯.choose ∈ s

Tactic:
]

Goal state after:
case refine_1.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, g a_2 = a
g' : { x // x ∈ d } → α :=
  fun x ↦
    match x with
    | ⟨x, hx⟩ => ⋯.choose
i : α
e : β
he : e ∈ d
hi : ⋯.choose = i
⊢ ⋯.choose ∈ s
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ s(x, x) :: (map (fun y ↦ s(x, y)) xs.dedup ++ xs.sym2.dedup) =
    s(x, x) :: (map (fun y ↦ s(x, y)) xs.dedup ++ xs.sym2.dedup)

pp: case cons.inr.hf
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ Function.Injective fun y ↦ s(x, y)

pp: case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ (map (fun y ↦ s(x, y)) xs).Disjoint xs.sym2

pp: case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ s(x, x) ∉ map (fun y ↦ s(x, y)) xs ++ xs.sym2

Tactic:
]

Goal state after:
case cons.inr.hf
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ Function.Injective fun y ↦ s(x, y)

case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ (map (fun y ↦ s(x, y)) xs).Disjoint xs.sym2

case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ s(x, x) ∉ map (fun y ↦ s(x, y)) xs ++ xs.sym2
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
x✝ : ∃ a, (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g) a = d
d' : β
b : Sym α n
hd : ∃ a ∈ b, g a = d'
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g) b = d
⊢ ∃ a ∈ s, g a = d'

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
x✝ : ∃ a, (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g) a = d
d' : β
b : Sym α n
hd : ∃ a ∈ b, g a = d'
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g) b = d
⊢ ∃ a ∈ s, g a = d'
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
ha : a ∈ s
n : ℕ
b : α
hb : b ∈ Sym.replicate n a
⊢ a ∈ s

Tactic:
]

Goal state after:
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
ha : a ∈ s
n : ℕ
b : α
hb : b ∈ Sym.replicate n a
⊢ a ∈ s
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
m : ↥((insert a s).sym n)
⊢ s = s

Tactic:
]

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

Goal state before:
pp: case cons
α : Type u_1
x : α
xs : List α
ih : xs.sym2.length = (xs.length + 1).choose 2
⊢ xs.length + 1 + xs.sym2.length = xs.length + 1 + xs.sym2.length

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
f : M →ₗ[R] N
h :
  ∀ (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
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
s : S
x✝ x y : S ⊗[R] M
hx : f' (s • x) = s • f' x
hy : f' (s • y) = s • f' y
⊢ s • f' x + s • f' y = s • f' x + s • f' y

Tactic:
]

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

Goal state before:
pp: case cons
α : Type u_1
xs✝ : List α
x : α
xs : List α
ih : List.sym 1 xs = map (fun x ↦ x ::ₛ Sym.nil) xs
⊢ (x ::ₛ Sym.nil) :: List.sym (0 + 1) xs = (x ::ₛ Sym.nil) :: List.sym 1 xs

Tactic:
]

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
⊢ ∏ i ∈ s, i ^ Multiset.count i ↑k = ∏ d ∈ s, d ^ Multiset.count d ↑k

pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ (↑k).toFinset ⊆ s

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ ∏ i ∈ s, i ^ Multiset.count i ↑k = ∏ d ∈ s, d ^ Multiset.count d ↑k

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ (↑k).toFinset ⊆ s
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons
α : Type u_1
xs✝ : List α
x : α
xs : List α
ih : map (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs
⊢ map (⇑(Sym2.equivSym α) ∘ fun y ↦ s(x, y)) (x :: xs) ++ map (⇑(Sym2.equivSym α)) xs.sym2 =
    map ((fun p ↦ x ::ₛ p) ∘ fun x ↦ x ::ₛ Sym.nil) (x :: xs) ++ map (⇑(Sym2.equivSym α)) xs.sym2

Tactic:
]

Goal state after:
case cons
α : Type u_1
xs✝ : List α
x : α
xs : List α
ih : map (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs
⊢ map (⇑(Sym2.equivSym α) ∘ fun y ↦ s(x, y)) (x :: xs) ++ map (⇑(Sym2.equivSym α)) xs.sym2 =
    map ((fun p ↦ x ::ₛ p) ∘ fun x ↦ x ::ₛ Sym.nil) (x :: xs) ++ map (⇑(Sym2.equivSym α)) xs.sym2
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:
]

Goal state after:
α : 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))
Module: Mathlib.Algebra.BigOperators.Sym

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
⊢ ∑ i ∈ s.sym2 with ¬i.IsDiag, p i = ∑ i ∈ s.offDiag with i.1 ≤ i.2, p s(i.1, i.2)

Tactic:
]

Goal state after:
ι : Type u_1
M : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
⊢ ∑ i ∈ s.sym2 with ¬i.IsDiag, p i = ∑ i ∈ s.offDiag with i.1 ≤ i.2, p s(i.1, i.2)
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ ys : List α
h✝ : xs✝ <+ ys
xs : List α
n : ℕ
l₂✝ : List α
a : α
h : xs <+ l₂✝
⊢ [] ++ List.sym (n + 1) xs <+ map (fun p ↦ a ::ₛ p) (List.sym n (a :: l₂✝)) ++ List.sym (n + 1) l₂✝

Tactic:
]

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ ys : List α
h✝ : xs✝ <+ ys
xs : List α
n : ℕ
l₂✝ : List α
a : α
h : xs <+ l₂✝
⊢ [] ++ List.sym (n + 1) xs <+ map (fun p ↦ a ::ₛ p) (List.sym n (a :: l₂✝)) ++ List.sym (n + 1) l₂✝
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ map (fun p ↦ a ::ₛ p) (List.sym n (a :: l₁✝)) ++ List.sym (n + 1) l₁✝ <+
    map (fun p ↦ a ::ₛ p) (List.sym n (a :: l₂✝)) ++ List.sym (n + 1) l₂✝

Tactic:
]

Goal state after:
α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ map (fun p ↦ a ::ₛ p) (List.sym n (a :: l₁✝)) ++ List.sym (n + 1) l₁✝ <+
    map (fun p ↦ a ::ₛ p) (List.sym n (a :: l₂✝)) ++ List.sym (n + 1) l₂✝
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : (∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z) ∨ z ∈ List.sym (n + 1) xs
⊢ a ∈ x :: xs

Tactic:
]

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : (∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z) ∨ z ∈ List.sym (n + 1) xs
⊢ a ∈ x :: xs
Module: Mathlib.Data.List.Sym

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

Tactic:
]

Goal state after:
case inl
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a = x ∨ a ∈ z
⊢ a ∈ x :: xs
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_1
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 :
  ∀ (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
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
⊢ ↑ULift.moduleEquiv.symm ∘ₗ f'' ∘ₗ ↑ULift.moduleEquiv ∘ₗ g = ↑ULift.moduleEquiv.symm ∘ₗ LinearMap.id

Tactic:
]

Goal state after:
case refine_1
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 :
  ∀ (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
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
⊢ ↑ULift.moduleEquiv.symm ∘ₗ f'' ∘ₗ ↑ULift.moduleEquiv ∘ₗ g = ↑ULift.moduleEquiv.symm ∘ₗ LinearMap.id
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case inr
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) xs
⊢ a = x ∨ a ∈ xs

Tactic:
]

Goal state after:
case inr
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) xs
⊢ a = x ∨ a ∈ xs
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p ↦ x ::ₛ p) (List.sym n (x :: xs)) ++ List.sym (n + 1) xs).Nodup

Tactic:
]

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p ↦ x ::ₛ p) (List.sym n (x :: xs)) ++ List.sym (n + 1) xs).Nodup
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
hz : ∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z
hz' : z ∈ List.sym (n + 1) xs
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
hz : ∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z
hz' : z ∈ List.sym (n + 1) xs
⊢ False
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 :
  ∀ (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
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
x : M
⊢ (↑ULift.moduleEquiv.symm (((mk R S M) 1) x)).down = ((AlgebraTensorModule.curry LinearMap.id) 1) x

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
f : M →ₗ[R] N
h :
  ∀ (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
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
x : M
⊢ (↑ULift.moduleEquiv.symm (((mk R S M) 1) x)).down = ((AlgebraTensorModule.curry LinearMap.id) 1) x
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n : ℕ
xs x✝ : List α
⊢ [Sym.nil].length = 1

Tactic:
]

Goal state after:
α : Type u_1
n : ℕ
xs x✝ : List α
⊢ [Sym.nil].length = 1
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (List.sym n (x :: xs)).length + (List.sym (n + 1) xs).length = (xs.length + 1).multichoose (n + 1)

Tactic:
]

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (List.sym n (x :: xs)).length + (List.sym (n + 1) xs).length = (xs.length + 1).multichoose (n + 1)
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) = (xs.length + 1).multichoose (n + 1)

Tactic:
]

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) = (xs.length + 1).multichoose (n + 1)
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n =
    xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n

Tactic:
]

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₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
r : R
q : Q
⊢ (r * 1) • q = (r * 1) • q

Tactic:
]

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

Goal state before:
pp: α : Type u_1
a b c w✝ : α
h : b = a ∧ c = w✝ ∨ b = w✝ ∧ c = a
⊢ a = b ∨ a = c

Tactic:
]

Goal state after:
α : Type u_1
a b c w✝ : α
h : b = a ∧ c = w✝ ∨ b = w✝ ∧ c = a
⊢ a = b ∨ a = c
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case inr
α : Type u_1
a b : α
⊢ Sym2.Mem a s(a, b)

Tactic:
]

Goal state after:
case inr
α : Type u_1
a b : α
⊢ Sym2.Mem a s(a, 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
⊢ (∏ x ∈ s.erase i, f x) * f i = ⊤

Tactic:
]

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
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
⊢ (∏ x ∈ s.erase i, f x) * f i = ⊤
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
e : Sym2 α
⊢ e = e

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case mp.h
α : Type u_1
x y : α
hne : x ≠ y
x✝ y✝ : α
⊢ (x = x✝ ∨ x = y✝) ∧ (y = x✝ ∨ y = y✝) → s(x✝, y✝) = s(x, y)

Tactic:
]

Goal state after:
case mp.h
α : Type u_1
x y : α
hne : x ≠ y
x✝ y✝ : α
⊢ (x = x✝ ∨ x = y✝) ∧ (y = x✝ ∨ y = y✝) → s(x✝, y✝) = s(x, y)
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
i : M →ₗ[R] Q
this : Module S Q := Module.compHom Q (algebraMap S T)
x : S
y : T
z : Q
⊢ (algebraMap S T) x • y • z = x • y • z

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
i : M →ₗ[R] Q
this : Module S Q := Module.compHom Q (algebraMap S T)
x : S
y : T
z : Q
⊢ (algebraMap S T) x • y • z = x • y • z
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : 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 q : α × α
hpq✝ : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
⊢ Eq.ndrec (motive := fun x ↦ (∀ a ∈ x, P a) → Sym2 β) (g p) ⋯ Hq = g q Hq

Tactic:
]

Goal state after:
α : 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 q : α × α
hpq✝ : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
⊢ Eq.ndrec (motive := fun x ↦ (∀ a ∈ x, P a) → Sym2 β) (g p) ⋯ Hq = g q Hq
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : 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 q : α × α
hpq✝ : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
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
⊢ f p.1 ⋯ = f q.1 ⋯ ∧ f p.2 ⋯ = f q.2 ⋯ ∨ (f p.1 ⋯, f p.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)

Tactic:
]

Goal state after:
α : 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 q : α × α
hpq✝ : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
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
⊢ f p.1 ⋯ = f q.1 ⋯ ∧ f p.2 ⋯ = f q.2 ⋯ ∨ (f p.1 ⋯, f p.2 ⋯) = (f q.2 ⋯, f q.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
i : M →ₗ[R] Q
this✝¹ : Module S Q := Module.compHom Q (algebraMap S T)
this✝ : IsScalarTower S T Q
this : IsScalarTower R S Q
g' : O →ₗ[T] Q
e : ↑R g' ∘ₗ ↑R g ∘ₗ f = i
⊢ ↑R (↑S g' ∘ₗ g) ∘ₗ f = ↑R g' ∘ₗ ↑R g ∘ₗ f

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
i : M →ₗ[R] Q
this✝¹ : Module S Q := Module.compHom Q (algebraMap S T)
this✝ : IsScalarTower S T Q
this : IsScalarTower R S Q
g' : O →ₗ[T] Q
e : ↑R g' ∘ₗ ↑R g ∘ₗ f = i
⊢ ↑R (↑S g' ∘ₗ g) ∘ₗ f = ↑R g' ∘ₗ ↑R g ∘ₗ f
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
z : Sym2 α
b : β
x y : α
h : ∀ a ∈ Quot.mk (Rel α) (x, y), P a
⊢ b ∈ s(f x ⋯, f y ⋯) ↔ ∃ a, ∃ (ha : a ∈ Quot.mk (Rel α) (x, y)), b = f a ⋯

Tactic:
]

Goal state after:
case mk
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
z : Sym2 α
b : β
x y : α
h : ∀ a ∈ Quot.mk (Rel α) (x, y), P a
⊢ b ∈ s(f x ⋯, f y ⋯) ↔ ∃ a, ∃ (ha : a ∈ Quot.mk (Rel α) (x, y)), b = f a ⋯
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y : V
f f' : X ⟶ Y
e : f = f'
⊢ f ≍ f'

Tactic:
]

Goal state after:
V : Type u_1
inst✝ : Quiver V
X Y : V
f f' : X ⟶ Y
e : f = f'
⊢ f ≍ f'
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y : V
f f' : X ⟶ Y
e : f = f'
⊢ f' ≍ f'

Tactic:
]

Goal state after: