awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop
    (HSub.hSub (α := ℕ → ℝ) (fun (n : ℕ) ↦ -4 * √(Real.log (↑n : ℝ))) fun (n : ℕ) ↦
      -4 * √(Real.log (↑((n - 3) / 6) : ℝ)))
have refine_3 : ∀ᶠ (x : ℝ) in
  Filter.map
    (HSub.hSub (α := ℕ → ℝ) (fun (n : ℕ) ↦ -4 * √(Real.log (↑n : ℝ))) fun (n : ℕ) ↦
      -4 * √(Real.log (↑((n - 3) / 6) : ℝ)))
    atTop,
  (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x 0
Tactic: refine ⟨0, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
⊢ ∀ᶠ (x : ℝ) in
    Filter.map
      (HSub.hSub (α := ℕ → ℝ) (fun (n : ℕ) ↦ -4 * √(Real.log (↑n : ℝ))) fun (n : ℕ) ↦
        -4 * √(Real.log (↑((n - 3) / 6) : ℝ)))
      atTop,
    (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x 0
have refine_3 : ∃ (a : ℕ), ∀ b ≥ a, 4 * √(Real.log (↑((b - 3) / 6) : ℝ)) ≤ 4 * √(Real.log (↑b : ℝ))
Tactic: simp only [neg_mul, eventually_map, Pi.sub_apply, sub_neg_eq_add, neg_add_le_iff_le_add,
        add_zero, eventually_atTop]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
⊢ ∃ (a : ℕ), ∀ b ≥ a, 4 * √(Real.log (↑((b - 3) / 6) : ℝ)) ≤ 4 * √(Real.log (↑b : ℝ))
have refine_3 : ∀ (x : ℕ) (hx : x ≥ 9), 4 * √(Real.log (↑((x - 3) / 6) : ℝ)) ≤ 4 * √(Real.log (↑x : ℝ))
Tactic: refine ⟨9, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
x : ℕ
hx : x ≥ 9
⊢ 4 * √(Real.log (↑((x - 3) / 6) : ℝ)) ≤ 4 * √(Real.log (↑x : ℝ))
have refine_3 : LT.lt (α := ℝ) 0 (↑((x - 3) / 6) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
x : ℕ
hx : x ≥ 9
refine_3 : LT.lt (α := ℝ) 0 (↑((x - 3) / 6) : ℝ)
⊢ 4 * √(Real.log (↑((x - 3) / 6) : ℝ)) ≤ 4 * √(Real.log (↑x : ℝ))
have refine_3₁ : (x - 3) / 6 ≤ x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
x : ℕ
hx : x ≥ 9
⊢ LT.lt (α := ℝ) 0 (↑((x - 3) / 6) : ℝ)
have refine_3 : 6 ≤ x - 3
Tactic: simp
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ))))
    fun (n : ℕ) ↦ (↑(ruzsaSzemerediNumberNat n) : ℝ)
have refine : EventuallyLE (β := ℝ) atTop
  (fun (x : ℕ) ↦
    ‖(HDiv.hDiv (α := ℝ) (↑x : ℝ) 3 - 2) * (↑((x - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((x - 3) / 6) : ℝ)))‖)
  fun (n : ℕ) ↦ (↑(ruzsaSzemerediNumberNat n) : ℝ)
Tactic: refine .of_norm_eventuallyLE ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
⊢ EventuallyLE (β := ℝ) atTop
    (fun (x : ℕ) ↦
      ‖(HDiv.hDiv (α := ℝ) (↑x : ℝ) 3 - 2) * (↑((x - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((x - 3) / 6) : ℝ)))‖)
    fun (n : ℕ) ↦ (↑(ruzsaSzemerediNumberNat n) : ℝ)
have h : ∀ (n : ℕ) (hn : 6 ≤ n),
  ‖(HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))‖ ≤
    (↑(ruzsaSzemerediNumberNat n) : ℝ)
Tactic: filter_upwards [eventually_ge_atTop 6] with n hn
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (hypothesis)
Goal:
n : ℕ
hn : 6 ≤ n
⊢ 0 ≤ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
have hn₁ : LE.le (α := ℝ) 6 (↑n : ℝ)
Tactic: rify at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
n : ℕ
hn : LE.le (α := ℝ) 6 (↑n : ℝ)
⊢ 0 ≤ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
have linarith : HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2 < 0 → 3 / 3 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
n : ℕ
hn : LE.le (α := ℝ) 6 (↑n : ℝ)
linarith : HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2 < 0 → 3 / 3 = 1
⊢ 0 ≤ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
have linarith₁ : HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2 < 0 → HMul.hMul (α := ℝ) 1 3 = 3
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
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
⊢ 0 ≤ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
have linarith₂ : HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2 < 0 → GT.gt (α := ℝ) 3 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
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
⊢ 0 ≤ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
have linarith₃ : HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2 < 0 →
  HSub.hSub (α := ℝ) 6 (↑n : ℝ) + (HMul.hMul (α := ℝ) 1 (↑n : ℝ) - HMul.hMul (α := ℝ) 3 2 - HMul.hMul (α := ℝ) 3 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (hypothesis)
Goal:
n : ℕ
hn : 6 ≤ n
⊢ ‖(HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))‖ ≤
    (↑(ruzsaSzemerediNumberNat n) : ℝ)
