awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
a b : α
⊢ ReflTransGen (hasse α).Adj a b

Tactic:
reflTransGen_of_succ _ (fun c hc => Or.inl <| covBy_succ_of_not_isMax hc.2.not_isMax)
      fun c hc => Or.inr <| covBy_succ_of_not_isMax hc.2.not_isMax

Premises used: And.right, Or.inl, LT.lt.not_isMax, Order.covBy_succ_of_not_isMax, Or.inr, reflTransGen_of_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
a b : α
⊢ ReflTransGen (hasse α).Adj a b

Tactic:
exact
    reflTransGen_of_succ _ (fun c hc => Or.inl <| covBy_succ_of_not_isMax hc.2.not_isMax)
      fun c hc => Or.inr <| covBy_succ_of_not_isMax hc.2.not_isMax
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
a b : α
rw : ReflTransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) (hasse α).Adj) b a
⊢ (hasse α).Reachable a b

Tactic:
rw [reachable_iff_reflTransGen, ← reflTransGen_swap]

Premises used: Relation.reflTransGen_swap, SimpleGraph.reachable_iff_reflTransGen
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
a b : α
⊢ ReflTransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) (hasse α).Adj) b a

Tactic:
reflTransGen_of_pred _ (fun c hc => Or.inl <| pred_covBy_of_not_isMin hc.1.not_isMin)
      fun c hc => Or.inr <| pred_covBy_of_not_isMin hc.1.not_isMin

Premises used: Order.pred_covBy_of_not_isMin, reflTransGen_of_pred, LT.lt.not_isMin, And.left, Or.inl, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
a b : α
⊢ ReflTransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) (hasse α).Adj) b a

Tactic:
exact
    reflTransGen_of_pred _ (fun c hc => Or.inl <| pred_covBy_of_not_isMin hc.1.not_isMin)
      fun c hc => Or.inr <| pred_covBy_of_not_isMin hc.1.not_isMin
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
n : ℕ
u v : Fin n
⊢ (pathGraph n).Adj u v ↔ (↑u : ℕ) + 1 = (↑v : ℕ) ∨ (↑v : ℕ) + 1 = (↑u : ℕ)

Tactic:
simp [pathGraph, hasse]

Premises used: SimpleGraph.hasse, SimpleGraph.pathGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
n : ℕ
⊢ (pathGraph n).Preconnected

Tactic:
hasse_preconnected_of_succ _

Premises used: SimpleGraph.hasse_preconnected_of_succ, SimpleGraph.pathGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
n : ℕ
⊢ Connected (V := Fin (n + 1)) (pathGraph (n + 1))

Tactic:
⟨pathGraph_preconnected _⟩

Premises used: SimpleGraph.Connected.mk, SimpleGraph.pathGraph_preconnected
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
Adj : ∀ (u v : Fin 2), SimpleGraph.Adj (pathGraph 2) u v ↔ SimpleGraph.Adj ⊤ u v
⊢ Eq (α := SimpleGraph (Fin 2)) (pathGraph 2) ⊤

Tactic:
ext u v
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
Adj₁ :
  SimpleGraph.Adj (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) v ↔ SimpleGraph.Adj ⊤ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) v
⊢ SimpleGraph.Adj (pathGraph 2) u v ↔ SimpleGraph.Adj ⊤ u v

Tactic:
fin_cases u
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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, ⋯⟩)
Adj₁ :
  SimpleGraph.Adj (V := Fin 2) (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ↔
    SimpleGraph.Adj (V := Fin 2) ⊤ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ SimpleGraph.Adj (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) v ↔ SimpleGraph.Adj ⊤ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) v

Tactic:
fin_cases v
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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, ⋯⟩)
Adj₁ :
  SimpleGraph.Adj (V := Fin 2) (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ↔
    SimpleGraph.Adj (V := Fin 2) ⊤ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ SimpleGraph.Adj (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) v ↔ SimpleGraph.Adj ⊤ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) v

