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 α β
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 → α
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
mp₁₄ 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 → (∃ (e : β), G.IsLink e w_1 w_2) ∧ f w_1 = x ∧ f w_2 = y
mp₁₇ 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
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 → α
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
mp₁₄ 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 → (∃ (e : β), G.IsLink e w_1 w_2) ∧ f w_1 = x ∧ f w_2 = y
mp₁₇ 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 → ∃ (e : β), G.IsLink e w_1 w_2
⊢ (∃ (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 → 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 α β
u v : α
f : α → α'
h : G.Adj u v
⊢ (map f G).Adj (f u) (f v)
have obtain : ∀ (e : β) (h : G.IsLink e u v), (map f G).Adj (f u) (f v)
Tactic: obtain ⟨e, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
β : Type u_4
G : Graph α β
⊢ map id G = G
have hV : ∀ (a : α), a ∈ V(map id G) ↔ a ∈ V(G)
Tactic: ext a b c
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
β : Type u_4
G : Graph α β
hV : ∀ (a : α), a ∈ V(map id G) ↔ a ∈ V(G)
⊢ map id G = G
have h : ∀ (a : β) (b c : α), (map id G).IsLink a b c ↔ G.IsLink a b c
Tactic: ext a b c
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G : Graph α β
f : α → α'
f' : α' → α''
⊢ map f' (map f G) = map (f' ∘ f) G
have hV : ∀ (a : α''), a ∈ V(map f' (map f G)) ↔ a ∈ V(map (f' ∘ f) G)
Tactic: ext a b c
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G : Graph α β
f : α → α'
f' : α' → α''
hV : ∀ (a : α''), a ∈ V(map f' (map f G)) ↔ a ∈ V(map (f' ∘ f) G)
⊢ map f' (map f G) = map (f' ∘ f) G
have h : ∀ (a : β) (b c : α''), (map f' (map f G)).IsLink a b c ↔ (map (f' ∘ f) G).IsLink a b c
Tactic: ext a b c
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
⊢ map f G = map g G
have refine_1 : ∀ (x : β) (x_1 x_2 : α'),
  (map f G).IsLink x x_1 x_2 →
    ∀ (w w_1 : α) (hvw : G.IsLink x w w_1), f w = x_1 → f w_1 = x_2 → (map g G).IsLink x x_1 x_2
Tactic: refine Graph.ext (by grind) fun _ _ _ ↦ ⟨fun ⟨_, _, hvw, _, _⟩ ↦ ?_, fun ⟨_, _, hvw, _, _⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
refine_1 :
  ∀ (x : β) (x_1 x_2 : α'),
    (map f G).IsLink x x_1 x_2 →
      ∀ (w w_1 : α) (hvw : G.IsLink x w w_1), f w = x_1 → f w_1 = x_2 → (map g G).IsLink x x_1 x_2
⊢ map f G = map g G
have refine_2 : ∀ (x : β) (x_1 x_2 : α'),
  (map g G).IsLink x x_1 x_2 →
    ∀ (w w_1 : α) (hvw : G.IsLink x w w_1), g w = x_1 → g w_1 = x_2 → (map f G).IsLink x x_1 x_2
Tactic: refine Graph.ext (by grind) fun _ _ _ ↦ ⟨fun ⟨_, _, hvw, _, _⟩ ↦ ?_, fun ⟨_, _, hvw, _, _⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
e : β
he : e ∈ E(H)
⊢ e ∈ E(G)
have obtain : ∀ (x y : α) (h' : H.IsLink e x y), e ∈ E(G)
Tactic: obtain ⟨x, y, h'⟩ := exists_isLink_of_mem_edgeSet he
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
h : G.IsLink e x y
hHG : H ≤ G
he : e ∈ E(H)
⊢ H.IsLink e x y
have obtain : ∀ (u v : α) (huv : H.IsLink e u v), H.IsLink e x y
Tactic: obtain ⟨u, v, huv⟩ := exists_isLink_of_mem_edgeSet he
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
h : G.IsLink e x y
hHG : H ≤ G
he : e ∈ E(H)
u v : α
huv : H.IsLink e u v
⊢ H.IsLink e x y
have inl : ∀ (h : G.IsLink e u v), H.IsLink e u v
Tactic: obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := (huv.mono hHG).eq_and_eq_or_eq_and_eq h
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
h : G.IsLink e x y
hHG : H ≤ G
he : e ∈ E(H)
u v : α
huv : H.IsLink e u v
inl : ∀ (h : G.IsLink e u v), H.IsLink e u v
⊢ H.IsLink e x y
have inr : ∀ (h : G.IsLink e v u), H.IsLink e v u
Tactic: obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := (huv.mono hHG).eq_and_eq_or_eq_and_eq h
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
⊢ H.IsLink e = G.IsLink e
have h : ∀ (x y : α), H.IsLink e x y ↔ G.IsLink e x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
⊢ H.Inc e = G.Inc e
have h : ∀ (x : α), H.Inc e x ↔ G.Inc e x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
he : e ∈ E(H)
⊢ H.IsLink e x x ↔ G.IsLink e x x
have rw : G.IsLink e x x ↔ G.IsLink e x x
Tactic: rw [hHG.isLink_iff he]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
⊢ H.IsLoopAt e = G.IsLoopAt e
have h : ∀ (x : α), H.IsLoopAt e x ↔ G.IsLoopAt e x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
h : H.IsNonloopAt e x
⊢ G.IsNonloopAt e x
have obtain : ∀ (y : α) (hxy : y ≠ x) (he : H.IsLink e x y), G.IsNonloopAt e x
Tactic: obtain ⟨y, hxy, he⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
⊢ H.IsNonloopAt e = G.IsNonloopAt e
have h : ∀ (x : α), H.IsNonloopAt e x ↔ G.IsNonloopAt e x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
H₁ H₂ : Graph α β
hH : H₁.Compatible H₂
⊢ H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) ↔ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
have mp : H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
H₁ H₂ : Graph α β
hH : H₁.Compatible H₂
mp : H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
⊢ H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) ↔ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
have mpr : V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
H₁ H₂ : Graph α β
hH : H₁.Compatible H₂
mp : H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mpr : V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
⊢ H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) ↔ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
have mp₁ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
H₁ H₂ : Graph α β
hH : H₁.Compatible H₂
mp : H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mpr : V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mp₁ mp₂ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
⊢ H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) ↔ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
have mp₃ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
H₁ H₂ : Graph α β
hH : H₁.Compatible H₂
mp : H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mpr : V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mp₁ mp₂ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mp₃ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂)
⊢ H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) ↔ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
have mp₄ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → E(H₁) ⊆ E(H₂)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
H₁ H₂ : Graph α β
hH : H₁.Compatible H₂
mp : H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mpr : V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mp₁ mp₂ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mp₃ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂)
mp₄ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → E(H₁) ⊆ E(H₂)
⊢ H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) ↔ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
have mpr₁ : V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
H₁ H₂ : Graph α β
hH : H₁.Compatible H₂
mp : H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mpr : V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mp₁ mp₂ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mp₃ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂)
mp₄ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → E(H₁) ⊆ E(H₂)
mpr₁ mpr₂ : V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
⊢ H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) ↔ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
have mpr₃ : V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → H₁.Compatible H₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
H₁ H₂ : Graph α β
hH : H₁.Compatible H₂
mp : H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mpr : V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mp₁ mp₂ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mp₃ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂)
mp₄ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → E(H₁) ⊆ E(H₂)
mpr₁ mpr₂ : V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mpr₃ : V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → H₁.Compatible H₂
⊢ H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) ↔ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
have mpr₄ : V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
H₁ H₂ : Graph α β
hH : H₁.Compatible H₂
mp : H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mpr : V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mp₁ mp₂ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mp₃ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂)
mp₄ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → E(H₁) ⊆ E(H₂)
mpr₁ mpr₂ : V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mpr₃ : V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → H₁.Compatible H₂
mpr₄ : V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂)
⊢ H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) ↔ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
have mpr₅ : V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → E(H₁) ⊆ E(H₂)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (hypothesis)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hGH : G < H
⊢ V(G) ⊂ V(H) ∨ E(G) ⊂ E(H)
have hGH₁ : G ≤ H ∧ G ≠ H
Tactic: rw [lt_iff_le_and_ne] at hGH
Cleared hypotheses: hGH
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hGH : G ≤ H ∧ G ≠ H
⊢ V(G) ⊂ V(H) ∨ E(G) ⊂ E(H)
have simp : ¬V(G) = V(H) ∨ ¬E(G) = E(H)
Tactic: simp only [ssubset_iff_subset_ne, hGH.1.vertexSet_mono, ne_eq, true_and, hGH.1.edgeSet_mono]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hGH : G ≤ H ∧ G ≠ H
⊢ ¬V(G) = V(H) ∨ ¬E(G) = E(H)
have by_contra! : ∀ (heq : V(G) = V(H) ∧ E(G) = E(H)), False
Tactic: by_contra! heq
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H K : Graph α β
h' : K ≤ G
hsu : V(K) ⊆ V(H)
h : H ≤i G
⊢ K ≤ H
have refine : ∀ (e : β) (he : e ∈ E(K)), e ∈ E(H)
Tactic: refine (Compatible.of_le_le h' h.le).le_iff.mpr ⟨hsu, fun e he ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H K : Graph α β
h' : K ≤ G
hsu : V(K) ⊆ V(H)
h : H ≤i G
e : β
he : e ∈ E(K)
⊢ e ∈ E(H)
have obtain : ∀ (u v : α) (huv : K.IsLink e u v), e ∈ E(H)
Tactic: obtain ⟨u, v, huv⟩ := K.exists_isLink_of_mem_edgeSet he
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hV : V(H) = V(G)
h : H ≤i G
e : β
he : e ∈ E(G)
⊢ e ∈ E(H)
have obtain : ∀ (w w_1 : α) (hxy : G.IsLink e w w_1), e ∈ E(H)
Tactic: obtain ⟨_, _, hxy⟩ := G.exists_isLink_of_mem_edgeSet he
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ ¬H ≤i G ↔ ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∈ V(H) ∧ e ∉ E(H)
have contrapose! : H ≤i G ↔ ∀ (e : β) (x y : α) (_ : G.IsLink e x y) (_ : x ∈ V(H)) (_ : y ∈ V(H)), e ∈ E(H)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ H ≤i G ↔ ∀ (e : β) (x y : α) (_ : G.IsLink e x y) (_ : x ∈ V(H)) (_ : y ∈ V(H)), e ∈ E(H)
have symm : (∀ (e : β) (x y : α) (_ : G.IsLink e x y) (_ : x ∈ V(H)) (_ : y ∈ V(H)), e ∈ E(H)) ↔ H ≤i G
Tactic: symm
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
⊢ x ∈ V(H) ↔ y ∈ V(H)
have refine_1 : ∀ (hin : x ∈ V(H)), y ∈ V(H)
Tactic: refine ⟨fun hin ↦ ?_, fun hin ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
refine_1 : ∀ (hin : x ∈ V(H)), y ∈ V(H)
⊢ x ∈ V(H) ↔ y ∈ V(H)
have refine_2 : ∀ (hin : y ∈ V(H)), x ∈ V(H)
Tactic: refine ⟨fun hin ↦ ?_, fun hin ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (hypothesis)
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
hin : y ∈ V(H)
⊢ x ∈ V(H)
have he₁ : G.IsLink e y x
Tactic: rw [isLink_comm] at he
Cleared hypotheses: he, hHG, hin
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (hypothesis)
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
hin : y ∈ V(H)
⊢ x ∈ V(H)
have he₁ : G.IsLink e y x
Tactic: on_goal 2 => rw [isLink_comm] at he
Cleared hypotheses: he, hHG, hin
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (hypothesis)
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
hin : x ∈ V(H)
⊢ y ∈ V(H)
have he₁ : H.IsLink e x y
Tactic: rw [← hHG.isLink_congr hin] at he
Cleared hypotheses: he, hHG, hin
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (hypothesis)
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e y x
hHG : H ≤c G
hin : y ∈ V(H)
⊢ x ∈ V(H)
have he₁ : H.IsLink e y x
Tactic: rw [← hHG.isLink_congr hin] at he
Cleared hypotheses: he, hHG, hin
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (hypothesis)
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
⊢ [x ∈ V(H), y ∈ V(H), e ∈ E(H)].TFAE
have tfae_1_to_2 : ∀ (a : x ∈ V(H)), y ∈ V(H)
Tactic: tfae_have 1 → 2 := (hHG.mem_iff_of_isLink he).mp
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (hypothesis)
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
tfae_1_to_2 : ∀ (a : x ∈ V(H)), y ∈ V(H)
⊢ [x ∈ V(H), y ∈ V(H), e ∈ E(H)].TFAE
have tfae_2_to_3 : ∀ (a : y ∈ V(H)), e ∈ E(H)
Tactic: tfae_have 2 → 3 := (hHG.isLink_congr · |>.mpr he.symm |>.edge_mem)
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (hypothesis)
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
tfae_1_to_2 : ∀ (a : x ∈ V(H)), y ∈ V(H)
tfae_2_to_3 : ∀ (a : y ∈ V(H)), e ∈ E(H)
⊢ [x ∈ V(H), y ∈ V(H), e ∈ E(H)].TFAE
have tfae_3_to_1 : ∀ (a : e ∈ E(H)), x ∈ V(H)
Tactic: tfae_have 3 → 1 := (he.anti_of_mem hHG.le · |>.left_mem)
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
⊢ ¬H ≤c G ↔ ∃ (x : α) (y : α), G.Adj x y ∧ x ∈ V(H) ∧ y ∉ V(H)
have contrapose! : H ≤c G ↔ ∀ (x y : α) (_ : G.Adj x y) (_ : x ∈ V(H)), y ∈ V(H)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
⊢ H ≤c G ↔ ∀ (x y : α) (_ : G.Adj x y) (_ : x ∈ V(H)), y ∈ V(H)
have symm : (∀ (x y : α) (_ : G.Adj x y) (_ : x ∈ V(H)), y ∈ V(H)) ↔ H ≤c G
Tactic: symm
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
⊢ ¬H ≤c G ↔ ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
have rw : (∃ (x : α) (y : α), G.Adj x y ∧ x ∈ V(H) ∧ y ∉ V(H)) ↔ ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
Tactic: rw [hHG.not_isClosedSubgraph_iff_exists_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
⊢ (∃ (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 : (∃ (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)
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)
⊢ (∃ (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 : (∃ (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)
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)
⊢ (∃ (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) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
Tactic: tauto