awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
Adj : SimpleGraph.Adj (hasse (α × β)) x y ↔ (hasse α).Adj x.1 y.1 ∧ x.2 = y.2 ∨ (hasse β).Adj x.2 y.2 ∧ x.1 = y.1
Adj₁ : x ⋖ y ∨ y ⋖ x ↔ (x.1 ⋖ y.1 ∨ y.1 ⋖ x.1) ∧ x.2 = y.2 ∨ (x.2 ⋖ y.2 ∨ y.2 ⋖ x.2) ∧ x.1 = y.1
Adj₂ :
  (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1) ∨ y.1 ⋖ x.1 ∧ y.2 = x.2 ∨ y.2 ⋖ x.2 ∧ y.1 = x.1 ↔
    (x.1 ⋖ y.1 ∨ y.1 ⋖ x.1) ∧ x.2 = y.2 ∨ (x.2 ⋖ y.2 ∨ y.2 ⋖ x.2) ∧ x.1 = y.1
Adj₃ :
  (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1) ∨ y.1 ⋖ x.1 ∧ y.2 = x.2 ∨ y.2 ⋖ x.2 ∧ y.1 = x.1 ↔
    (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ y.1 ⋖ x.1 ∧ x.2 = y.2) ∨ x.2 ⋖ y.2 ∧ x.1 = y.1 ∨ y.2 ⋖ x.2 ∧ x.1 = y.1
Adj₄ :
  (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1) ∨ y.1 ⋖ x.1 ∧ y.2 = x.2 ∨ y.2 ⋖ x.2 ∧ x.1 = y.1 ↔
    (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ y.1 ⋖ x.1 ∧ x.2 = y.2) ∨ x.2 ⋖ y.2 ∧ x.1 = y.1 ∨ y.2 ⋖ x.2 ∧ x.1 = y.1
⊢ SimpleGraph.Adj (hasse (α × β)) x y ↔ (hasse α □ hasse β).Adj x y
have Adj₅ : (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1) ∨ y.1 ⋖ x.1 ∧ x.2 = y.2 ∨ y.2 ⋖ x.2 ∧ x.1 = y.1 ↔
  (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ y.1 ⋖ x.1 ∧ x.2 = y.2) ∨ x.2 ⋖ y.2 ∧ x.1 = y.1 ∨ y.2 ⋖ x.2 ∧ x.1 = y.1
Tactic: simp_rw [boxProd_adj, hasse_adj, Prod.covBy_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2,
    or_or_or_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
a b : α
⊢ (hasse α).Reachable a b
have rw : ReflTransGen (hasse α).Adj a b
Tactic: rw [reachable_iff_reflTransGen]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
a b : α
⊢ (hasse α).Reachable a b
have rw : ReflTransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) (hasse α).Adj) b a
Tactic: rw [reachable_iff_reflTransGen, ← reflTransGen_swap]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
⊢ Eq (α := SimpleGraph (Fin 2)) (pathGraph 2) ⊤
have Adj : ∀ (u v : Fin 2), Adj (pathGraph 2) u v ↔ Adj ⊤ u v
Tactic: ext u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
u v : Fin 2
⊢ Adj (pathGraph 2) u v ↔ Adj ⊤ u v
have Adj : Adj (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) v ↔ Adj ⊤ ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) v
Tactic: fin_cases u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
u v : Fin 2
Adj :
  SimpleGraph.Adj (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) v ↔ SimpleGraph.Adj ⊤ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) v