Tactic:
fin_cases v
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
⊢ Adj (V := Fin 2) (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ↔
    Adj (V := Fin 2) ⊤ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [pathGraph]

Premises used: SimpleGraph.pathGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
⊢ Adj (V := Fin 2) (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ↔
    Adj (V := Fin 2) ⊤ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [pathGraph]

Premises used: SimpleGraph.pathGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
⊢ Adj (V := Fin 2) (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ↔
    Adj (V := Fin 2) ⊤ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [pathGraph]

Premises used: SimpleGraph.pathGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
⊢ Adj (V := Fin 2) (pathGraph 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ↔
    Adj (V := Fin 2) ⊤ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [pathGraph]

Premises used: SimpleGraph.pathGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
a b : Fin (w.length + 1)
h : Adj (pathGraph (w.length + 1)) a b
⊢ w.toSubgraph.coe.Adj
    (Subtype.mk (p := fun (x : V) ↦ x ∈ w.toSubgraph.verts)
      (getElem (valid := fun (xs : List V) (i : Fin (w.length + 1)) ↦ (↑i : ℕ) < xs.length) w.support a ⋯) ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ w.toSubgraph.verts)
      (getElem (valid := fun (xs : List V) (i : Fin (w.length + 1)) ↦ (↑i : ℕ) < xs.length) w.support b ⋯) ⋯)

Tactic:
grind [support_getElem_eq_getVert, Subgraph.coe_adj, pathGraph_adj, toSubgraph_adj_getVert,
      Subgraph.Adj.symm]

Premises used: SimpleGraph.Subgraph.Adj.symm, SimpleGraph.pathGraph_adj, SimpleGraph.Subgraph.coe_adj, SimpleGraph.Walk.support_getElem_eq_getVert, SimpleGraph.Walk.toSubgraph_adj_getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
α : Type u_1
β : Type u_2
V : Type u_3
inst : DecidableEq V
G : SimpleGraph V
u v_1 : V
w : G.Walk u v_1
hw : w.IsPath
v : (↑w.toSubgraph.verts : Type u_3)
⊢ List.idxOf (↑v : V) w.support < w.length + 1

Tactic:
grind [w.mem_verts_toSubgraph]

Premises used: SimpleGraph.Walk.mem_verts_toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
⊢ Function.LeftInverse (α := Fin (w.length + 1))
    (fun (v_1 : (↑w.toSubgraph.verts : Type u_3)) ↦ ⟨List.idxOf (↑v_1 : V) w.support, ⋯⟩)
    (⇑w.pathGraphHomToSubgraph : (a : Fin (w.length + 1)) → (↑w.toSubgraph.verts : Type u_3))

Tactic:
grind [pathGraphHomToSubgraph, RelHom.coeFn_mk, hw.support_nodup]

Premises used: RelHom.coeFn_mk, SimpleGraph.Walk.pathGraphHomToSubgraph, SimpleGraph.Walk.IsPath.support_nodup
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
⊢ Function.RightInverse (α := Fin (w.length + 1))
    (fun (v_1 : (↑w.toSubgraph.verts : Type u_3)) ↦ ⟨List.idxOf (↑v_1 : V) w.support, ⋯⟩)
    (⇑w.pathGraphHomToSubgraph : (a : Fin (w.length + 1)) → (↑w.toSubgraph.verts : Type u_3))

Tactic:
grind [pathGraphHomToSubgraph, RelHom.coeFn_mk]

Premises used: RelHom.coeFn_mk, SimpleGraph.Walk.pathGraphHomToSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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

Tactic:
⟨fun hadj ↦ ?_, w.pathGraphHomToSubgraph.map_rel'⟩

Premises used: SimpleGraph.Walk.pathGraphHomToSubgraph, RelHom.map_rel', Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
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, ⋯⟩ : 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
⊢ ∀ {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

Tactic:
refine ⟨fun hadj ↦ ?_, w.pathGraphHomToSubgraph.map_rel'⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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)
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, ⋯⟩ : 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

Tactic:
grind [w.toSubgraph_adj_iff.mp hadj, pathGraph_adj, getVert_eq_getD_support,
      pathGraphHomToSubgraph, RelHom.coeFn_mk, hw.support_nodup.getElem_inj_iff]

Premises used: SimpleGraph.Walk.toSubgraph_adj_iff, SimpleGraph.pathGraph_adj, RelHom.coeFn_mk, List.Nodup.getElem_inj_iff, SimpleGraph.Walk.pathGraphHomToSubgraph, Iff.mp, SimpleGraph.Walk.IsPath.support_nodup, SimpleGraph.Walk.getVert_eq_getD_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
V : Type u_3
G : SimpleGraph V
u v : V
w : G.Walk u v
hw : w.IsPath
⊢ IsContained (α := Fin (w.length + 1)) (pathGraph (w.length + 1)) G

Tactic:
⟨hw.pathGraphCopy⟩

Premises used: SimpleGraph.Walk.IsPath.pathGraphCopy, Nonempty.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
V : Type u_3
G : SimpleGraph V
u v : V
w : G.Walk u v
hw : w.IsPath
⊢ IsContained (α := Fin (w.length + 1)) (pathGraph (w.length + 1)) G

Tactic:
exact ⟨hw.pathGraphCopy⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
V : Type u_3
G : SimpleGraph V
u v : V
w : G.Walk u v
hw : w.IsPath
⊢ IsContained (α := Fin (w.length + 1)) (pathGraph (w.length + 1)) G

Tactic:
classical
  exact ⟨hw.pathGraphCopy⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : Zero R
inst_1 : One R
inst_2 : DecidableEq α
inst_3 : DecidableRel G.Adj
a : α
e : Sym2 α
⊢ incMatrix R G a e = (G.incidenceSet a).indicator 1 e

Tactic:
simp [incMatrix, Set.indicator]

Premises used: Set.indicator, SimpleGraph.incMatrix
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : Zero R
inst_1 : One R
inst_2 : DecidableEq α
inst_3 : DecidableRel G.Adj
a : α
e : Sym2 α
⊢ incMatrix R G a e = if e ∈ G.incidenceSet a then 1 else 0

Tactic:
rfl

Premises used: SimpleGraph.incMatrix, rfl, ite
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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 α
⊢ incMatrix R G a e * incMatrix R G b e = (G.incidenceSet a ∩ G.incidenceSet b).indicator 1 e

Tactic:
simp [incMatrix_apply', Set.indicator_apply, ← ite_and, and_comm]

Premises used: Set.indicator_apply, SimpleGraph.incMatrix_apply', and_comm, ite_and
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
h₁ : e ∉ G.incidenceSet a ∩ G.incidenceSet b
⊢ incMatrix R G a e * incMatrix R G b e = 0

Tactic:
rw [incMatrix_apply_mul_incMatrix_apply, Set.indicator_of_notMem]

Premises used: SimpleGraph.incMatrix_apply_mul_incMatrix_apply, Set.indicator_of_notMem
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
h₁ : e ∉ ∅
⊢ e ∉ G.incidenceSet a ∩ G.incidenceSet b

Tactic:
rw [G.incidenceSet_inter_incidenceSet_of_not_adj h hab]

Premises used: SimpleGraph.incidenceSet_inter_incidenceSet_of_not_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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 ∉ ∅

Tactic:
Set.notMem_empty e

Premises used: Set.notMem_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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 ∉ ∅

Tactic:
exact Set.notMem_empty e

Premises used: Set.notMem_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ incMatrix R G a e = 0

Tactic:
rw [incMatrix_apply, Set.indicator_of_notMem h]

Premises used: Set.indicator_of_notMem, SimpleGraph.incMatrix_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ incMatrix R G a e = 1

Tactic:
rw [incMatrix_apply, Set.indicator_of_mem h, Pi.one_apply]

Premises used: Pi.one_apply, Set.indicator_of_mem, SimpleGraph.incMatrix_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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 = 0 ↔ e ∉ G.incidenceSet a

Tactic:
simp only [incMatrix_apply, Set.indicator_apply_eq_zero, Pi.one_apply, one_ne_zero]

Premises used: Pi.one_apply, one_ne_zero, Set.indicator_apply_eq_zero, SimpleGraph.incMatrix_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
⊢ Eq.{u_1 + 1} (α := R) (if e ∈ G.incidenceSet a then 1 else 0) 1 ↔ e ∈ G.incidenceSet a

Tactic:
one_ne_zero.ite_eq_left_iff

Premises used: Ne.ite_eq_left_iff, one_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
convert_3 : NeZero.{u_1} (R := R) 1
⊢ incMatrix R G a e = 1 ↔ e ∈ G.incidenceSet a

Tactic:
convert! one_ne_zero.ite_eq_left_iff

Premises used: Ne.ite_eq_left_iff, one_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
⊢ NeZero.{u_1} (R := R) 1

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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)
⊢ Eq.{u_1 + 1} (α := R) (∑ e : Sym2 α, incMatrix R G a e) (↑(G.degree a) : R)

Tactic:
simp [incMatrix_apply', sum_boole, Set.filter_mem_univ_eq_toFinset, card_incidenceSet_eq_degree]

Premises used: Set.filter_mem_univ_eq_toFinset, SimpleGraph.card_incidenceSet_eq_degree, SimpleGraph.incMatrix_apply', Finset.sum_boole
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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)
rw : (incMatrix R G * (incMatrix R G)ᵀ) a a = ∑ e : Sym2 α, incMatrix R G a e
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = (↑(G.degree a) : R)

Tactic:
rw [← sum_incMatrix_apply]

Premises used: SimpleGraph.sum_incMatrix_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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)
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)
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ∑ e : Sym2 α, incMatrix R G a e

Tactic:
simp only [mul_apply, incMatrix_apply', transpose_apply, mul_ite, mul_one, mul_zero]

Premises used: SimpleGraph.incMatrix_apply', mul_ite, Matrix.mul_apply, MulZeroClass.mul_zero, mul_one, Matrix.transpose_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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)
⊢ 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_all only [ite_true, sum_boole]

Premises used: ite_true, Finset.sum_boole
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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

Tactic:
e.ind ?_

Premises used: Sym2.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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 α
refine : ∀ (x y : α), s(x, y) ∈ G.edgeSet → Eq.{u_1 + 1} (α := R) (∑ a : α, incMatrix R G a s(x, y)) 2
⊢ e ∈ G.edgeSet → Eq.{u_1 + 1} (α := R) (∑ a : α, incMatrix R G a e) 2

Tactic:
refine e.ind ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
⊢ G.Adj a b

Tactic:
rw [mem_edgeSet] at h

Premises used: SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
rw : Eq.{u_1 + 1} (α := R) (∑ a_1 : α, incMatrix R G a_1 s(a, b)) (↑(card (α := α) {a, b}) : R)
⊢ Eq.{u_1 + 1} (α := R) (∑ a_1 : α, incMatrix R G a_1 s(a, b)) 2

Tactic:
rw [← Nat.cast_two, ← card_pair h.ne]

Premises used: SimpleGraph.Adj.ne, Finset.card_pair, Nat.cast_two
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
simp : Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | True ∧ (x = a ∨ x = b)}) : R) (↑(card (α := α) {a, b}) : R)
⊢ Eq.{u_1 + 1} (α := R) (∑ a_1 : α, incMatrix R G a_1 s(a, b)) (↑(card (α := α) {a, b}) : R)

Tactic:
simp only [incMatrix_apply', sum_boole, mk'_mem_incidenceSet_iff, h]

Premises used: SimpleGraph.incMatrix_apply', SimpleGraph.mk'_mem_incidenceSet_iff, Finset.sum_boole
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
e_a : Eq (α := Finset α) {x : α | True ∧ (x = a ∨ x = b)} {a, b}
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | True ∧ (x = a ∨ x = b)}) : R) (↑(card (α := α) {a, b}) : R)

Tactic:
congr 2