mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
⊢ m ≠ 0

Tactic:
by

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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
i : Fin m
h : ε i = 0
⊢ False

Tactic:
by

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 : ℝ
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
⊢ 0 < ↑(#A)

Tactic:
by

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 : ℝ
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
⊢ 3 ≠ 0

Tactic:
by

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 : ℝ
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
⊢ ↑(#A) ≤ ↑(#(A ^ 3))

Tactic:
by

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 : ℝ
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
δ : Fin 3 → ℤ
hδ : (δ 0 = 1 ∨ δ 0 = -1) ∧ (δ 1 = 1 ∨ δ 1 = -1) ∧ (δ 2 = 1 ∨ δ 2 = -1)
⊢ K ^ 2 ≤ K ^ 3

Tactic:
by

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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
⊢ ↑(#(List.map (fun i ↦ A ^ ε i) (finRange m)).prod) ≤ K ^ (3 * (m - 2)) * ↑(#A)

Tactic:
by

Goal state after:
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
f : V → W
G : SimpleGraph V
a b : W
⊢ (Ne ⊓ Relation.Map G.Adj f f) a b → (Ne ⊓ Relation.Map G.Adj f f) b a

Tactic:
by

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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
ε : ℤ
hε : |ε| = 1
⊢ A ^ ε = A

Tactic:
by

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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ), |ε| = 1 → A ^ ε = A
⊢ ↑(#(A ^ m)) = ↑(#(List.map (fun i ↦ A ^ 1) (finRange m)).prod)

Tactic:
by

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

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
u v : W
⊢ (SimpleGraph.map (⇑f) G).Adj u v ↔ ∃ u' v', G.Adj u' v' ∧ f u' = u ∧ f v' = v

Tactic:
by

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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ), |ε| = 1 → A ^ ε = A
δ : Fin 3 → ℤ
hδ : ∀ (i : Fin 3), |δ i| = 1
⊢ ↑(#(List.map (fun i ↦ A ^ δ i) (finRange 3)).prod) ≤ K * ↑(#A)

Tactic:
by

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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ), |ε| = 1 → A ^ ε = A
⊢ ∀ (i : Fin m), |1| = 1

Tactic:
by

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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
⊢ ↑(#(A ^ m)) ≤ K ^ (m - 2) * ↑(#A)

Tactic:
by

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
inst✝ : DecidableEq V
d : G.Dart
⊢ G.dartOfNeighborSet d.toProd.1 ⟨d.toProd.2, ⋯⟩ = d

Tactic:
by

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
inst✝ : DecidableEq V
v : V
⊢ {d | d.toProd.1 = v} = image (G.dartOfNeighborSet v) univ

Tactic:
by

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
inst✝ : DecidableEq V
v : V
⊢ #{d | d.toProd.1 = v} = G.degree v

Tactic:
by

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
this : DecidableEq V
⊢ Set.MapsTo (fun d ↦ d.toProd.1) ↑univ ↑univ

Tactic:
by

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
⊢ Fintype.card G.Dart = ∑ v, G.degree v

Tactic:
by

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
inst✝ : DecidableEq V
d d' : G.Dart
⊢ d' ∈ {d' | d'.edge = d.edge} ↔ d' ∈ {d, d.symm}

Tactic:
by

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

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
⊢ (SimpleGraph.map (⇑f) G).edgeSet = ⇑f.sym2Map '' G.edgeSet

Tactic:
by

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
inst✝ : DecidableEq V
e : Sym2 V
h : e ∈ G.edgeSet
⊢ #{d | d.edge = e} = 2

Tactic:
by

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
⊢ (SimpleGraph.map (⇑f) G).neighborSet (f v) = ⇑f '' G.neighborSet v

Tactic:
by

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
a b : V
⊢ (SimpleGraph.map (⇑f) G).Adj (f a) (f b) ↔ G.Adj a b

Tactic:
by

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

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V → W
⊢ Monotone (SimpleGraph.map f)

Tactic:
by

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
d : G.Dart
_h : d ∈ ↑univ
⊢ d.edge ∈ ↑G.edgeFinset

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ SimpleGraph.map id G = G

Tactic:
by

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
f : V → W
g : W → X
⊢ SimpleGraph.map g (SimpleGraph.map f G) = SimpleGraph.map (g ∘ f) G

Tactic:
by

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
⊢ Fintype.card G.Dart = 2 * #G.edgeFinset

Tactic:
by

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

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
⊢ (SimpleGraph.map (⇑f) G).support = ⇑f '' G.support

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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
⊢ 2 * #G.edgeFinset =
    #{x |
        match x with
        | (x, y) => G.Adj x y}

Tactic:
by

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

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V → W
hf : Injective f
⊢ SimpleGraph.comap f (completeGraph W) = completeGraph V

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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 ∈ G.support.toFinset, G.degree v = 2 * #G.edgeFinset

Tactic:
by

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

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

Tactic:
by

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:
by

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
⊢ SimpleGraph.map (⇑f) G ≤ G'

Tactic:
by

Goal state after:
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
e : V ≃ W
x✝ : SimpleGraph V
⊢ SimpleGraph.comap (⇑e) (SimpleGraph.comap (⇑e.symm) x✝) = x✝

Tactic:
by

Goal state after:
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
e : V ≃ W
x✝ : SimpleGraph W
⊢ SimpleGraph.comap (⇑e.symm) (SimpleGraph.comap (⇑e) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: V : Type u_1
⊢ (Equiv.refl V).simpleGraph = Equiv.refl (SimpleGraph V)

Tactic:
by

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

Goal state before:
pp: V : Type u_1
s : Set V
⊢ induce s ⊥ = ⊥

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set V
⊢ (induce s G).spanningCoe = G ↔ G.support ⊆ s

Tactic:
by

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
⊢ Even #{v | Odd (G.degree v)}

Tactic:
by

Goal state after:
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
⊢ (SimpleGraph.induce u G).IsCompleteBetween (u ↓∩ s) (u ↓∩ t)

Tactic:
by

Goal state after:
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
⊢ {v | Odd (G.degree v)}.Nonempty

Tactic:
by

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 : G →g G'
hinj : Injective ⇑f
⊢ Injective f.mapEdgeSet

Tactic:
by

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G' : SimpleGraph W
f : ⊤ →g G'
⊢ Injective ⇑f

Tactic:
by

Goal state after:
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
G₁ G₂ : SimpleGraph V
H : SimpleGraph W
f✝ : G✝ →g G'
f : V → W
G : SimpleGraph W
⊢ ∀ {a b : V}, (SimpleGraph.comap f G).Adj a b → G.Adj (f a) (f b)

Tactic:
by

Goal state after:
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 : V
⊢ Injective fun w ↦ ⟨f ↑w, ⋯⟩

Tactic:
by

Goal state after:
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'
⊢ ∀ {a b : V}, (induce (Set.range ⇑f) G').Adj ((Equiv.ofInjective ⇑f ⋯) a) ((Equiv.ofInjective ⇑f ⋯) b) ↔ G.Adj a b

Tactic:
by

Goal state after:
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'
f : V ↪ W
G : SimpleGraph W
⊢ ∀ {a b : V}, G.Adj (f a) (f b) ↔ (SimpleGraph.comap (⇑f) G).Adj a b

Tactic:
by

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

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

Tactic:
by

Goal state after:
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'
f : V ↪ W
G : SimpleGraph V
⊢ ∀ {a b : V}, (SimpleGraph.map (⇑f) G).Adj (f a) (f b) ↔ G.Adj a b

Tactic:
by

Goal state after:
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'
α : Type u_5
β : Type u_6
f : α ↪ β
⊢ ∀ {a b : α}, (completeGraph β).Adj (f a) (f b) ↔ (completeGraph α).Adj a b

Tactic:
by

Goal state after:
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'
G'' : SimpleGraph X
G''' : SimpleGraph Y
f : G ↪g H
⊢ ∀ {a b : V}, Hᶜ.Adj (f.toEmbedding a) (f.toEmbedding b) ↔ Gᶜ.Adj a b

Tactic:
by

Goal state after:
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
⊢ 0 < k

Tactic:
by

Goal state after:
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'
G'' : SimpleGraph X
G''' : SimpleGraph Y
f : Gᶜ ↪g Hᶜ
v w : V
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding w) ↔ G.Adj v w

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set V
⊢ induceHom Hom.id ⋯ = Hom.id

Tactic:
by

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
G'' : SimpleGraph X
s : Set V
t : Set W
r : Set X
φ : G →g G'
φst : Set.MapsTo (⇑φ) s t
ψ : G' →g G''
ψtr : Set.MapsTo (⇑ψ) t r
⊢ (induceHom ψ ψtr).comp (induceHom φ φst) = induceHom (ψ.comp φ) ⋯

Tactic:
by

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
s : Set V
t : Set W
φ : G →g G'
φst : Set.MapsTo (⇑φ) s t
hi : Set.InjOn (⇑φ) s
⊢ Injective ⇑(induceHom φ φst)

Tactic:
by

Goal state after:
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
s s' : Set V
h✝ h : s ⊆ s'
⊢ ∀ {a b : ↑s}, (induce s' G).Adj ((s.embeddingOfSubset s' h) a) ((s.embeddingOfSubset s' h) b) ↔ (induce s G).Adj a b

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s s' : Set V
h : s ⊆ s'
⊢ (G.induceHomOfLE h).toHom = induceHom Hom.id ⋯

Tactic:
by

Goal state after:
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
hk : 0 < k
⊢ (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v

Tactic:
by

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
v : V
f : G ≃g G'
⊢ ⇑f '' G.neighborSet v = G'.neighborSet (f v)

Tactic:
by

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 : G ≃g G'
⊢ f.symm.toHom.comp f.toHom = Hom.id

Tactic:
by

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 : G ≃g G'
⊢ f.toHom.comp f.symm.toHom = Hom.id

Tactic:
by

Goal state after:
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
f : G ≃g G'
⊢ LeftInverse (Hom.mapEdgeSet (RelIso.toRelEmbedding f.symm).toRelHom)
    (Hom.mapEdgeSet (RelIso.toRelEmbedding f).toRelHom)

Tactic:
by

Goal state after:
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
f : G ≃g G'
⊢ RightInverse (Hom.mapEdgeSet (RelIso.toRelEmbedding f.symm).toRelHom)
    (Hom.mapEdgeSet (RelIso.toRelEmbedding f).toRelHom)

Tactic:
by

Goal state after:
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
f : G ≃g G'
v : V
w : ↑(G'.neighborSet (f v))
⊢ f.symm ↑w ∈ G.neighborSet v

Tactic:
by

Goal state after:
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
f : G ≃g G'
v : V
w : ↑(G.neighborSet v)
⊢ (fun w ↦ ⟨f.symm ↑w, ⋯⟩) ((fun w ↦ ⟨f ↑w, ⋯⟩) w) = w

Tactic:
by

Goal state after:
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
f : G ≃g G'
v : V
w : ↑(G'.neighborSet (f v))
⊢ (fun w ↦ ⟨f ↑w, ⋯⟩) ((fun w ↦ ⟨f.symm ↑w, ⋯⟩) w) = w

Tactic:
by

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 : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
⊢ Fintype.card V = Fintype.card W

Tactic:
by

Goal state after:
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
f✝ : G✝ ≃g G'
f : V ≃ W
G : SimpleGraph W
⊢ ∀ {a b : V}, G.Adj (f a) (f b) ↔ (SimpleGraph.comap (⇑f) G).Adj a b

Tactic:
by

Goal state after:
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
f✝ : G✝ ≃g G'
f : V ≃ W
G : SimpleGraph V
⊢ ∀ {a b : V}, (SimpleGraph.map (⇑f) G).Adj (f a) (f b) ↔ G.Adj a b

Tactic:
by

Goal state after:
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
f✝ : G ≃g G'
α : Type u_5
β : Type u_6
f : α ≃ β
⊢ ∀ {a b : α}, (completeGraph β).Adj (f a) (f b) ↔ (completeGraph α).Adj a b

Tactic:
by

Goal state after:
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
f : G ≃g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
s : Set V
t : Set W
r : Set X
φ : G ≃g G'
φst : Set.BijOn (⇑φ) s t
ψ : G' ≃g G''
ψtr : Set.BijOn (⇑ψ) t r
v : ↑s
⊢ (fun w ↦ ⟨φ.symm ↑w, ⋯⟩) ((fun v ↦ ⟨φ ↑v, ⋯⟩) v) = v

Tactic:
by

Goal state after:
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
f : G ≃g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
s : Set V
t : Set W
r : Set X
φ : G ≃g G'
φst : Set.BijOn (⇑φ) s t
ψ : G' ≃g G''
ψtr : Set.BijOn (⇑ψ) t r
w : ↑t
⊢ (fun v ↦ ⟨φ ↑v, ⋯⟩) ((fun w ↦ ⟨φ.symm ↑w, ⋯⟩) w) = w

Tactic:
by

Goal state after:
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
f : G ≃g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
s : Set V
t : Set W
r : Set X
φ : G ≃g G'
φst : Set.BijOn (⇑φ) s t
ψ : G' ≃g G''
ψtr : Set.BijOn (⇑ψ) t r
⊢ ∀ {a b : ↑s},
    (induce t G').Adj
        ({ toFun := fun v ↦ ⟨φ ↑v, ⋯⟩, invFun := fun w ↦ ⟨φ.symm ↑w, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } a)
        ({ toFun := fun v ↦ ⟨φ ↑v, ⋯⟩, invFun := fun w ↦ ⟨φ.symm ↑w, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } b) ↔
      (induce s G).Adj a b

Tactic:
by

Goal state after:
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)
⊢ Odd #{w | w ≠ v ∧ Odd (G.degree w)}

Tactic:
by

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
G'' : SimpleGraph X
s : Set V
t : Set W
r : Set X
φ : G ≃g G'
φst : Set.BijOn (⇑φ) s t
ψ : G' ≃g G''
ψtr : Set.BijOn (⇑ψ) t r
⊢ (ψ.induce ψtr).comp (φ.induce φst) = (ψ.comp φ).induce ⋯

Tactic:
by

Goal state after:
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
G : SimpleGraph V
⊢ ∀ {a b : ↑Set.univ}, G.Adj ((Equiv.Set.univ V) a) ((Equiv.Set.univ V) b) ↔ (induce Set.univ G).Adj a b

Tactic:
by

Goal state after:
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
V₁ : Type u_5
V₂ : Type u_6
W₁ : Type u_7
W₂ : Type u_8
hV : V₁ ≃ V₂
hW : W₁ ≃ W₂
⊢ ∀ {a b : V₁ ⊕ W₁},
    (completeBipartiteGraph V₂ W₂).Adj ((hV.sumCongr hW) a) ((hV.sumCongr hW) b) ↔
      (completeBipartiteGraph V₁ W₁).Adj a b

Tactic:
by

Goal state after: