mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : Mul α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this : s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
⊢ #(s * {t.min' ht} ∪ {s.max' hs} * t) ≤ #(s * t)

Tactic:
]

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : Mul α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this : s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
⊢ #(s * {t.min' ht} ∪ {s.max' hs} * t) ≤ #(s * t)
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ #(A ∩ x •> B⁻¹) ≤ #A

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ #(A ∩ x •> B⁻¹) ≤ #A
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ #(x⁻¹ •> A ∩ B⁻¹) ≤ #B⁻¹

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ #(x⁻¹ •> A ∩ B⁻¹) ≤ #B⁻¹
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B⁻¹⁻¹ x⁻¹ = B⁻¹.convolution A⁻¹ x

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B⁻¹⁻¹ x⁻¹ = B⁻¹.convolution A⁻¹ x
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ #(B⁻¹ ∩ x •> A) = #(B⁻¹ ∩ x •> A)

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ #(A <• s ∩ x •> B⁻¹) = #(A ∩ x •> B⁻¹ <• s⁻¹)

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ #(A <• s ∩ x •> B⁻¹) = #(A ∩ x •> B⁻¹ <• s⁻¹)
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ (s •> A).convolution B x⁻¹⁻¹ = A.convolution B (s⁻¹ * x)⁻¹⁻¹

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ (s •> A).convolution B x⁻¹⁻¹ = A.convolution B (s⁻¹ * x)⁻¹⁻¹
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ #((x⁻¹ * s) •> A ∩ B⁻¹) = #((x⁻¹ * s) •> A ∩ B⁻¹)

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ A.convolution (B <• s) x = A.convolution B⁻¹⁻¹ (x * s⁻¹)

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ A.convolution (B <• s) x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ #(A ∩ (x * s⁻¹) •> B⁻¹) = #(A ∩ (x * s⁻¹) •> B⁻¹)

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁ : x₁ ∈ s
hy₁ : y₁ ∈ s
hx₂ : x₂ ∈ s
hy₂ : y₂ ∈ s
hf' : InjOn (fun x ↦ (f x.1, f x.2)) (s ×ˢ s)
⊢ (f x₁, f y₁) ∈ Prod.map f f '' A ∧
      (f x₁, f y₂) ∈ Prod.map f f '' A ∧ (f x₂, f y₁) ∈ Prod.map f f '' A ∧ f x₁ + f y₂ = f x₂ + f y₁ ↔
    (x₁, y₁) ∈ A ∧ (x₁, y₂) ∈ A ∧ (x₂, y₁) ∈ A ∧ x₁ + y₂ = x₂ + y₁

Tactic:
]

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁ : x₁ ∈ s
hy₁ : y₁ ∈ s
hx₂ : x₂ ∈ s
hy₂ : y₂ ∈ s
hf' : InjOn (fun x ↦ (f x.1, f x.2)) (s ×ˢ s)
⊢ (f x₁, f y₁) ∈ Prod.map f f '' A ∧
      (f x₁, f y₂) ∈ Prod.map f f '' A ∧ (f x₂, f y₁) ∈ Prod.map f f '' A ∧ f x₁ + f y₂ = f x₂ + f y₁ ↔
    (x₁, y₁) ∈ A ∧ (x₁, y₂) ∈ A ∧ (x₂, y₁) ∈ A ∧ x₁ + y₂ = x₂ + y₁
