awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(Gᶜ.neighborFinset v ∩ G.neighborFinset w) = k - ℓ - 1
have convert_3 : #(G.neighborFinset w) - #(G.neighborFinset w ∩ G.neighborFinset v) - 1 = k - ℓ - 1
Tactic: rw [inter_comm, neighborFinset_compl, ← inter_sdiff_assoc, ← sdiff_eq_inter_compl,
      card_sdiff_of_subset s, card_singleton, ← sdiff_inter_self_left,
      card_sdiff_of_subset inter_subset_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset w) - #(G.neighborFinset w ∩ G.neighborFinset v) - 1 = k - ℓ - 1
have convert_3 : #(G.neighborFinset w) = k
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
convert_3 : #(G.neighborFinset w) = k
⊢ #(G.neighborFinset w) - #(G.neighborFinset w ∩ G.neighborFinset v) - 1 = k - ℓ - 1
have convert_3₁ : #(G.neighborFinset w ∩ G.neighborFinset v) = ℓ
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset w ∩ G.neighborFinset v) = ℓ
have convert_3 : #(G.neighborSet v ∩ G.neighborSet w).toFinset = #(G.commonNeighbors v w).toFinset
Tactic: simp_rw [inter_comm, neighborFinset_def, ← Set.toFinset_inter, ← h.of_adj v w hw,
        ← Set.toFinset_card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (hypothesis)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : w ∈ Gᶜ.neighborFinset v
⊢ #(bipartiteBelow G.Adj (G.neighborFinset v) w) = μ
have hw₁ : ¬G.Adj v w ∧ w ≠ v
Tactic: simp_rw [neighborFinset_compl, mem_sdiff, mem_compl, mem_singleton, mem_neighborFinset,
      ← Ne.eq_def] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : ¬G.Adj v w ∧ w ≠ v
⊢ #(bipartiteBelow G.Adj (G.neighborFinset v) w) = μ
have convert_4 : #(G.neighborSet v ∩ G.neighborSet w).toFinset = #(G.commonNeighbors v w).toFinset
Tactic: simp_rw [bipartiteBelow, adj_comm, ← mem_neighborFinset, filter_mem_eq_inter,
      neighborFinset_def, ← Set.toFinset_inter, ← h.of_not_adj hw.2.symm hw.1,
      ← Set.toFinset_card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
⊢ HPow.hPow (β := ℕ) (adjMatrix α G) 2 = HSMul.hSMul (β := Matrix V V α) k 1 + ℓ • adjMatrix α G + μ • adjMatrix α Gᶜ
have a : ∀ (v w : V),
  HPow.hPow (β := ℕ) (adjMatrix α G) 2 v w =
    (HSMul.hSMul (β := Matrix V V α) k 1 + ℓ • adjMatrix α G + μ • adjMatrix α Gᶜ) v w
Tactic: ext v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
⊢ HPow.hPow (β := ℕ) (adjMatrix α G) 2 v w =
    (HSMul.hSMul (β := Matrix V V α) k 1 + ℓ • adjMatrix α G + μ • adjMatrix α Gᶜ) v w
have a : (↑(Fintype.card.{u} (↑{p : G.Walk v w | p.length = 2} : Type u)) : α) =
  HSMul.hSMul (β := α) k (1 v w) + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
    HSMul.hSMul (β := α) μ (if v ≠ w ∧ ¬G.Adj v w then 1 else 0)
Tactic: simp only [adjMatrix_pow_apply_eq_card_walk, Matrix.add_apply, Matrix.smul_apply,
    adjMatrix_apply, compl_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
⊢ (↑(Fintype.card.{u} (↑{p : G.Walk v w | p.length = 2} : Type u)) : α) =
    HSMul.hSMul (β := α) k (1 v w) + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if v ≠ w ∧ ¬G.Adj v w then 1 else 0)
have a : (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
  HSMul.hSMul (β := α) k (1 v w) + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
    HSMul.hSMul (β := α) μ (if v ≠ w ∧ ¬G.Adj v w then 1 else 0)
Tactic: rw [@Fintype.card_congr _ _ (G.fintypeSetWalkLength v w 2) _
    (G.walkLengthTwoEquivCommonNeighbors v w)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v : V
⊢ (↑(Fintype.card.{u} (↑(G.commonNeighbors v v) : Type u)) : α) =
    HSMul.hSMul (β := α) k (1 v v) + HSMul.hSMul (β := α) ℓ (if G.Adj v v then 1 else 0) +
      HSMul.hSMul (β := α) μ (if v ≠ v ∧ ¬G.Adj v v then 1 else 0)
have a : (↑(#(G.commonNeighbors v v).toFinset) : α) =
  HSMul.hSMul (β := α) k (1 v v) + HSMul.hSMul (β := α) ℓ (if G.Adj v v then 1 else 0) +
    HSMul.hSMul (β := α) μ (if v ≠ v ∧ ¬G.Adj v v then 1 else 0)
Tactic: rw [← Set.toFinset_card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
⊢ (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
    HSMul.hSMul (β := α) k (1 v w) + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if v ≠ w ∧ ¬G.Adj v w then 1 else 0)
have a : (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
  HSMul.hSMul (β := α) k 0 + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
    HSMul.hSMul (β := α) μ (if ¬False ∧ ¬G.Adj v w then 1 else 0)
Tactic: simp only [Matrix.one_apply_ne' hn.symm, ne_eq, hn]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
⊢ (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
    HSMul.hSMul (β := α) k 0 + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if ¬False ∧ ¬G.Adj v w then 1 else 0)
have pos : ∀ (ha : G.Adj v w),
  (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
    HSMul.hSMul (β := α) k 0 + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if ¬False ∧ ¬G.Adj v w then 1 else 0)
Tactic: by_cases ha : G.Adj v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
pos :
  ∀ (ha : G.Adj v w),
    (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
      HSMul.hSMul (β := α) k 0 + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
        HSMul.hSMul (β := α) μ (if ¬False ∧ ¬G.Adj v w then 1 else 0)
⊢ (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
    HSMul.hSMul (β := α) k 0 + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if ¬False ∧ ¬G.Adj v w then 1 else 0)
have neg : ∀ (ha : ¬G.Adj v w),
  (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
    HSMul.hSMul (β := α) k 0 + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if ¬False ∧ ¬G.Adj v w then 1 else 0)
Tactic: by_cases ha : G.Adj v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : G.Adj v w
⊢ (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
    HSMul.hSMul (β := α) k 0 + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if ¬False ∧ ¬G.Adj v w then 1 else 0)
have pos : Eq.{u_1 + 1} (α := α) (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) (↑ℓ : α)
Tactic: simp only [ha, ite_true, ite_false, add_zero, zero_add, nsmul_eq_mul, smul_zero, mul_one,
        not_true_eq_false, not_false_eq_true, and_false, and_self]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : ¬G.Adj v w
⊢ (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
    HSMul.hSMul (β := α) k 0 + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if ¬False ∧ ¬G.Adj v w then 1 else 0)
have neg : Eq.{u_1 + 1} (α := α) (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) (↑μ : α)
Tactic: simp only [ha, ite_true, ite_false, add_zero, zero_add, nsmul_eq_mul, smul_zero, mul_one,
        not_true_eq_false, not_false_eq_true, and_false, and_self]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : G.Adj v w
⊢ Eq.{u_1 + 1} (α := α) (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) (↑ℓ : α)
have pos : Eq.{u_1 + 1} (α := α) (↑ℓ : α) (↑ℓ : α)
Tactic: rw [h.of_adj v w ha]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.StronglyRegular (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : ¬G.Adj v w
⊢ Eq.{u_1 + 1} (α := α) (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) (↑μ : α)
have neg : Eq.{u_1 + 1} (α := α) (↑μ : α) (↑μ : α)
Tactic: rw [h.of_not_adj hn ha]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : G.Adj v w
v_1 w_1 : V
h : s(v, w) = s(v_1, w_1)
⊢ G.Adj v_1 w_1
have rw : s(v, w) ∈ G.edgeSet
Tactic: rw [← G.mem_edgeSet, ← h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (hypothesis)
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a b : V
h : s(v, w) = s(a, b)
⊢ Membership.mem (γ := Set V) {v, w} a
have h₁ : (a ∈ s(v, w)) = (a ∈ s(a, b))
Tactic: apply_fun fun e ↦ a ∈ e at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (hypothesis)
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a b : V
h : (a ∈ s(v, w)) = (a ∈ s(a, b))
⊢ Membership.mem (γ := Set V) {v, w} a
have h₁ : a = v ∨ a = w
Tactic: simp only [Sym2.mem_iff, true_or, eq_iff_iff, iff_true] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
h2 : s(u, v) = s(w, x)
⊢ H.Adj u v ↔ H.Adj w x
have h2₁ : u = w ∧ v = x ∨ u = x ∧ v = w
Tactic: simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
h2 : u = w ∧ v = x ∨ u = x ∧ v = w
⊢ H.Adj u v ↔ H.Adj w x
have inl : ∀ (hl : u = w ∧ v = x), H.Adj u v ↔ H.Adj w x
Tactic: rcases h2 with hl | hr
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
h2 : u = w ∧ v = x ∨ u = x ∧ v = w
inl : ∀ (hl : u = w ∧ v = x), H.Adj u v ↔ H.Adj w x
⊢ H.Adj u v ↔ H.Adj w x
have inr : ∀ (hr : u = x ∧ v = w), H.Adj u v ↔ H.Adj w x
Tactic: rcases h2 with hl | hr
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hl : u = w ∧ v = x
⊢ H.Adj u v ↔ H.Adj w x
have inl : H.Adj w v ↔ H.Adj w x
Tactic: rw [hl.1, hl.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hl : u = w ∧ v = x
inl : H.Adj w v ↔ H.Adj w x
⊢ H.Adj u v ↔ H.Adj w x
have inl₁ : H.Adj w x ↔ H.Adj w x
Tactic: rw [hl.1, hl.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hr : u = x ∧ v = w
⊢ H.Adj u v ↔ H.Adj w x
have inr : H.Adj x v ↔ H.Adj w x
Tactic: rw [hr.1, hr.2, Subgraph.adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hr : u = x ∧ v = w
inr : H.Adj x v ↔ H.Adj w x
⊢ H.Adj u v ↔ H.Adj w x
have inr₁ : H.Adj x w ↔ H.Adj w x
Tactic: rw [hr.1, hr.2, Subgraph.adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hr : u = x ∧ v = w
inr : H.Adj x v ↔ H.Adj w x
inr₁ : H.Adj x w ↔ H.Adj w x
⊢ H.Adj u v ↔ H.Adj w x
have inr₂ : H.Adj w x ↔ H.Adj w x
Tactic: rw [hr.1, hr.2, Subgraph.adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.coe.spanningCoe (s := G'.verts) = G'.spanningCoe
have Adj : ∀ (x x_1 : V), G'.coe.spanningCoe (s := G'.verts).Adj x x_1 ↔ G'.spanningCoe.Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x x_1 : V
⊢ G'.coe.spanningCoe (s := G'.verts).Adj x x_1 ↔ G'.spanningCoe.Adj x x_1
have Adj : (∃ (a : V) (h : a ∈ G'.verts) (a_1 : V) (h_1 : a_1 ∈ G'.verts),
    G'.coe.Adj (Subtype.mk (p := fun (a : V) ↦ a ∈ G'.verts) a sorry) (Subtype.mk (p := fun (a : V) ↦ a ∈ G'.verts) a_1 sorry) ∧
      a = x ∧ a_1 = x_1) ↔
  G'.spanningCoe.Adj x x_1
Tactic: simp only [map_adj, Function.Embedding.subtype_apply, Subtype.exists]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hadj : G.Adj v w
⊢ (G.subgraphOfAdj hadj).spanningCoe = fromEdgeSet {s(v, w)}
have Adj : ∀ (v_1 w_1 : V), (G.subgraphOfAdj hadj).spanningCoe.Adj v_1 w_1 ↔ SimpleGraph.Adj (fromEdgeSet {s(v, w)}) v_1 w_1
Tactic: ext v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.coe.edgeSet = Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) ⁻¹' G'.edgeSet
have h : ∀ (e : Sym2 (↑G'.verts : Type u)),
  e ∈ G'.coe.edgeSet ↔
    Membership.mem (γ := Set (Sym2 (↑G'.verts : Type u)))
      (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) ⁻¹' G'.edgeSet) e
Tactic: ext e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 (↑G'.verts : Type u)
⊢ e ∈ G'.coe.edgeSet ↔
    Membership.mem (γ := Set (Sym2 (↑G'.verts : Type u)))
      (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) ⁻¹' G'.edgeSet) e
have h : ∀ (x y : (↑G'.verts : Type u)),
  s(x, y) ∈ G'.coe.edgeSet ↔
    Membership.mem (γ := Set (Sym2 (↑G'.verts : Type u)))
      (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) ⁻¹' G'.edgeSet) s(x, y)
Tactic: induction e using Sym2.ind
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) '' G'.coe.edgeSet = G'.edgeSet
have rw : G'.edgeSet ⊆ Set.range (ι := Sym2 (↑G'.verts : Type u)) (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)))
Tactic: rw [edgeSet_coe, Set.image_preimage_eq_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
a b : V
he : s(a, b) ∈ G'.edgeSet
⊢ Membership.mem (γ := Set (Sym2 V))
    (Set.range (ι := Sym2 (↑G'.verts : Type u)) (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)))) s(a, b)
have he₁ : G'.Adj a b
Tactic: rw [Subgraph.mem_edgeSet] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 V
he : e ∈ G'.edgeSet
⊢ Membership.mem (γ := Set (Sym2 V))
    (Set.range (ι := Sym2 (↑G'.verts : Type u)) (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)))) e
have h : ∀ (a b : V) (he : s(a, b) ∈ G'.edgeSet),
  Membership.mem (γ := Set (Sym2 V))
    (Set.range (ι := Sym2 (↑G'.verts : Type u)) (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)))) s(a, b)
Tactic: induction e using Sym2.ind with | h a b =>
  rw [Subgraph.mem_edgeSet] at he
  exact ⟨s(⟨a, edge_vert _ he⟩, ⟨b, edge_vert _ he.symm⟩), Sym2.map_mk ..⟩
Cleared hypotheses: e, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 V
v : V
he : e ∈ G'.edgeSet
hv : v ∈ e
⊢ v ∈ G'.verts
have h : ∀ (x y : V) (he : s(x, y) ∈ G'.edgeSet) (hv : v ∈ s(x, y)), v ∈ G'.verts
Tactic: induction e
Cleared hypotheses: e, he, hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v x y : V
he : s(x, y) ∈ G'.edgeSet
hv : v ∈ s(x, y)
⊢ v ∈ G'.verts
have h : ∀ (he : s(v, y) ∈ G'.edgeSet) (hv : v ∈ s(v, y)), v ∈ G'.verts
Tactic: rcases Sym2.mem_iff.mp hv with (rfl | rfl)
Cleared hypotheses: x, he, hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v x y : V
he : s(x, y) ∈ G'.edgeSet
hv : v ∈ s(x, y)
h : ∀ (he : s(v, y) ∈ G'.edgeSet) (hv : v ∈ s(v, y)), v ∈ G'.verts
⊢ v ∈ G'.verts
have h₁ : ∀ (he : s(x, v) ∈ G'.edgeSet) (hv : v ∈ s(x, v)), v ∈ G'.verts
Tactic: rcases Sym2.mem_iff.mp hv with (rfl | rfl)
Cleared hypotheses: y, he, hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
a b : V
s : Set G.Subgraph
hs : s.Nonempty
⊢ (∀ G' ∈ s, G'.Adj a b) → G.Adj a b
have obtain : ∀ (G' : G.Subgraph) (hG' : G' ∈ s), (∀ G' ∈ s, G'.Adj a b) → G.Adj a b
Tactic: obtain ⟨G', hG'⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
inst : Nonempty ι
f : ι → G.Subgraph
⊢ Adj (G := G) (⨅ (i : ι), f i) a b ↔ ∀ (i : ι), (f i).Adj a b
have rw : (∀ (G' : G.Subgraph), Membership.mem (γ := Set G.Subgraph) (Set.range fun (i : ι) ↦ f i) G' → G'.Adj a b) ↔
  ∀ (i : ι), (f i).Adj a b
Tactic: rw [iInf, sInf_adj_of_nonempty (Set.range_nonempty _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
h :
  Eq.{u + 1} (α := Set V × SimpleGraph V) ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₁)
    ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₂)
⊢ G₁ = G₂
have h₁ : Eq.{u + 1} (α := Set V) ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₁).1
    ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₂).1 ∧
  Eq.{u + 1} (α := SimpleGraph V) ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₁).2
    ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₂).2
Tactic: rw [Prod.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
ι_1 : Type u
κ : ι_1 → Type u
f : (a : ι_1) → κ a → G.Subgraph
⊢ Eq.{u + 1} (α := V → V → Prop) (Adj (G := G) (⨅ (a : ι_1), ⨆ (b : κ a), f a b))
    (Adj (G := G) (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a)))
have h : ∀ (x x_1 : V),
  Adj (G := G) (⨅ (a : ι_1), ⨆ (b : κ a), f a b) x x_1 ↔
    Adj (G := G) (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a)) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v : V
⊢ (sSup s).neighborSet v = ⋃ G' ∈ s, G'.neighborSet v
have h : ∀ (x : V), x ∈ (sSup s).neighborSet v ↔ Membership.mem (γ := Set V) (⋃ G' ∈ s, G'.neighborSet v) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v : V
⊢ (sInf s).neighborSet v = (⋂ G' ∈ s, G'.neighborSet v) ∩ G.neighborSet v
have h : ∀ (x : V), x ∈ (sInf s).neighborSet v ↔ x ∈ (⋂ G' ∈ s, G'.neighborSet v) ∩ G.neighborSet v
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
⊢ (sSup s).edgeSet = ⋃ G' ∈ s, G'.edgeSet
have h : ∀ (e : Sym2 V), e ∈ (sSup s).edgeSet ↔ Membership.mem (γ := Set (Sym2 V)) (⋃ G' ∈ s, G'.edgeSet) e
Tactic: ext e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
e : Sym2 V
⊢ e ∈ (sSup s).edgeSet ↔ Membership.mem (γ := Set (Sym2 V)) (⋃ G' ∈ s, G'.edgeSet) e
have h : ∀ (x y : V), s(x, y) ∈ (sSup s).edgeSet ↔ Membership.mem (γ := Set (Sym2 V)) (⋃ G' ∈ s, G'.edgeSet) s(x, y)
Tactic: induction e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
⊢ (sInf s).edgeSet = (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet
have h : ∀ (e : Sym2 V), e ∈ (sInf s).edgeSet ↔ e ∈ (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet
Tactic: ext e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
e : Sym2 V
⊢ e ∈ (sInf s).edgeSet ↔ e ∈ (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet
have h : ∀ (x y : V), s(x, y) ∈ (sInf s).edgeSet ↔ s(x, y) ∈ (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet
Tactic: induction e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
⊢ Disjoint H.verts H'.verts ↔ Disjoint H H'
have mp : Disjoint H.verts H'.verts → Disjoint H H'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
mp : Disjoint H.verts H'.verts → Disjoint H H'
⊢ Disjoint H.verts H'.verts ↔ Disjoint H H'
have mpr : Disjoint H H' → Disjoint H.verts H'.verts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right_1 : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
⊢ M' ≤ ⊥
have mp : M' = ⊥
Tactic: rw [le_bot_iff]