awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
map_rel_iff' :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
          a)
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
          b) ↔
      A'.coe.Adj a b
map_rel_iff'₁ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
          ((f.toHom : (a : α) → β) (↑a : α)) ⋯)
        (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
          ((f.toHom : (a : α) → β) (↑b : α)) ⋯) ↔
      A'.coe.Adj a b
⊢ ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          a)
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          b) ↔
      A'.coe.Adj a b
have map_rel_iff'₂ : ∀ {a b : (↑A'.verts : Type u_4)},
  (Subgraph.map f.toHom A').Adj ((f.toHom : (a : α) → β) (↑a : α)) ((f.toHom : (a : α) → β) (↑b : α)) ↔
    A'.Adj (↑a : α) (↑b : α)
Tactic: simp_rw [Subgraph.map_verts, Equiv.Set.image_apply, Subgraph.coe_adj, Subgraph.map_adj,
    Relation.map_apply, f.injective.eq_iff, exists_eq_right_right, exists_eq_right, forall_true_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
map_rel_iff' :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
          a)
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
          b) ↔
      A'.coe.Adj a b
map_rel_iff'₁ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
          ((f.toHom : (a : α) → β) (↑a : α)) ⋯)
        (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
          ((f.toHom : (a : α) → β) (↑b : α)) ⋯) ↔
      A'.coe.Adj a b
map_rel_iff'₂ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').Adj ((f.toHom : (a : α) → β) (↑a : α)) ((f.toHom : (a : α) → β) (↑b : α)) ↔
      A'.Adj (↑a : α) (↑b : α)
⊢ ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          a)
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          b) ↔
      A'.coe.Adj a b
have map_rel_iff'₃ : ∀ {a b : (↑A'.verts : Type u_4)},
  Relation.Map.{u_4 + 1, u_4 + 1, u_5 + 1, u_5 + 1} (γ := β) (δ := β) A'.Adj ((⇑f.toHom : (a : α) → β) : (a : α) → β)
      ((⇑f.toHom : (a : α) → β) : (a : α) → β) ((f.toHom : (a : α) → β) (↑a : α) : β)
      ((f.toHom : (a : α) → β) (↑b : α) : β) ↔
    A'.Adj (↑a : α) (↑b : α)
Tactic: simp_rw [Subgraph.map_verts, Equiv.Set.image_apply, Subgraph.coe_adj, Subgraph.map_adj,
    Relation.map_apply, f.injective.eq_iff, exists_eq_right_right, exists_eq_right, forall_true_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
map_rel_iff' :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
          a)
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
          b) ↔
      A'.coe.Adj a b
map_rel_iff'₁ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
          ((f.toHom : (a : α) → β) (↑a : α)) ⋯)
        (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
          ((f.toHom : (a : α) → β) (↑b : α)) ⋯) ↔
      A'.coe.Adj a b
map_rel_iff'₂ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').Adj ((f.toHom : (a : α) → β) (↑a : α)) ((f.toHom : (a : α) → β) (↑b : α)) ↔
      A'.Adj (↑a : α) (↑b : α)
map_rel_iff'₃ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    Relation.Map.{u_4 + 1, u_4 + 1, u_5 + 1, u_5 + 1} (γ := β) (δ := β) A'.Adj ((⇑f.toHom : (a : α) → β) : (a : α) → β)
        ((⇑f.toHom : (a : α) → β) : (a : α) → β) ((f.toHom : (a : α) → β) (↑a : α) : β)
        ((f.toHom : (a : α) → β) (↑b : α) : β) ↔
      A'.Adj (↑a : α) (↑b : α)
⊢ ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          a)
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          b) ↔
      A'.coe.Adj a b
have map_rel_iff'₄ : ∀ {a b : (↑A'.verts : Type u_4)},
  (∃ (a_1 : α) (b_1 : α),
      A'.Adj a_1 b_1 ∧
        Eq.{u_5 + 1} (α := β) ((f.toHom : (a : α) → β) a_1 : β) ((f.toHom : (a : α) → β) (↑a : α) : β) ∧
          Eq.{u_5 + 1} (α := β) ((f.toHom : (a : α) → β) b_1 : β) ((f.toHom : (a : α) → β) (↑b : α) : β)) ↔
    A'.Adj (↑a : α) (↑b : α)
