awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
hn : LE.le (α := ℝ) 6 (↑n : ℝ)
linarith : HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2 < 0 → 3 / 3 = 1
linarith₁ : HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2 < 0 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2 < 0 → GT.gt (α := ℝ) 3 0
linarith₃ :
  HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2 < 0 →
    HSub.hSub (α := ℝ) 6 (↑n : ℝ) + (HMul.hMul (α := ℝ) 1 (↑n : ℝ) - HMul.hMul (α := ℝ) 3 2 - HMul.hMul (α := ℝ) 3 0) =
      0
⊢ 0 ≤ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2

Tactic:
linarith
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
hn : 6 ≤ n
⊢ 0 ≤ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2

Tactic:
have : (0 : ℝ) ≤ n / 3 - 2 := by rify at hn; linarith
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
hn : 6 ≤ n
this : 0 ≤ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
⊢ ‖(HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))‖ ≤
    (↑(ruzsaSzemerediNumberNat n) : ℝ)

Tactic:
simpa [neg_mul, abs_mul, abs_of_nonneg this] using ruzsaSzemerediNumberNat_lower_bound n

Premises used: abs_mul, abs_of_nonneg, neg_mul, ruzsaSzemerediNumberNat_lower_bound
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
⊢ e ∈ E(G)

Tactic:
(edge_mem_iff_exists_isLink ..).2 ⟨x, y, h⟩

Premises used: Iff.mpr, Graph.edge_mem_iff_exists_isLink, Exists.intro
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
he : e ∉ E(G)
⊢ ¬G.IsLink e x y

Tactic:
mt IsLink.edge_mem he

Premises used: Graph.IsLink.edge_mem, mt
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
⊢ G.IsLink e y x

Tactic:
G.isLink_symm h.edge_mem h

Premises used: Graph.IsLink.edge_mem, Graph.isLink_symm
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
⊢ x ∈ V(G)

Tactic:
G.left_mem_of_isLink h

Premises used: Graph.left_mem_of_isLink
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
⊢ y ∈ V(G)

Tactic:
h.symm.left_mem

Premises used: Graph.IsLink.left_mem, Graph.IsLink.symm
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
⊢ G.IsLink e x y ↔ G.IsLink e y x

Tactic:
⟨.symm, .symm⟩

Premises used: Graph.IsLink.symm, Iff.intro
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
e : β
G : Graph α β
h : e ∈ E(G)
⊢ ∃ (x : α) (y : α), G.IsLink e x y

Tactic:
(edge_mem_iff_exists_isLink ..).1 h

Premises used: Graph.edge_mem_iff_exists_isLink, Iff.mp
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ E(G) = {e : β | ∃ (x : α) (y : α), G.IsLink e x y}

Tactic:
Set.ext G.edge_mem_iff_exists_isLink

Premises used: Set.ext, Graph.edge_mem_iff_exists_isLink
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z w : α
e : β
G : Graph α β
h : G.IsLink e x y
h' : G.IsLink e z w
⊢ x = z ∨ x = w

Tactic:
G.eq_or_eq_of_isLink_of_isLink h h'

Premises used: Graph.eq_or_eq_of_isLink_of_isLink
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z w : α
e : β
G : Graph α β
h : G.IsLink e x y
h' : G.IsLink e z w
⊢ y = z ∨ y = w

Tactic:
h.symm.left_eq_or_eq h'

Premises used: Graph.IsLink.symm, Graph.IsLink.left_eq_or_eq
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z w : α
e : β
G : Graph α β
h : G.IsLink e x y
h' : G.IsLink e z w
hzx : x ≠ z
⊢ x = w

