awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ ∃ s' ⊆ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V),
    ∃ (hu' : u ∈ s') (hv' : v ∈ s'),
      (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') u hu')
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hv')
have refine_2 : {x : V | x ∈ (Nonempty.some sorry).support} ⊆ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some sorry).support.toFinset) : Set V)
Tactic: refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
refine_2 :
  {x : V | x ∈ (Nonempty.some ⋯).support} ⊆ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V)
⊢ ∃ s' ⊆ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V),
    ∃ (hu' : u ∈ s') (hv' : v ∈ s'),
      (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') u hu')
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hv')
have refine_2₁ : ∃ (hu' : Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some sorry).support} u) (hv' :
  Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some sorry).support} v),
  Reachable (induce {x : V | x ∈ (Nonempty.some sorry).support} G)
    (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some sorry).support} x) u hu')
    (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some sorry).support} x) v hv')
Tactic: refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ {x : V | x ∈ (Nonempty.some ⋯).support} ⊆ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V)
have refine_2 : Subset.{u} (α := Set V) {x : V | x ∈ (Nonempty.some sorry).support} (⋃ x ∈ t, {a : V | a ∈ (Nonempty.some sorry).support})
Tactic: simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ ∃ (hu' : Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some ⋯).support} u) (hv' :
    Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some ⋯).support} v),
    Reachable (induce {x : V | x ∈ (Nonempty.some ⋯).support} G)
      (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some ⋯).support} x) u hu')
      (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some ⋯).support} x) v hv')
have refine_2 : ∃ (h : v ∈ (Nonempty.some sorry).support),
  Reachable (induce {x : V | x ∈ (Nonempty.some sorry).support} G)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (Nonempty.some sorry).support) u sorry)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (Nonempty.some sorry).support) v sorry)
Tactic: simp only [Set.mem_setOf_eq, Walk.start_mem_support, exists_true_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
tn : t.Nonempty
⊢ ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t' : Set V) G).Connected
have obtain : ∀ (u : V) (ut : u ∈ t), ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t' : Set V) G).Connected
Tactic: classical
  obtain ⟨u, ut⟩ := tn
  refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩
  · simp only [Finset.mem_biUnion, List.mem_toFinset]
    exact ⟨v, vt, Walk.end_mem_support _⟩
  · apply G.induce_connected_of_patches u
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset, Set.mem_iUnion,
                 Set.mem_setOf_eq, Walk.start_mem_support, exists_prop, and_true]
      exact ⟨u, ut⟩
    intro v hv
    simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset] at hv
    obtain ⟨w, wt, hw⟩ := hv
    refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]
      exact fun x xw => Set.mem_iUnion₂.mpr ⟨w, wt, xw⟩
    · simp only [Set.mem_setOf_eq, Walk.start_mem_support, exists_true_left]
      refine ⟨hw, Walk.connected_induce_support _ _ _⟩
Cleared hypotheses: tn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
tn : t.Nonempty
obtain : ∀ (u : V) (ut : u ∈ t), ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t' : Set V) G).Connected
⊢ ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t' : Set V) G).Connected
have refine_1 : ∀ (u : V) (ut : u ∈ t) (v : V) (vt : v ∈ t),
  Membership.mem (γ := Finset V) (t.biUnion fun (v : V) ↦ (Nonempty.some sorry).support.toFinset) v
Tactic: classical
  obtain ⟨u, ut⟩ := tn
  refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩
  · simp only [Finset.mem_biUnion, List.mem_toFinset]
    exact ⟨v, vt, Walk.end_mem_support _⟩
  · apply G.induce_connected_of_patches u
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset, Set.mem_iUnion,
                 Set.mem_setOf_eq, Walk.start_mem_support, exists_prop, and_true]
      exact ⟨u, ut⟩
    intro v hv
    simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset] at hv
    obtain ⟨w, wt, hw⟩ := hv
    refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]
      exact fun x xw => Set.mem_iUnion₂.mpr ⟨w, wt, xw⟩
    · simp only [Set.mem_setOf_eq, Walk.start_mem_support, exists_true_left]
      refine ⟨hw, Walk.connected_induce_support _ _ _⟩
