awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
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)) : α)
⊢ (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
have 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)) : α)
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
Cleared hypotheses: n, u, v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : MulZeroOneClass α
inst_1 : Nontrivial α
A : Matrix V V α
h : A.IsAdjMatrix
inst_2 : DecidableEq α
⊢ adjMatrix α h.toGraph = A
have a : ∀ (i j : V), adjMatrix α h.toGraph i j = A i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
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
⊢ adjMatrix α h.toGraph i j = A i j
have a : ∀ (h' : A i j = 0), adjMatrix α h.toGraph i j = A i j
Tactic: obtain h' | h' := h.zero_or_one i j
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
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
⊢ adjMatrix α h.toGraph i j = A i j
have a₁ : ∀ (h' : A i j = 1), adjMatrix α h.toGraph i j = A i j
Tactic: obtain h' | h' := h.zero_or_one i j
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
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
⊢ 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)
have 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'
Tactic: simp only [mk.injEq, Subtype.mk.injEq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
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
⊢ adj = adj'
have h₁ : ∀ (v w : V), adj v w = adj' v w
Tactic: funext v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
inst_1 : DecidableEq V
Adj : V → V → Prop
hs : Symmetric Adj
hi : Std.Irrefl Adj
⊢ Membership.mem (γ := Finset (SimpleGraph V)) (map SimpleGraph.mk' univ)
    { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }
have 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 sorry) =
    { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }
Tactic: simp only [mem_map, mem_univ, true_and, Subtype.exists, Bool.not_eq_true]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
inst_1 : DecidableEq V
Adj : V → V → Prop
hs : Symmetric Adj
hi : Std.Irrefl Adj
⊢ ∃ (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 }
have refine_1 : ∀ (x y : V), Eq (α := Bool) ((fun (v w : V) ↦ decide (Adj v w)) x y) ((fun (v w : V) ↦ decide (Adj v w)) y x)
Tactic: refine ⟨fun v w ↦ Adj v w, ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
inst_1 : DecidableEq V
Adj : V → V → Prop
hs : Symmetric Adj
hi : Std.Irrefl Adj
refine_1 : ∀ (x y : V), Eq (α := Bool) ((fun (v w : V) ↦ decide (Adj v w)) x y) ((fun (v w : V) ↦ decide (Adj v w)) y x)
⊢ ∃ (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 }
have refine_2 : ∀ (x : V), (fun (v w : V) ↦ decide (Adj v w)) x x = false
Tactic: refine ⟨fun v w ↦ Adj v w, ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
inst_1 : DecidableEq V
Adj : V → V → Prop
hs : Symmetric Adj
hi : Std.Irrefl Adj
refine_1 : ∀ (x y : V), Eq (α := Bool) ((fun (v w : V) ↦ decide (Adj v w)) x y) ((fun (v w : V) ↦ decide (Adj v w)) y x)
refine_2 : ∀ (x : V), (fun (v w : V) ↦ decide (Adj v w)) x x = false
⊢ ∃ (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 }
have refine_3 : (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)
      (fun (v w : V) ↦ decide (Adj v w)) sorry) =
  { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }
Tactic: refine ⟨fun v w ↦ Adj v w, ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
inst_1 : DecidableEq V
Adj : V → V → Prop
hs : Symmetric Adj
hi : Std.Irrefl Adj
⊢ (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)
        (fun (v w : V) ↦ decide (Adj v w)) ⋯) =
    { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }
have refine_3 : ∀ (x x_1 : V),
  SimpleGraph.Adj
      ((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)
          (fun (v w : V) ↦ decide (Adj v w)) sorry))
      x x_1 ↔
    { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }.Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