⊢ SimpleGraph.Adj (pathGraph 2) u v ↔ SimpleGraph.Adj ⊤ u v
have Adj₁ : SimpleGraph.Adj (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) v ↔ SimpleGraph.Adj ⊤ ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) v
Tactic: fin_cases u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
v : Fin 2
⊢ Adj (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) v ↔ Adj ⊤ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) v
have Adj : Adj (V := Fin 2) (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ↔
  Adj (V := Fin 2) ⊤ ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
v : Fin 2
Adj :
  SimpleGraph.Adj (V := Fin 2) (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ↔
    SimpleGraph.Adj (V := Fin 2) ⊤ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ SimpleGraph.Adj (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) v ↔ SimpleGraph.Adj ⊤ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) v
have Adj₁ : SimpleGraph.Adj (V := Fin 2) (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ↔
  SimpleGraph.Adj (V := Fin 2) ⊤ ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
v : Fin 2
⊢ Adj (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) v ↔ Adj ⊤ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) v
have Adj : Adj (V := Fin 2) (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ↔
  Adj (V := Fin 2) ⊤ ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
v : Fin 2
Adj :
  SimpleGraph.Adj (V := Fin 2) (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ↔
    SimpleGraph.Adj (V := Fin 2) ⊤ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ SimpleGraph.Adj (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) v ↔ SimpleGraph.Adj ⊤ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) v
have Adj₁ : SimpleGraph.Adj (V := Fin 2) (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ↔
  SimpleGraph.Adj (V := Fin 2) ⊤ ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
β : Type u_2
V : Type u_3
inst : DecidableEq V
G : SimpleGraph V
u v : V
w : G.Walk u v
hw : w.IsPath
⊢ ∀ {a b : Fin (w.length + 1)},
    w.toSubgraph.coe.Adj
        (({ toFun := (⇑w.pathGraphHomToSubgraph : (a : Fin (w.length + 1)) → (↑w.toSubgraph.verts : Type u_3)),
              invFun := fun (v_1 : (↑w.toSubgraph.verts : Type u_3)) ↦
                (⟨List.idxOf (↑v_1 : V) w.support, ⋯⟩ : Fin (w.length + 1)),
              left_inv := ⋯, right_inv := ⋯ : Fin (w.length + 1) ≃ (↑w.toSubgraph.verts : Type u_3) } :
            (a : Fin (w.length + 1)) → (↑w.toSubgraph.verts : Type u_3))
          a)
        (({ toFun := (⇑w.pathGraphHomToSubgraph : (a : Fin (w.length + 1)) → (↑w.toSubgraph.verts : Type u_3)),
              invFun := fun (v_1 : (↑w.toSubgraph.verts : Type u_3)) ↦
                (⟨List.idxOf (↑v_1 : V) w.support, ⋯⟩ : Fin (w.length + 1)),
              left_inv := ⋯, right_inv := ⋯ : Fin (w.length + 1) ≃ (↑w.toSubgraph.verts : Type u_3) } :
            (a : Fin (w.length + 1)) → (↑w.toSubgraph.verts : Type u_3))
          b) ↔
      Adj (pathGraph (w.length + 1)) a b
have refine : ∀ {a b : Fin (w.length + 1)}
  (hadj :
    w.toSubgraph.coe.Adj
      (({ toFun := (⇑w.pathGraphHomToSubgraph : (a : Fin (w.length + 1)) → (↑w.toSubgraph.verts : Type u_3)),
            invFun := fun (v_1 : (↑w.toSubgraph.verts : Type u_3)) ↦
              (⟨List.idxOf (↑v_1 : V) w.support, sorry⟩ : Fin (w.length + 1)),
            left_inv := sorry, right_inv := sorry : Fin (w.length + 1) ≃ (↑w.toSubgraph.verts : Type u_3) } :
          (a : Fin (w.length + 1)) → (↑w.toSubgraph.verts : Type u_3))
        a)
      (({ toFun := (⇑w.pathGraphHomToSubgraph : (a : Fin (w.length + 1)) → (↑w.toSubgraph.verts : Type u_3)),
            invFun := fun (v_1 : (↑w.toSubgraph.verts : Type u_3)) ↦
              (⟨List.idxOf (↑v_1 : V) w.support, sorry⟩ : Fin (w.length + 1)),
            left_inv := sorry, right_inv := sorry : Fin (w.length + 1) ≃ (↑w.toSubgraph.verts : Type u_3) } :
          (a : Fin (w.length + 1)) → (↑w.toSubgraph.verts : Type u_3))
        b)),
  Adj (pathGraph (w.length + 1)) a b
Tactic: refine ⟨fun hadj ↦ ?_, w.pathGraphHomToSubgraph.map_rel'⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : MulZeroOneClass R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬G.Adj a b
⊢ incMatrix R G a e * incMatrix R G b e = 0
have h₁ : e ∉ G.incidenceSet a ∩ G.incidenceSet b
Tactic: rw [incMatrix_apply_mul_incMatrix_apply, Set.indicator_of_notMem]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : MulZeroOneClass R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬G.Adj a b
⊢ e ∉ G.incidenceSet a ∩ G.incidenceSet b
have h₁ : e ∉ ∅
Tactic: rw [G.incidenceSet_inter_incidenceSet_of_not_adj h hab]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : MulZeroOneClass R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
a : α
e : Sym2 α
h : e ∉ G.incidenceSet a
⊢ incMatrix R G a e = 0
have rw : Eq.{u_1 + 1} (α := R) ((G.incidenceSet a).indicator 1 e) 0
Tactic: rw [incMatrix_apply, Set.indicator_of_notMem h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : MulZeroOneClass R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
a : α
e : Sym2 α
h : e ∉ G.incidenceSet a
rw : Eq.{u_1 + 1} (α := R) ((G.incidenceSet a).indicator 1 e) 0
⊢ incMatrix R G a e = 0
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [incMatrix_apply, Set.indicator_of_notMem h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : MulZeroOneClass R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
a : α
e : Sym2 α
h : e ∈ G.incidenceSet a
⊢ incMatrix R G a e = 1
have rw : Eq.{u_1 + 1} (α := R) ((G.incidenceSet a).indicator 1 e) 1
Tactic: rw [incMatrix_apply, Set.indicator_of_mem h, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : MulZeroOneClass R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
a : α
e : Sym2 α
h : e ∈ G.incidenceSet a
rw : Eq.{u_1 + 1} (α := R) ((G.incidenceSet a).indicator 1 e) 1
⊢ incMatrix R G a e = 1
have rw₁ : Eq.{u_1 + 1} (α := R) (1 e) 1
Tactic: rw [incMatrix_apply, Set.indicator_of_mem h, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : MulZeroOneClass R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
a : α
e : Sym2 α
h : e ∈ G.incidenceSet a
rw : Eq.{u_1 + 1} (α := R) ((G.incidenceSet a).indicator 1 e) 1
rw₁ : Eq.{u_1 + 1} (α := R) (1 e) 1
⊢ incMatrix R G a e = 1
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [incMatrix_apply, Set.indicator_of_mem h, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : MulZeroOneClass R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
a : α
e : Sym2 α
inst_3 : Nontrivial R
⊢ incMatrix R G a e = 1 ↔ e ∈ G.incidenceSet a
have convert_3 : NeZero.{u_1} (R := R) 1
Tactic: convert! one_ne_zero.ite_eq_left_iff
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
a : α
inst_3 : Fintype (Sym2 α)
inst_4 : Fintype (↑(G.neighborSet a) : Type u_2)
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = (↑(G.degree a) : R)
have rw : (incMatrix R G * (incMatrix R G)ᵀ) a a = ∑ e : Sym2 α, incMatrix R G a e
Tactic: rw [← sum_incMatrix_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
a : α
inst_3 : Fintype (Sym2 α)
inst_4 : Fintype (↑(G.neighborSet a) : Type u_2)
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ∑ e : Sym2 α, incMatrix R G a e
have simp : Eq.{u_1 + 1} (α := R) (∑ x : Sym2 α, if x ∈ G.incidenceSet a then if x ∈ G.incidenceSet a then 1 else 0 else 0)
  (∑ x : Sym2 α, if x ∈ G.incidenceSet a then 1 else 0)
Tactic: simp only [mul_apply, incMatrix_apply', transpose_apply, mul_ite, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
⊢ e ∈ G.edgeSet → Eq.{u_1 + 1} (α := R) (∑ a : α, incMatrix R G a e) 2
have refine : ∀ (x y : α), s(x, y) ∈ G.edgeSet → Eq.{u_1 + 1} (α := R) (∑ a : α, incMatrix R G a s(x, y)) 2
Tactic: refine e.ind ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (hypothesis)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
a b : α
h : s(a, b) ∈ G.edgeSet
⊢ Eq.{u_1 + 1} (α := R) (∑ a_1 : α, incMatrix R G a_1 s(a, b)) 2
have h₁ : G.Adj a b
Tactic: rw [mem_edgeSet] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
a b : α
h : G.Adj a b
⊢ Eq.{u_1 + 1} (α := R) (∑ a_1 : α, incMatrix R G a_1 s(a, b)) 2
have rw : Eq.{u_1 + 1} (α := R) (∑ a_1 : α, incMatrix R G a_1 s(a, b)) (↑(card (α := α) {a, b}) : R)
Tactic: rw [← Nat.cast_two, ← card_pair h.ne]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
a b : α
h : G.Adj a b
⊢ Eq.{u_1 + 1} (α := R) (∑ a_1 : α, incMatrix R G a_1 s(a, b)) (↑(card (α := α) {a, b}) : R)
have simp : Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | True ∧ (x = a ∨ x = b)}) : R) (↑(card (α := α) {a, b}) : R)
Tactic: simp only [incMatrix_apply', sum_boole, mk'_mem_incidenceSet_iff, h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
a b : α
h : G.Adj a b
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | True ∧ (x = a ∨ x = b)}) : R) (↑(card (α := α) {a, b}) : R)
have e_a : Eq (α := Finset α) {x : α | True ∧ (x = a ∨ x = b)} {a, b}
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
a b : α
h : G.Adj a b
⊢ Eq (α := Finset α) {x : α | True ∧ (x = a ∨ x = b)} {a, b}
have e_a : ∀ (e : α), Membership.mem (γ := Finset α) {x : α | True ∧ (x = a ∨ x = b)} e ↔ Membership.mem (γ := Finset α) {a, b} e
Tactic: ext e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
⊢ ((incMatrix R G)ᵀ * incMatrix R G) e e = if e ∈ G.edgeSet then 2 else 0
have simp : Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) (if e ∈ G.edgeSet then 2 else 0)
Tactic: simp only [Matrix.mul_apply, incMatrix_apply', transpose_apply, ite_zero_mul_ite_zero, one_mul,
    sum_boole, and_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) (if e ∈ G.edgeSet then 2 else 0)
have pos : ∀ (h : e ∈ G.edgeSet), Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 2
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
pos : ∀ (h : e ∈ G.edgeSet), Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 2
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) (if e ∈ G.edgeSet then 2 else 0)
have neg : ∀ (h : e ∉ G.edgeSet), Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
h : e ∈ G.edgeSet
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 2
have pos : ∀ (h : e ∈ G.edgeSet), Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 2
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
⊢ ∀ (h : e ∈ G.edgeSet), Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 2
have pos : ∀ (x y : α) (h : s(x, y) ∈ G.edgeSet),
  Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x_1 : α | s(x, y) ∈ G.incidenceSet x_1}) : R) 2
