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

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
| ∑ x ∈ Ico m (n - 1), f x • ∑ i ∈ range (x + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i -
    ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i

Tactic:
;

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
| ∑ x ∈ Ico m (n - 1), f x • ∑ i ∈ range (x + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i -
    ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : R
⊢ (AlgebraTensorModule.rid R S S) (1 ⊗ₜ[R] x) = (Algebra.linearMap R S) x

Tactic:
simpa using (Algebra.algebraMap_eq_smul_one x).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : Multiset α
x✝¹ x✝ : List α
h : x✝¹ ≈ x✝
⊢ x✝¹.sym2.Perm x✝.sym2

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
m : Multiset α
x✝¹ x✝ : List α
h : x✝¹ ≈ x✝
⊢ x✝¹.sym2.Perm x✝.sym2
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
z : Sym2 α
⊢ z ∈ xs.sym2 ↔ ∀ y ∈ z, y ∈ xs

Tactic:
by
  refine z.ind (fun a b => ?_)
  simp [mk_mem_sym2_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : Fintype α
x : Sym2 α
⊢ ∀ a ∈ x, a ∈ univ

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : Fintype α
x : Sym2 α
⊢ ∀ a ∈ x, a ∈ univ
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.sym2 = ∅ ↔ s = ∅

Tactic:
;

Goal state after:
α : Type u_1
s : Finset α
⊢ s.sym2 = ∅ ↔ s = ∅
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case mk
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a✝ : Sym2 α
a b : α
⊢ Quot.mk (Sym2.Rel α) (a, b) ∈ s.sym2 ↔ Quot.mk (Sym2.Rel α) (a, b) ∈ image (Function.uncurry Sym2.mk) (s ×ˢ s)

Tactic:
;

Goal state after:
case mk
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a✝ : Sym2 α
a b : α
⊢ Quot.mk (Sym2.Rel α) (a, b) ∈ s.sym2 ↔ Quot.mk (Sym2.Rel α) (a, b) ∈ image (Function.uncurry Sym2.mk) (s ×ˢ s)
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case mk
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a✝ : Sym2 α
a b : α
⊢ a ∈ s ∧ b ∈ s ↔ ∃ a_1 b_1, (a_1 ∈ s ∧ b_1 ∈ s) ∧ (a_1 = a ∧ b_1 = b ∨ a_1 = b ∧ b_1 = a)

Tactic:
;

Goal state after:
case mk
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a✝ : Sym2 α
a b : α
⊢ a ∈ s ∧ b ∈ s ↔ ∃ a_1 b_1, (a_1 ∈ s ∧ b_1 ∈ s) ∧ (a_1 = a ∧ b_1 = b ∨ a_1 = b ∧ b_1 = a)
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
a b : α
h : a ∈ s ∧ a = b
⊢ a = b

Tactic:
;

Goal state after:
α : Type u_1
s : Finset α
a b : α
h : a ∈ s ∧ a = b
⊢ a = b
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
a b : α
h : a ∈ s ∧ b ∈ s ∧ ¬a = b
⊢ ¬a = b

Tactic:
;

Goal state after:
α : Type u_1
s : Finset α
a b : α
h : a ∈ s ∧ b ∈ s ∧ ¬a = b
⊢ ¬a = b
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
⊢ f' (s • 0) = s • f' 0

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)
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
⊢ f' (s • 0) = s • f' 0
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:
;

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)
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)
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
| s(y, x)

Tactic:
;

Goal state after:
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
| s(y, x)
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
h : s.Nonempty
⊢ (s.sym n).Nonempty

Tactic:
;

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
h : s.Nonempty
⊢ (s.sym n).Nonempty
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
⊢ s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅

Tactic:
;

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
⊢ s.sym n = ∅ ↔ n ≠ 0 ∧ 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 = (insert a s).erase a

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
m : ↥((insert a s).sym n)
⊢ s = (insert a s).erase a
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: case h
α : Type u_1
inst✝ : Lattice α
x✝ y✝ : α
⊢ s(x✝, y✝).inf ≤ s(x✝, y✝).sup

Tactic:
;

