awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
mp :
  (∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)) →
    ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr :
  (∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)) →
    ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₁ mp₂ mp₃ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
⊢ (∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)) ↔
    ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
have mpr₁ : ∀ (w : β) (w_1 w_2 : α),
  G.IsLink w w_1 w_2 → w_1 ∈ V(H) → w_2 ∉ V(H) → ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
mp :
  (∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)) →
    ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr :
  (∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)) →
    ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₁ mp₂ mp₃ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr₁ mpr₂ mpr₃ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → w_1 ∈ V(H) → w_2 ∉ V(H) → ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₄ mp₅ mp₆ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr₄ mpr₅ mpr₆ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → w_1 ∈ V(H) → w_2 ∉ V(H) → ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₇ mp₈ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
⊢ (∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)) ↔
    ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
have mp₉ : ∀ (w w_1 : α) (w_2 : β),
  G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (x : α) (y : α), G.IsLink w_2 x y ∧ x ∈ V(H) ∧ y ∉ V(H)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
mp :
  (∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)) →
    ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr :
  (∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)) →
    ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₁ mp₂ mp₃ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr₁ mpr₂ mpr₃ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → w_1 ∈ V(H) → w_2 ∉ V(H) → ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₄ mp₅ mp₆ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr₄ mpr₅ mpr₆ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → w_1 ∈ V(H) → w_2 ∉ V(H) → ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₇ mp₈ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₉ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (x : α) (y : α), G.IsLink w_2 x y ∧ x ∈ V(H) ∧ y ∉ V(H)
⊢ (∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)) ↔
    ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
have mp₁₀ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → β
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
mp :
  (∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)) →
    ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr :
  (∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)) →
    ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₁ mp₂ mp₃ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr₁ mpr₂ mpr₃ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → w_1 ∈ V(H) → w_2 ∉ V(H) → ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₄ mp₅ mp₆ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr₄ mpr₅ mpr₆ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → w_1 ∈ V(H) → w_2 ∉ V(H) → ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₇ mp₈ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₉ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (x : α) (y : α), G.IsLink w_2 x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₁₀ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → β
mp₁₁ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (x : α) (y : α), G.IsLink w_2 x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₁₂ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → β
⊢ (∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)) ↔
    ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
have mp₁₃ : ∀ (w w_1 : α) (w_2 : β), G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (y : α), G.IsLink w_2 w y ∧ w ∈ V(H) ∧ y ∉ V(H)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
mp :
  (∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)) →
    ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr :
  (∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)) →
    ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₁ mp₂ mp₃ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr₁ mpr₂ mpr₃ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → w_1 ∈ V(H) → w_2 ∉ V(H) → ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₄ mp₅ mp₆ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr₄ mpr₅ mpr₆ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → w_1 ∈ V(H) → w_2 ∉ V(H) → ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₇ mp₈ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₉ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (x : α) (y : α), G.IsLink w_2 x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₁₀ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → β
mp₁₁ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (x : α) (y : α), G.IsLink w_2 x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₁₂ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → β
mp₁₃ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (y : α), G.IsLink w_2 w y ∧ w ∈ V(H) ∧ y ∉ V(H)
⊢ (∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)) ↔
    ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
have mp₁₄ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → α
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
mp :
  (∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)) →
    ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr :
  (∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)) →
    ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₁ mp₂ mp₃ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr₁ mpr₂ mpr₃ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → w_1 ∈ V(H) → w_2 ∉ V(H) → ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₄ mp₅ mp₆ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr₄ mpr₅ mpr₆ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → w_1 ∈ V(H) → w_2 ∉ V(H) → ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₇ mp₈ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₉ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (x : α) (y : α), G.IsLink w_2 x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₁₀ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → β
mp₁₁ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (x : α) (y : α), G.IsLink w_2 x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₁₂ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → β
mp₁₃ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (y : α), G.IsLink w_2 w y ∧ w ∈ V(H) ∧ y ∉ V(H)
mp₁₄ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → α
mp₁₅ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → β
mp₁₆ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (y : α), G.IsLink w_2 w y ∧ w ∈ V(H) ∧ y ∉ V(H)
mp₁₇ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → α
mp₁₈ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → β
⊢ (∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)) ↔
    ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