Tactic: refine e.ind ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | s(v, w) ∈ G.incidenceSet x}) : R) 2
have pos : Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | s(v, w) ∈ G.incidenceSet x}) : R)
  (↑(card (α := α) {(v, w).1, (v, w).2}) : R)
Tactic: rw [← Nat.cast_two, ← card_pair (G.ne_of_adj h)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | s(v, w) ∈ G.incidenceSet x}) : R)
    (↑(card (α := α) {(v, w).1, (v, w).2}) : R)
have pos : Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | x = v ∨ x = w}) : R) (↑(card (α := α) {v, w}) : R)
Tactic: simp only [mk'_mem_incidenceSet_iff, G.mem_edgeSet.mp h, true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | x = v ∨ x = w}) : R) (↑(card (α := α) {v, w}) : R)
have pos : Eq (α := Finset α) {x : α | x = v ∨ x = w} {v, w}
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ Eq (α := Finset α) {x : α | x = v ∨ x = w} {v, w}
have pos : ∀ (u : α), Membership.mem (γ := Finset α) {x : α | x = v ∨ x = w} u ↔ Membership.mem (γ := Finset α) {v, w} u
Tactic: ext u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
h : e ∉ G.edgeSet
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 0
have neg : ∀ (h : e ∉ G.edgeSet), Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 0
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
⊢ ∀ (h : e ∉ G.edgeSet), Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 0
have neg : ∀ (x y : α) (h : s(x, y) ∉ G.edgeSet),
  Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x_1 : α | s(x, y) ∈ G.incidenceSet x_1}) : R) 0
