awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
⊢ G.maxDegree ≤ k
have inl : IsEmpty V → G.maxDegree ≤ k
Tactic: cases isEmpty_or_nonempty V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ G.maxDegree ≤ k
have inr : Nonempty V → G.maxDegree ≤ k
Tactic: cases isEmpty_or_nonempty V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ G.maxDegree ≤ k
have inr : ∀ (w : V) (hv : G.maxDegree = G.degree w), G.maxDegree ≤ k
Tactic: obtain ⟨_, hv⟩ := G.exists_maximal_degree_vertex
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
⊢ maxDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1
have inl : IsEmpty V → maxDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1
Tactic: cases isEmpty_or_nonempty V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
inl : IsEmpty V → maxDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1
⊢ maxDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1
have inr : Nonempty V → maxDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1
Tactic: cases isEmpty_or_nonempty V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ G.minDegree ≤ G.maxDegree
have pos : ∀ (he : IsEmpty V), G.minDegree ≤ G.maxDegree
Tactic: by_cases! he : IsEmpty V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
pos : ∀ (he : IsEmpty V), G.minDegree ≤ G.maxDegree
⊢ G.minDegree ≤ G.maxDegree
have neg : ∀ (he : Nonempty V), G.minDegree ≤ G.maxDegree
Tactic: by_cases! he : IsEmpty V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
⊢ minDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1
have inl : IsEmpty V → minDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1
Tactic: cases isEmpty_or_nonempty V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
inl : IsEmpty V → minDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1
⊢ minDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1
have inr : Nonempty V → minDegree.{u_1} (V := V) ⊤ = Fintype.card V - 1
Tactic: cases isEmpty_or_nonempty V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Nonempty V
⊢ G.maxDegree < Fintype.card V
have obtain : ∀ (v : V) (hv : G.maxDegree = G.degree v), G.maxDegree < Fintype.card V
Tactic: obtain ⟨v, hv⟩ := G.exists_maximal_degree_vertex
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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.maxDegree < Fintype.card V
have rw : G.degree v < Fintype.card V
Tactic: rw [hv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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) ≤ G.degree v
have rw : Fintype.card.{u_1} (↑(G.commonNeighbors v w) : Type u_1) ≤ Fintype.card.{u_1} (↑(G.neighborSet v) : Type u_1)
Tactic: rw [← card_neighborSet_eq_degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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) ≤ G.degree w
have simp_rw : Fintype.card.{u_1} (↑(G.commonNeighbors w v) : Type u_1) ≤ G.degree w
Tactic: simp_rw [commonNeighbors_symm _ v w, card_commonNeighbors_le_degree_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ Fintype.card.{u_1} (↑(G.commonNeighbors v w) : Type u_1) < G.degree v
have rw : #(G.commonNeighbors v w).toFinset < G.degree v
Tactic: rw [← Set.toFinset_card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
have refine_1 : w ∉ (G.commonNeighbors v w).toFinset
Tactic: refine Finset.card_lt_card <| Finset.ssubset_iff.mpr ⟨w, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ #(G.commonNeighbors v w).toFinset < G.degree v
have refine_2 : insert w (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v
Tactic: refine Finset.card_lt_card <| Finset.ssubset_iff.mpr ⟨w, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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).toFinset
have refine_1 : w ∉ G.commonNeighbors v w
Tactic: rw [Set.mem_toFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ Fintype.card.{u_1} (↑(G.commonNeighbors v w) : Type u_1) < G.degree v
have rw : #(G.commonNeighbors v w).toFinset < 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ Fintype.card.{u_1} (↑(G.commonNeighbors v w) : Type u_1) < G.degree v
have refine_1 : w ∉ (G.commonNeighbors v w).toFinset
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ Fintype.card.{u_1} (↑(G.commonNeighbors v w) : Type u_1) < G.degree v
have refine_2 : insert w (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)
⊢ #G.edgeFinset = #G'.edgeFinset
have i : Equiv.{u_1 + 1, u_2 + 1} ↥G.edgeFinset ↥G'.edgeFinset
Tactic: apply Finset.card_eq_of_equiv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)
⊢ G'.degree ((f : (a : V) → W) x) = G.degree x
have rw : Fintype.card.{u_2} (↑(G'.neighborSet ((f : (a : V) → W) x)) : Type u_2) = G.degree x
Tactic: rw [← card_neighborSet_eq_degree, ← card_neighborSet_eq_degree,
    ← Fintype.card_congr (mapNeighborSet f x).symm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ G'.degree ((f : (a : V) → W) x) = G.degree x
have 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)
Tactic: rw [← card_neighborSet_eq_degree, ← card_neighborSet_eq_degree,
    ← Fintype.card_congr (mapNeighborSet f x).symm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)
⊢ G'.degree ((f : (a : V) → W) x) = G.degree x
have 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)
Tactic: rw [← card_neighborSet_eq_degree, ← card_neighborSet_eq_degree,
    ← Fintype.card_congr (mapNeighborSet f x).symm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (hypothesis)
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'
⊢ G.minDegree = G'.minDegree
have this : 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 ·)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ G.minDegree = G'.minDegree
have rw : WithTop.untopD 0 (Finset.min (image (fun (v : V) ↦ G.degree v) univ)) = G'.minDegree
Tactic: rw [minDegree, minDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ G.minDegree = G'.minDegree
have 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)))
Tactic: rw [minDegree, minDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)))
⊢ G.minDegree = G'.minDegree
have 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)))
Tactic: rw [minDegree, minDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)))
⊢ G.minDegree = G'.minDegree
have 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)))
Tactic: rw [minDegree, minDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)))
⊢ G.minDegree = G'.minDegree
have 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)))
Tactic: rw [minDegree, minDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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'
⊢ G.minDegree = G'.minDegree
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
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (hypothesis)
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'
⊢ G.maxDegree = G'.maxDegree
have this : 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 ·)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ G.maxDegree = G'.maxDegree
have rw : WithBot.unbotD 0 (Finset.max (image (fun (v : V) ↦ G.degree v) univ)) = G'.maxDegree
Tactic: rw [maxDegree, maxDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ G.maxDegree = G'.maxDegree
have 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)))
Tactic: rw [maxDegree, maxDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)))
⊢ G.maxDegree = G'.maxDegree
have 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)))
Tactic: rw [maxDegree, maxDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)))
⊢ G.maxDegree = G'.maxDegree
have 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)))
Tactic: rw [maxDegree, maxDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)))
⊢ G.maxDegree = G'.maxDegree
have 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)))
Tactic: rw [maxDegree, maxDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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'
⊢ G.maxDegree = G'.maxDegree
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
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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.edgeFinset ⊆ s.toFinset.sym2
have rw : G.edgeSet ⊆ s.sym2
Tactic: rw [← coe_subset, coe_sym2, edgeFinset, Set.coe_toFinset, Set.coe_toFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ #(induce s G).edgeFinset = #G.edgeFinset
have rw : #(induce s G).edgeFinset = #(map (Embedding.sym2Map (Embedding.subtype fun (x : V) ↦ x ∈ s)) (induce s G).edgeFinset)
Tactic: rw [← map_edgeFinset_induce_of_support_subset h, card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)
⊢ #(induce s G).edgeFinset = #G.edgeFinset
have rw₁ : #(induce s G).edgeFinset = #(induce s G).edgeFinset
Tactic: rw [← map_edgeFinset_induce_of_support_subset h, card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)
⊢ map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V) ∩ s.toFinset
have h : ∀ (a : V),
  a ∈ map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) ↔
    a ∈ G.neighborFinset (↑v : V) ∩ s.toFinset
Tactic: ext