awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
u v : V
rw : (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
⊢ (adjMatrix α G ^ n) u v = (↑(Fintype.card.{u_2} (↑{p : G.Walk u v | p.length = n} : Type u_2)) : α)

Tactic:
rw [card_set_walk_length_eq]

Premises used: SimpleGraph.card_set_walk_length_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
u v : V
zero : HPow.hPow (β := ℕ) (adjMatrix α G) 0 u u = (↑(#(G.finsetWalkLength 0 u u)) : α)
zero₁ : ∀ (h : u ≠ v), HPow.hPow (β := ℕ) (adjMatrix α G) 0 u v = (↑(#(G.finsetWalkLength 0 u v)) : α)
⊢ HPow.hPow (β := ℕ) (adjMatrix α G) 0 u v = (↑(#(G.finsetWalkLength 0 u v)) : α)

Tactic:
obtain rfl | h := eq_or_ne u v

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
u : V
⊢ HPow.hPow (β := ℕ) (adjMatrix α G) 0 u u = (↑(#(G.finsetWalkLength 0 u u)) : α)

Tactic:
simp [finsetWalkLength, *]

Premises used: SimpleGraph.finsetWalkLength
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
u v : V
h : u ≠ v
⊢ HPow.hPow (β := ℕ) (adjMatrix α G) 0 u v = (↑(#(G.finsetWalkLength 0 u v)) : α)

Tactic:
simp [finsetWalkLength, *]

Premises used: SimpleGraph.finsetWalkLength
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v : V
succ :
  Eq.{u_1 + 1} (α := α) (∑ x ∈ G.neighborFinset u, (↑(#(G.finsetWalkLength n x v)) : α))
    (↑(card.{u_2} (α := G.Walk u v)
          (Finset.biUnion univ fun (w : (↑(G.neighborSet u) : Type u_2)) ↦
            Finset.map (α := G.Walk (↑w : V) v) { toFun := fun (p : G.Walk (↑w : V) v) ↦ Walk.cons ⋯ p, inj' := ⋯ }
              (G.finsetWalkLength n (↑w : V) v))) :
      α)
⊢ (adjMatrix α G ^ (n + 1)) u v = (↑(#(G.finsetWalkLength (n + 1) u v)) : α)

Tactic:
simp only [pow_succ', finsetWalkLength, ih, adjMatrix_mul_apply]

Premises used: SimpleGraph.finsetWalkLength, SimpleGraph.adjMatrix_mul_apply, pow_succ'
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v : V
succ :
  Eq.{u_1 + 1} (α := α) (∑ x ∈ G.neighborFinset u, (↑(#(G.finsetWalkLength n x v)) : α))
    (↑(∑ u_1 : (↑(G.neighborSet u) : Type u_2),
          card (α := G.Walk u v)
            (Finset.map (α := G.Walk (↑u_1 : V) v) { toFun := fun (p : G.Walk (↑u_1 : V) v) ↦ Walk.cons ⋯ p, inj' := ⋯ }
              (G.finsetWalkLength n (↑u_1 : V) v))) :
      α)
succ₁ :
  (↑univ : Set (↑(G.neighborSet u) : Type u_2)).PairwiseDisjoint (α := Finset (G.Walk u v))
    fun (w : (↑(G.neighborSet u) : Type u_2)) ↦
    Finset.map (α := G.Walk (↑w : V) v) { toFun := fun (p : G.Walk (↑w : V) v) ↦ Walk.cons ⋯ p, inj' := ⋯ }
      (G.finsetWalkLength n (↑w : V) v)
⊢ Eq.{u_1 + 1} (α := α) (∑ x ∈ G.neighborFinset u, (↑(#(G.finsetWalkLength n x v)) : α))
    (↑(card.{u_2} (α := G.Walk u v)
          (Finset.biUnion univ fun (w : (↑(G.neighborSet u) : Type u_2)) ↦
            Finset.map (α := G.Walk (↑w : V) v) { toFun := fun (p : G.Walk (↑w : V) v) ↦ Walk.cons ⋯ p, inj' := ⋯ }
              (G.finsetWalkLength n (↑w : V) v))) :
      α)

Tactic:
rw [Finset.card_biUnion]

Premises used: Finset.card_biUnion
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v : V
succ :
  Eq.{u_1 + 1} (α := α) (↑(∑ x ∈ G.neighborFinset u, #(G.finsetWalkLength n x v)) : α)
    (↑(∑ u_1 : (↑(G.neighborSet u) : Type u_2),
          card (α := G.Walk u v)
            (Finset.map (α := G.Walk (↑u_1 : V) v) { toFun := fun (p : G.Walk (↑u_1 : V) v) ↦ Walk.cons ⋯ p, inj' := ⋯ }
              (G.finsetWalkLength n (↑u_1 : V) v))) :
      α)
⊢ Eq.{u_1 + 1} (α := α) (∑ x ∈ G.neighborFinset u, (↑(#(G.finsetWalkLength n x v)) : α))
    (↑(∑ u_1 : (↑(G.neighborSet u) : Type u_2),
          card (α := G.Walk u v)
            (Finset.map (α := G.Walk (↑u_1 : V) v) { toFun := fun (p : G.Walk (↑u_1 : V) v) ↦ Walk.cons ⋯ p, inj' := ⋯ }
              (G.finsetWalkLength n (↑u_1 : V) v))) :
      α)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v : V
succ :
  Eq.{u_1 + 1} (α := α) (∑ x ∈ (G.neighborSet u).toFinset, (↑(#(G.finsetWalkLength n x v)) : α))
    (∑ x : (↑(G.neighborSet u) : Type u_2), (↑(card (α := G.Walk (↑x : V) v) (G.finsetWalkLength n (↑x : V) v)) : α))
⊢ Eq.{u_1 + 1} (α := α) (↑(∑ x ∈ G.neighborFinset u, #(G.finsetWalkLength n x v)) : α)
    (↑(∑ u_1 : (↑(G.neighborSet u) : Type u_2),
          card (α := G.Walk u v)
            (Finset.map (α := G.Walk (↑u_1 : V) v) { toFun := fun (p : G.Walk (↑u_1 : V) v) ↦ Walk.cons ⋯ p, inj' := ⋯ }
              (G.finsetWalkLength n (↑u_1 : V) v))) :
      α)

Tactic:
simp only [Nat.cast_sum, card_map, neighborFinset_def]

Premises used: Finset.card_map, Nat.cast_sum, SimpleGraph.neighborFinset_def
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v : V
⊢ Eq.{u_1 + 1} (α := α) (∑ x ∈ (G.neighborSet u).toFinset, (↑(#(G.finsetWalkLength n x v)) : α))
    (∑ x : (↑(G.neighborSet u) : Type u_2), (↑(card (α := G.Walk (↑x : V) v) (G.finsetWalkLength n (↑x : V) v)) : α))

Tactic:
apply Finset.sum_toFinset_eq_subtype

Premises used: Finset.sum_toFinset_eq_subtype
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v x : V
hx : x ∈ G.neighborSet u
y : V
hy : y ∈ G.neighborSet u
hxy :
  Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy
succ :
  LE.le (α := Finset (G.Walk u v))
    (Finset.map (α := G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx) : V) v)
        { toFun := fun (p : G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx) : V) v) ↦ Walk.cons ⋯ p,
          inj' := ⋯ }
        (G.finsetWalkLength n (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx) : V) v) ⊓
      Finset.map (α := G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy) : V) v)
        { toFun := fun (p : G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy) : V) v) ↦ Walk.cons ⋯ p,
          inj' := ⋯ }
        (G.finsetWalkLength n (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy) : V) v))
    ⊥
⊢ Function.onFun (β := Finset (G.Walk u v)) Disjoint
    (fun (w : (↑(G.neighborSet u) : Type u_2)) ↦
      Finset.map (α := G.Walk (↑w : V) v) { toFun := fun (p : G.Walk (↑w : V) v) ↦ Walk.cons ⋯ p, inj' := ⋯ }
        (G.finsetWalkLength n (↑w : V) v))
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy)

Tactic:
rw [Function.onFun, disjoint_iff_inf_le]

Premises used: Function.onFun, disjoint_iff_inf_le
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v x : V
hx : x ∈ G.neighborSet u
y : V
hy : y ∈ G.neighborSet u
hxy :
  Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy
p : G.Walk u v
hp :
  Membership.mem (γ := Finset (G.Walk u v))
    (Finset.map (α := G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx) : V) v)
        { toFun := fun (p : G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx) : V) v) ↦ Walk.cons ⋯ p,
          inj' := ⋯ }
        (G.finsetWalkLength n (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx) : V) v) ⊓
      Finset.map (α := G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy) : V) v)
        { toFun := fun (p : G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy) : V) v) ↦ Walk.cons ⋯ p,
          inj' := ⋯ }
        (G.finsetWalkLength n (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy) : V) v))
    p
⊢ (∃ a ∈ G.finsetWalkLength n x v, Walk.cons ⋯ a = p) ∧ ∃ a ∈ G.finsetWalkLength n y v, Walk.cons ⋯ a = p

Tactic:
simp only [inf_eq_inter, mem_inter, mem_map, Function.Embedding.coeFn_mk] at hp

Premises used: Finset.inf_eq_inter, Function.Embedding.coeFn_mk, Finset.mem_map, Finset.mem_inter
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v x : V
hx : x ∈ G.neighborSet u
y : V
hy : y ∈ G.neighborSet u
hxy :
  Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy
p : G.Walk u v
hp : (∃ a ∈ G.finsetWalkLength n x v, Walk.cons ⋯ a = p) ∧ ∃ a ∈ G.finsetWalkLength n y v, Walk.cons ⋯ a = p
succ :
  ∀ px ∈ G.finsetWalkLength n x v,
    ∀ (py : G.Walk y v) (hpy : py ∈ G.finsetWalkLength n y v)
      (hp : Eq (α := G.Walk u v) (Walk.cons ⋯ py) (Walk.cons ⋯ px)),
      Membership.mem (γ := Finset (G.Walk u v)) ⊥ (Walk.cons ⋯ px)
⊢ Membership.mem (γ := Finset (G.Walk u v)) ⊥ p

Tactic:
obtain ⟨⟨px, _, rfl⟩, ⟨py, hpy, hp⟩⟩ := hp

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v x : V
hx : x ∈ G.neighborSet u
y : V
hy : y ∈ G.neighborSet u
hxy :
  Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy
px : G.Walk x v
left : px ∈ G.finsetWalkLength n x v
py : G.Walk y v
hpy : py ∈ G.finsetWalkLength n y v
hp : Eq (α := G.Walk u v) (Walk.cons ⋯ py) (Walk.cons ⋯ px)
⊢ x ∈ G.neighborSet u

Tactic:
cases hp
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v x : V
hx : x ∈ G.neighborSet u
y : V
hy : y ∈ G.neighborSet u
hxy :
  Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy
px : G.Walk x v
left : px ∈ G.finsetWalkLength n x v
py : G.Walk y v
hpy : py ∈ G.finsetWalkLength n y v
hp : Eq (α := G.Walk u v) (Walk.cons ⋯ py) (Walk.cons ⋯ px)
hy₁ : x ∈ G.neighborSet u
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hy₁

Tactic:
cases hp
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v x : V
hx : x ∈ G.neighborSet u
y : V
hy : y ∈ G.neighborSet u
hxy :
  Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy
px : G.Walk x v
left : px ∈ G.finsetWalkLength n x v
py : G.Walk y v
hpy : py ∈ G.finsetWalkLength n y v
hp : Eq (α := G.Walk u v) (Walk.cons ⋯ py) (Walk.cons ⋯ px)
hy₁ : x ∈ G.neighborSet u
hxy₁ :
  Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hy₁
⊢ px ∈ G.finsetWalkLength n x v

Tactic:
cases hp
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v x : V
hx : x ∈ G.neighborSet u
px : G.Walk x v
left : px ∈ G.finsetWalkLength n x v
hy : x ∈ G.neighborSet u
hxy :
  Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hy
hpy : px ∈ G.finsetWalkLength n x v
⊢ Membership.mem (γ := Finset (G.Walk u v)) ⊥ (Walk.cons ⋯ px)

Tactic:
simp at hxy
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
u v : V
zero : ∀ (u v : V), HPow.hPow (β := ℕ) (adjMatrix α G) 0 u v = (↑(#(G.finsetWalkLength 0 u v)) : α)
succ :
  ∀ (n : ℕ) (ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)) (u v : V),
    (adjMatrix α G ^ (n + 1)) u v = (↑(#(G.finsetWalkLength (n + 1) u v)) : α)
⊢ (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)

Tactic:
induction n generalizing u v with
  | zero => obtain rfl | h := eq_or_ne u v <;> simp [finsetWalkLength, *]
  | succ n ih =>
    simp only [pow_succ', finsetWalkLength, ih, adjMatrix_mul_apply]
    rw [Finset.card_biUnion]
    · norm_cast
      simp only [Nat.cast_sum, card_map, neighborFinset_def]
      apply Finset.sum_toFinset_eq_subtype
    -- Disjointness for card_bUnion
    · rintro ⟨x, hx⟩ - ⟨y, hy⟩ - hxy
      rw [Function.onFun, disjoint_iff_inf_le]
      intro p hp
      simp only [inf_eq_inter, mem_inter, mem_map, Function.Embedding.coeFn_mk] at hp
      obtain ⟨⟨px, _, rfl⟩, ⟨py, hpy, hp⟩⟩ := hp
      cases hp
      simp at hxy

Premises used: SimpleGraph.finsetWalkLength, Function.onFun, Finset.card_map, Finset.inf_eq_inter, Finset.card_biUnion, Nat.cast_sum, SimpleGraph.adjMatrix_mul_apply, Finset.sum_toFinset_eq_subtype, Function.Embedding.coeFn_mk, eq_or_ne, Finset.mem_map, disjoint_iff_inf_le, Finset.mem_inter, Matrix.zero, SimpleGraph.neighborFinset_def, pow_succ', rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
x y : V → α
⊢ x ⬝ᵥ adjMatrix α G *ᵥ y = ∑ i : V, ∑ j : V, if G.Adj i j then x i * y j else 0

Tactic:
simp [dotProduct, mulVec, mul_sum]

Premises used: Finset.mul_sum, dotProduct, Matrix.mulVec
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : MulZeroOneClass α
d : V → α
⊢ adjMatrix α G ⊙ diagonal d = 0

Tactic:
simp [hadamard_diagonal]

Premises used: Matrix.hadamard_diagonal
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : MulZeroOneClass α
d : V → α
⊢ diagonal d ⊙ adjMatrix α G = 0

Tactic:
simp [diagonal_hadamard]

Premises used: Matrix.diagonal_hadamard
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : MulZeroOneClass α
inst_3 : NatCast α
a : ℕ
⊢ adjMatrix α G ⊙ (↑a : Matrix V V α) = 0

Tactic:
adjMatrix_hadamard_diagonal _ _ _

Premises used: SimpleGraph.adjMatrix_hadamard_diagonal
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : MulZeroOneClass α
inst_3 : NatCast α
a : ℕ
⊢ (↑a : Matrix V V α) ⊙ adjMatrix α G = 0

Tactic:
diagonal_hadamard_adjMatrix _ _ _

Premises used: SimpleGraph.diagonal_hadamard_adjMatrix
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : MulZeroOneClass α
inst_3 : NatCast α
a : ℕ
inst_4 : a.AtLeastTwo
⊢ adjMatrix α G ⊙ OfNat.ofNat a = 0

Tactic:
adjMatrix_hadamard_diagonal _ _ _

Premises used: SimpleGraph.adjMatrix_hadamard_diagonal, Matrix.diagonal
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : MulZeroOneClass α
inst_3 : NatCast α
a : ℕ
inst_4 : a.AtLeastTwo
⊢ OfNat.ofNat a ⊙ adjMatrix α G = 0

Tactic:
diagonal_hadamard_adjMatrix _ _ _

Premises used: SimpleGraph.diagonal_hadamard_adjMatrix, Matrix.diagonal
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : MulZeroOneClass α
inst_3 : IntCast α
a : ℤ
⊢ adjMatrix α G ⊙ (↑a : Matrix V V α) = 0

Tactic:
adjMatrix_hadamard_diagonal _ _ _

Premises used: SimpleGraph.adjMatrix_hadamard_diagonal
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : MulZeroOneClass α
inst_3 : IntCast α
a : ℤ
⊢ (↑a : Matrix V V α) ⊙ adjMatrix α G = 0

Tactic:
diagonal_hadamard_adjMatrix _ _ _

Premises used: SimpleGraph.diagonal_hadamard_adjMatrix
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : MulZeroOneClass α
⊢ adjMatrix α G ⊙ 1 = 0

Tactic:
adjMatrix_hadamard_diagonal _ _ _

Premises used: SimpleGraph.adjMatrix_hadamard_diagonal
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : MulZeroOneClass α
⊢ 1 ⊙ adjMatrix α G = 0

Tactic:
diagonal_hadamard_adjMatrix _ _ _

Premises used: SimpleGraph.diagonal_hadamard_adjMatrix
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : MulZeroOneClass α
inst_1 : Nontrivial α
A : Matrix V V α
h : A.IsAdjMatrix
inst_2 : DecidableEq α
a : ∀ (i j : V), adjMatrix α h.toGraph i j = A i j
⊢ adjMatrix α h.toGraph = A

Tactic:
ext i j
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : MulZeroOneClass α
inst_1 : Nontrivial α
A : Matrix V V α
h : A.IsAdjMatrix
inst_2 : DecidableEq α
i j : V
a : ∀ (h' : A i j = 0), adjMatrix α h.toGraph i j = A i j
a₁ : ∀ (h' : A i j = 1), adjMatrix α h.toGraph i j = A i j
⊢ adjMatrix α h.toGraph i j = A i j

Tactic:
obtain h' | h' := h.zero_or_one i j

Premises used: Matrix.IsAdjMatrix.zero_or_one
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : MulZeroOneClass α
inst_1 : Nontrivial α
A : Matrix V V α
h : A.IsAdjMatrix
inst_2 : DecidableEq α
i j : V
h' : A i j = 0
⊢ adjMatrix α h.toGraph i j = A i j

Tactic:
simp [h']
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : MulZeroOneClass α
inst_1 : Nontrivial α
A : Matrix V V α
h : A.IsAdjMatrix
inst_2 : DecidableEq α
i j : V
h' : A i j = 1
⊢ adjMatrix α h.toGraph i j = A i j

Tactic:
simp [h']
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
x : { adj : V → V → Bool // (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true }
v w : V
⊢ (fun (v w : V) ↦ (↑x : V → V → Bool) v w = true) v w → (fun (v w : V) ↦ (↑x : V → V → Bool) v w = true) w v

Tactic:
simp [x.2.1]

Premises used: And.left, Subtype.property
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
x : { adj : V → V → Bool // (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true }
v : V
⊢ ¬(↑x : V → V → Bool) v v = true

Tactic:
simp [x.2.2]

Premises used: And.right, Subtype.property
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
adj : V → V → Bool
property : (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true
adj' : V → V → Bool
property_1 : (∀ (x y : V), adj' x y = adj' y x) ∧ ∀ (x : V), ¬adj' x x = true
simp : (Eq.{u + 1} (α := V → V → Prop) (fun (v w : V) ↦ adj v w = true) fun (v w : V) ↦ adj' v w = true) → adj = adj'
⊢ Eq.{u + 1} (α := SimpleGraph V)
      ((fun (x : { adj : V → V → Bool // (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true }) ↦
          ({ Adj := fun (v w : V) ↦ (↑x : V → V → Bool) v w = true, symm := ⋯, loopless := ⋯ } : SimpleGraph V))
        (Subtype.mk (p := fun (adj : V → V → Bool) ↦ (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true) adj
          property))
      ((fun (x : { adj : V → V → Bool // (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true }) ↦
          ({ Adj := fun (v w : V) ↦ (↑x : V → V → Bool) v w = true, symm := ⋯, loopless := ⋯ } : SimpleGraph V))
        (Subtype.mk (p := fun (adj : V → V → Bool) ↦ (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true) adj'
          property_1)) →
    Eq (α := { adj : V → V → Bool // (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true })
      (Subtype.mk (p := fun (adj : V → V → Bool) ↦ (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true) adj
        property)
      (Subtype.mk (p := fun (adj : V → V → Bool) ↦ (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true) adj'
        property_1)

Tactic:
simp only [mk.injEq, Subtype.mk.injEq]

Premises used: Subtype.mk.injEq, SimpleGraph.mk.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
adj : V → V → Bool
property : (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true
adj' : V → V → Bool
property_1 : (∀ (x y : V), adj' x y = adj' y x) ∧ ∀ (x : V), ¬adj' x x = true
h : Eq.{u + 1} (α := V → V → Prop) (fun (v w : V) ↦ adj v w = true) fun (v w : V) ↦ adj' v w = true
h₁ : ∀ (v w : V), adj v w = adj' v w
⊢ adj = adj'

Tactic:
funext v w
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
adj : V → V → Bool
property : (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true
adj' : V → V → Bool
property_1 : (∀ (x y : V), adj' x y = adj' y x) ∧ ∀ (x : V), ¬adj' x x = true
h : Eq.{u + 1} (α := V → V → Prop) (fun (v w : V) ↦ adj v w = true) fun (v w : V) ↦ adj' v w = true
v w : V
⊢ adj v w = adj' v w

Tactic:
simpa [Bool.coe_iff_coe] using congr_fun₂ h v w

Premises used: Bool.coe_iff_coe, congr_fun₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
inst : Fintype V
inst_1 : DecidableEq V
Adj : V → V → Prop
hs : Symmetric Adj
hi : Std.Irrefl Adj
simp :
  ∃ (a : V → V → Bool) (h : (∀ (x y : V), a x y = a y x) ∧ ∀ (x : V), a x x = false),
    (SimpleGraph.mk' :
          (a : { adj : V → V → Bool // (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true }) → SimpleGraph V)
        (Subtype.mk (p := fun (a : V → V → Bool) ↦ (∀ (x y : V), a x y = a y x) ∧ ∀ (x : V), ¬a x x = true) a ⋯) =
      { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }
⊢ Membership.mem (γ := Finset (SimpleGraph V)) (map SimpleGraph.mk' univ)
    { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }

Tactic:
simp only [mem_map, mem_univ, true_and, Subtype.exists, Bool.not_eq_true]

Premises used: Finset.mem_univ, Subtype.exists, Bool.not_eq_true, Finset.mem_map, true_and