Tactic:
(h.left_eq_or_eq h').elim (False.elim ∘ hzx) id

Premises used: False.elim, Function.comp, id, Graph.IsLink.left_eq_or_eq, Or.elim
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
h : G.IsLink e x y
h' : G.IsLink e x z
inl : ∀ (h' : G.IsLink e x y), y = y
inr : ∀ (h : G.IsLink e y y) (h' : G.IsLink e y z), y = z
⊢ y = z

Tactic:
obtain rfl | rfl := h.right_eq_or_eq h'.symm

Premises used: Graph.IsLink.symm, Graph.IsLink.right_eq_or_eq, rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h h' : G.IsLink e x y
⊢ y = y

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
y z : α
e : β
G : Graph α β
h : G.IsLink e y y
h' : G.IsLink e y z
inr inr₁ : ∀ (h h' : G.IsLink e z z), z = z
⊢ y = z

Tactic:
obtain rfl | rfl := h'.right_eq_or_eq h.symm

Premises used: Graph.IsLink.symm, Graph.IsLink.right_eq_or_eq, rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
z : α
e : β
G : Graph α β
h h' : G.IsLink e z z
⊢ z = z

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
h : G.IsLink e x z
h' : G.IsLink e y z
⊢ x = y

Tactic:
h.symm.right_unique h'.symm

Premises used: Graph.IsLink.symm, Graph.IsLink.right_unique
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
x' y' : α
h : G.IsLink e x y
h' : G.IsLink e x' y'
inl : ∀ (h' : G.IsLink e x y'), x = x ∧ y = y' ∨ x = y' ∧ y = x
inr : ∀ (h' : G.IsLink e x' x), x = x' ∧ y = x ∨ x = x ∧ y = x'
⊢ x = x' ∧ y = y' ∨ x = y' ∧ y = x'

Tactic:
obtain rfl | rfl := h.left_eq_or_eq h'

Premises used: Graph.IsLink.left_eq_or_eq, rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
y' : α
h : G.IsLink e x y
h' : G.IsLink e x y'
⊢ x = x ∧ y = y' ∨ x = y' ∧ y = x

Tactic:
simp [h.right_unique h']

Premises used: Graph.IsLink.right_unique
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
x' : α
h : G.IsLink e x y
h' : G.IsLink e x' x
⊢ x = x' ∧ y = x ∨ x = x ∧ y = x'

Tactic:
simp [h'.symm.right_unique h]

Premises used: Graph.IsLink.symm, Graph.IsLink.right_unique
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
x' y' : α
⊢ G.IsLink e x' y' ↔ x = x' ∧ y = y' ∨ x = y' ∧ y = x'

Tactic:
⟨h.eq_and_eq_or_eq_and_eq, ?_⟩

Premises used: Iff.intro, Graph.IsLink.eq_and_eq_or_eq_and_eq
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
x' y' : α
refine : x = x' ∧ y = y' ∨ x = y' ∧ y = x' → G.IsLink e x' y'
⊢ G.IsLink e x' y' ↔ x = x' ∧ y = y' ∨ x = y' ∧ y = x'

Tactic:
refine ⟨h.eq_and_eq_or_eq_and_eq, ?_⟩
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
⊢ G.IsLink e x y

Tactic:
assumption
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
⊢ G.IsLink e y x

Tactic:
h.symm

Premises used: Graph.IsLink.symm
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
⊢ G.IsLink e y x

Tactic:
exact h.symm

Premises used: Graph.IsLink.symm
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
x' y' : α
rw : x = x' ∧ y = y' ∨ x = y' ∧ y = x' ↔ s(x, y) = s(x', y')
rw₁ rw₂ : x = x' ∧ y = y' ∨ x = y' ∧ y = x' ↔ x = x' ∧ y = y' ∨ x = y' ∧ y = x'
⊢ G.IsLink e x' y' ↔ s(x, y) = s(x', y')

Tactic:
rw [h.isLink_iff, Sym2.eq_iff]

Premises used: Graph.IsLink.isLink_iff, Sym2.eq_iff
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.Inc e x
⊢ e ∈ E(G)

Tactic:
h.choose_spec.edge_mem

Premises used: Graph.IsLink.edge_mem, Exists.choose_spec
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
he : e ∉ E(G)
⊢ ¬G.Inc e x

Tactic:
mt Inc.edge_mem he

Premises used: mt, Graph.Inc.edge_mem
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.Inc e x
⊢ x ∈ V(G)

Tactic:
h.choose_spec.left_mem

Premises used: Exists.choose_spec, Graph.IsLink.left_mem
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
⊢ G.Inc e x

Tactic:
⟨y, h⟩

Premises used: Graph.Inc, Exists.intro
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
⊢ G.Inc e y

Tactic:
⟨x, h.symm⟩

Premises used: Graph.Inc, Graph.IsLink.symm, Exists.intro
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
h : G.Inc e x
h' : G.IsLink e y z
⊢ x = y ∨ x = z

Tactic:
h.choose_spec.left_eq_or_eq h'

Premises used: Exists.choose_spec, Graph.IsLink.left_eq_or_eq
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
h : G.Inc e x
h' : G.IsLink e y z
hxy : x ≠ y
⊢ x = z

Tactic:
(h.eq_or_eq_of_isLink h').elim (False.elim ∘ hxy) id

Premises used: False.elim, Function.comp, id, Graph.Inc.eq_or_eq_of_isLink, Or.elim
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
h : G.IsLink e x y
⊢ G.IsLink e x z ↔ z = y

Tactic:
⟨fun h' ↦ h'.right_unique h, fun h' ↦ h' ▸ h⟩

Premises used: Eq.rec, Iff.intro, Graph.IsLink.right_unique, Eq.symm
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
⊢ G.IsLink e x y ↔ G.Inc e x ∧ G.Inc e y ∧ ∀ (z : α), G.Inc e z → z = x ∨ z = y

Tactic:
⟨fun h ↦ ⟨h.inc_left, h.inc_right, fun z h' ↦ h'.eq_or_eq_of_isLink h⟩, ?_⟩

Premises used: Graph.IsLink.inc_left, Graph.IsLink.inc_right, And.intro, Iff.intro, Graph.Inc.eq_or_eq_of_isLink
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
refine : (G.Inc e x ∧ G.Inc e y ∧ ∀ (z : α), G.Inc e z → z = x ∨ z = y) → G.IsLink e x y
⊢ G.IsLink e x y ↔ G.Inc e x ∧ G.Inc e y ∧ ∀ (z : α), G.Inc e z → z = x ∨ z = y

Tactic:
refine ⟨fun h ↦ ⟨h.inc_left, h.inc_right, fun z h' ↦ h'.eq_or_eq_of_isLink h⟩, ?_⟩
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
x' : α
hx' : G.IsLink e x x'
h : ∀ (z : α), G.Inc e z → z = x ∨ z = y
y' : α
hy' : G.IsLink e y y'
inl : ∀ (hx' : G.IsLink e x' x') (h : ∀ (z : α), G.Inc e z → z = x' ∨ z = y), G.IsLink e x' y
inr : ∀ (h : ∀ (z : α), G.Inc e z → z = x ∨ z = x') (hy' : G.IsLink e x' y'), G.IsLink e x x'
⊢ G.IsLink e x y

Tactic:
obtain rfl | rfl := h _ hx'.inc_right

Premises used: Graph.IsLink.inc_right, rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
y : α
e : β
G : Graph α β
x' y' : α
hy' : G.IsLink e y y'
hx' : G.IsLink e x' x'
h : ∀ (z : α), G.Inc e z → z = x' ∨ z = y
inl : ∀ (hy' : G.IsLink e x' y') (h : ∀ (z : α), G.Inc e z → z = x' ∨ z = x'), G.IsLink e x' x'
inl₁ : ∀ (hy' : G.IsLink e y x'), G.IsLink e x' y
⊢ G.IsLink e x' y

Tactic:
obtain rfl | rfl := hx'.left_eq_or_eq hy'

Premises used: Graph.IsLink.left_eq_or_eq, rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
e : β
G : Graph α β
x' y' : α
hx' : G.IsLink e x' x'
hy' : G.IsLink e x' y'
h : ∀ (z : α), G.Inc e z → z = x' ∨ z = x'
⊢ G.IsLink e x' x'

Tactic:
assumption
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
y : α
e : β
G : Graph α β
x' : α
hx' : G.IsLink e x' x'
h : ∀ (z : α), G.Inc e z → z = x' ∨ z = y
hy' : G.IsLink e y x'
⊢ G.IsLink e x' y

Tactic:
hy'.symm

Premises used: Graph.IsLink.symm
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
y : α
e : β
G : Graph α β
x' : α
hx' : G.IsLink e x' x'
h : ∀ (z : α), G.Inc e z → z = x' ∨ z = y
hy' : G.IsLink e y x'
⊢ G.IsLink e x' y

Tactic:
exact hy'.symm

Premises used: Graph.IsLink.symm
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
x' : α
hx' : G.IsLink e x x'
y' : α
h : ∀ (z : α), G.Inc e z → z = x ∨ z = x'
hy' : G.IsLink e x' y'
⊢ G.IsLink e x x'

Tactic:
assumption
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.Inc e x
⊢ G.IsLink e x h.other

Tactic:
h.choose_spec

Premises used: Exists.choose_spec, Graph.Inc.other
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.Inc e x
⊢ G.Inc e h.other

Tactic:
h.isLink_other.inc_right

Premises used: Graph.Inc.isLink_other, Graph.IsLink.inc_right
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
hx : G.Inc e x
hy : G.Inc e y
hz : G.Inc e z
by_contra! : ∀ (hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z), False
⊢ x = y ∨ x = z ∨ y = z

Tactic:
by_contra! ⟨hxy, hxz, hyz⟩
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
hx : G.Inc e x
hy : G.Inc e y
hz : G.Inc e z
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
obtain : ∀ (x' : α) (hx' : G.IsLink e x x'), False
⊢ False

Tactic:
obtain ⟨x', hx'⟩ := hx
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
hy : G.Inc e y
hz : G.Inc e z
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
x' : α
hx' : G.IsLink e x x'
⊢ G.IsLink e x y

Tactic:
obtain rfl := hy.eq_of_isLink_of_ne_left hx' hxy.symm

Premises used: Graph.Inc.eq_of_isLink_of_ne_left, Ne.symm, rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
hy : G.Inc e y
hz : G.Inc e z
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
hx' : G.IsLink e x y
⊢ G.Inc e z

Tactic:
obtain rfl := hz.eq_of_isLink_of_ne_left hx' hxz.symm

Premises used: Graph.Inc.eq_of_isLink_of_ne_left, Ne.symm, rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
hy : G.Inc e y
hz : G.Inc e z
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
hx' : G.IsLink e x y
hy₁ : G.Inc e z
⊢ x ≠ z

Tactic:
obtain rfl := hz.eq_of_isLink_of_ne_left hx' hxz.symm

Premises used: Graph.Inc.eq_of_isLink_of_ne_left, Ne.symm, rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
hy : G.Inc e y
hz : G.Inc e z
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
hx' : G.IsLink e x y
hy₁ : G.Inc e z
hxy₁ : x ≠ z
⊢ z ≠ z

Tactic:
obtain rfl := hz.eq_of_isLink_of_ne_left hx' hxz.symm

Premises used: Graph.Inc.eq_of_isLink_of_ne_left, Ne.symm, rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
hy : G.Inc e y
hz : G.Inc e z
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
hx' : G.IsLink e x y
hy₁ : G.Inc e z
hxy₁ : x ≠ z
hyz₁ : z ≠ z
⊢ G.IsLink e x z

Tactic:
obtain rfl := hz.eq_of_isLink_of_ne_left hx' hxz.symm

Premises used: Graph.Inc.eq_of_isLink_of_ne_left, Ne.symm, rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x z : α
e : β
G : Graph α β
hz : G.Inc e z
hxz : x ≠ z
hy : G.Inc e z
hxy : x ≠ z
hyz : z ≠ z
hx' : G.IsLink e x z
⊢ False

Tactic:
hyz rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x z : α
e : β
G : Graph α β
hz : G.Inc e z
hxz : x ≠ z
hy : G.Inc e z
hxy : x ≠ z
hyz : z ≠ z
hx' : G.IsLink e x z
⊢ False

Tactic:
exact hyz rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
mp : G₁.Inc e = G₂.Inc f → G₁.IsLink e = G₂.IsLink f
mpr : G₁.IsLink e = G₂.IsLink f → G₁.Inc e = G₂.Inc f
⊢ G₁.Inc e = G₂.Inc f ↔ G₁.IsLink e = G₂.IsLink f

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.Inc e = G₂.Inc f
mp : ∀ (x y : α), G₁.IsLink e x y ↔ G₂.IsLink f x y
⊢ G₁.IsLink e = G₂.IsLink f

Tactic:
ext x y
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.Inc e = G₂.Inc f
x y : α
mp : (G₁.Inc e x ∧ G₁.Inc e y ∧ ∀ (z : α), G₁.Inc e z → z = x ∨ z = y) ↔ G₂.IsLink f x y
mp₁ :
  (G₁.Inc e x ∧ G₁.Inc e y ∧ ∀ (z : α), G₁.Inc e z → z = x ∨ z = y) ↔
    G₂.Inc f x ∧ G₂.Inc f y ∧ ∀ (z : α), G₂.Inc f z → z = x ∨ z = y
mp₂ mp₃ :
  (G₂.Inc f x ∧ G₂.Inc f y ∧ ∀ (z : α), G₂.Inc f z → z = x ∨ z = y) ↔
    G₂.Inc f x ∧ G₂.Inc f y ∧ ∀ (z : α), G₂.Inc f z → z = x ∨ z = y
⊢ G₁.IsLink e x y ↔ G₂.IsLink f x y

Tactic:
rw [isLink_iff_inc, isLink_iff_inc, h]

Premises used: Graph.isLink_iff_inc
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.IsLink e = G₂.IsLink f
⊢ G₁.Inc e = G₂.Inc f

Tactic:
simp [funext_iff, Inc, h]

Premises used: Graph.Inc, funext_iff
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
⊢ G.IsLink e x x ↔ G.IsLoopAt e x

Tactic:
Iff.rfl

Premises used: Graph.IsLoopAt, Iff.rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsLoopAt e x
⊢ G.Inc e x

Tactic:
IsLink.inc_left h

Premises used: Graph.IsLink.inc_left
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLoopAt e x
h' : G.Inc e y
inl inr : ∀ (h : G.IsLoopAt e y), y = y
⊢ x = y

Tactic:
obtain rfl | rfl := h'.eq_or_eq_of_isLink h

Premises used: Graph.Inc.eq_or_eq_of_isLink, rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
y : α
e : β
G : Graph α β
h' : G.Inc e y
h : G.IsLoopAt e y
⊢ y = y

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsLoopAt e x
⊢ e ∈ E(G)

Tactic:
h.inc.edge_mem

Premises used: Graph.IsLoopAt.inc, Graph.Inc.edge_mem
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsLoopAt e x
⊢ x ∈ V(G)

Tactic:
h.inc.vertex_mem

Premises used: Graph.Inc.vertex_mem, Graph.IsLoopAt.inc
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsNonloopAt e x
⊢ G.Inc e x

Tactic:
h.choose_spec.2.inc_left

Premises used: Exists.choose_spec, Graph.IsLink.inc_left, And.right
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsNonloopAt e x
⊢ e ∈ E(G)

Tactic:
h.inc.edge_mem

Premises used: Graph.IsNonloopAt.inc, Graph.Inc.edge_mem
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsNonloopAt e x
⊢ x ∈ V(G)

Tactic:
h.inc.vertex_mem

Premises used: Graph.IsNonloopAt.inc, Graph.Inc.vertex_mem
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsLoopAt e x
y z : α
hyz : z ≠ y
hy : G.IsLink e y z
⊢ x ≠ x

Tactic:
rw [← h.eq_of_inc hy.inc_left, ← h.eq_of_inc hy.inc_right] at hyz

Premises used: Graph.IsLink.inc_left, Graph.IsLoopAt.eq_of_inc, Graph.IsLink.inc_right
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsLoopAt e x
y z : α
hyz : z ≠ y
hy : G.IsLink e y z
hyz₁ : x ≠ x
⊢ G.IsLink e y z

Tactic:
rw [← h.eq_of_inc hy.inc_left, ← h.eq_of_inc hy.inc_right] at hyz

Premises used: Graph.IsLink.inc_left, Graph.IsLoopAt.eq_of_inc, Graph.IsLink.inc_right
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsLoopAt e x
y z : α
hyz : x ≠ x
hy : G.IsLink e y z
⊢ False

Tactic:
hyz rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsLoopAt e x
y z : α
hyz : x ≠ x
hy : G.IsLink e y z
⊢ False

Tactic:
exact hyz rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsNonloopAt e x
y : α
⊢ ¬G.IsLoopAt e y

Tactic:
fun h' ↦ h'.not_isNonloopAt x h

Premises used: Graph.IsLoopAt.not_isNonloopAt, Not
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
⊢ G.IsNonloopAt e x ↔ G.Inc e x ∧ ¬G.IsLoopAt e x

Tactic:
⟨fun h ↦ ⟨h.inc, h.not_isLoopAt _⟩, fun ⟨⟨y, hy⟩, hn⟩ ↦ ⟨y, mt (fun h ↦ h ▸ hy) hn, hy⟩⟩

Premises used: Graph.IsNonloopAt.not_isLoopAt, mt, Graph.IsNonloopAt.inc, Graph.IsNonloopAt, And.intro, Iff.intro, Exists.intro, _private.0.Graph.isNonloopAt_iff_inc_not_isLoopAt.match_1
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
⊢ G.IsLoopAt e x ↔ G.Inc e x ∧ ¬G.IsNonloopAt e x

Tactic:
simp +contextual [isNonloopAt_iff_inc_not_isLoopAt, iff_def, IsLoopAt.inc]

Premises used: Graph.isNonloopAt_iff_inc_not_isLoopAt, iff_def, Graph.IsLoopAt.inc
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.Inc e x
⊢ G.IsLoopAt e x ∨ G.IsNonloopAt e x

Tactic:
simp [isNonloopAt_iff_inc_not_isLoopAt, h, em]

Premises used: em, Graph.isNonloopAt_iff_inc_not_isLoopAt
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
G : Graph α β
h : G.Adj x y
⊢ G.Adj y x

Tactic:
⟨_, h.choose_spec.symm⟩

Premises used: Exists.choose_spec, Graph.Adj, Graph.IsLink.symm, Exists.intro
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
x y : α
⊢ G.Adj x y ↔ G.Adj y x

Tactic:
⟨.symm, .symm⟩

Premises used: Graph.Adj.symm, Iff.intro
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
G : Graph α β
h : G.Adj x y
⊢ x ∈ V(G)

Tactic:
h.choose_spec.left_mem

Premises used: Exists.choose_spec, Graph.IsLink.left_mem
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
G : Graph α β
h : G.Adj x y
⊢ y ∈ V(G)

Tactic:
h.symm.left_mem

Premises used: Graph.Adj.left_mem, Graph.Adj.symm
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
⊢ G.Adj x y

Tactic:
⟨e, h⟩

Premises used: Graph.Adj, Exists.intro
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 H G : Graph α β
E : Set β
hE : ∀ (e : β), e ∈ E ↔ ∃ (x : α) (y : α), G.IsLink e x y
⊢ E = E(G)

Tactic:
simp [Set.ext_iff, hE, G.edge_mem_iff_exists_isLink]

Premises used: Graph.edge_mem_iff_exists_isLink, Set.ext_iff
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 H G : Graph α β
E : Set β
hE : ∀ (e : β), e ∈ E ↔ ∃ (x : α) (y : α), G.IsLink e x y
⊢ ∀ ⦃e : β⦄, e ∈ E → Symmetric (G.IsLink e)

Tactic:
simpa [show E = E(G) by simp [Set.ext_iff, hE, G.edge_mem_iff_exists_isLink]]
      using G.isLink_symm

Premises used: Graph.isLink_symm
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
E : Set β
hE : ∀ (e : β), e ∈ E ↔ ∃ (x : α) (y : α), G.IsLink e x y
⊢ E = E(G)

Tactic:
simp [Set.ext_iff, hE, G.edge_mem_iff_exists_isLink]

Premises used: Graph.edge_mem_iff_exists_isLink, Set.ext_iff
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
E : Set β
hE : ∀ (e : β), e ∈ E ↔ ∃ (x : α) (y : α), G.IsLink e x y
obtain :
  ∀ (hE : ∀ (e : β), e ∈ E(G) ↔ ∃ (x : α) (y : α), G.IsLink e x y),
    { vertexSet := V(G), IsLink := G.IsLink, edgeSet := E(G), isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
        edge_mem_iff_exists_isLink := hE, left_mem_of_isLink := ⋯ : Graph α β } =
      G
⊢ { vertexSet := V(G), IsLink := G.IsLink, edgeSet := E, isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := hE, left_mem_of_isLink := ⋯ : Graph α β } =
    G

Tactic:
obtain rfl : E = E(G) := by simp [Set.ext_iff, hE, G.edge_mem_iff_exists_isLink]

Premises used: rfl