Cleared hypotheses: tn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
tn : t.Nonempty
obtain : ∀ (u : V) (ut : u ∈ t), ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t' : Set V) G).Connected
refine_1 :
  ∀ (u : V) (ut : u ∈ t) (v : V) (vt : v ∈ t),
    Membership.mem (γ := Finset V) (t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) v
⊢ ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t' : Set V) G).Connected
have refine_2 : ∀ (u : V) (ut : u ∈ t), (induce (↑(t.biUnion fun (v : V) ↦ (Nonempty.some sorry).support.toFinset) : Set V) G).Connected
Tactic: classical
  obtain ⟨u, ut⟩ := tn
  refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩
  · simp only [Finset.mem_biUnion, List.mem_toFinset]
    exact ⟨v, vt, Walk.end_mem_support _⟩
  · apply G.induce_connected_of_patches u
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset, Set.mem_iUnion,
                 Set.mem_setOf_eq, Walk.start_mem_support, exists_prop, and_true]
      exact ⟨u, ut⟩
    intro v hv
    simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset] at hv
    obtain ⟨w, wt, hw⟩ := hv
    refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]
      exact fun x xw => Set.mem_iUnion₂.mpr ⟨w, wt, xw⟩
    · simp only [Set.mem_setOf_eq, Walk.start_mem_support, exists_true_left]
      refine ⟨hw, Walk.connected_induce_support _ _ _⟩
