mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: case nil
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ x ∈ [], f x ≡ g x [ZMOD n]
⊢ (List.map f []).sum ≡ (List.map g []).sum [ZMOD n]

pp: case cons
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ x ∈ tail✝, f x ≡ g x [ZMOD n]) → (List.map f tail✝).sum ≡ (List.map g tail✝).sum [ZMOD n]
h : ∀ x ∈ head✝ :: tail✝, f x ≡ g x [ZMOD n]
⊢ (List.map f (head✝ :: tail✝)).sum ≡ (List.map g (head✝ :: tail✝)).sum [ZMOD n]

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ x ∈ [], f x ≡ g x [ZMOD n]
⊢ (List.map f []).sum ≡ (List.map g []).sum [ZMOD n]

case cons
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ x ∈ tail✝, f x ≡ g x [ZMOD n]) → (List.map f tail✝).sum ≡ (List.map g tail✝).sum [ZMOD n]
h : ∀ x ∈ head✝ :: tail✝, f x ≡ g x [ZMOD n]
⊢ (List.map f (head✝ :: tail✝)).sum ≡ (List.map g (head✝ :: tail✝)).sum [ZMOD n]
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: case h₀
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 1
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 1
⊢ ∀ b ∈ s, b ≠ a → ↑(f b) = 1

pp: case h₁
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 1
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 1
⊢ a ∉ s → ↑(f a) = 1

Tactic:
<;>

Goal state after:
case h₀
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 1
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 1
⊢ ∀ b ∈ s, b ≠ a → ↑(f b) = 1

case h₁
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 1
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 1
⊢ a ∉ s → ↑(f a) = 1
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: case h₀
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ ∀ b ∈ s, b ≠ a → ↑(f b) = 0

pp: case h₁
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ a ∉ s → ↑(f a) = 0

Tactic:
<;>

Goal state after:
case h₀
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ ∀ b ∈ s, b ≠ a → ↑(f b) = 0

case h₁
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ a ∉ s → ↑(f a) = 0
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case e'_2
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
hF : ∀ (s : S) (m : M), (h.lift g) (s • f m) = s • g m
⊢ f x = 1 • f x

pp: case e'_3
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 u_3
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
hF : ∀ (s : S) (m : M), (h.lift g) (s • f m) = s • g m
⊢ g x = 1 • g x

Tactic:
<;>

Goal state after:
case e'_2
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
hF : ∀ (s : S) (m : M), (h.lift g) (s • f m) = s • g m
⊢ f x = 1 • f x

case e'_3
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 u_3
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
hF : ∀ (s : S) (m : M), (h.lift g) (s • f m) = s • g m
⊢ g x = 1 • g x
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case nil
α : Type u_1
⊢ [].sym2 = [] ↔ [] = []

pp: case cons
α : Type u_1
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).sym2 = [] ↔ head✝ :: tail✝ = []

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
⊢ [].sym2 = [] ↔ [] = []

case cons
α : Type u_1
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).sym2 = [] ↔ head✝ :: tail✝ = []
Module: Mathlib.Data.List.Sym

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case inl
α : Type u_1
xs : List α
ih : xs.sym2.Nodup
w✝ : α
h : w✝ ∉ xs ∧ xs.Nodup
hz' : s(w✝, w✝) ∈ xs.sym2
⊢ False

pp: case inr
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
w✝ : α
h✝ : w✝ ∈ xs
hz' : s(x, w✝) ∈ xs.sym2
⊢ False

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
xs : List α
ih : xs.sym2.Nodup
w✝ : α
h : w✝ ∉ xs ∧ xs.Nodup
hz' : s(w✝, w✝) ∈ xs.sym2
⊢ False

case inr
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
w✝ : α
h✝ : w✝ ∈ xs
hz' : s(x, w✝) ∈ xs.sym2
⊢ False
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case inl
α : Type u_1
xs : List α
ih : xs.sym2.Nodup
w✝ : α
h : w✝ ∉ xs ∧ xs.Nodup
hz' : s(w✝, w✝) ∈ xs.sym2
⊢ False

Tactic:
simp [left_mem_of_mk_mem_sym2 hz'] at h

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

Goal state before:
pp: case inr
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
w✝ : α
h✝ : w✝ ∈ xs
hz' : s(x, w✝) ∈ xs.sym2
⊢ False

Tactic:
simp [left_mem_of_mk_mem_sym2 hz'] at h

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

Goal state before:
pp: case inl
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
a : α
⊢ a = a

pp: case inr
α : Type u_1
xs : List α
ih : xs.sym2.Nodup
a : α
h : a ∉ xs ∧ xs.Nodup
⊢ a = a

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
a : α
⊢ a = a

case inr
α : Type u_1
xs : List α
ih : xs.sym2.Nodup
a : α
h : a ∉ xs ∧ xs.Nodup
⊢ a = a
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 ++ xs.sym2)).dedup = s(x, x) :: map (fun y ↦ s(x, y)) xs.dedup ++ xs.sym2.dedup

