awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : IsEmpty V
rw : Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max (image (fun (v : V) ↦ G.degree v) univ))) 0
rw₁ : Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max (image (fun (v : V) ↦ G.degree v) ∅))) 0
rw₂ : Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max ∅)) 0
rw₃ : Eq (α := ℕ) (WithBot.unbotD 0 ⊥) 0
rw₄ rw₅ : Eq (α := ℕ) 0 0
⊢ G.maxDegree = 0

Tactic:
rw [maxDegree, univ_eq_empty, image_empty, max_empty, WithBot.unbotD_bot]

Premises used: SimpleGraph.maxDegree, Finset.image_empty, WithBot.unbotD_bot, Finset.univ_eq_empty, Finset.max_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
inl : IsEmpty V → G.maxDegree ≤ k
inr : Nonempty V → G.maxDegree ≤ k
⊢ G.maxDegree ≤ k

Tactic:
cases isEmpty_or_nonempty V

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
h_1 : IsEmpty V
⊢ G.maxDegree ≤ k

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
h_1 : Nonempty V
inr : ∀ (w : V) (hv : G.maxDegree = G.degree w), G.maxDegree ≤ k
⊢ G.maxDegree ≤ k

Tactic:
obtain ⟨_, hv⟩ := G.exists_maximal_degree_vertex

Premises used: SimpleGraph.exists_maximal_degree_vertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
h_1 : Nonempty V
w : V
hv : G.maxDegree = G.degree w
⊢ G.maxDegree ≤ k

Tactic:
hv ▸ h _

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
h_1 : Nonempty V
w : V
hv : G.maxDegree = G.degree w
⊢ G.maxDegree ≤ k

Tactic:
exact hv ▸ h _
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Nonempty V
inst_2 : DecidableRel G.Adj
d : ℕ
h : G.IsRegularOfDegree d
⊢ G.maxDegree = d

Tactic:
simp [maxDegree, h.degree_eq, Finset.image_const]

Premises used: SimpleGraph.maxDegree, Finset.image_const, SimpleGraph.IsRegularOfDegree.degree_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
⊢ ∀ (v : V), degree ⊥ v ≤ 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
inl : IsEmpty V → maxDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1
inr : Nonempty V → maxDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1
⊢ maxDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1

Tactic:
cases isEmpty_or_nonempty V

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
h : IsEmpty V
⊢ maxDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
h : Nonempty V
⊢ maxDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1

Tactic:
IsRegularOfDegree.top.maxDegree_eq

Premises used: SimpleGraph.IsRegularOfDegree.maxDegree_eq, SimpleGraph.IsRegularOfDegree.top
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
h : Nonempty V
⊢ maxDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1

Tactic:
exact IsRegularOfDegree.top.maxDegree_eq

Premises used: SimpleGraph.IsRegularOfDegree.maxDegree_eq, SimpleGraph.IsRegularOfDegree.top
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
pos : ∀ (he : IsEmpty V), G.minDegree ≤ G.maxDegree
neg : ∀ (he : Nonempty V), G.minDegree ≤ G.maxDegree
⊢ G.minDegree ≤ G.maxDegree

Tactic:
by_cases! he : IsEmpty V

Premises used: IsEmpty
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
he : IsEmpty V
⊢ G.minDegree ≤ G.maxDegree

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
he : Nonempty V
⊢ G.minDegree ≤ G.maxDegree

Tactic:
he.elim fun v ↦ (minDegree_le_degree _ v).trans (degree_le_maxDegree _ v)

Premises used: SimpleGraph.degree_le_maxDegree, Nonempty.elim, LE.le.trans, SimpleGraph.minDegree_le_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
he : Nonempty V
⊢ G.minDegree ≤ G.maxDegree

Tactic:
exact he.elim fun v ↦ (minDegree_le_degree _ v).trans (degree_le_maxDegree _ v)

Premises used: SimpleGraph.degree_le_maxDegree, Nonempty.elim, LE.le.trans, SimpleGraph.minDegree_le_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Nonempty V
inst_2 : DecidableRel G.Adj
d : ℕ
h : G.IsRegularOfDegree d
⊢ G.minDegree = d

Tactic:
simp [minDegree, h.degree_eq, Finset.image_const]

Premises used: Finset.image_const, SimpleGraph.minDegree, SimpleGraph.IsRegularOfDegree.degree_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
⊢ maxDegree.{u_1} (V := V) ⊥ ≤ 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
inl : IsEmpty V → minDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1
inr : Nonempty V → minDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1
⊢ minDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1