have this : 0 ≤ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
Tactic: have : (0 : ℝ) ≤ n / 3 - 2 := by rify at hn; linarith
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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
⊢ y = z
have inl : ∀ (h' : G.IsLink e x y), y = y
Tactic: obtain rfl | rfl := h.right_eq_or_eq h'.symm
Cleared hypotheses: z, h'
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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
⊢ y = z
have inr : ∀ (h : G.IsLink e y y) (h' : G.IsLink e y z), y = z
Tactic: obtain rfl | rfl := h.right_eq_or_eq h'.symm
Cleared hypotheses: x, h, h'
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
y z : α
e : β
G : Graph α β
h : G.IsLink e y y
h' : G.IsLink e y z
⊢ y = z
have inr : ∀ (h h' : G.IsLink e z z), z = z
Tactic: obtain rfl | rfl := h'.right_eq_or_eq h.symm
Cleared hypotheses: y, h, h'
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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'
⊢ x = x' ∧ y = y' ∨ x = y' ∧ y = x'
have inl : ∀ (h' : G.IsLink e x y'), x = x ∧ y = y' ∨ x = y' ∧ y = x
Tactic: obtain rfl | rfl := h.left_eq_or_eq h'
Cleared hypotheses: x', h'
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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
⊢ x = x' ∧ y = y' ∨ x = y' ∧ y = x'
have inr : ∀ (h' : G.IsLink e x' x), x = x' ∧ y = x ∨ x = x ∧ y = x'
Tactic: obtain rfl | rfl := h.left_eq_or_eq h'
Cleared hypotheses: y', h'
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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'
have refine : x = x' ∧ y = y' ∨ x = y' ∧ y = x' → G.IsLink e x' y'
Tactic: refine ⟨h.eq_and_eq_or_eq_and_eq, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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' ↔ s(x, y) = s(x', y')
have rw : x = x' ∧ y = y' ∨ x = y' ∧ y = x' ↔ s(x, y) = s(x', y')
Tactic: rw [h.isLink_iff, Sym2.eq_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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')
⊢ G.IsLink e x' y' ↔ s(x, y) = s(x', y')
have rw₁ : x = x' ∧ y = y' ∨ x = y' ∧ y = x' ↔ x = x' ∧ y = y' ∨ x = y' ∧ y = x'
Tactic: rw [h.isLink_iff, Sym2.eq_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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
have refine : (G.Inc e x ∧ G.Inc e y ∧ ∀ (z : α), G.Inc e z → z = x ∨ z = y) → G.IsLink e x y
Tactic: refine ⟨fun h ↦ ⟨h.inc_left, h.inc_right, fun z h' ↦ h'.eq_or_eq_of_isLink h⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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'
⊢ G.IsLink e x y
have inl : ∀ (hx' : G.IsLink e x' x') (h : ∀ (z : α), G.Inc e z → z = x' ∨ z = y), G.IsLink e x' y
Tactic: obtain rfl | rfl := h _ hx'.inc_right
Cleared hypotheses: x, hx', h
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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
⊢ G.IsLink e x y
have inr : ∀ (h : ∀ (z : α), G.Inc e z → z = x ∨ z = x') (hy' : G.IsLink e x' y'), G.IsLink e x x'
Tactic: obtain rfl | rfl := h _ hx'.inc_right
Cleared hypotheses: y, h, hy'
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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
⊢ G.IsLink e x' y
have inl : ∀ (hy' : G.IsLink e x' y') (h : ∀ (z : α), G.Inc e z → z = x' ∨ z = x'), G.IsLink e x' x'
Tactic: obtain rfl | rfl := hx'.left_eq_or_eq hy'
Cleared hypotheses: y, hy', h
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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'
⊢ G.IsLink e x' y
have inl₁ : ∀ (hy' : G.IsLink e y x'), G.IsLink e x' y
Tactic: obtain rfl | rfl := hx'.left_eq_or_eq hy'
Cleared hypotheses: y', hy'
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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
⊢ x = y ∨ x = z ∨ y = z
have by_contra! : ∀ (hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z), False
Tactic: by_contra! ⟨hxy, hxz, hyz⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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
⊢ False
have obtain : ∀ (x' : α) (hx' : G.IsLink e x x'), False
Tactic: obtain ⟨x', hx'⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (hypothesis)
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'
⊢ False
have hx'₁ : G.IsLink e x y
Tactic: obtain rfl := hy.eq_of_isLink_of_ne_left hx' hxy.symm
Cleared hypotheses: x', hx'
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (hypothesis)
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
⊢ False
have hyz₁ : z ≠ z
Tactic: obtain rfl := hz.eq_of_isLink_of_ne_left hx' hxz.symm
Cleared hypotheses: y, hy, hxy, hyz, hx'
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (hypothesis)
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
⊢ False
have hx'₁ : G.IsLink e x z
Tactic: obtain rfl := hz.eq_of_isLink_of_ne_left hx' hxz.symm
Cleared hypotheses: y, hy, hxy, hyz, hx'
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
⊢ G₁.Inc e = G₂.Inc f ↔ G₁.IsLink e = G₂.IsLink f
have mp : G₁.Inc e = G₂.Inc f → G₁.IsLink e = G₂.IsLink f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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
⊢ G₁.Inc e = G₂.Inc f ↔ G₁.IsLink e = G₂.IsLink f
have mpr : G₁.IsLink e = G₂.IsLink f → G₁.Inc e = G₂.Inc f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.Inc e = G₂.Inc f
⊢ G₁.IsLink e = G₂.IsLink f
have mp : ∀ (x y : α), G₁.IsLink e x y ↔ G₂.IsLink f x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.Inc e = G₂.Inc f
x y : α
⊢ G₁.IsLink e x y ↔ G₂.IsLink f x y
have mp : (G₁.Inc e x ∧ G₁.Inc e y ∧ ∀ (z : α), G₁.Inc e z → z = x ∨ z = y) ↔ G₂.IsLink f x y
Tactic: rw [isLink_iff_inc, isLink_iff_inc, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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
⊢ G₁.IsLink e x y ↔ G₂.IsLink f x y
have 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
Tactic: rw [isLink_iff_inc, isLink_iff_inc, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
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
⊢ G₁.IsLink e x y ↔ G₂.IsLink f x y
have 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
Tactic: rw [isLink_iff_inc, isLink_iff_inc, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLoopAt e x
h' : G.Inc e y
⊢ x = y
have inl : ∀ (h : G.IsLoopAt e y), y = y
Tactic: obtain rfl | rfl := h'.eq_or_eq_of_isLink h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (hypothesis)
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
⊢ False
have hyz₁ : x ≠ x
Tactic: rw [← h.eq_of_inc hy.inc_left, ← h.eq_of_inc hy.inc_right] at hyz
Cleared hypotheses: hyz, hy
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
E : Set β
hE : ∀ (e : β), e ∈ E ↔ ∃ (x : α) (y : α), G.IsLink e x y
⊢ { 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
have obtain : ∀ (hE : ∀ (e : β), e ∈ E(G) ↔ ∃ (x : α) (y : α), G.IsLink e x y),
  { vertexSet := V(G), IsLink := G.IsLink, edgeSet := E(G), isLink_symm := sorry, eq_or_eq_of_isLink_of_isLink := sorry,
      edge_mem_iff_exists_isLink := hE, left_mem_of_isLink := sorry : Graph α β } =
    G
Tactic: obtain rfl : E = E(G) := by simp [Set.ext_iff, hE, G.edge_mem_iff_exists_isLink]
Cleared hypotheses: E, hE
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
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
have mk : ∀ (vertexSet : Set α) (IsLink : β → α → α → Prop) (edgeSet : Set β)
  (isLink_symm : ∀ ⦃e : β⦄, e ∈ edgeSet → Symmetric (IsLink e))
  (eq_or_eq_of_isLink_of_isLink : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w)
  (h : ∀ (e : β), e ∈ edgeSet ↔ ∃ (x : α) (y : α), IsLink e x y)
  (left_mem_of_isLink : ∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink e x y → x ∈ vertexSet)
  (hE :
    ∀ (e : β),
      e ∈
          E({ vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
              eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
              left_mem_of_isLink := left_mem_of_isLink : Graph α β }) ↔
        ∃ (x : α) (y : α),
          { vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
                eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
                left_mem_of_isLink := left_mem_of_isLink : Graph α β }.IsLink
            e x y),
  {
      vertexSet :=
        V({ vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
            eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
            left_mem_of_isLink := left_mem_of_isLink : Graph α β }),
      IsLink :=
        { vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
            eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
            left_mem_of_isLink := left_mem_of_isLink : Graph α β }.IsLink,
      edgeSet :=
        E({ vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
            eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
            left_mem_of_isLink := left_mem_of_isLink : Graph α β }),
      isLink_symm := sorry, eq_or_eq_of_isLink_of_isLink := sorry, edge_mem_iff_exists_isLink := hE, left_mem_of_isLink := sorry :
      Graph α β } =
    { vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
      eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
      left_mem_of_isLink := left_mem_of_isLink }
Tactic: cases G with | _ _ _ _ _ _ h _ => simp
Cleared hypotheses: G, hE
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e 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 := ⋯, left_mem_of_isLink := ⋯ : Graph α β } =
    { vertexSet := V(G₂), IsLink := G₂.IsLink, edgeSet := E(G₂), isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }
have h₁ : V(G₂) = V(G₁)
Tactic: convert! rfl using 2
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
h₁ : V(G₂) = V(G₁)
⊢ { vertexSet := V(G₁), IsLink := G₁.IsLink, edgeSet := E(G₁), isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ : Graph α β } =
    { vertexSet := V(G₂), IsLink := G₂.IsLink, edgeSet := E(G₂), isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }
have h₂ : G₂.IsLink = G₁.IsLink
Tactic: convert! rfl using 2
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
h₁ : V(G₂) = V(G₁)
h₂ : G₂.IsLink = G₁.IsLink
⊢ { vertexSet := V(G₁), IsLink := G₁.IsLink, edgeSet := E(G₁), isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ : Graph α β } =
    { vertexSet := V(G₂), IsLink := G₂.IsLink, edgeSet := E(G₂), isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }
have h₃ : E(G₂) = E(G₁)
Tactic: convert! rfl using 2
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x : α), G₁.Inc e x ↔ G₂.Inc e x
x : β
x_1 x_2 : α
⊢ G₁.IsLink x x_1 x_2 ↔ G₂.IsLink x x_1 x_2
have simp_rw : (G₁.Inc x x_1 ∧ G₁.Inc x x_2 ∧ ∀ (z : α), G₁.Inc x z → z = x_1 ∨ z = x_2) ↔
  G₂.Inc x x_1 ∧ G₂.Inc x x_2 ∧ ∀ (z : α), G₂.Inc x z → z = x_1 ∨ z = x_2
Tactic: simp_rw [isLink_iff_inc, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x_1 y_1 z u v w : α
e_1 f : β
G_1 H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
e : β
he : e ∈ edgeSet
x y : α
⊢ IsLink e x y → IsLink e y x
have simp_rw : G.IsLink e x y → G.IsLink e y x
Tactic: simp_rw [← hIsLink]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w
have simp_rw : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, G.IsLink e x y → G.IsLink e v w → x = v ∨ x = w
Tactic: simp_rw [← hIsLink]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ (e : β), e ∈ edgeSet ↔ ∃ (x : α) (y : α), IsLink e x y
have simp_rw : ∀ (e : β), e ∈ E(G) ↔ ∃ (x : α) (y : α), G.IsLink e x y
Tactic: simp_rw [← hIsLink, ← hedgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink e x y → x ∈ vertexSet
have simp_rw : ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → x ∈ V(G)
Tactic: simp_rw [← hIsLink, ← hvertexSet]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
V : Set α
E : Set β
IsLink : β → α → α → Prop
hV : V(G) = V
hE : E(G) = E
h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ G.copy (vertexSet := V) (edgeSet := E) (IsLink := IsLink) hV hE h_isLink = G
have hV₁ : ∀ (x : α), x ∈ V(G.copy (vertexSet := V) (edgeSet := E) (IsLink := IsLink) hV hE h_isLink) ↔ x ∈ V(G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
V : Set α
E : Set β
IsLink : β → α → α → Prop
hV : V(G) = V
hE : E(G) = E
h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
hV₁ : ∀ (x : α), x ∈ V(G.copy (vertexSet := V) (edgeSet := E) (IsLink := IsLink) hV hE h_isLink) ↔ x ∈ V(G)
⊢ G.copy (vertexSet := V) (edgeSet := E) (IsLink := IsLink) hV hE h_isLink = G
have h : ∀ (e : β) (x y : α),
  (G.copy (vertexSet := V) (edgeSet := E) (IsLink := IsLink) hV hE h_isLink).IsLink e x y ↔ G.IsLink e x y
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hGH : G.Compatible H
heH : e ∈ E(H)
h : G.Inc e x
⊢ H.Inc e x
have obtain : ∀ (y : α) (hy : G.IsLink e x y), H.Inc e x
Tactic: obtain ⟨y, hy⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hGH : G.Compatible H
heH : e ∈ E(H)
h : G.IsNonloopAt e x
⊢ H.IsNonloopAt e x
have obtain : ∀ (y : α) (hne : y ≠ x) (hy : G.IsLink e x y), H.IsNonloopAt e x
Tactic: obtain ⟨y, hne, hy⟩ := h
Cleared hypotheses: h