Tactic: refine e.ind ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : Fintype (Sym2 α)
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
inst_3 : Semiring R
a b : α
h : G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1
have simp_rw : Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := Sym2 α) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b}) : R) 1
Tactic: simp_rw [Matrix.mul_apply, Matrix.transpose_apply, incMatrix_apply_mul_incMatrix_apply,
    Set.indicator_apply, Pi.one_apply, sum_boole]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : Fintype (Sym2 α)
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
inst_3 : Semiring R
a b : α
h : G.Adj a b
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := Sym2 α) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b}) : R) 1
have h₁ : card.{u_2} (α := Sym2 α) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b} = 1
Tactic: convert! @Nat.cast_one R _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : Fintype (Sym2 α)
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
inst_3 : Semiring R
a b : α
h : G.Adj a b
⊢ card.{u_2} (α := Sym2 α) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b} = 1
have h₁ : Eq (α := Finset (Sym2 α)) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b} {s(a, b)}
Tactic: convert! card_singleton s(a, b)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : Fintype (Sym2 α)
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
inst_3 : Semiring R
a b : α
h : G.Adj a b
⊢ Eq (α := Finset (Sym2 α)) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b} {s(a, b)}
have h₁ : Eq (α := Set (Sym2 α)) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b} {s(a, b)}
Tactic: rw [← coe_eq_singleton, coe_filter_univ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : Fintype (Sym2 α)
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
inst_3 : Semiring R
inst_4 : (a : α) → Fintype (↑(G.neighborSet a) : Type u_2)
⊢ incMatrix R G * (incMatrix R G)ᵀ =
    (of : (a : α → α → R) → Matrix α α R) fun (a b : α) ↦
      if a = b then (↑(G.degree a) : R) else if G.Adj a b then 1 else 0
have a : ∀ (a b : α),
  (incMatrix R G * (incMatrix R G)ᵀ) a b =
    (of : (a : α → α → R) → Matrix α α R)
      (fun (a b : α) ↦ if a = b then (↑(G.degree a) : R) else if G.Adj a b then 1 else 0) a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : Fintype (Sym2 α)
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
inst_3 : Semiring R
inst_4 : (a : α) → Fintype (↑(G.neighborSet a) : Type u_2)
a b : α
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b =
    (of : (a : α → α → R) → Matrix α α R)
      (fun (a b : α) ↦ if a = b then (↑(G.degree a) : R) else if G.Adj a b then 1 else 0) a b
have a₁ : (incMatrix R G * (incMatrix R G)ᵀ) a b = if a = b then (↑(G.degree a) : R) else if G.Adj a b then 1 else 0
Tactic: dsimp