have mp₁₉ : ∀ (w w_1 : α) (w_2 : β), G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → G.IsLink w_2 w w_1 ∧ w ∈ V(H) ∧ w_1 ∉ V(H)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
⊢ noEdge ∅ β ≤ G
have vertexSet_mono : autoParam (V(noEdge ∅ β) ⊆ V(G)) IsSubgraph.vertexSet_mono._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
vertexSet_mono : autoParam (V(noEdge ∅ β) ⊆ V(G)) IsSubgraph.vertexSet_mono._autoParam
⊢ noEdge ∅ β ≤ G
have isLink_mono : autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink (noEdge ∅ β) e x y → G.IsLink e x y) IsSubgraph.isLink_mono._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G = ⊥ ∨ V(G).Nonempty
have refine : ∀ (he : V(G) = ∅) (e : β) (x y : α), G.IsLink e x y ↔ IsLink ⊥ e x y
Tactic: refine (em (V(G) = ∅)).elim (fun he ↦ .inl (Graph.ext he fun e x y ↦ ?_)) (Or.inr ∘
    nonempty_iff_ne_empty.mpr)
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
he : V(G) = ∅
e : β
x y : α
⊢ G.IsLink e x y ↔ IsLink ⊥ e x y
have simp : ¬G.IsLink e x y
Tactic: simp only [edgeSet_bot, mem_empty_iff_false, not_false_eq_true, not_isLink_of_notMem_edgeSet,
    iff_false]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ V(G) = ∅ ↔ G = ⊥