Tactic:
dedup_cons_of_notMem,

Goal state after:
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).dedup = s(x, x) :: map (fun y ↦ s(x, y)) xs.dedup ++ xs.sym2.dedup

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.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
⊢ List.sym 1 (x :: xs) = (x ::ₛ Sym.nil) :: List.sym 1 xs

Tactic:
List.sym,

Goal state after:
case cons
α : Type u_1
xs✝ : List α
x : α
xs : List α
ih : List.sym 1 xs = map (fun x ↦ x ::ₛ Sym.nil) xs
⊢ map (fun p ↦ x ::ₛ p) (List.sym 0 (x :: xs)) ++ List.sym (0 + 1) xs = (x ::ₛ Sym.nil) :: List.sym 1 xs
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
⊢ map (fun p ↦ x ::ₛ p) (List.sym 0 (x :: xs)) ++ List.sym (0 + 1) xs = (x ::ₛ Sym.nil) :: List.sym 1 xs

Tactic:
List.sym,

Goal state after:
case cons
α : Type u_1
xs✝ : List α
x : α
xs : List α
ih : List.sym 1 xs = map (fun x ↦ x ::ₛ Sym.nil) xs
⊢ map (fun p ↦ x ::ₛ p) [Sym.nil] ++ List.sym (0 + 1) xs = (x ::ₛ Sym.nil) :: List.sym 1 xs
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
⊢ f' (s • (x + y)) = s • f' (x + y)

Tactic:
rw [smul_add, map_add, map_add, smul_add, hx, hy]

Goal state after:
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 α)) (x :: xs).sym2 = List.sym 2 (x :: xs)

Tactic:
List.sym,

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 α)) (x :: xs).sym2 = map (fun p ↦ x ::ₛ p) (List.sym 1 (x :: xs)) ++ List.sym (1 + 1) xs
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: case h.h.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

pp: case h.h.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hba : b ≤ a
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

Tactic:
<;>

Goal state after:
case h.h.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

case h.h.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hba : b ≤ a
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: case h.h.inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

pp: case h.h.inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hdc : d ≤ c
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

pp: case h.h.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hba : b ≤ a
hcd : c ≤ d
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

pp: case h.h.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hba : b ≤ a
hdc : d ≤ c
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

Tactic:
<;>

Goal state after:
case h.h.inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

case h.h.inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hdc : d ≤ c
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

case h.h.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hba : b ≤ a
hcd : c ≤ d
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

case h.h.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hba : b ≤ a
hdc : d ≤ c
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
Module: Mathlib.Data.List.Sym

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

Tactic:
List.sym,

Goal state after:
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ map (fun p ↦ f x ::ₛ p) (List.sym n (f x :: map f xs)) ++ List.sym (n + 1) (map f xs) =
    map (Sym.map f) (List.sym (n + 1) (x :: xs))
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 <+ List.sym (n + 1) (a :: l₂✝)

Tactic:
List.sym,

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₂✝
⊢ List.sym (n + 1) (a :: l₁✝) <+ List.sym (n + 1) (a :: l₂✝)

