awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∃ (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 }

Tactic:
⟨fun v w ↦ Adj v w, ⟨?_, ?_⟩, ?_⟩

Premises used: And.intro, Exists.intro, Decidable.decide
-- 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
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
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)) ⋯) =
    { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }
⊢ ∃ (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 }

Tactic:
refine ⟨fun v w ↦ Adj v w, ⟨?_, ?_⟩, ?_⟩
-- 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
⊢ ∀ (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:
simp [hs.iff]

Premises used: Symmetric.iff
-- 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
v : V
⊢ (fun (v w : V) ↦ decide (Adj v w)) v v = false

Tactic:
simp [hi.irrefl v]

Premises used: Std.Irrefl.irrefl
-- 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
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)) ⋯))
        x x_1 ↔
      { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }.Adj x x_1
⊢ (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 }

Tactic:
ext
-- 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
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)) ⋯))
      x x_1 ↔
    { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }.Adj x x_1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
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
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)) ⋯) =
      { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }
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
refine_3₁ 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)) ⋯) =
      { Adj := Adj, symm := hs, loopless := hi : SimpleGraph V }
⊢ ∀ (x : SimpleGraph V), Membership.mem (γ := Finset (SimpleGraph V)) (map SimpleGraph.mk' univ) 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

Premises used: Finset.mem_univ, Subtype.exists, Bool.not_eq_true, Finset.mem_map, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
inst : Finite V
⊢ Finite.{u + 1} (SimpleGraph V)

Tactic:
.of_injective SimpleGraph.Adj fun _ _ ↦ SimpleGraph.ext

Premises used: SimpleGraph.Adj, SimpleGraph.ext, Finite.of_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
r : V → V → Prop
v w : V
⊢ (fromRel r).Adj v w ↔ v ≠ w ∧ (r v w ∨ r w v)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
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)
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)
⊢ (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

Tactic:
cases v
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
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)
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)
⊢ (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 w
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
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)
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)
⊢ (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 w
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u_1
W : Type u_2
val 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:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u_1
W : Type u_2
val : V
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:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u_1
W : Type u_2
val : W
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:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u_1
W : Type u_2
val 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:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
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)
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)
⊢ ¬(v.isLeft = true ∧ v.isRight = true ∨ v.isRight = true ∧ v.isLeft = true)

Tactic:
cases v
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u_1
W : Type u_2
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:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u_1
W : Type u_2
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:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ ¬G.Adj v v

Tactic:
G.loopless.irrefl v

Premises used: Std.Irrefl.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
⊢ G.Adj u v ↔ G.Adj v u

Tactic:
⟨fun x => G.symm x, fun x => G.symm x⟩

Premises used: SimpleGraph.symm, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ G.Adj v u

Tactic:
G.symm h

Premises used: SimpleGraph.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a : V
h : G.Adj a a
⊢ False

Tactic:
G.irrefl h

Premises used: SimpleGraph.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a : V
h : G.Adj a a
⊢ False

Tactic:
exact G.irrefl h

Premises used: SimpleGraph.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
h : G.Adj a b
⊢ a ≠ b

Tactic:
G.ne_of_adj h

Premises used: SimpleGraph.ne_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
h : G.Adj a b
⊢ b ≠ a

Tactic:
h.ne.symm

Premises used: SimpleGraph.Adj.ne, Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w x : V
h : G.Adj v x
hn : ¬G.Adj w x
⊢ v ≠ w

