awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
mp : (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr :
  (∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v) → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₁ mp₂ mp₃ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
⊢ (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔ ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
have mpr₁ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
mp : (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr :
  (∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v) → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₁ mp₂ mp₃ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr₁ mpr₂ mpr₃ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₄ mp₅ mp₆ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr₄ mpr₅ mpr₆ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₇ mp₈ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
⊢ (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔ ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
have mp₉ : ∀ (w : α') (w_1 w_2 : α), G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → (∃ (y : α), G.IsLink e w_1 y) ∧ x = f w_1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
mp : (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr :
  (∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v) → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₁ mp₂ mp₃ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr₁ mpr₂ mpr₃ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₄ mp₅ mp₆ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr₄ mpr₅ mpr₆ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₇ mp₈ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mp₉ : ∀ (w : α') (w_1 w_2 : α), G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → (∃ (y : α), G.IsLink e w_1 y) ∧ x = f w_1
⊢ (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔ ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
have mp₁₀ : (w : α') → (w_1 w_2 : α) → G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → α
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
mp : (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr :
  (∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v) → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₁ mp₂ mp₃ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr₁ mpr₂ mpr₃ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₄ mp₅ mp₆ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr₄ mpr₅ mpr₆ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₇ mp₈ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mp₉ : ∀ (w : α') (w_1 w_2 : α), G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → (∃ (y : α), G.IsLink e w_1 y) ∧ x = f w_1
mp₁₀ : (w : α') → (w_1 w_2 : α) → G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → α
mp₁₁ : ∀ (w : α') (w_1 w_2 : α), G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → (∃ (y : α), G.IsLink e w_1 y) ∧ x = f w_1
mp₁₂ : (w : α') → (w_1 w_2 : α) → G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → α
mpr₇ mpr₈ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
⊢ (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔ ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
have mpr₉ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = f w_1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
mp : (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr :
  (∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v) → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₁ mp₂ mp₃ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr₁ mpr₂ mpr₃ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₄ mp₅ mp₆ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr₄ mpr₅ mpr₆ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₇ mp₈ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mp₉ : ∀ (w : α') (w_1 w_2 : α), G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → (∃ (y : α), G.IsLink e w_1 y) ∧ x = f w_1
mp₁₀ : (w : α') → (w_1 w_2 : α) → G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → α
mp₁₁ : ∀ (w : α') (w_1 w_2 : α), G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → (∃ (y : α), G.IsLink e w_1 y) ∧ x = f w_1
mp₁₂ : (w : α') → (w_1 w_2 : α) → G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → α
mpr₇ mpr₈ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mpr₉ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = f w_1
⊢ (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔ ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
have mpr₁₀ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α'
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
mp : (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr :
  (∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v) → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₁ mp₂ mp₃ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr₁ mpr₂ mpr₃ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₄ mp₅ mp₆ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr₄ mpr₅ mpr₆ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₇ mp₈ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mp₉ : ∀ (w : α') (w_1 w_2 : α), G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → (∃ (y : α), G.IsLink e w_1 y) ∧ x = f w_1
mp₁₀ : (w : α') → (w_1 w_2 : α) → G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → α
mp₁₁ : ∀ (w : α') (w_1 w_2 : α), G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → (∃ (y : α), G.IsLink e w_1 y) ∧ x = f w_1
mp₁₂ : (w : α') → (w_1 w_2 : α) → G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → α
mpr₇ mpr₈ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mpr₉ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = f w_1
mpr₁₀ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α'
mpr₁₁ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = f w_1
mpr₁₂ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α'
⊢ (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔ ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
have mpr₁₃ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (b : α), G.IsLink e w b ∧ f w = x ∧ f b = f w_1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
mp : (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr :
  (∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v) → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₁ mp₂ mp₃ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr₁ mpr₂ mpr₃ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₄ mp₅ mp₆ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr₄ mpr₅ mpr₆ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₇ mp₈ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mp₉ : ∀ (w : α') (w_1 w_2 : α), G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → (∃ (y : α), G.IsLink e w_1 y) ∧ x = f w_1
mp₁₀ : (w : α') → (w_1 w_2 : α) → G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → α
mp₁₁ : ∀ (w : α') (w_1 w_2 : α), G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → (∃ (y : α), G.IsLink e w_1 y) ∧ x = f w_1
mp₁₂ : (w : α') → (w_1 w_2 : α) → G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → α
mpr₇ mpr₈ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mpr₉ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = f w_1
mpr₁₀ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α'
mpr₁₁ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = f w_1
mpr₁₂ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α'
mpr₁₃ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (b : α), G.IsLink e w b ∧ f w = x ∧ f b = f w_1
⊢ (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔ ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
have mpr₁₄ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
mp : (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr :
  (∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v) → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₁ mp₂ mp₃ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr₁ mpr₂ mpr₃ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₄ mp₅ mp₆ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr₄ mpr₅ mpr₆ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₇ mp₈ :
  ∀ (w : α') (w_1 w_2 : α),
    G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mp₉ : ∀ (w : α') (w_1 w_2 : α), G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → (∃ (y : α), G.IsLink e w_1 y) ∧ x = f w_1
mp₁₀ : (w : α') → (w_1 w_2 : α) → G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → α
mp₁₁ : ∀ (w : α') (w_1 w_2 : α), G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → (∃ (y : α), G.IsLink e w_1 y) ∧ x = f w_1
mp₁₂ : (w : α') → (w_1 w_2 : α) → G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → α
mpr₇ mpr₈ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mpr₉ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = f w_1
mpr₁₀ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α'
mpr₁₁ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = f w_1
mpr₁₂ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α'
mpr₁₃ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (b : α), G.IsLink e w b ∧ f w = x ∧ f b = f w_1
mpr₁₄ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α
mpr₁₅ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α'
mpr₁₆ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (b : α), G.IsLink e w b ∧ f w = x ∧ f b = f w_1
mpr₁₇ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α
mpr₁₈ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α'
⊢ (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔ ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
have mpr₁₉ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → G.IsLink e w w_1 ∧ f w = x ∧ f w_1 = f w_1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
v : α
e : β
f : α → α'
h : G.Inc e v
⊢ (map f G).Inc e (f v)
have obtain : ∀ (w : α) (hw : G.IsLink e v w), (map f G).Inc e (f v)
Tactic: obtain ⟨w, hw⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
x y : α'
f : α → α'
⊢ (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔
    ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
have mp : (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) →
  ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
x y : α'
f : α → α'
mp :
  (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) →
    ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
⊢ (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔
    ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
have mpr : (∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y) →
  ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
x y : α'
f : α → α'
mp :
  (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) →
    ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mpr :
  (∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y) →
    ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
⊢ (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔
    ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
have mp₁ : ∀ (w : β) (w_1 w_2 : α),
  G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
x y : α'
f : α → α'
mp :
  (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) →
    ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mpr :
  (∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y) →
    ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₁ mp₂ mp₃ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
⊢ (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔
    ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
have mpr₁ : ∀ (w w_1 : α) (w_2 : β),
  G.IsLink w_2 w w_1 → f w = x → f w_1 = y → ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
x y : α'
f : α → α'
mp :
  (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) →
    ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mpr :
  (∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y) →
    ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₁ mp₂ mp₃ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mpr₁ mpr₂ mpr₃ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → f w = x → f w_1 = y → ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₄ mp₅ mp₆ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mpr₄ mpr₅ mpr₆ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → f w = x → f w_1 = y → ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₇ mp₈ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
⊢ (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔
    ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
have mp₉ : ∀ (w : β) (w_1 w_2 : α),
  G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (b : α), (∃ (e : β), G.IsLink e w_1 b) ∧ f w_1 = x ∧ f b = y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
x y : α'
f : α → α'
mp :
  (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) →
    ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mpr :
  (∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y) →
    ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₁ mp₂ mp₃ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mpr₁ mpr₂ mpr₃ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → f w = x → f w_1 = y → ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₄ mp₅ mp₆ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mpr₄ mpr₅ mpr₆ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → f w = x → f w_1 = y → ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₇ mp₈ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mp₉ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (b : α), (∃ (e : β), G.IsLink e w_1 b) ∧ f w_1 = x ∧ f b = y
⊢ (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔
    ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
have mp₁₀ : (w : β) → (w_1 w_2 : α) → G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → α
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
x y : α'
f : α → α'
mp :
  (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) →
    ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mpr :
  (∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y) →
    ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₁ mp₂ mp₃ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mpr₁ mpr₂ mpr₃ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → f w = x → f w_1 = y → ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₄ mp₅ mp₆ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mpr₄ mpr₅ mpr₆ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → f w = x → f w_1 = y → ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₇ mp₈ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mp₉ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (b : α), (∃ (e : β), G.IsLink e w_1 b) ∧ f w_1 = x ∧ f b = y
mp₁₀ : (w : β) → (w_1 w_2 : α) → G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → α
mp₁₁ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (b : α), (∃ (e : β), G.IsLink e w_1 b) ∧ f w_1 = x ∧ f b = y
mp₁₂ : (w : β) → (w_1 w_2 : α) → G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → α
⊢ (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔
    ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
have mp₁₃ : ∀ (w : β) (w_1 w_2 : α),
  G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → (∃ (e : β), G.IsLink e w_1 w_2) ∧ f w_1 = x ∧ f w_2 = y
Tactic: tauto