Goal state after:
case h
α : Type u_1
inst✝ : Lattice α
x✝ y✝ : α
⊢ s(x✝, y✝).inf ≤ s(x✝, y✝).sup
Module: Mathlib.Data.List.Sym

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_3
f : α → β
n : ℕ
xs x✝ : List α
⊢ [Sym.nil] = map (Sym.map f) [Sym.nil]
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.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
x✝ : Module R Q := I₂
⊢ ?m.148

Tactic:
;

Goal state after:
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
x✝ : Module R Q := I₂
⊢ ?m.148
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
x✝ : Module R Q := I₃
⊢ Q

Tactic:
;

Goal state after:
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
x✝ : Module R Q := I₃
⊢ Q
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a✝ b✝ : α × α
h : 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✝ : α × α
h : Rel α a✝ b✝
⊢ Rel β (Prod.map f f a✝) (Prod.map f f b✝)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x✝ y✝ : α
⊢ map g (map f s(x✝, y✝)) = map (g ∘ f) s(x✝, y✝)

Tactic:
;

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x✝ y✝ : α
⊢ map g (map f s(x✝, y✝)) = map (g ∘ f) s(x✝, y✝)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
hx' : Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
hx' : Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
x y z : α
⊢ z ∈ ↑s(x, y) ↔ z ∈ {x, y}

Tactic:
;

Goal state after:
α : Type u_1
x y z : α
⊢ z ∈ ↑s(x, y) ↔ z ∈ {x, y}
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z

Tactic:
convert! mem_mk_right a <| Mem.other h
  rw [other_spec h]

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
P : α → Prop
f : α → β
x✝ y✝ : α
h : ∀ a ∈ s(x✝, y✝), P a
⊢ pmap (fun a x ↦ f a) s(x✝, y✝) h = map f s(x✝, y✝)

Tactic:
;

Goal state after:
case h
α : Type u_1
β : Type u_2
P : α → Prop
f : α → β
x✝ y✝ : α
h : ∀ a ∈ s(x✝, y✝), P a
⊢ pmap (fun a x ↦ f a) s(x✝, y✝) h = map f s(x✝, y✝)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
Q : β → Prop
f : α → β
g : (b : β) → Q b → γ
x✝ y✝ : α
h : ∀ b ∈ map f s(x✝, y✝), Q b
⊢ pmap g (map f s(x✝, y✝)) h = pmap (fun a ha ↦ g (f a) ⋯) s(x✝, y✝) ⋯

Tactic:
;

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
Q : β → Prop
f : α → β
g : (b : β) → Q b → γ
x✝ y✝ : α
h : ∀ b ∈ map f s(x✝, y✝), Q b
⊢ pmap g (map f s(x✝, y✝)) h = pmap (fun a ha ↦ g (f a) ⋯) s(x✝, y✝) ⋯
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y : V
f g : X ⟶ Y
⊢ homOfEq f ⋯ ⋯ = g ↔ f = homOfEq g ⋯ ⋯

Tactic:
;

Goal state after:
V : Type u_1
inst✝ : Quiver V
X Y : V
f g : X ⟶ Y
⊢ homOfEq f ⋯ ⋯ = g ↔ f = homOfEq g ⋯ ⋯
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : β → γ
x✝ y✝ : α
h : ∀ a ∈ s(x✝, y✝), P a
h' : ∀ b ∈ pmap f s(x✝, y✝) h, Q b
⊢ map g (pmap f s(x✝, y✝) h) = pmap (fun a ha ↦ g (f a ⋯)) s(x✝, y✝) ⋯

Tactic:
;

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : β → γ
x✝ y✝ : α
h : ∀ a ∈ s(x✝, y✝), P a
h' : ∀ b ∈ pmap f s(x✝, y✝) h, Q b
⊢ map g (pmap f s(x✝, y✝) h) = pmap (fun a ha ↦ g (f a ⋯)) s(x✝, y✝) ⋯
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X' Y' : V
g f : X' ⟶ Y'
⊢ f = homOfEq g ⋯ ⋯ ↔ homOfEq f ⋯ ⋯ = g