Tactic:
List.sym,

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₁✝ <+ List.sym (n + 1) (a :: 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 : z ∈ List.sym (n + 1) (x :: xs)
⊢ a ∈ x :: xs

Tactic:
List.sym,

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

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

Tactic:
List.sym,

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

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

Tactic:
List.sym,

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

Goal state before:
pp: case refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x✝ y✝ : α
⊢ Rel β (Prod.map f f (x✝, y✝)) (Prod.map f f (x✝, y✝))

pp: case swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x✝ y✝ : α
⊢ Rel β (Prod.map f f (x✝, y✝)) (Prod.map f f (y✝, x✝))

Tactic:
<;>

Goal state after:
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x✝ y✝ : α
⊢ Rel β (Prod.map f f (x✝, y✝)) (Prod.map f f (x✝, y✝))

case swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x✝ y✝ : α
⊢ Rel β (Prod.map f f (x✝, y✝)) (Prod.map f f (y✝, x✝))
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
a b₁ : α
⊢ b₁ = b₁

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
b₁ : α
⊢ b₁ = b₁

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
a b₁ : α
⊢ b₁ = b₁

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
b₁ : α
⊢ b₁ = b₁
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: case empty
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
⊢ ∑ i ∈ ∅, f i = ⊤ ↔ ∃ i ∈ ∅, f i = ⊤

pp: case cons
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∑ i ∈ s✝, f i = ⊤ ↔ ∃ i ∈ s✝, f i = ⊤
⊢ ∑ i ∈ cons a✝¹ s✝ h✝, f i = ⊤ ↔ ∃ i ∈ cons a✝¹ s✝ h✝, f i = ⊤

Tactic:
<;>

Goal state after:
case empty
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
⊢ ∑ i ∈ ∅, f i = ⊤ ↔ ∃ i ∈ ∅, f i = ⊤

case cons
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∑ i ∈ s✝, f i = ⊤ ↔ ∃ i ∈ s✝, f i = ⊤
⊢ ∑ i ∈ cons a✝¹ s✝ h✝, f i = ⊤ ↔ ∃ i ∈ cons a✝¹ s✝ h✝, f i = ⊤
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: case empty
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
⊢ ∑ i ∈ ∅, f i = ⊥ ↔ ∃ i ∈ ∅, f i = ⊥

pp: case cons
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∑ i ∈ s✝, f i = ⊥ ↔ ∃ i ∈ s✝, f i = ⊥
⊢ ∑ i ∈ cons a✝¹ s✝ h✝, f i = ⊥ ↔ ∃ i ∈ cons a✝¹ s✝ h✝, f i = ⊥

Tactic:
<;>

Goal state after:
case empty
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
⊢ ∑ i ∈ ∅, f i = ⊥ ↔ ∃ i ∈ ∅, f i = ⊥

case cons
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∑ i ∈ s✝, f i = ⊥ ↔ ∃ i ∈ s✝, f i = ⊥
⊢ ∑ i ∈ cons a✝¹ s✝ h✝, f i = ⊥ ↔ ∃ i ∈ cons a✝¹ s✝ h✝, f i = ⊥
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ (∃ a ∈ s, f a = y) → ∃ a ∈ s, g a = y

pp: case mpr
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ (∃ a ∈ s, g a = y) → ∃ a ∈ s, f a = y

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ (∃ a ∈ s, f a = y) → ∃ a ∈ s, g a = y

case mpr
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ (∃ a ∈ s, g a = y) → ∃ a ∈ s, f a = y
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case f
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := ⋯
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
⊢ p = q → f p.1 ⋯ = f q.1 ⋯ ∧ f p.2 ⋯ = f q.2 ⋯

pp: case g
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := ⋯
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
⊢ p = q.swap → (f p.1 ⋯, f p.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)

Tactic:
<;>

Goal state after:
case f
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := ⋯
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
⊢ p = q → f p.1 ⋯ = f q.1 ⋯ ∧ f p.2 ⋯ = f q.2 ⋯

case g
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := ⋯
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
⊢ p = q.swap → (f p.1 ⋯, f p.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)
Module: Mathlib.Data.Sym.Sym2

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case refl
α : Type u_1
x : α
h : diag x = diag x
⊢ x = x

pp: case swap
α : Type u_1
x : α
h : diag x = diag x
⊢ x = x

Tactic:
<;>

Goal state after:
case refl
α : Type u_1
x : α
h : diag x = diag x
⊢ x = x

case swap
α : Type u_1
x : α
h : diag x = diag x
⊢ x = x
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case refl.refl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a : α
⊢ Eq.ndrec (motive := fun x ↦ x.IsDiag → α) (fun x ↦ a) ⋯ ⋯ = a

pp: case refl.swap
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a : α
⊢ Eq.ndrec (motive := fun x ↦ x.IsDiag → α) (fun x ↦ a) ⋯ ⋯ = a

Tactic:
<;>

Goal state after:
case refl.refl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a : α
⊢ Eq.ndrec (motive := fun x ↦ x.IsDiag → α) (fun x ↦ a) ⋯ ⋯ = a

case refl.swap
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a : α
⊢ Eq.ndrec (motive := fun x ↦ x.IsDiag → α) (fun x ↦ a) ⋯ ⋯ = a
Module: Mathlib.Data.Sym.Sym2

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

Tactic:
simp [diag, eq_comm]

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

Goal state before:
pp: α : Type u_1
⊢ fromRel ⋯ = {z | ¬z.IsDiag}

Tactic:
by
  ext z; exact z.ind (by simp)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
⊢ ∀ ⦃a b : List.Vector α 2⦄, (Vector.Perm.isSetoid α 2) a b → Rel α (fromVector a) (fromVector b)

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : List α
hx : x.length = 2
y : List α
hy : y.length = 2
h : (Vector.Perm.isSetoid α 2) ⟨x, hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨x, hx⟩) (fromVector ⟨y, hy⟩)
Module: Mathlib.CategoryTheory.Category.Basic

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

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

Tactic:
<;>

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

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