Tactic: simp_rw [Subgraph.map_verts, Equiv.Set.image_apply, Subgraph.coe_adj, Subgraph.map_adj,
    Relation.map_apply, f.injective.eq_iff, exists_eq_right_right, exists_eq_right, forall_true_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
map_rel_iff' :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
          a)
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
          b) ↔
      A'.coe.Adj a b
map_rel_iff'₁ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
          ((f.toHom : (a : α) → β) (↑a : α)) ⋯)
        (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
          ((f.toHom : (a : α) → β) (↑b : α)) ⋯) ↔
      A'.coe.Adj a b
map_rel_iff'₂ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').Adj ((f.toHom : (a : α) → β) (↑a : α)) ((f.toHom : (a : α) → β) (↑b : α)) ↔
      A'.Adj (↑a : α) (↑b : α)
map_rel_iff'₃ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    Relation.Map.{u_4 + 1, u_4 + 1, u_5 + 1, u_5 + 1} (γ := β) (δ := β) A'.Adj ((⇑f.toHom : (a : α) → β) : (a : α) → β)
        ((⇑f.toHom : (a : α) → β) : (a : α) → β) ((f.toHom : (a : α) → β) (↑a : α) : β)
        ((f.toHom : (a : α) → β) (↑b : α) : β) ↔
      A'.Adj (↑a : α) (↑b : α)
map_rel_iff'₄ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (∃ (a_1 : α) (b_1 : α),
        A'.Adj a_1 b_1 ∧
          Eq.{u_5 + 1} (α := β) ((f.toHom : (a : α) → β) a_1 : β) ((f.toHom : (a : α) → β) (↑a : α) : β) ∧
            Eq.{u_5 + 1} (α := β) ((f.toHom : (a : α) → β) b_1 : β) ((f.toHom : (a : α) → β) (↑b : α) : β)) ↔
      A'.Adj (↑a : α) (↑b : α)
⊢ ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          a)
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          b) ↔
      A'.coe.Adj a b
have map_rel_iff'₅ : ∀ {a b : (↑A'.verts : Type u_4)},
  (∃ (a_1 : α) (b_1 : α), A'.Adj a_1 b_1 ∧ a_1 = (↑a : α) ∧ b_1 = (↑b : α)) ↔ A'.Adj (↑a : α) (↑b : α)
Tactic: simp_rw [Subgraph.map_verts, Equiv.Set.image_apply, Subgraph.coe_adj, Subgraph.map_adj,
    Relation.map_apply, f.injective.eq_iff, exists_eq_right_right, exists_eq_right, forall_true_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
map_rel_iff' :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
          a)
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
          b) ↔
      A'.coe.Adj a b
map_rel_iff'₁ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
          ((f.toHom : (a : α) → β) (↑a : α)) ⋯)
        (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
          ((f.toHom : (a : α) → β) (↑b : α)) ⋯) ↔
      A'.coe.Adj a b
map_rel_iff'₂ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').Adj ((f.toHom : (a : α) → β) (↑a : α)) ((f.toHom : (a : α) → β) (↑b : α)) ↔
      A'.Adj (↑a : α) (↑b : α)
map_rel_iff'₃ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    Relation.Map.{u_4 + 1, u_4 + 1, u_5 + 1, u_5 + 1} (γ := β) (δ := β) A'.Adj ((⇑f.toHom : (a : α) → β) : (a : α) → β)
        ((⇑f.toHom : (a : α) → β) : (a : α) → β) ((f.toHom : (a : α) → β) (↑a : α) : β)
        ((f.toHom : (a : α) → β) (↑b : α) : β) ↔
      A'.Adj (↑a : α) (↑b : α)
map_rel_iff'₄ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (∃ (a_1 : α) (b_1 : α),
        A'.Adj a_1 b_1 ∧
          Eq.{u_5 + 1} (α := β) ((f.toHom : (a : α) → β) a_1 : β) ((f.toHom : (a : α) → β) (↑a : α) : β) ∧
            Eq.{u_5 + 1} (α := β) ((f.toHom : (a : α) → β) b_1 : β) ((f.toHom : (a : α) → β) (↑b : α) : β)) ↔
      A'.Adj (↑a : α) (↑b : α)
map_rel_iff'₅ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (∃ (a_1 : α) (b_1 : α), A'.Adj a_1 b_1 ∧ a_1 = (↑a : α) ∧ b_1 = (↑b : α)) ↔ A'.Adj (↑a : α) (↑b : α)
⊢ ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          a)
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          b) ↔
      A'.coe.Adj a b
have map_rel_iff'₆ : ∀ {a b : (↑A'.verts : Type u_4)}, (∃ (a_1 : α), A'.Adj a_1 (↑b : α) ∧ a_1 = (↑a : α)) ↔ A'.Adj (↑a : α) (↑b : α)
Tactic: simp_rw [Subgraph.map_verts, Equiv.Set.image_apply, Subgraph.coe_adj, Subgraph.map_adj,
    Relation.map_apply, f.injective.eq_iff, exists_eq_right_right, exists_eq_right, forall_true_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
map_rel_iff' :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
          a)
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
          b) ↔
      A'.coe.Adj a b
map_rel_iff'₁ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
          ((f.toHom : (a : α) → β) (↑a : α)) ⋯)
        (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
          ((f.toHom : (a : α) → β) (↑b : α)) ⋯) ↔
      A'.coe.Adj a b
map_rel_iff'₂ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').Adj ((f.toHom : (a : α) → β) (↑a : α)) ((f.toHom : (a : α) → β) (↑b : α)) ↔
      A'.Adj (↑a : α) (↑b : α)
map_rel_iff'₃ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    Relation.Map.{u_4 + 1, u_4 + 1, u_5 + 1, u_5 + 1} (γ := β) (δ := β) A'.Adj ((⇑f.toHom : (a : α) → β) : (a : α) → β)
        ((⇑f.toHom : (a : α) → β) : (a : α) → β) ((f.toHom : (a : α) → β) (↑a : α) : β)
        ((f.toHom : (a : α) → β) (↑b : α) : β) ↔
      A'.Adj (↑a : α) (↑b : α)
map_rel_iff'₄ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (∃ (a_1 : α) (b_1 : α),
        A'.Adj a_1 b_1 ∧
          Eq.{u_5 + 1} (α := β) ((f.toHom : (a : α) → β) a_1 : β) ((f.toHom : (a : α) → β) (↑a : α) : β) ∧
            Eq.{u_5 + 1} (α := β) ((f.toHom : (a : α) → β) b_1 : β) ((f.toHom : (a : α) → β) (↑b : α) : β)) ↔
      A'.Adj (↑a : α) (↑b : α)
map_rel_iff'₅ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (∃ (a_1 : α) (b_1 : α), A'.Adj a_1 b_1 ∧ a_1 = (↑a : α) ∧ b_1 = (↑b : α)) ↔ A'.Adj (↑a : α) (↑b : α)
map_rel_iff'₆ :
  ∀ {a b : (↑A'.verts : Type u_4)}, (∃ (a_1 : α), A'.Adj a_1 (↑b : α) ∧ a_1 = (↑a : α)) ↔ A'.Adj (↑a : α) (↑b : α)
⊢ ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          a)
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          b) ↔
      A'.coe.Adj a b
have map_rel_iff'₇ : ∀ {a b : (↑A'.verts : Type u_4)}, True
Tactic: simp_rw [Subgraph.map_verts, Equiv.Set.image_apply, Subgraph.coe_adj, Subgraph.map_adj,
    Relation.map_apply, f.injective.eq_iff, exists_eq_right_right, exists_eq_right, forall_true_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
⊢ Eq.{u_5 + 1} (α := Set B.Subgraph) (Set.range (ι := A.Copy B) toSubgraph) {B' : B.Subgraph | Nonempty (A ≃g B'.coe)}
have h : ∀ (H' : B.Subgraph),
  Membership.mem (γ := Set B.Subgraph) (Set.range (ι := A.Copy B) toSubgraph) H' ↔
    Membership.mem (γ := Set B.Subgraph) {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} H'
Tactic: ext H'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
⊢ Membership.mem (γ := Set B.Subgraph) (Set.range (ι := A.Copy B) toSubgraph) H' ↔
    Membership.mem (γ := Set B.Subgraph) {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} H'
have h : Membership.mem (γ := Set B.Subgraph) (Set.range (ι := A.Copy B) toSubgraph) H' →
  Membership.mem (γ := Set B.Subgraph) {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} H'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
h :
  Membership.mem (γ := Set B.Subgraph) (Set.range (ι := A.Copy B) toSubgraph) H' →
    Membership.mem (γ := Set B.Subgraph) {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} H'
⊢ Membership.mem (γ := Set B.Subgraph) (Set.range (ι := A.Copy B) toSubgraph) H' ↔
    Membership.mem (γ := Set B.Subgraph) {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} H'
have h₁ : Membership.mem (γ := Set B.Subgraph) {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} H' →
  Membership.mem (γ := Set B.Subgraph) (Set.range (ι := A.Copy B) toSubgraph) H'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
e : A ≃g H'.coe
⊢ Membership.mem (γ := Set B.Subgraph) (Set.range (ι := A.Copy B) toSubgraph) H'
have h : { toHom := H'.hom.comp e.toHom, injective' := sorry : A.Copy B }.toSubgraph = H'
Tactic: refine ⟨⟨H'.hom.comp e.toHom, Subgraph.hom_injective.comp e.injective⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
⊢ G.maxDegree ≤ H.maxDegree
have inl : IsEmpty V → G.maxDegree ≤ H.maxDegree
Tactic: cases isEmpty_or_nonempty V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
inl : IsEmpty V → G.maxDegree ≤ H.maxDegree
⊢ G.maxDegree ≤ H.maxDegree
have inr : Nonempty V → G.maxDegree ≤ H.maxDegree
Tactic: cases isEmpty_or_nonempty V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
h : Nonempty V
⊢ G.maxDegree ≤ H.maxDegree
have inr : ∀ (v : V) (h : G.maxDegree = G.degree v), G.maxDegree ≤ H.maxDegree
Tactic: obtain ⟨v, h⟩ := exists_maximal_degree_vertex G
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
h : G ⊑ H
⊢ G.maxDegree ≤ H.maxDegree
have have : ∀ (f : G.Copy H), G.maxDegree ≤ H.maxDegree
Tactic: have ⟨f⟩ := h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
⊢ G.minDegree ≤ H.minDegree
have inl : IsEmpty W → G.minDegree ≤ H.minDegree
Tactic: cases isEmpty_or_nonempty W
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
inl : IsEmpty W → G.minDegree ≤ H.minDegree
⊢ G.minDegree ≤ H.minDegree
have inr : Nonempty W → G.minDegree ≤ H.minDegree
Tactic: cases isEmpty_or_nonempty W
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
h : Nonempty W
⊢ G.minDegree ≤ H.minDegree
have inr : ∀ (w : W), G.minDegree ≤ H.degree w
Tactic: refine H.le_minDegree_of_forall_le_degree _ fun w ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
h : Nonempty W
w : W
⊢ G.minDegree ≤ H.degree w
have inr : ∀ (v : V), G.minDegree ≤ H.degree ((f : (a : V) → W) v)
Tactic: obtain ⟨v, rfl⟩ := hf w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
h : Nonempty W
v : V
⊢ G.minDegree ≤ H.degree ((f : (a : V) → W) v)
have inr : G.minDegree ≤ G.degree v
Tactic: grw [← f.degree_le, ← minDegree_le_degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
h : Nonempty W
v : V
inr : G.minDegree ≤ G.degree v
⊢ G.minDegree ≤ H.degree ((f : (a : V) → W) v)
have inr₁ : G.minDegree ≤ G.minDegree
Tactic: grw [← f.degree_le, ← minDegree_le_degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (hypothesis)
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
h : A ≠ ⊥
⊢ Free.{u_4, u_5} (β := β) A ⊥
have h₁ : A.edgeSet.Nonempty
Tactic: rw [← edgeSet_nonempty] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
h : A.edgeSet.Nonempty
f : Hom.{u_4, u_5} (W := β) A ⊥
hf : Injective.{u_4 + 1, u_5 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ False
have absurd : Sym2.map (⇑f : (a : α) → β) (Exists.choose (p := Membership.mem A.edgeSet) h) ∉ edgeSet ⊥
Tactic: absurd f.map_mem_edgeSet h.choose_spec
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
h : A.edgeSet.Nonempty
f : Hom.{u_4, u_5} (W := β) A ⊥
hf : Injective.{u_4 + 1, u_5 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ Sym2.map (⇑f : (a : α) → β) (Exists.choose (p := Membership.mem A.edgeSet) h) ∉ edgeSet ⊥
have rw : Sym2.map (⇑f : (a : α) → β) (Exists.choose (p := Membership.mem A.edgeSet) h) ∉ ∅
Tactic: rw [edgeSet_bot]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ G ⊴ H ↔ ∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced
have mp : G ⊴ H → ∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
mp : G ⊴ H → ∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced
⊢ G ⊴ H ↔ ∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced
have mpr : (∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced) → G ⊴ H
Tactic: constructor