Tactic:
;

Goal state after:
V : Type u_1
inst✝ : Quiver V
X' Y' : V
g f : X' ⟶ Y'
⊢ f = homOfEq g ⋯ ⋯ ↔ homOfEq f ⋯ ⋯ = g
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: case refl
V : Type u_1
inst✝ : Quiver V
X Y Y' : V
f : X ⟶ Y
hY : Y = Y'
g : X ⟶ Y'
⊢ homOfEq f ⋯ hY ≍ g ↔ f ≍ g

Tactic:
;

Goal state after:
case refl
V : Type u_1
inst✝ : Quiver V
X Y Y' : V
f : X ⟶ Y
hY : Y = Y'
g : X ⟶ Y'
⊢ homOfEq f ⋯ hY ≍ g ↔ f ≍ g
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: case refl.refl
V : Type u_1
inst✝ : Quiver V
X Y : V
f g : X ⟶ Y
⊢ homOfEq f ⋯ ⋯ ≍ g ↔ f ≍ g

Tactic:
;

Goal state after:
case refl.refl
V : Type u_1
inst✝ : Quiver V
X Y : V
f g : X ⟶ Y
⊢ homOfEq f ⋯ ⋯ ≍ g ↔ f ≍ g
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : (b : β) → Q b → γ
x✝ y✝ : α
h : ∀ a ∈ s(x✝, y✝), P a
h' : ∀ b ∈ pmap f s(x✝, y✝) h, Q b
⊢ pmap g (pmap f s(x✝, y✝) h) h' = pmap (fun a ha ↦ g (f a ⋯) ⋯) s(x✝, y✝) ⋯

Tactic:
;

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : (b : β) → Q b → γ
x✝ y✝ : α
h : ∀ a ∈ s(x✝, y✝), P a
h' : ∀ b ∈ pmap f s(x✝, y✝) h, Q b
⊢ pmap g (pmap f s(x✝, y✝) h) h' = pmap (fun a ha ↦ g (f a ⋯) ⋯) s(x✝, y✝) ⋯
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: case refl
V : Type u_1
inst✝ : Quiver V
X Y Y' : V
f : X ⟶ Y
hY : Y' = Y
g : X ⟶ Y'
⊢ f ≍ homOfEq g ⋯ hY ↔ f ≍ g

Tactic:
;

Goal state after:
case refl
V : Type u_1
inst✝ : Quiver V
X Y Y' : V
f : X ⟶ Y
hY : Y' = Y
g : X ⟶ Y'
⊢ f ≍ homOfEq g ⋯ hY ↔ f ≍ g
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: case refl.refl
V : Type u_1
inst✝ : Quiver V
X Y : V
f g : X ⟶ Y
⊢ f ≍ homOfEq g ⋯ ⋯ ↔ f ≍ g

Tactic:
;

Goal state after:
case refl.refl
V : Type u_1
inst✝ : Quiver V
X Y : V
f g : X ⟶ Y
⊢ f ≍ homOfEq g ⋯ ⋯ ↔ f ≍ g
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h
α : Type u_1
P : α → Prop
x✝ y✝ : α
h : ∀ a ∈ s(x✝, y✝), P a
⊢ map Subtype.val (pmap Subtype.mk s(x✝, y✝) h) = s(x✝, y✝)

Tactic:
;

Goal state after:
case h
α : Type u_1
P : α → Prop
x✝ y✝ : α
h : ∀ a ∈ s(x✝, y✝), P a
⊢ map Subtype.val (pmap Subtype.mk s(x✝, y✝) h) = s(x✝, y✝)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h
α : Type u_1
P : α → Prop
x✝ y✝ : α
h : ∀ a ∈ s(x✝, y✝), P a
⊢ map Subtype.val (s(x✝, y✝).attachWith h) = s(x✝, y✝)

Tactic:
;

Goal state after:
case h
α : Type u_1
P : α → Prop
x✝ y✝ : α
h : ∀ a ∈ s(x✝, y✝), P a
⊢ map Subtype.val (s(x✝, y✝).attachWith h) = s(x✝, y✝)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h
α : Type u_1
x✝ y✝ : α
h : s(x✝, y✝).IsDiag
⊢ diag (s(x✝, y✝).diagElem h) = s(x✝, y✝)