Tactic:
fun h' =>
  hn (h' ▸ h)

Premises used: Eq.rec, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
⊢ Injective.{u + 1, u + 1} (α := SimpleGraph V) Adj

Tactic:
fun _ _ => SimpleGraph.ext

Premises used: SimpleGraph.ext, Function.Injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G H : SimpleGraph V
⊢ G.Adj = H.Adj ↔ G = H

Tactic:
adj_injective.eq_iff

Premises used: SimpleGraph.adj_injective, Function.Injective.eq_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
h : s(u, v) = s(w, x)
⊢ 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

Premises used: Sym2.eq, Prod.swap_prod_mk, Sym2.rel_iff', Prod.mk.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
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
inr : ∀ (hr : u = x ∧ v = w), G.Adj u v ↔ G.Adj w x
⊢ G.Adj u v ↔ G.Adj w x

Tactic:
rcases h with hl | hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
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
inl₁ inl₂ : G.Adj w x ↔ G.Adj w x
⊢ G.Adj u v ↔ G.Adj w x

Tactic:
rw [hl.1, hl.2]

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
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
inr₂ inr₃ : G.Adj w x ↔ G.Adj w x
⊢ G.Adj u v ↔ G.Adj w x

Tactic:
rw [hr.1, hr.2, adj_comm]

Premises used: And.right, And.left, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G H : SimpleGraph V
⊢ G ≤ H ↔ ∀ (v w : V), G.Adj v w → H.Adj v w

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
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
rwa : (x.Adj w ⊔ y.Adj w) v
rwa₁ : max (x.Adj w v) (y.Adj w v)
rwa₂ : max (x.Adj v w) (y.Adj w v)
rwa₃ rwa₄ rwa₅ rwa₆ : max (x.Adj v w) (y.Adj v w)
⊢ (x.Adj ⊔ y.Adj) w v

Tactic:
rwa [Pi.sup_apply, Pi.sup_apply, x.adj_comm, y.adj_comm]

Premises used: Pi.sup_apply, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
x y : SimpleGraph V
v w : V
⊢ (x ⊔ y).Adj v w ↔ x.Adj v w ∨ y.Adj v w

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
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
rwa : (x.Adj w ⊓ y.Adj w) v
rwa₁ : min (x.Adj w v) (y.Adj w v)
rwa₂ : min (x.Adj v w) (y.Adj w v)
rwa₃ rwa₄ rwa₅ rwa₆ : min (x.Adj v w) (y.Adj v w)
⊢ (x.Adj ⊓ y.Adj) w v

Tactic:
rwa [Pi.inf_apply, Pi.inf_apply, x.adj_comm, y.adj_comm]

Premises used: Pi.inf_apply, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
x y : SimpleGraph V
v w : V
⊢ (x ⊓ y).Adj v w ↔ x.Adj v w ∧ y.Adj v w

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G_1 : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
G : SimpleGraph V
v w : V
h : (fun (v w : V) ↦ v ≠ w ∧ ¬G.Adj v w) v w
hne : v ≠ w
right rwa rwa₁ rwa₂ rwa₃ : ¬G.Adj v w
⊢ ¬G.Adj w v

Tactic:
rwa [adj_comm]

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ Gᶜ.Adj v w ↔ v ≠ w ∧ ¬G.Adj v w

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
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
rwa : x.Adj v w ∧ ¬y.Adj w v
rwa₁ rwa₂ rwa₃ rwa₄ : x.Adj v w ∧ ¬y.Adj v w
⊢ x.Adj w v ∧ ¬y.Adj w v

Tactic:
rwa [x.adj_comm, y.adj_comm]

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
x y : SimpleGraph V
v w : V
⊢ (x \ y).Adj v w ↔ x.Adj v w ∧ ¬y.Adj v w

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
s : Set (SimpleGraph V)
a b : V
⊢ (sSup s).Adj a b ↔ ∃ G ∈ s, G.Adj a b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
a b : V
s : Set (SimpleGraph V)
⊢ (sInf s).Adj a b ↔ (∀ G ∈ s, G.Adj a b) ∧ a ≠ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
a b : V
f : ι → SimpleGraph V
⊢ Adj (⨆ (i : ι), f i) a b ↔ ∃ (i : ι), (f i).Adj a b

Tactic:
simp [iSup]

Premises used: iSup
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
a b : V
f : ι → SimpleGraph V
⊢ Adj (⨅ (i : ι), f i) a b ↔ (∀ (i : ι), (f i).Adj a b) ∧ a ≠ b

Tactic:
simp [iInf]

Premises used: iInf
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
a b : V
s : Set (SimpleGraph V)
hs : s.Nonempty
obtain : ∀ (G : SimpleGraph V) (hG : G ∈ s), (∀ G ∈ s, G.Adj a b) → a ≠ b
⊢ (∀ G ∈ s, G.Adj a b) → a ≠ b

Tactic:
obtain ⟨G, hG⟩ := hs
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
a b : V
s : Set (SimpleGraph V)
G : SimpleGraph V
hG : G ∈ s
⊢ (∀ G ∈ s, G.Adj a b) → a ≠ b

Tactic:
fun h => (h _ hG).ne

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
a b : V
s : Set (SimpleGraph V)
G : SimpleGraph V
hG : G ∈ s
⊢ (∀ G ∈ s, G.Adj a b) → a ≠ b

Tactic:
exact fun h => (h _ hG).ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
a b : V
inst : Nonempty ι
f : ι → SimpleGraph V
rw : Adj (sInf (Set.range fun (i : ι) ↦ f i)) a b ↔ ∀ (i : ι), (f i).Adj a b
rw₁ :
  (∀ (G : SimpleGraph V), Membership.mem (γ := Set (SimpleGraph V)) (Set.range fun (i : ι) ↦ f i) G → G.Adj a b) ↔
    ∀ (i : ι), (f i).Adj a b
rw₂ rw₃ : (∀ (i : ι), (f i).Adj a b) ↔ ∀ (i : ι), (f i).Adj a b
⊢ Adj (⨅ (i : ι), f i) a b ↔ ∀ (i : ι), (f i).Adj a b

Tactic:
rw [iInf, sInf_adj_of_nonempty (Set.range_nonempty _), Set.forall_mem_range]

Premises used: iInf, Set.forall_mem_range, Set.range_nonempty, SimpleGraph.sInf_adj_of_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G_1 : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
G : SimpleGraph V
v w : V
hvw : Adj { Adj := Ne, symm := ⋯, loopless := ⋯ } v w
pos : ∀ (h : G.Adj v w), (G ⊔ Gᶜ).Adj v w
neg : ∀ (h : ¬G.Adj v w), (G ⊔ Gᶜ).Adj v w
⊢ (G ⊔ Gᶜ).Adj v w

Tactic:
by_cases h : G.Adj v w

Premises used: SimpleGraph.Adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G_1 : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
G : SimpleGraph V
v w : V
hvw : Adj { Adj := Ne, symm := ⋯, loopless := ⋯ } v w
h : G.Adj v w
⊢ (G ⊔ Gᶜ).Adj v w

Tactic:
Or.inl h

Premises used: Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G_1 : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
G : SimpleGraph V
v w : V
hvw : Adj { Adj := Ne, symm := ⋯, loopless := ⋯ } v w
h : G.Adj v w
⊢ (G ⊔ Gᶜ).Adj v w

Tactic:
exact Or.inl h

Premises used: Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G_1 : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
G : SimpleGraph V
v w : V
hvw : Adj { Adj := Ne, symm := ⋯, loopless := ⋯ } v w
h : ¬G.Adj v w
⊢ (G ⊔ Gᶜ).Adj v w

Tactic:
Or.inr ⟨hvw, h⟩

Premises used: And.intro, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G_1 : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
G : SimpleGraph V
v w : V
hvw : Adj { Adj := Ne, symm := ⋯, loopless := ⋯ } v w
h : ¬G.Adj v w
⊢ (G ⊔ Gᶜ).Adj v w

Tactic:
exact Or.inr ⟨hvw, h⟩

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v w : V
e : Sym2 V
x y : SimpleGraph V
Adj : ∀ (v w : V), (x \ y).Adj v w ↔ (x ⊓ yᶜ).Adj v w
⊢ x \ y = x ⊓ yᶜ

Tactic:
ext v w
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
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
⊢ (x \ y).Adj v w ↔ (x ⊓ yᶜ).Adj v w

Tactic:
⟨fun h => ⟨h.1, ⟨?_, h.2⟩⟩, fun h => ⟨h.1, h.2.2⟩⟩

Premises used: And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
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
Adj : ∀ (h : (x \ y).Adj v w), v ≠ w
⊢ (x \ y).Adj v w ↔ (x ⊓ yᶜ).Adj v w

Tactic:
refine ⟨fun h => ⟨h.1, ⟨?_, h.2⟩⟩, fun h => ⟨h.1, h.2.2⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w : V
e : Sym2 V
x y : SimpleGraph V
v : V
h : (x \ y).Adj v v
⊢ False

Tactic:
x.irrefl h.1

Premises used: And.left, SimpleGraph.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w : V
e : Sym2 V
x y : SimpleGraph V
v : V
h : (x \ y).Adj v v
⊢ False

Tactic:
exact x.irrefl h.1

Premises used: And.left, SimpleGraph.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v w : V
e : Sym2 V
ι_1 : Type u
κ : ι_1 → Type u
f : (a : ι_1) → κ a → SimpleGraph V
Adj :
  ∀ (x x_1 : V),
    SimpleGraph.Adj (⨅ (a : ι_1), ⨆ (b : κ a), f a b) x x_1 ↔
      SimpleGraph.Adj (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a)) x x_1
⊢ Eq.{u + 1} (α := SimpleGraph V) (⨅ (a : ι_1), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a))

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v w : V
e : Sym2 V
ι_1 : Type u
κ : ι_1 → Type u
f : (a : ι_1) → κ a → SimpleGraph V
x x_1 : V
⊢ Adj (⨅ (a : ι_1), ⨆ (b : κ a), f a b) x x_1 ↔ Adj (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a)) x x_1

Tactic:
simp [Classical.skolem]

Premises used: Classical.skolem
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
v w : V
⊢ Adj ⊤ v w ↔ v ≠ w

Tactic:
Iff.rfl

Premises used: Iff.rfl, Not