Cleared hypotheses: tn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
u v : (↑G''.verts : Type u)
hreachable : G''.coe.Reachable u v
a b : (↑G''.verts : Type u)
r : G''.coe.Adj a b
⊢ ∃ (a_1 : (↑G'.verts : Type u)) (b_1 : (↑G'.verts : Type u)),
    G''.Adj a_1 b_1 ∧
      (f : (a : (↑G'.verts : Type u)) → V) a_1 =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u))) ⋯) : V) ∧
        (f : (a : (↑G'.verts : Type u)) → V) b_1 =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u))) ⋯) : V)
have h : ∃ (b_1 : (↑G'.verts : Type u)),
  G''.Adj (↑a : (↑G'.verts : Type u)) b_1 ∧
    (f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u)) =
        (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u))) sorry) : V) ∧
      (f : (a : (↑G'.verts : Type u)) → V) b_1 =
        (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u))) sorry) : V)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
u v : (↑G''.verts : Type u)
hreachable : G''.coe.Reachable u v
a b : (↑G''.verts : Type u)
r : G''.coe.Adj a b
h :
  ∃ (b_1 : (↑G'.verts : Type u)),
    G''.Adj (↑a : (↑G'.verts : Type u)) b_1 ∧
      (f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u)) =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u))) ⋯) : V) ∧
        (f : (a : (↑G'.verts : Type u)) → V) b_1 =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u))) ⋯) : V)
⊢ ∃ (a_1 : (↑G'.verts : Type u)) (b_1 : (↑G'.verts : Type u)),
    G''.Adj a_1 b_1 ∧
      (f : (a : (↑G'.verts : Type u)) → V) a_1 =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u))) ⋯) : V) ∧
        (f : (a : (↑G'.verts : Type u)) → V) b_1 =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u))) ⋯) : V)
have w : (↑G'.verts : Type u)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
u v : (↑G''.verts : Type u)
hreachable : G''.coe.Reachable u v
a b : (↑G''.verts : Type u)
r : G''.coe.Adj a b
h :
  ∃ (b_1 : (↑G'.verts : Type u)),
    G''.Adj (↑a : (↑G'.verts : Type u)) b_1 ∧
      (f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u)) =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u))) ⋯) : V) ∧
        (f : (a : (↑G'.verts : Type u)) → V) b_1 =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u))) ⋯) : V)
w : (↑G'.verts : Type u)
h₁ :
  ∃ (b_1 : (↑G'.verts : Type u)),
    G''.Adj (↑a : (↑G'.verts : Type u)) b_1 ∧
      (f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u)) =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u))) ⋯) : V) ∧
        (f : (a : (↑G'.verts : Type u)) → V) b_1 =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u))) ⋯) : V)
w₁ : (↑G'.verts : Type u)
⊢ ∃ (a_1 : (↑G'.verts : Type u)) (b_1 : (↑G'.verts : Type u)),
    G''.Adj a_1 b_1 ∧
      (f : (a : (↑G'.verts : Type u)) → V) a_1 =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u))) ⋯) : V) ∧
        (f : (a : (↑G'.verts : Type u)) → V) b_1 =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u))) ⋯) : V)
have h₂ : G''.Adj (↑a : (↑G'.verts : Type u)) (↑b : (↑G'.verts : Type u)) ∧
  (f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u)) =
      (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u))) sorry) : V) ∧
    (f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u)) =
      (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u))) sorry) : V)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
⊢ (Subgraph.map f G'').Preconnected
have rw : (Subgraph.map f G'').coe.Preconnected
Tactic: rw [Subgraph.preconnected_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
u' : V
u : (↑G'.verts : Type u)
hu : u ∈ G''.verts
hfu : (f : (a : (↑G'.verts : Type u)) → V) u = u'
⊢ ∀ (v : (↑(Subgraph.map f G'').verts : Type u)),
    (Subgraph.map f G'').coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) u' ⋯) v
have this : ∀ (v' : V) (v : (↑G'.verts : Type u)) (hv : v ∈ G''.verts) (hfv : (f : (a : (↑G'.verts : Type u)) → V) v = v'),
  (Subgraph.map f G'').coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) u' sorry)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) v' sorry)
Tactic: ⟨v', v, hv, hfv⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
u' : V
u : (↑G'.verts : Type u)
hu : u ∈ G''.verts
hfu : (f : (a : (↑G'.verts : Type u)) → V) u = u'
v' : V
v : (↑G'.verts : Type u)
hv : v ∈ G''.verts
hfv : (f : (a : (↑G'.verts : Type u)) → V) v = v'
⊢ (Subgraph.map f G'').coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) u' ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) v' ⋯)
have simp_rw : (Subgraph.map f G'').coe.Reachable
  (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) ((f : (a : (↑G'.verts : Type u)) → V) u) sorry)
  (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) ((f : (a : (↑G'.verts : Type u)) → V) v) sorry)
Tactic: simp_rw [← hfu, ← hfv]
-- 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 g : A.Copy B
h :
  Eq (α := (a : α) → β) ((fun (f : A.Copy B) ↦ ((⇑f.toHom : (a : α) → β) : (a : α) → β)) f)
    ((fun (f : A.Copy B) ↦ ((⇑f.toHom : (a : α) → β) : (a : α) → β)) g)
⊢ f = g
have obtain : ∀ (toFun : α → β) (map_rel' : ∀ {a b : α}, A.Adj a b → B.Adj (toFun a) (toFun b))
  (injective' :
    Injective.{u_4 + 1, u_5 + 1} (α := α) (β := β)
      (⇑(RelHom.mk (r := A.Adj) (s := B.Adj) toFun @map_rel') : (a : α) → β))
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : A.Copy B) ↦ ((⇑f.toHom : (a : α) → β) : (a : α) → β))
        { toHom := RelHom.mk (r := A.Adj) (s := B.Adj) toFun @map_rel', injective' := injective' })
      ((fun (f : A.Copy B) ↦ ((⇑f.toHom : (a : α) → β) : (a : α) → β)) g)),
  { toHom := RelHom.mk (r := A.Adj) (s := B.Adj) toFun @map_rel', injective' := injective' : A.Copy B } = g
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- 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 : α
x x_1 : (↑(A.neighborSet a) : Type u_4)
h :
  Eq.{u_5 + 1} (α := (↑(B.neighborSet ((f : (a : α) → β) a)) : Type u_5))
    ((fun (v : (↑(A.neighborSet a) : Type u_4)) ↦
        (Subtype.mk (p := fun (x : β) ↦ x ∈ B.neighborSet ((f : (a : α) → β) a)) ((f : (a : α) → β) (↑v : α)) ⋯ :
          { x : β // x ∈ B.neighborSet ((f : (a : α) → β) a) }))
      x)
    ((fun (v : (↑(A.neighborSet a) : Type u_4)) ↦
        (Subtype.mk (p := fun (x : β) ↦ x ∈ B.neighborSet ((f : (a : α) → β) a)) ((f : (a : α) → β) (↑v : α)) ⋯ :
          { x : β // x ∈ B.neighborSet ((f : (a : α) → β) a) }))
      x_1)
⊢ x = x_1
have rw : ∀ (h : Eq.{u_5 + 1} (α := β) ((f : (a : α) → β) (↑x : α) : β) ((f : (a : α) → β) (↑x_1 : α) : β)), (↑x : α) = (↑x_1 : α)
Tactic: rw [Subtype.mk_eq_mk] at h ⊢
Cleared hypotheses: h
-- 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 γ
g : B.Copy C
f : A.Copy B
⊢ A.Copy C
have injective' : Injective.{u_4 + 1, u_6 + 1} (α := α) (β := γ) (⇑(g.toHom.comp f.toHom) : (a : α) → γ)
Tactic: use g.toHom.comp f.toHom
-- 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 γ
g : B.Copy C
f : A.Copy B
⊢ Injective.{u_4 + 1, u_6 + 1} (α := α) (β := γ) (⇑(g.toHom.comp f.toHom) : (a : α) → γ)
have injective' : Injective.{u_4 + 1, u_6 + 1} (α := α) (β := γ)
  (Function.comp.{u_4 + 1, u_5 + 1, u_6 + 1} (β := β) (⇑g.toHom : (a : β) → γ) (⇑f.toHom : (a : α) → β))
Tactic: rw [Hom.coe_comp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
⊢ Eq (α := (a : α) → γ) (⇑(g.comp f) : (a : α) → γ)
    (Function.comp.{u_4 + 1, u_5 + 1, u_6 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β))
have h : ∀ (x : α),
  Eq.{u_6 + 1} (α := γ) ((g.comp f : (a : α) → γ) x : γ)
    (Function.comp.{u_4 + 1, u_5 + 1, u_6 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β) x : γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ ofLE G G ⋯ = id G
have a : ∀ (a : V), Eq (α := V) ((ofLE G G sorry : (a : V) → V) a : V) ((id G : (a : V) → V) a : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
G₁ G₂ G₃ : SimpleGraph V
h₁₂ : G₁ ≤ G₂
h₂₃ : G₂ ≤ G₃
⊢ (ofLE G₂ G₃ h₂₃).comp (ofLE G₁ G₂ h₁₂) = ofLE G₁ G₃ ⋯
have a : ∀ (a : V),
  Eq (α := V) (((ofLE G₂ G₃ h₂₃).comp (ofLE G₁ G₂ h₁₂) : (a : V) → V) a : V) ((ofLE G₁ G₃ sorry : (a : V) → V) a : V)
Tactic: ext
-- 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
⊢ A'.coe ≃g (Subgraph.map f.toHom A').coe
have 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 sorry :
          (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
        a)
      ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts sorry :
          (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
        b) ↔
    A'.coe.Adj a b
Tactic: use Equiv.Set.image f.toHom _ f.injective
-- 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
⊢ ∀ {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').coe.Adj
      ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts sorry :
          (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
        a)
      ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts sorry :
          (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
        b) ↔
    A'.coe.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
⊢ ∀ {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').coe.Adj
      (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
        ((f.toHom : (a : α) → β) (↑a : α)) sorry)
      (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
        ((f.toHom : (a : α) → β) (↑b : α)) sorry) ↔
    A'.coe.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]