Tactic:
cases isEmpty_or_nonempty V

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
h : IsEmpty V
⊢ minDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
h : Nonempty V
⊢ minDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1

Tactic:
IsRegularOfDegree.top.minDegree_eq

Premises used: SimpleGraph.IsRegularOfDegree.minDegree_eq, SimpleGraph.IsRegularOfDegree.top
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
h : Nonempty V
⊢ minDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1

Tactic:
exact IsRegularOfDegree.top.minDegree_eq

Premises used: SimpleGraph.IsRegularOfDegree.minDegree_eq, SimpleGraph.IsRegularOfDegree.top
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Nonempty V
obtain : ∀ (v : V) (hv : G.maxDegree = G.degree v), G.maxDegree < Fintype.card V
⊢ G.maxDegree < Fintype.card V

Tactic:
obtain ⟨v, hv⟩ := G.exists_maximal_degree_vertex

Premises used: SimpleGraph.exists_maximal_degree_vertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Nonempty V
v : V
hv : G.maxDegree = G.degree v
rw : G.degree v < Fintype.card V
⊢ G.maxDegree < Fintype.card V

Tactic:
rw [hv]
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.degree v < Fintype.card V

Tactic:
apply G.degree_lt_card_verts v

Premises used: SimpleGraph.degree_lt_card_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v w : V
rw : Fintype.card.{u_1} (↑(G.commonNeighbors v w) : Type u_1) ≤ Fintype.card.{u_1} (↑(G.neighborSet v) : Type u_1)
⊢ Fintype.card.{u_1} (↑(G.commonNeighbors v w) : Type u_1) ≤ G.degree v

Tactic:
rw [← card_neighborSet_eq_degree]

Premises used: SimpleGraph.card_neighborSet_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v w : V
⊢ Fintype.card.{u_1} (↑(G.commonNeighbors v w) : Type u_1) ≤ Fintype.card.{u_1} (↑(G.neighborSet v) : Type u_1)

Tactic:
Set.card_le_card Set.inter_subset_left

Premises used: Set.inter_subset_left, Set.card_le_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v w : V
⊢ Fintype.card.{u_1} (↑(G.commonNeighbors v w) : Type u_1) ≤ Fintype.card.{u_1} (↑(G.neighborSet v) : Type u_1)

Tactic:
exact Set.card_le_card Set.inter_subset_left

Premises used: Set.inter_subset_left, Set.card_le_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v w : V
simp_rw : Fintype.card.{u_1} (↑(G.commonNeighbors w v) : Type u_1) ≤ G.degree w
⊢ Fintype.card.{u_1} (↑(G.commonNeighbors v w) : Type u_1) ≤ G.degree w

Tactic:
simp_rw [commonNeighbors_symm _ v w, card_commonNeighbors_le_degree_left]

Premises used: SimpleGraph.card_commonNeighbors_le_degree_left, SimpleGraph.commonNeighbors_symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v w : V
⊢ Fintype.card.{u_1} (↑(G.commonNeighbors v w) : Type u_1) < Fintype.card V

Tactic:
Nat.lt_of_le_of_lt (G.card_commonNeighbors_le_degree_left _ _) (G.degree_lt_card_verts v)

Premises used: SimpleGraph.degree_lt_card_verts, SimpleGraph.card_commonNeighbors_le_degree_left, Nat.lt_of_le_of_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
v w : V
h : G.Adj v w
rw : #(G.commonNeighbors v w).toFinset < G.degree v
⊢ Fintype.card.{u_1} (↑(G.commonNeighbors v w) : Type u_1) < G.degree v

Tactic:
rw [← Set.toFinset_card]

Premises used: Set.toFinset_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ #(G.commonNeighbors v w).toFinset < G.degree v

Tactic:
Finset.card_lt_card <| Finset.ssubset_iff.mpr ⟨w, ?_, ?_⟩