Tactic:
;

Goal state after:
case h
α : Type u_1
x✝ y✝ : α
h : s(x✝, y✝).IsDiag
⊢ diag (s(x✝, y✝).diagElem h) = s(x✝, y✝)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h.refl
α : Type u_1
x✝ : α
⊢ diag (s(x✝, x✝).diagElem ⋯) = s(x✝, x✝)

Tactic:
;

Goal state after:
case h.refl
α : Type u_1
x✝ : α
⊢ diag (s(x✝, x✝).diagElem ⋯) = s(x✝, x✝)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : { a // a.IsDiag }
x✝ : α
⊢ x✝ ∈ ↑((fun a ↦ ⟨diag a, ⋯⟩) ((fun x ↦ (↑x).diagElem ⋯) x)) ↔ x✝ ∈ ↑x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : { a // a.IsDiag }
x✝ : α
⊢ x✝ ∈ ↑((fun a ↦ ⟨diag a, ⋯⟩) ((fun x ↦ (↑x).diagElem ⋯) x)) ↔ x✝ ∈ ↑x
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:
;

Goal state after:
case mk
α : Type u_1
x✝ : Sym2 α
a b : α
⊢ Quot.mk (Rel α) (a, b) ∈ Set.range diag ↔ Quot.mk (Rel α) (a, b) ∈ diagSet
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
x✝ : Sym2 α
⊢ x✝ ∈ diagSet ↔ x✝ ∈ Set.univ

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Subsingleton α
x✝ : Sym2 α
⊢ x✝ ∈ diagSet ↔ x✝ ∈ Set.univ
Module: Mathlib.Data.Sym.Sym2

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

Tactic:
;

Goal state after:
α : Type u_1
z : Sym2 α
⊢ z ∈ fromRel ⋯ ↔ z ∈ {z | ¬z.IsDiag}
Module: Mathlib.Data.Sym.Sym2

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

Tactic:
;

Goal state after:
case mk
α : Type u_1
x✝ : Sym2 α
a b : α
⊢ Quot.mk (Rel α) (a, b) ∈ diagSet ↔ Quot.mk (Rel α) (a, b) ∈ fromRel ⋯
Module: Mathlib.Data.Sym.Sym2

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

Tactic:
;

Goal state after:
case mk
α : Type u_1
x✝ : Sym2 α
a b : α
⊢ Quot.mk (Rel α) (a, b) ∈ diagSetᶜ ↔ Quot.mk (Rel α) (a, b) ∈ fromRel ⋯
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : ∀ (a : α), ¬r a a
⊢ ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬z.IsDiag

Tactic:
;

Goal state after:
α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : ∀ (a : α), ¬r a a
⊢ ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬z.IsDiag
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : ∀ (a : α), ¬r a a
⊢ ∀ (x y : α), s(x, y) ∈ fromRel sym → ¬s(x, y).IsDiag

Tactic:
;

Goal state after:
α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : ∀ (a : α), ¬r a a
⊢ ∀ (x y : α), s(x, y) ∈ fromRel sym → ¬s(x, y).IsDiag
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y a✝ : α
⊢ a✝ ∈ s(x, y).toFinset ↔ a✝ ∈ {x, y}

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y a✝ : α
⊢ a✝ ∈ s(x, y).toFinset ↔ a✝ ∈ {x, y}
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case refl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ y✝ : α
⊢ [(x✝, y✝).2].Perm [(x✝, y✝).2]

Tactic:
;

Goal state after:
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ y✝ : α
⊢ [(x✝, y✝).2].Perm [(x✝, y✝).2]
Module: Mathlib.Data.Sym.Sym2

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

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

Tactic:
;

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

case cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝ : α
x : List α
hx : (head✝ :: x).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨head✝ :: x, hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨head✝ :: x, hx⟩) (fromVector ⟨y, hy⟩)
Module: Mathlib.Data.Sym.Sym2

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

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

Tactic:
;

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

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