Module: Mathlib.Combinatorics.SimpleGraph.Dart

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
a b : V
h : G.Adj (a, b).1 (a, b).2
u v : V
⊢ { fst := a, snd := b, adj := h }.toProd = (u, v) ∨ { fst := a, snd := b, adj := h }.toProd = (v, u) ↔
    { fst := a, snd := b, adj := h }.toProd.1 = u ∧ { fst := a, snd := b, adj := h }.toProd.2 = v ∨
      { fst := a, snd := b, adj := h }.toProd.1 = v ∧ { fst := a, snd := b, adj := h }.toProd.2 = u

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
a b : V
h : G.Adj (a, b).1 (a, b).2
u v : V
⊢ { fst := a, snd := b, adj := h }.toProd = (u, v) ∨ { fst := a, snd := b, adj := h }.toProd = (v, u) ↔
    { fst := a, snd := b, adj := h }.toProd.1 = u ∧ { fst := a, snd := b, adj := h }.toProd.2 = v ∨
      { fst := a, snd := b, adj := h }.toProd.1 = v ∧ { fst := a, snd := b, adj := h }.toProd.2 = u
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (Fin n → ℤ) → Finset G := fun {n} δ ↦ (List.map (fun i ↦ A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
⊢ k * ↑(#A) * (k ^ (m - 1) * ↑(#A)) = ↑(#A) * (k ^ (m - 1) * k * ↑(#A))

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (Fin n → ℤ) → Finset G := fun {n} δ ↦ (List.map (fun i ↦ A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
⊢ k * ↑(#A) * (k ^ (m - 1) * ↑(#A)) = ↑(#A) * (k ^ (m - 1) * k * ↑(#A))
Module: Mathlib.Combinatorics.Additive.Corner.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
this : Prod.map f f '' A ⊆ t ×ˢ t
⊢ (∀ ⦃x₁ : H⦄,
      x₁ ∈ t →
        ∀ ⦃y₁ : H⦄,
          y₁ ∈ t → ∀ ⦃x₂ : H⦄, x₂ ∈ t → ∀ ⦃y₂ : H⦄, y₂ ∈ t → IsCorner (Prod.map f f '' A) x₁ y₁ x₂ y₂ → x₁ = x₂) ↔
    ∀ ⦃x₁ : G⦄, x₁ ∈ s → ∀ ⦃y₁ : G⦄, y₁ ∈ s → ∀ ⦃x₂ : G⦄, x₂ ∈ s → ∀ ⦃y₂ : G⦄, y₂ ∈ s → IsCorner A x₁ y₁ x₂ y₂ → x₁ = x₂

Tactic:
]

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
this : Prod.map f f '' A ⊆ t ×ˢ t
⊢ (∀ ⦃x₁ : H⦄,
      x₁ ∈ t →
        ∀ ⦃y₁ : H⦄,
          y₁ ∈ t → ∀ ⦃x₂ : H⦄, x₂ ∈ t → ∀ ⦃y₂ : H⦄, y₂ ∈ t → IsCorner (Prod.map f f '' A) x₁ y₁ x₂ y₂ → x₁ = x₂) ↔
    ∀ ⦃x₁ : G⦄, x₁ ∈ s → ∀ ⦃y₁ : G⦄, y₁ ∈ s → ∀ ⦃x₂ : G⦄, x₂ ∈ s → ∀ ⦃y₂ : G⦄, y₂ ∈ s → IsCorner A x₁ y₁ x₂ y₂ → x₁ = x₂
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (Fin n → ℤ) → Finset G := fun {n} δ ↦ (List.map (fun i ↦ A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
⊢ k * ↑(#A) * (k ^ (m - 1) * ↑(#A)) = ↑(#A) * (k ^ m * ↑(#A))

Tactic:
by rw [← pow_sub_one_mul hm₀]; ring

Goal state after:
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#A) * ↑(#(A⁻¹ * (A * A))) = ↑(#A) * ↑(#(A⁻¹ * (A * A)))

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ K * ↑(#A) * (K * ↑(#A)) = ↑(#A) * (K ^ 2 * ↑(#A))

Tactic:
by ring

Goal state after:
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A⁻¹ * A⁻¹ * A)⁻¹) ≤ K ^ 2 * ↑(#A)

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A⁻¹ * A⁻¹ * A)⁻¹) ≤ K ^ 2 * ↑(#A)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A * A * A⁻¹)⁻¹) ≤ K ^ 2 * ↑(#A)

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A * A * A⁻¹)⁻¹) ≤ K ^ 2 * ↑(#A)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
⊢ K ^ 2 * ↑(#A) * (K * ↑(#A)) = ↑(#A) * (K ^ 3 * ↑(#A))

Tactic:
by ring

Goal state after:
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A⁻¹ * A * A⁻¹)⁻¹) ≤ K ^ 3 * ↑(#A)

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A⁻¹ * A * A⁻¹)⁻¹) ≤ K ^ 3 * ↑(#A)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
⊢ ↑(#(List.map (fun i ↦ A ^ ε i) (finRange m)).prod) ≤ (K ^ 3) ^ (m - 2) * ↑(#A)

Tactic:
]

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
⊢ ↑(#(List.map (fun i ↦ A ^ ε i) (finRange m)).prod) ≤ (K ^ 3) ^ (m - 2) * ↑(#A)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case h
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝) ↔ ∃ x ∈ G.edgeSet, f.sym2Map x = s(x✝, y✝)

Tactic:
]

Goal state after:
case h
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝) ↔ ∃ x ∈ G.edgeSet, f.sym2Map x = s(x✝, y✝)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case right
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
a b : V
hadj : G.Adj a b
ha : f a = x✝
hb : f b = y✝
⊢ s(x✝, y✝) = s(x✝, y✝)

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case h.mpr.h
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝¹ y✝¹ : W
x✝ y✝ : V
hadj : s(x✝, y✝) ∈ G.edgeSet
he : f x✝ = x✝¹ ∧ f y✝ = y✝¹ ∨ f x✝ = y✝¹ ∧ f y✝ = x✝¹
⊢ ∃ u' v', G.Adj u' v' ∧ f u' = x✝¹ ∧ f v' = y✝¹

Tactic:
]

Goal state after:
case h.mpr.h
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝¹ y✝¹ : W
x✝ y✝ : V
hadj : s(x✝, y✝) ∈ G.edgeSet
he : f x✝ = x✝¹ ∧ f y✝ = y✝¹ ∨ f x✝ = y✝¹ ∧ f y✝ = x✝¹
⊢ ∃ u' v', G.Adj u' v' ∧ f u' = x✝¹ ∧ f v' = y✝¹
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: case e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ 2 = 1 + 1

pp: case e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ d ∉ {d.symm}

Tactic:
]

Goal state after:
case e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ d ∉ {d.symm}
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: case e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ ¬d = d.symm

Tactic:
]

Goal state after:
case e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ ¬d = d.symm
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #univ = 2 * #G.edgeFinset

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #univ = 2 * #G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
d : G.Dart
_h : d ∈ ↑univ
⊢ d.edge ∈ G.edgeSet

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
d : G.Dart
_h : d ∈ ↑univ
⊢ d.edge ∈ G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∑ b ∈ G.edgeFinset, #{a | a.edge = b} = 2 * #G.edgeFinset

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∑ b ∈ G.edgeFinset, #{a | a.edge = b} = 2 * #G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #G.edgeFinset * ?m.53 = #G.edgeFinset * 2

pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ x ∈ G.edgeFinset, #{a | a.edge = x} = ?m.53

pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ℕ

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ x ∈ G.edgeFinset, #{a | a.edge = x} = 2
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
h : e ∈ G.edgeFinset
⊢ e ∈ G.edgeFinset

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
h : e ∈ G.edgeFinset
⊢ e ∈ G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #univ =
    #{x |
        match x with
        | (x, y) => G.Adj x y}

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #univ =
    #{x |
        match x with
        | (x, y) => G.Adj x y}
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph W
e : V ≃ W
⊢ SimpleGraph.comap (⇑e.toEmbedding) G = SimpleGraph.comap (⇑e.toEmbedding) G

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
hv : v ∈ G.support.toFinsetᶜ
⊢ v ∉ G.support

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
hv : v ∈ G.support.toFinsetᶜ
⊢ v ∉ G.support
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
hv : v ∉ G.support
⊢ v ∉ G.support

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
hv : v ∉ G.support
⊢ v ∉ G.support
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph W
⊢ SimpleGraph.comap (⇑f) G ≤ SimpleGraph.comap (⇑f) G

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V ↪ W
inst✝ : Subsingleton V
⊢ G ≤ SimpleGraph.comap (⇑f) G'

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V ↪ W
inst✝ : Subsingleton V
⊢ G ≤ SimpleGraph.comap (⇑f) G'
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
⊢ Even #{v | Odd (G.degree v)}

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
⊢ Even #{v | Odd (G.degree v)}
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ _v with ↑(G.degree _v) ≠ 0, 1 = 0
⊢ Even #{v | Odd (G.degree v)}

pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
⊢ ∀ x ∈ {x | ↑(G.degree x) ≠ 0}, ↑(G.degree x) = 1

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ _v with ↑(G.degree _v) ≠ 0, 1 = 0
⊢ Even #{v | Odd (G.degree v)}

V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
⊢ ∀ x ∈ {x | ↑(G.degree x) ≠ 0}, ↑(G.degree x) = 1
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
⊢ ⊤ ≤ induce {v} G

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
⊢ ⊤ ≤ induce {v} G
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(#{x | ¬↑(G.degree x) = 0}) = 0
⊢ ↑(#{v | Odd (G.degree v)}) = 0

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(#{x | ¬↑(G.degree x) = 0}) = 0
⊢ ↑(#{v | Odd (G.degree v)}) = 0
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe = G
v : V
hv : v ∈ Subtype.val '' (induce s G).support
⊢ v ∈ s

Tactic:
]

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe = G
v : V
hv : v ∈ Subtype.val '' (induce s G).support
⊢ v ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
v : V
⊢ ¬Even (G.degree v) → ¬Even (G.degree v)

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
v : V
⊢ ¬Even (G.degree v) → ¬Even (G.degree v)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁✝ : ↑u
hs : v₁✝ ∈ u ↓∩ s
v₂✝ : ↑u
ht : v₂✝ ∈ u ↓∩ t
⊢ G.Adj ↑v₁✝ ↑v₂✝

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁✝ : ↑u
hs : v₁✝ ∈ u ↓∩ s
v₂✝ : ↑u
ht : v₂✝ ∈ u ↓∩ t
⊢ G.Adj ↑v₁✝ ↑v₂✝
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Sym2.map (⇑f) e₁ = Sym2.map (⇑f) e₂ → ⟨e₁, h₁⟩ = ⟨e₂, h₂⟩

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Sym2.map (⇑f) e₁ = Sym2.map (⇑f) e₂ → ⟨e₁, h₁⟩ = ⟨e₂, h₂⟩
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
⊢ Odd (G.degree v)

Tactic:
]

Goal state after:
case h
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
⊢ Odd (G.degree v)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Sym2.map (⇑f) e₁ = Sym2.map (⇑f) e₂ → e₁ = e₂

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Sym2.map (⇑f) e₁ = Sym2.map (⇑f) e₂ → e₁ = e₂
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v✝ : V
H : SimpleGraph W
f : G ↪g G'
v w₁ : V
h₁ : w₁ ∈ G.neighborSet v
w₂ : V
h₂ : w₂ ∈ G.neighborSet v
h : f ↑⟨w₁, h₁⟩ = f ↑⟨w₂, h₂⟩
⊢ w₁ = w₂

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v✝ : V
H : SimpleGraph W
f : G ↪g G'
v w₁ : V
h₁ : w₁ ∈ G.neighborSet v
w₂ : V
h₂ : w₂ ∈ G.neighborSet v
h : f ↑⟨w₁, h₁⟩ = f ↑⟨w₂, h₂⟩
⊢ w₁ = w₂
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hh : 0 < k
⊢ 0 < k

pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hh : 0 < 2 * k
⊢ 0 < 2

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hh : 0 < k
⊢ 0 < k

V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hh : 0 < 2 * k
⊢ 0 < 2