Premises used: Iff.mpr, Finset.ssubset_iff, Finset.card_lt_card, And.intro, Exists.intro, SimpleGraph.degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
v w : V
h : G.Adj v w
refine_1 : w ∉ (G.commonNeighbors v w).toFinset
refine_2 : insert w (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v
⊢ #(G.commonNeighbors v w).toFinset < G.degree v

Tactic:
refine Finset.card_lt_card <| Finset.ssubset_iff.mpr ⟨w, ?_, ?_⟩

Premises used: Iff.mpr, Finset.ssubset_iff, Finset.card_lt_card, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
v w : V
h : G.Adj v w
refine_1 : w ∉ G.commonNeighbors v w
⊢ w ∉ (G.commonNeighbors v w).toFinset

Tactic:
rw [Set.mem_toFinset]

Premises used: Set.mem_toFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∉ G.commonNeighbors v w

Tactic:
apply notMem_commonNeighbors_right

Premises used: SimpleGraph.notMem_commonNeighbors_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ insert w (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v

Tactic:
simpa [Finset.insert_subset_iff, G.commonNeighbors_subset_neighborSet_left v w]

Premises used: Finset.insert_subset_iff, SimpleGraph.commonNeighbors_subset_neighborSet_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
v w : V
h : G.Adj v w
rw rw₁ rw₂ : #(G.commonNeighbors v w).toFinset < G.degree v
refine_1 : w ∉ (G.commonNeighbors v w).toFinset
refine_2 refine_2₁ : insert w (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v
⊢ Fintype.card.{u_1} (↑(G.commonNeighbors v w) : Type u_1) < G.degree v

Tactic:
classical
  rw [← Set.toFinset_card]
  refine Finset.card_lt_card <| Finset.ssubset_iff.mpr ⟨w, ?_, ?_⟩
  · rw [Set.mem_toFinset]
    apply notMem_commonNeighbors_right
  · simpa [Finset.insert_subset_iff, G.commonNeighbors_subset_neighborSet_left v w]

Premises used: Iff.mpr, Finset.insert_subset_iff, Set.toFinset_card, Finset.ssubset_iff, Finset.card_lt_card, And.intro, Exists.intro, Set.mem_toFinset, SimpleGraph.notMem_commonNeighbors_right, SimpleGraph.commonNeighbors_subset_neighborSet_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
v w : V
h : v ≠ w
⊢ Fintype.card.{u_1} (↑(commonNeighbors ⊤ v w) : Type u_1) = Fintype.card V - 2

Tactic:
simp [commonNeighbors_top_eq, ← Set.toFinset_card, Finset.card_sdiff, h]

Premises used: Finset.card_sdiff, Set.toFinset_card, SimpleGraph.commonNeighbors_top_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
f : G ≃g G'
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype (↑G'.edgeSet : Type u_2)
i : Equiv.{u_1 + 1, u_2 + 1} ↥G.edgeFinset ↥G'.edgeFinset
⊢ #G.edgeFinset = #G'.edgeFinset

Tactic:
apply Finset.card_eq_of_equiv

Premises used: Finset.card_eq_of_equiv
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
f : G ≃g G'
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype (↑G'.edgeSet : Type u_2)
⊢ Equiv.{u_1 + 1, u_2 + 1} ↥G.edgeFinset ↥G'.edgeFinset

Tactic:
simpa using f.mapEdgeSet

Premises used: SimpleGraph.Iso.mapEdgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
f : G ≃g G'
x : V
inst : Fintype (↑(G.neighborSet x) : Type u_1)
inst_1 : Fintype (↑(G'.neighborSet ((f : (a : V) → W) x)) : Type u_2)
rw : Fintype.card.{u_2} (↑(G'.neighborSet ((f : (a : V) → W) x)) : Type u_2) = G.degree x
rw₁ :
  Fintype.card.{u_2} (↑(G'.neighborSet ((f : (a : V) → W) x)) : Type u_2) =
    Fintype.card.{u_1} (↑(G.neighborSet x) : Type u_1)
rw₂ rw₃ :
  Fintype.card.{u_2} (↑(G'.neighborSet ((f : (a : V) → W) x)) : Type u_2) =
    Fintype.card.{u_2} (↑(G'.neighborSet ((f : (a : V) → W) x)) : Type u_2)
⊢ G'.degree ((f : (a : V) → W) x) = G.degree x

Tactic:
rw [← card_neighborSet_eq_degree, ← card_neighborSet_eq_degree,
    ← Fintype.card_congr (mapNeighborSet f x).symm]

Premises used: Fintype.card_congr, SimpleGraph.card_neighborSet_eq_degree, SimpleGraph.Iso.mapNeighborSet, Equiv.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Fintype W
inst_3 : DecidableRel G'.Adj
f : G ≃g G'
⊢ Eq.{u_1 + 1} (α := V → ℕ) ((fun (x : W) ↦ G'.degree x) ∘ (⇑f : (a : V) → W)) fun (x : V) ↦ G.degree x

Tactic:
have : (G'.degree ·) ∘ f = (G.degree ·) := funext (f.degree_eq ·)
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Fintype W
inst_3 : DecidableRel G'.Adj
f : G ≃g G'
this : Eq.{u_1 + 1} (α := V → ℕ) ((fun (x : W) ↦ G'.degree x) ∘ (⇑f : (a : V) → W)) fun (x : V) ↦ G.degree x
rw : WithTop.untopD 0 (Finset.min (image (fun (v : V) ↦ G.degree v) univ)) = G'.minDegree
rw₁ :
  Eq (α := ℕ) (WithTop.untopD 0 (Finset.min (image (fun (v : V) ↦ G.degree v) univ)))
    (WithTop.untopD 0 (Finset.min (image (fun (v : W) ↦ G'.degree v) univ)))
rw₂ :
  Eq (α := ℕ)
    (WithTop.untopD 0 (Finset.min (image.{u_1, 0} (α := V) ((fun (x : W) ↦ G'.degree x) ∘ (⇑f : (a : V) → W)) univ)))
    (WithTop.untopD 0 (Finset.min (image (fun (v : W) ↦ G'.degree v) univ)))
rw₃ :
  Eq (α := ℕ)
    (WithTop.untopD 0
      (Finset.min (image (fun (x : W) ↦ G'.degree x) (image.{u_1, u_2} (α := V) (⇑f : (a : V) → W) univ))))
    (WithTop.untopD 0 (Finset.min (image (fun (v : W) ↦ G'.degree v) univ)))
rw₄ rw₅ :
  Eq (α := ℕ) (WithTop.untopD 0 (Finset.min (image (fun (x : W) ↦ G'.degree x) univ)))
    (WithTop.untopD 0 (Finset.min (image (fun (v : W) ↦ G'.degree v) univ)))
⊢ G.minDegree = G'.minDegree

Tactic:
rw [minDegree, minDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]

Premises used: Finset.image_univ_of_surjective, SimpleGraph.minDegree, RelIso.surjective, Finset.image_image
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Fintype W
inst_3 : DecidableRel G'.Adj
f : G ≃g G'
have have₁ have₂ :
  ∀ (this : Eq.{u_1 + 1} (α := V → ℕ) ((fun (x : W) ↦ G'.degree x) ∘ (⇑f : (a : V) → W)) fun (x : V) ↦ G.degree x),
    G.minDegree = G'.minDegree
⊢ G.minDegree = G'.minDegree

Tactic:
classical
  have : (G'.degree ·) ∘ f = (G.degree ·) := funext (f.degree_eq ·)
  rw [minDegree, minDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]

Premises used: SimpleGraph.minDegree, Finset.image_image
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Fintype W
inst_3 : DecidableRel G'.Adj
f : G ≃g G'
this : Eq.{u_1 + 1} (α := V → ℕ) ((fun (x : W) ↦ G'.degree x) ∘ (⇑f : (a : V) → W)) fun (x : V) ↦ G.degree x
rw : WithBot.unbotD 0 (Finset.max (image (fun (v : V) ↦ G.degree v) univ)) = G'.maxDegree
rw₁ :
  Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max (image (fun (v : V) ↦ G.degree v) univ)))
    (WithBot.unbotD 0 (Finset.max (image (fun (v : W) ↦ G'.degree v) univ)))
rw₂ :
  Eq (α := ℕ)
    (WithBot.unbotD 0 (Finset.max (image.{u_1, 0} (α := V) ((fun (x : W) ↦ G'.degree x) ∘ (⇑f : (a : V) → W)) univ)))
    (WithBot.unbotD 0 (Finset.max (image (fun (v : W) ↦ G'.degree v) univ)))
rw₃ :
  Eq (α := ℕ)
    (WithBot.unbotD 0
      (Finset.max (image (fun (x : W) ↦ G'.degree x) (image.{u_1, u_2} (α := V) (⇑f : (a : V) → W) univ))))
    (WithBot.unbotD 0 (Finset.max (image (fun (v : W) ↦ G'.degree v) univ)))
rw₄ rw₅ :
  Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max (image (fun (x : W) ↦ G'.degree x) univ)))
    (WithBot.unbotD 0 (Finset.max (image (fun (v : W) ↦ G'.degree v) univ)))
⊢ G.maxDegree = G'.maxDegree

Tactic:
rw [maxDegree, maxDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]

Premises used: SimpleGraph.maxDegree, Finset.image_univ_of_surjective, RelIso.surjective, Finset.image_image
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Fintype W
inst_3 : DecidableRel G'.Adj
f : G ≃g G'
have have₁ have₂ :
  ∀ (this : Eq.{u_1 + 1} (α := V → ℕ) ((fun (x : W) ↦ G'.degree x) ∘ (⇑f : (a : V) → W)) fun (x : V) ↦ G.degree x),
    G.maxDegree = G'.maxDegree
⊢ G.maxDegree = G'.maxDegree

Tactic:
classical
  have : (G'.degree ·) ∘ f = (G.degree ·) := funext (f.degree_eq ·)
  rw [maxDegree, maxDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]

Premises used: SimpleGraph.maxDegree, Finset.image_image
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
s : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ s
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
h : G.support ⊆ s
rw : G.edgeSet ⊆ s.sym2
⊢ G.edgeFinset ⊆ s.toFinset.sym2

Tactic:
rw [← coe_subset, coe_sym2, edgeFinset, Set.coe_toFinset, Set.coe_toFinset]

Premises used: SimpleGraph.edgeFinset, Finset.coe_sym2, Set.coe_toFinset, Finset.coe_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
s : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ s
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
h : G.support ⊆ s
⊢ G.edgeSet ⊆ s.sym2

Tactic:
edgeSet_subset_sym2_iff.mpr h

Premises used: Iff.mpr, SimpleGraph.edgeSet_subset_sym2_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
s : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ s
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
h : G.support ⊆ s
⊢ G.edgeSet ⊆ s.sym2

Tactic:
exact edgeSet_subset_sym2_iff.mpr h

Premises used: Iff.mpr, SimpleGraph.edgeSet_subset_sym2_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
s : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ s
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
inst_3 : DecidableEq V
⊢ map (Embedding.sym2Map (Embedding.subtype fun (x : V) ↦ x ∈ s)) (induce s G).edgeFinset =
    G.edgeFinset ∩ s.toFinset.sym2

Tactic:
aesop (add simp [Finset.ext_iff, Sym2.exists, Sym2.forall, adj_comm])

Premises used: Sym2.exists, Finset.ext_iff, Sym2.forall, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
s : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ s
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
h : G.support ⊆ s
⊢ map (Embedding.sym2Map (Embedding.subtype fun (x : V) ↦ x ∈ s)) (induce s G).edgeFinset = G.edgeFinset

Tactic:
simpa [map_edgeFinset_induce] using edgeFinset_subset_sym2_of_support_subset h

Premises used: SimpleGraph.edgeFinset_subset_sym2_of_support_subset, SimpleGraph.map_edgeFinset_induce
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
s : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ s
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
h : G.support ⊆ s
⊢ map (Embedding.sym2Map (Embedding.subtype fun (x : V) ↦ x ∈ s)) (induce s G).edgeFinset = G.edgeFinset

Tactic:
classical
  simpa [map_edgeFinset_induce] using edgeFinset_subset_sym2_of_support_subset h

Premises used: SimpleGraph.edgeFinset_subset_sym2_of_support_subset, SimpleGraph.map_edgeFinset_induce
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
s : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ s
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
h : G.support ⊆ s
rw :
  #(induce s G).edgeFinset = #(map (Embedding.sym2Map (Embedding.subtype fun (x : V) ↦ x ∈ s)) (induce s G).edgeFinset)
rw₁ rw₂ : #(induce s G).edgeFinset = #(induce s G).edgeFinset
⊢ #(induce s G).edgeFinset = #G.edgeFinset

Tactic:
rw [← map_edgeFinset_induce_of_support_subset h, card_map]

Premises used: SimpleGraph.map_edgeFinset_induce_of_support_subset, Finset.card_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
⊢ #(induce G.support G).edgeFinset = #G.edgeFinset

Tactic:
card_edgeFinset_induce_of_support_subset subset_rfl

Premises used: SimpleGraph.card_edgeFinset_induce_of_support_subset, subset_rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
s : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ s
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
inst_3 : DecidableEq V
v : (↑s : Type u_1)
h :
  ∀ (a : V),
    a ∈ map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) ↔
      a ∈ G.neighborFinset (↑v : V) ∩ s.toFinset
⊢ map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V) ∩ s.toFinset

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
s : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ s
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
inst_3 : DecidableEq V
v : (↑s : Type u_1)
a : V
⊢ a ∈ map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) ↔
    a ∈ G.neighborFinset (↑v : V) ∩ s.toFinset

Tactic:
simp