have refine : ∀ (h : V(G) = ∅) (e : β) (x y : α) (he : G.IsLink e x y), IsLink ⊥ e x y
Tactic: refine ⟨fun h ↦ bot_le.antisymm' ⟨by simp [h], fun e x y he ↦ ?_⟩, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
G H : Graph α β
h : x ∈ V(G)
h' : x ∈ V(H)
⊢ ¬Disjoint G H
have simp : ∃ (x : Graph α β) (_ : x ≤ G) (_ : x ≤ H), V(x).Nonempty
Tactic: simp only [Disjoint, le_bot_iff, not_forall, ne_eq, ne_bot_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
G H : Graph α β
h : x ∈ V(G)
h' : x ∈ V(H)
⊢ ∃ (x : Graph α β) (_ : x ≤ G) (_ : x ≤ H), V(x).Nonempty
have h₁ : ∃ (_ : noEdge {x} β ≤ G) (_ : noEdge {x} β ≤ H), Set.Nonempty (α := α) V(noEdge {x} β)
Tactic: use noEdge {x} β
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
hlm : (↑l : (x : η → α) → (i : ι) → α) = (↑m : (x : η → α) → (i : ι) → α)
⊢ l = m
have idxFun : ∀ (i : ι), l.idxFun i = m.idxFun i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (hypothesis)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
hlm : (↑l : (x : η → α) → (i : ι) → α) = (↑m : (x : η → α) → (i : ι) → α)
i : ι
⊢ l.idxFun i = m.idxFun i
have hlm₁ : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
Tactic: simp only [funext_iff] at hlm
Cleared hypotheses: hlm
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
a : α
hl : l.idxFun i = Sum.inl a
⊢ Sum.inl a = m.idxFun i
have idxFun : ∀ (b : α) (hba : b ≠ a), Sum.inl a = m.idxFun i
Tactic: obtain ⟨b, hba⟩ := exists_ne a
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
⊢ Sum.inl a = m.idxFun i
have idxFun : ∀ (val : α) (hm : m.idxFun i = Sum.inl val), Eq (α := α ⊕ η) (Sum.inl a) (Sum.inl val)
Tactic: cases hm : idxFun m i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
idxFun : ∀ (val : α) (hm : m.idxFun i = Sum.inl val), Eq (α := α ⊕ η) (Sum.inl a) (Sum.inl val)
⊢ Sum.inl a = m.idxFun i
have idxFun₁ : ∀ (val : η) (hm : m.idxFun i = Sum.inr val), Sum.inl a = Sum.inr val
Tactic: cases hm : idxFun m i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
e : η
hl : l.idxFun i = Sum.inr e
a : α
hm : m.idxFun i = Sum.inl a
⊢ Sum.inr e = Sum.inl a
have idxFun : ∀ (b : α) (hba : b ≠ a), Sum.inr e = Sum.inl a
Tactic: obtain ⟨b, hba⟩ := exists_ne a
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
⊢ Eq (α := α ⊕ η) (Sum.inr e) (Sum.inr f)
have idxFun : ∀ (a b : α) (hab : a ≠ b), Eq (α := α ⊕ η) (Sum.inr e) (Sum.inr f)
Tactic: obtain ⟨a, b, hab⟩ := exists_pair_ne α
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
⊢ Eq (α := α ⊕ η) (Sum.inr e) (Sum.inr f)
have idxFun : e = f
Tactic: simp only [Sum.inr.injEq]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
⊢ e = f
have idxFun : ∀ (hef : e ≠ f), False
Tactic: by_contra! hef
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
e : η
hl : l.idxFun i = Sum.inr e
⊢ Sum.inr e = m.idxFun i
have idxFun : ∀ (x : α ⊕ η) (hm : m.idxFun i = x), Sum.inr e = x
Tactic: cases hm : idxFun m i with
    | inl a =>
      obtain ⟨b, hba⟩ := exists_ne a
      simpa [hl, hm, hba, coe_apply] using hlm (const _ b) i
    | inr f =>
      obtain ⟨a, b, hab⟩ := exists_pair_ne α
      simp only [Sum.inr.injEq]
      by_contra! hef
      simpa [hl, hm, hef, hab, coe_apply] using hlm (Function.update (const _ a) f b) i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
⊢ l.idxFun i = m.idxFun i
have idxFun : ∀ (x : α ⊕ η) (hl : l.idxFun i = x), x = m.idxFun i
Tactic: cases hl : idxFun l i with
  | inl a =>
    obtain ⟨b, hba⟩ := exists_ne a
    cases hm : idxFun m i <;> simpa [hl, hm, hba.symm, coe_apply] using hlm (const _ b) i
  | inr e =>
    cases hm : idxFun m i with
    | inl a =>
      obtain ⟨b, hba⟩ := exists_ne a
      simpa [hl, hm, hba, coe_apply] using hlm (const _ b) i
    | inr f =>
      obtain ⟨a, b, hab⟩ := exists_pair_ne α
      simp only [Sum.inr.injEq]
      by_contra! hef
      simpa [hl, hm, hef, hab, coe_apply] using hlm (Function.update (const _ a) f b) i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
⊢ Injective (α := Subspace η α ι) toFun
have rintro : ∀ ⦃l m : Subspace η α ι⦄ (hlm : (↑l : (x : η → α) → (i : ι) → α) = (↑m : (x : η → α) → (i : ι) → α)), l = m
Tactic: classical
  rintro l m hlm
  ext i
  simp only [funext_iff] at hlm
  cases hl : idxFun l i with
  | inl a =>
    obtain ⟨b, hba⟩ := exists_ne a
    cases hm : idxFun m i <;> simpa [hl, hm, hba.symm, coe_apply] using hlm (const _ b) i
  | inr e =>
    cases hm : idxFun m i with
    | inl a =>
      obtain ⟨b, hba⟩ := exists_ne a
      simpa [hl, hm, hba, coe_apply] using hlm (const _ b) i
    | inr f =>
      obtain ⟨a, b, hab⟩ := exists_pair_ne α
      simp only [Sum.inr.injEq]
      by_contra! hef
      simpa [hl, hm, hef, hab, coe_apply] using hlm (Function.update (const _ a) f b) i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
rintro : ∀ ⦃l m : Subspace η α ι⦄ (hlm : (↑l : (x : η → α) → (i : ι) → α) = (↑m : (x : η → α) → (i : ι) → α)), l = m
⊢ Injective (α := Subspace η α ι) toFun
have idxFun : ∀ ⦃l m : Subspace η α ι⦄ (hlm : (↑l : (x : η → α) → (i : ι) → α) = (↑m : (x : η → α) → (i : ι) → α)) (i : ι),
  l.idxFun i = m.idxFun i
Tactic: classical
  rintro l m hlm
  ext i
  simp only [funext_iff] at hlm
  cases hl : idxFun l i with
  | inl a =>
    obtain ⟨b, hba⟩ := exists_ne a
    cases hm : idxFun m i <;> simpa [hl, hm, hba.symm, coe_apply] using hlm (const _ b) i
  | inr e =>
    cases hm : idxFun m i with
    | inl a =>
      obtain ⟨b, hba⟩ := exists_ne a
      simpa [hl, hm, hba, coe_apply] using hlm (const _ b) i
    | inr f =>
      obtain ⟨a, b, hab⟩ := exists_pair_ne α
      simp only [Sum.inr.injEq]
      by_contra! hef
      simpa [hl, hm, hef, hab, coe_apply] using hlm (Function.update (const _ a) f b) i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
rintro : ∀ ⦃l m : Subspace η α ι⦄ (hlm : (↑l : (x : η → α) → (i : ι) → α) = (↑m : (x : η → α) → (i : ι) → α)), l = m
idxFun :
  ∀ ⦃l m : Subspace η α ι⦄ (hlm : (↑l : (x : η → α) → (i : ι) → α) = (↑m : (x : η → α) → (i : ι) → α)) (i : ι),
    l.idxFun i = m.idxFun i
⊢ Injective (α := Subspace η α ι) toFun
have idxFun₁ : ∀ ⦃l m : Subspace η α ι⦄ (i : ι)
  (hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1),
  l.idxFun i = m.idxFun i
Tactic: classical
  rintro l m hlm
  ext i
  simp only [funext_iff] at hlm
  cases hl : idxFun l i with
  | inl a =>
    obtain ⟨b, hba⟩ := exists_ne a
    cases hm : idxFun m i <;> simpa [hl, hm, hba.symm, coe_apply] using hlm (const _ b) i
  | inr e =>
    cases hm : idxFun m i with
    | inl a =>
      obtain ⟨b, hba⟩ := exists_ne a
      simpa [hl, hm, hba, coe_apply] using hlm (const _ b) i
    | inr f =>
      obtain ⟨a, b, hab⟩ := exists_pair_ne α
      simp only [Sum.inr.injEq]
      by_contra! hef
      simpa [hl, hm, hef, hab, coe_apply] using hlm (Function.update (const _ a) f b) i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η_1 : Type u_1
α_1 : Type u_2
ι_1 : Type u_3
κ_1 : Type u_4
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l_1 : Subspace η α ι
x : η → α
i_1 : ι
a : α
e_1 : η
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
e : η'
i : ι
⊢ l.idxFun i = Sum.inr ((eη.symm : (a : η') → η) e) ↔
    Eq (α := α' ⊕ η')
      (Sum.map (⇑eα : (a : α) → α') (⇑eη : (a : η) → η')
        (l.idxFun ((eι.symm : (a : ι') → ι) ((eι : (a : ι) → ι') i : ι'))))
      (Sum.inr e)
have inl : ∀ (val : α) (h : l.idxFun i = Sum.inl val),
  Eq (α := α ⊕ η) (Sum.inl val : α ⊕ η) (Sum.inr ((eη.symm : (a : η') → η) e) : α ⊕ η) ↔
    Eq (α := α' ⊕ η')
      (Sum.map (⇑eα : (a : α) → α') (⇑eη : (a : η) → η')
        (l.idxFun ((eι.symm : (a : ι') → ι) ((eι : (a : ι) → ι') i : ι'))))
      (Sum.inr e)
Tactic: cases h : idxFun l i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η_1 : Type u_1
α_1 : Type u_2
ι_1 : Type u_3
κ_1 : Type u_4
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l_1 : Subspace η α ι
x : η → α
i_1 : ι
a : α
e_1 : η
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
e : η'
i : ι
inl :
  ∀ (val : α) (h : l.idxFun i = Sum.inl val),
    Eq (α := α ⊕ η) (Sum.inl val : α ⊕ η) (Sum.inr ((eη.symm : (a : η') → η) e) : α ⊕ η) ↔
      Eq (α := α' ⊕ η')
        (Sum.map (⇑eα : (a : α) → α') (⇑eη : (a : η) → η')
          (l.idxFun ((eι.symm : (a : ι') → ι) ((eι : (a : ι) → ι') i : ι'))))
        (Sum.inr e)
⊢ l.idxFun i = Sum.inr ((eη.symm : (a : η') → η) e) ↔
    Eq (α := α' ⊕ η')
      (Sum.map (⇑eα : (a : α) → α') (⇑eη : (a : η) → η')
        (l.idxFun ((eι.symm : (a : ι') → ι) ((eι : (a : ι) → ι') i : ι'))))
      (Sum.inr e)
have inr : ∀ (val : η) (h : l.idxFun i = Sum.inr val),
  Eq (α := α ⊕ η) (Sum.inr val) (Sum.inr ((eη.symm : (a : η') → η) e)) ↔
    Eq (α := α' ⊕ η')
      (Sum.map (⇑eα : (a : α) → α') (⇑eη : (a : η) → η')
        (l.idxFun ((eι.symm : (a : ι') → ι) ((eι : (a : ι) → ι') i : ι'))))
      (Sum.inr e)
Tactic: cases h : idxFun l i