inst_1 : DecidableEq V
⊢ ∀ (x : SimpleGraph V), Membership.mem (γ := Finset (SimpleGraph V)) (map SimpleGraph.mk' univ) x
have rintro : ∀ (Adj : V → V → Prop) (hs : Symmetric Adj) (hi : Std.Irrefl Adj),
  Membership.mem (γ := Finset (SimpleGraph V)) (map SimpleGraph.mk' univ)
    { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }
Tactic: classical
    rintro ⟨Adj, hs, hi⟩
    simp only [mem_map, mem_univ, true_and, Subtype.exists, Bool.not_eq_true]
    refine ⟨fun v w ↦ Adj v w, ⟨?_, ?_⟩, ?_⟩
    · simp [hs.iff]
    · intro v; simp [hi.irrefl v]
    · ext
      simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
inst_1 : DecidableEq V
rintro :
  ∀ (Adj : V → V → Prop) (hs : Symmetric Adj) (hi : Std.Irrefl Adj),
    Membership.mem (γ := Finset (SimpleGraph V)) (map SimpleGraph.mk' univ)
      { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }
⊢ ∀ (x : SimpleGraph V), Membership.mem (γ := Finset (SimpleGraph V)) (map SimpleGraph.mk' univ) x
have rintro₁ : ∀ (Adj : V → V → Prop) (hs : Symmetric Adj) (hi : Std.Irrefl Adj),
  ∃ (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 sorry) =
      { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }
Tactic: classical
    rintro ⟨Adj, hs, hi⟩
    simp only [mem_map, mem_univ, true_and, Subtype.exists, Bool.not_eq_true]
    refine ⟨fun v w ↦ Adj v w, ⟨?_, ?_⟩, ?_⟩
    · simp [hs.iff]
    · intro v; simp [hi.irrefl v]
    · ext
      simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
inst_1 : DecidableEq V
rintro :
  ∀ (Adj : V → V → Prop) (hs : Symmetric Adj) (hi : Std.Irrefl Adj),
    Membership.mem (γ := Finset (SimpleGraph V)) (map SimpleGraph.mk' univ)
      { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }
rintro₁ :
  ∀ (Adj : V → V → Prop) (hs : Symmetric Adj) (hi : Std.Irrefl Adj),
    ∃ (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 }
⊢ ∀ (x : SimpleGraph V), Membership.mem (γ := Finset (SimpleGraph V)) (map SimpleGraph.mk' univ) x
have refine_1 : ∀ (Adj : V → V → Prop) (hs : Symmetric Adj) (hi : Std.Irrefl Adj) (x y : V),
  Eq (α := Bool) ((fun (v w : V) ↦ decide (Adj v w)) x y) ((fun (v w : V) ↦ decide (Adj v w)) y x)
Tactic: classical
    rintro ⟨Adj, hs, hi⟩
    simp only [mem_map, mem_univ, true_and, Subtype.exists, Bool.not_eq_true]
    refine ⟨fun v w ↦ Adj v w, ⟨?_, ?_⟩, ?_⟩
    · simp [hs.iff]
    · intro v; simp [hi.irrefl v]
    · ext
      simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
inst_1 : DecidableEq V
rintro :
  ∀ (Adj : V → V → Prop) (hs : Symmetric Adj) (hi : Std.Irrefl Adj),
    Membership.mem (γ := Finset (SimpleGraph V)) (map SimpleGraph.mk' univ)
      { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }
rintro₁ :
  ∀ (Adj : V → V → Prop) (hs : Symmetric Adj) (hi : Std.Irrefl Adj),
    ∃ (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 }
refine_1 :
  ∀ (Adj : V → V → Prop) (hs : Symmetric Adj) (hi : Std.Irrefl Adj) (x y : V),
    Eq (α := Bool) ((fun (v w : V) ↦ decide (Adj v w)) x y) ((fun (v w : V) ↦ decide (Adj v w)) y x)
⊢ ∀ (x : SimpleGraph V), Membership.mem (γ := Finset (SimpleGraph V)) (map SimpleGraph.mk' univ) x
have refine_2 : ∀ (Adj : V → V → Prop) (hs : Symmetric Adj) (hi : Std.Irrefl Adj) (x : V),
  (fun (v w : V) ↦ decide (Adj v w)) x x = false
Tactic: classical
    rintro ⟨Adj, hs, hi⟩
    simp only [mem_map, mem_univ, true_and, Subtype.exists, Bool.not_eq_true]
    refine ⟨fun v w ↦ Adj v w, ⟨?_, ?_⟩, ?_⟩
    · simp [hs.iff]
    · intro v; simp [hi.irrefl v]
    · ext
      simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
inst_1 : DecidableEq V
rintro :
  ∀ (Adj : V → V → Prop) (hs : Symmetric Adj) (hi : Std.Irrefl Adj),
    Membership.mem (γ := Finset (SimpleGraph V)) (map SimpleGraph.mk' univ)
      { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }
rintro₁ :
  ∀ (Adj : V → V → Prop) (hs : Symmetric Adj) (hi : Std.Irrefl Adj),
    ∃ (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 }
refine_1 :
  ∀ (Adj : V → V → Prop) (hs : Symmetric Adj) (hi : Std.Irrefl Adj) (x y : V),
    Eq (α := Bool) ((fun (v w : V) ↦ decide (Adj v w)) x y) ((fun (v w : V) ↦ decide (Adj v w)) y x)
refine_2 :
  ∀ (Adj : V → V → Prop) (hs : Symmetric Adj) (hi : Std.Irrefl Adj) (x : V),
    (fun (v w : V) ↦ decide (Adj v w)) x x = false
⊢ ∀ (x : SimpleGraph V), Membership.mem (γ := Finset (SimpleGraph V)) (map SimpleGraph.mk' univ) x
have refine_3 : ∀ (Adj : V → V → Prop) (hs : Symmetric Adj) (hi : Std.Irrefl Adj),
  (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)
        (fun (v w : V) ↦ decide (Adj v w)) sorry) =
    { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }
Tactic: classical
    rintro ⟨Adj, hs, hi⟩
    simp only [mem_map, mem_univ, true_and, Subtype.exists, Bool.not_eq_true]
    refine ⟨fun v w ↦ Adj v w, ⟨?_, ?_⟩, ?_⟩
    · simp [hs.iff]
    · intro v; simp [hi.irrefl v]
    · ext
      simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u_1
W : Type u_2
v w : V ⊕ W
⊢ (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) v w →
    (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) w v
have inl : ∀ (val : V),
  (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inl val) w →
    (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) w (Sum.inl val)
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u_1
W : Type u_2
v w : V ⊕ W
inl :
  ∀ (val : V),
    (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inl val) w →
      (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) w (Sum.inl val)
⊢ (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) v w →
    (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) w v
have inr : ∀ (val : W),
  (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inr val) w →
    (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) w (Sum.inr val)
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u_1
W : Type u_2
w : V ⊕ W
val : V
⊢ (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inl val) w →
    (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) w (Sum.inl val)
have inl : ∀ (val_1 : V),
  (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inl val)
      (Sum.inl val_1) →
    (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inl val_1)
      (Sum.inl val)
Tactic: cases w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u_1
W : Type u_2
w : V ⊕ W
val : V
inl :
  ∀ (val_1 : V),
    (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inl val)
        (Sum.inl val_1) →
      (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inl val_1)
        (Sum.inl val)
⊢ (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inl val) w →
    (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) w (Sum.inl val)
have inl₁ : ∀ (val_1 : W),
  (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inl val)
      (Sum.inr val_1) →
    (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inr val_1)
      (Sum.inl val)
Tactic: cases w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u_1
W : Type u_2
w : V ⊕ W
val : W
⊢ (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inr val) w →
    (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) w (Sum.inr val)
have inr : ∀ (val_1 : V),
  (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inr val)
      (Sum.inl val_1) →
    (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inl val_1)
      (Sum.inr val)
Tactic: cases w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u_1
W : Type u_2
w : V ⊕ W
val : W
inr :
  ∀ (val_1 : V),
    (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inr val)
        (Sum.inl val_1) →
      (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inl val_1)
        (Sum.inr val)
⊢ (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inr val) w →
    (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) w (Sum.inr val)
have inr₁ : ∀ (val_1 : W),
  (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inr val)
      (Sum.inr val_1) →
    (fun (v w : V ⊕ W) ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true) (Sum.inr val_1)
      (Sum.inr val)
Tactic: cases w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u_1
W : Type u_2
v : V ⊕ W
⊢ ¬(v.isLeft = true ∧ v.isRight = true ∨ v.isRight = true ∧ v.isLeft = true)
have inl : ∀ (val : V),
  ¬(Sum.isLeft.{u_1, u_2} (β := W) (Sum.inl val) = true ∧ Sum.isRight.{u_1, u_2} (β := W) (Sum.inl val) = true ∨
      Sum.isRight.{u_1, u_2} (β := W) (Sum.inl val) = true ∧ Sum.isLeft.{u_1, u_2} (β := W) (Sum.inl val) = true)
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u_1
W : Type u_2
v : V ⊕ W
inl :
  ∀ (val : V),
    ¬(Sum.isLeft.{u_1, u_2} (β := W) (Sum.inl val) = true ∧ Sum.isRight.{u_1, u_2} (β := W) (Sum.inl val) = true ∨
        Sum.isRight.{u_1, u_2} (β := W) (Sum.inl val) = true ∧ Sum.isLeft.{u_1, u_2} (β := W) (Sum.inl val) = true)
⊢ ¬(v.isLeft = true ∧ v.isRight = true ∨ v.isRight = true ∧ v.isLeft = true)
have inr : ∀ (val : W),
  ¬(Sum.isLeft.{u_1, u_2} (α := V) (Sum.inr val) = true ∧ Sum.isRight.{u_1, u_2} (α := V) (Sum.inr val) = true ∨
      Sum.isRight.{u_1, u_2} (α := V) (Sum.inr val) = true ∧ Sum.isLeft.{u_1, u_2} (α := V) (Sum.inr val) = true)
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
h : s(u, v) = s(w, x)
⊢ G.Adj u v ↔ G.Adj w x
have h₁ : u = w ∧ v = x ∨ u = x ∧ v = w
Tactic: simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
h : u = w ∧ v = x ∨ u = x ∧ v = w
⊢ G.Adj u v ↔ G.Adj w x
have inl : ∀ (hl : u = w ∧ v = x), G.Adj u v ↔ G.Adj w x
Tactic: rcases h with hl | hr
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
h : u = w ∧ v = x ∨ u = x ∧ v = w
inl : ∀ (hl : u = w ∧ v = x), G.Adj u v ↔ G.Adj w x
⊢ G.Adj u v ↔ G.Adj w x
have inr : ∀ (hr : u = x ∧ v = w), G.Adj u v ↔ G.Adj w x
Tactic: rcases h with hl | hr
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
hl : u = w ∧ v = x
⊢ G.Adj u v ↔ G.Adj w x
have inl : G.Adj w v ↔ G.Adj w x
Tactic: rw [hl.1, hl.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
hl : u = w ∧ v = x
inl : G.Adj w v ↔ G.Adj w x
⊢ G.Adj u v ↔ G.Adj w x
have inl₁ : G.Adj w x ↔ G.Adj w x
Tactic: rw [hl.1, hl.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
hr : u = x ∧ v = w
⊢ G.Adj u v ↔ G.Adj w x
have inr : G.Adj x v ↔ G.Adj w x
Tactic: rw [hr.1, hr.2, adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
hr : u = x ∧ v = w
inr : G.Adj x v ↔ G.Adj w x
⊢ G.Adj u v ↔ G.Adj w x
have inr₁ : G.Adj x w ↔ G.Adj w x
Tactic: rw [hr.1, hr.2, adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
hr : u = x ∧ v = w
inr : G.Adj x v ↔ G.Adj w x
inr₁ : G.Adj x w ↔ G.Adj w x
⊢ G.Adj u v ↔ G.Adj w x
have inr₂ : G.Adj w x ↔ G.Adj w x
Tactic: rw [hr.1, hr.2, adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
x y : SimpleGraph V
v w : V
h : (x.Adj ⊔ y.Adj) v w
⊢ (x.Adj ⊔ y.Adj) w v
have rwa : (x.Adj w ⊔ y.Adj w) v
Tactic: rwa [Pi.sup_apply, Pi.sup_apply, x.adj_comm, y.adj_comm]