awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
e : V ≃ W
⊢ Eq.{u_2 + 1} (α := SimpleGraph W) (SimpleGraph.comap (⇑e.symm.toEmbedding : (a : W) → V) G)
    (SimpleGraph.map (⇑e.toEmbedding : (a : V) → W) G)
have Adj : ∀ (x x_1 : W),
  Adj (SimpleGraph.comap (⇑e.symm.toEmbedding : (a : W) → V) G) x x_1 ↔
    Adj (SimpleGraph.map (⇑e.toEmbedding : (a : V) → W) G) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph W
e : V ≃ W
⊢ Eq.{u_1 + 1} (α := SimpleGraph V) (SimpleGraph.map (⇑e.symm.toEmbedding : (a : W) → V) G)
    (SimpleGraph.comap (⇑e.toEmbedding : (a : V) → W) G)
have rw : Eq.{u_1 + 1} (α := SimpleGraph V) (SimpleGraph.comap (⇑e.symm.symm.toEmbedding : (a : V) → W) G)
  (SimpleGraph.comap (⇑e.toEmbedding : (a : V) → W) G)
Tactic: rw [← comap_symm, e.symm_symm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph W
e : V ≃ W
rw :
  Eq.{u_1 + 1} (α := SimpleGraph V) (SimpleGraph.comap (⇑e.symm.symm.toEmbedding : (a : V) → W) G)
    (SimpleGraph.comap (⇑e.toEmbedding : (a : V) → W) G)
⊢ Eq.{u_1 + 1} (α := SimpleGraph V) (SimpleGraph.map (⇑e.symm.toEmbedding : (a : W) → V) G)
    (SimpleGraph.comap (⇑e.toEmbedding : (a : V) → W) G)
have rw₁ : Eq.{u_1 + 1} (α := SimpleGraph V) (SimpleGraph.comap (⇑e.toEmbedding : (a : V) → W) G)
  (SimpleGraph.comap (⇑e.toEmbedding : (a : V) → W) G)
Tactic: rw [← comap_symm, e.symm_symm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
f : V → W
hf : Injective f
⊢ SimpleGraph.comap f (completeGraph W) = completeGraph V
have Adj : ∀ (x x_1 : V), (SimpleGraph.comap f (completeGraph W)).Adj x x_1 ↔ (completeGraph V).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
⊢ SimpleGraph.comap.{u_1, u_2} (W := W) (⇑f : (a : V) → W) (SimpleGraph.map (⇑f : (a : V) → W) G) = G
have Adj : ∀ (x x_1 : V),
  Adj (SimpleGraph.comap.{u_1, u_2} (W := W) (⇑f : (a : V) → W) (SimpleGraph.map (⇑f : (a : V) → W) G)) x x_1 ↔
    G.Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph W
⊢ SimpleGraph.map.{u_1, u_2} (V := V) (⇑f : (a : V) → W) (SimpleGraph.comap (⇑f : (a : V) → W) G) ≤ G
have rw : LE.le.{u_1} (α := SimpleGraph V) (SimpleGraph.comap (⇑f : (a : V) → W) G) (SimpleGraph.comap (⇑f : (a : V) → W) G)
Tactic: rw [map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V ↪ W
inst : Subsingleton V
⊢ SimpleGraph.map (⇑f : (a : V) → W) G ≤ G'
have rw : G ≤ SimpleGraph.comap (⇑f : (a : V) → W) G'
Tactic: rw [map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
⊢ (Equiv.refl V).simpleGraph = Equiv.refl (SimpleGraph V)
have H : ∀ (x : SimpleGraph V) (x_1 x_2 : V),
  Adj (((Equiv.refl V).simpleGraph : (a : SimpleGraph V) → SimpleGraph V) x) x_1 x_2 ↔
    Adj ((Equiv.refl (SimpleGraph V) : (a : SimpleGraph V) → SimpleGraph V) x) x_1 x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
⊢ Eq (α := SimpleGraph (↑{v} : Type u_1)) (induce {v} G) ⊤
have rw : LE.le (α := SimpleGraph (↑{v} : Type u_1)) ⊤ (induce {v} G)
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
⊢ (induce s G).spanningCoe (s := s) = G ↔ G.support ⊆ s
have refine_1 : ∀ (h : (induce s G).spanningCoe (s := s) = G) (v : V) (hv : v ∈ G.support), v ∈ s
Tactic: refine ⟨fun h v hv ↦ ?_, fun h ↦ le_antisymm (G.spanningCoe_induce_le s) fun u v hadj ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
refine_1 : ∀ (h : (induce s G).spanningCoe (s := s) = G) (v : V) (hv : v ∈ G.support), v ∈ s
⊢ (induce s G).spanningCoe (s := s) = G ↔ G.support ⊆ s
have refine_2 : ∀ (h : G.support ⊆ s) (u v : V) (hadj : G.Adj u v), (induce s G).spanningCoe (s := s).Adj u v
Tactic: refine ⟨fun h v hv ↦ ?_, fun h ↦ le_antisymm (G.spanningCoe_induce_le s) fun u v hadj ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe (s := s) = G
v : V
hv : v ∈ G.support
⊢ v ∈ s
have hv₁ : v ∈ Subtype.val (p := fun (x : V) ↦ x ∈ s) '' (induce s G).support
Tactic: rw [← h, support_spanningCoe] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe (s := s) = G
v : V
hv : v ∈ Subtype.val (p := fun (x : V) ↦ x ∈ s) '' (induce s G).support
⊢ v ∈ s
have refine_1 : ∀ u ∈ (induce s G).support, ∀ (hvu : (↑u : V) = v), v ∈ s
Tactic: have ⟨u, _, hvu⟩ := hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁ : (↑u : Type u_1)
hs : Membership.mem (γ := Set (↑u : Type u_1)) (u ↓∩ s) v₁
v₂ : (↑u : Type u_1)
ht : Membership.mem (γ := Set (↑u : Type u_1)) (u ↓∩ t) v₂
⊢ (SimpleGraph.induce u G).Adj v₁ v₂
have rw : G.Adj (↑v₁ : V) (↑v₂ : V)
Tactic: rw [comap_adj, Embedding.coe_subtype]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ f.mapEdgeSet (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₁ h₁) =
      f.mapEdgeSet (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₂ h₂) →
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₁ h₁ = Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₂ h₂
have dsimp : Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → W) e₁) sorry =
    Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → W) e₂) sorry →
  Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₁ h₁ = Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₂ h₂
Tactic: dsimp [Hom.mapEdgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → W) e₁) ⋯ =
      Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → W) e₂) ⋯ →
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₁ h₁ = Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₂ h₂
have rw : Eq.{u_2 + 1} (α := Sym2 W) (Sym2.map (⇑f : (a : V) → W) e₁) (Sym2.map (⇑f : (a : V) → W) e₂) →
  Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₁ h₁ = Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₂ h₂
Tactic: rw [Subtype.mk_eq_mk]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Eq.{u_2 + 1} (α := Sym2 W) (Sym2.map (⇑f : (a : V) → W) e₁) (Sym2.map (⇑f : (a : V) → W) e₂) →
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₁ h₁ = Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₂ h₂
have rw : Eq.{u_2 + 1} (α := Sym2 W) (Sym2.map (⇑f : (a : V) → W) e₁) (Sym2.map (⇑f : (a : V) → W) e₂) → e₁ = e₂
Tactic: rw [Subtype.mk_eq_mk]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → W) e₁) ⋯ =
      Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → W) e₂) ⋯ →
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₁ h₁ = Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₂ h₂
have repeat : Eq.{u_2 + 1} (α := Sym2 W) (Sym2.map (⇑f : (a : V) → W) e₁) (Sym2.map (⇑f : (a : V) → W) e₂) → e₁ = e₂
Tactic: repeat rw [Subtype.mk_eq_mk]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G' : SimpleGraph W
f : Hom.{u_1, u_2} (V := V) ⊤ G'
v w : V
h : Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) v : W) ((f : (a : V) → W) w : W)
⊢ v = w
have contrapose! : ∀ (h : v ≠ w), Ne.{u_2 + 1} (α := W) ((f : (a : V) → W) v : W) ((f : (a : V) → W) w : W)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v_1 : V
H : SimpleGraph W
f : G ↪g G'
v w₁ : V
h₁ : w₁ ∈ G.neighborSet v
w₂ : V
h₂ : w₂ ∈ G.neighborSet v
h :
  Eq.{u_2 + 1} (α := (↑(G'.neighborSet ((f : (a : V) → W) v)) : Type u_2))
    ((fun (w : (↑(G.neighborSet v) : Type u_1)) ↦
        (Subtype.mk (p := fun (x : W) ↦ x ∈ G'.neighborSet ((f : (a : V) → W) v)) ((f : (a : V) → W) (↑w : V)) ⋯ :
          { x : W // x ∈ G'.neighborSet ((f : (a : V) → W) v) }))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₁ h₁))
    ((fun (w : (↑(G.neighborSet v) : Type u_1)) ↦
        (Subtype.mk (p := fun (x : W) ↦ x ∈ G'.neighborSet ((f : (a : V) → W) v)) ((f : (a : V) → W) (↑w : V)) ⋯ :
          { x : W // x ∈ G'.neighborSet ((f : (a : V) → W) v) }))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₂ h₂))
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₁ h₁ = Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₂ h₂
have rw : ∀
  (h :
    Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₁ h₁) : V) : W)
      ((f : (a : V) → W) (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₂ h₂) : V) : W)),
  w₁ = w₂
Tactic: rw [Subtype.mk_eq_mk] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : H ↪g G
⊢ SimpleGraph.comap (⇑f : (a : W) → V) G = H
have Adj : ∀ (x x_1 : W), Adj (SimpleGraph.comap (⇑f : (a : W) → V) G) x x_1 ↔ H.Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v_1 : V
H : SimpleGraph W
f_1 : G ↪g G'
G'' : SimpleGraph X
f : Gᶜ ↪g Hᶜ
v w : V
⊢ H.Adj ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) v)
      ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) w) ↔
    G.Adj v w
have inl : H.Adj ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) v)
    ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) v) ↔
  G.Adj v v
Tactic: obtain rfl | hvw := eq_or_ne v w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v_1 : V
H : SimpleGraph W
f_1 : G ↪g G'
G'' : SimpleGraph X
f : Gᶜ ↪g Hᶜ
v w : V
inl :
  H.Adj ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) v)
      ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) v) ↔
    G.Adj v v
⊢ H.Adj ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) v)
      ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) w) ↔
    G.Adj v w
have inr : ∀ (hvw : v ≠ w),
  H.Adj ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) v)
      ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) w) ↔
    G.Adj v w
Tactic: obtain rfl | hvw := eq_or_ne v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
⊢ Eq.{u_1 + 1} (α := induce s G →g induce s G) (induceHom (s := s) (t := s) Hom.id ⋯) Hom.id
have h : ∀ (x : (↑s : Type u_1)),
  Eq.{u_1 + 1} (α := V) (↑((induceHom (s := s) (t := s) Hom.id sorry : (a : (↑s : Type u_1)) → (↑s : Type u_1)) x) : V)
    (↑((Hom.id : (a : (↑s : Type u_1)) → (↑s : Type u_1)) x) : V)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
G'' : SimpleGraph X
s : Set V
t : Set W
r : Set X
φ : G →g G'
φst : Set.MapsTo (⇑φ : (a : V) → W) s t
ψ : G' →g G''
ψtr : Set.MapsTo (⇑ψ : (a : W) → X) t r
⊢ (induceHom (s := t) (t := r) ψ ψtr).comp (induceHom (s := s) (t := t) φ φst) =
    induceHom (s := s) (t := r) (ψ.comp φ) ⋯
have h : ∀ (x : (↑s : Type u_1)),
  Eq.{u_3 + 1} (α := X)
    (↑(((induceHom (s := t) (t := r) ψ ψtr).comp (induceHom (s := s) (t := t) φ φst) :
            (a : (↑s : Type u_1)) → (↑r : Type u_3))
          x) :
      X)
    (↑((induceHom (s := s) (t := r) (ψ.comp φ) sorry : (a : (↑s : Type u_1)) → (↑r : Type u_3)) x) : X)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s s' : Set V
h : s ≤ s'
⊢ (G.induceHomOfLE (s := s) (s' := s') h).toHom = induceHom (s := s) (t := s') Hom.id ⋯
have h₁ : ∀ (x : (↑s : Type u_1)),
  Eq.{u_1 + 1} (α := V)
    (↑(((G.induceHomOfLE (s := s) (s' := s') h).toHom : (a : (↑s : Type u_1)) → (↑s' : Type u_1)) x) : V)
    (↑((induceHom (s := s) (t := s') Hom.id sorry : (a : (↑s : Type u_1)) → (↑s' : Type u_1)) x) : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
v : V
f : G ≃g G'
⊢ (⇑f : (a : V) → W) '' G.neighborSet v = G'.neighborSet ((f : (a : V) → W) v)
have rw : Set.image.{u_1, u_2} (α := V) (⇑f : (a : V) → W)
    ((⇑f.toEmbedding : (a : V) → W) ⁻¹' G'.neighborSet ((f.toEmbedding : (a : V) → W) v)) =
  G'.neighborSet ((f : (a : V) → W) v)
Tactic: rw [← f.toEmbedding.preimage_neighborSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
⊢ f.symm.toHom.comp f.toHom = Hom.id
have h : ∀ (v : V), Eq (α := V) ((f.symm.toHom.comp f.toHom : (a : V) → V) v : V) ((Hom.id : (a : V) → V) v : V)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
⊢ f.toHom.comp f.symm.toHom = Hom.id
have h : ∀ (v : W), Eq (α := W) ((f.toHom.comp f.symm.toHom : (a : W) → W) v : W) ((Hom.id : (a : W) → W) v : W)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v : V
f : G ≃g G'
e : Sym2 V
h : e ∈ G.edgeSet
⊢ Hom.mapEdgeSet ((RelIso.toRelEmbedding (r := G'.Adj) (s := G.Adj) f.symm).toRelHom (r := G'.Adj) (s := G.Adj))
      (Hom.mapEdgeSet ((RelIso.toRelEmbedding (r := G.Adj) (s := G'.Adj) f).toRelHom (r := G.Adj) (s := G'.Adj))
        (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e h)) =
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e h
have simp : Sym2.map
    (fun (x : V) ↦
      (RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) sorry :
          (a : W) → V)
        ((RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) sorry : (a : V) → W)
            x :
          W))
    e =
  e
Tactic: simp only [Hom.mapEdgeSet, RelEmbedding.toRelHom, Sym2.map_map, comp_apply, Subtype.mk.injEq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v : V
f : G ≃g G'
e : Sym2 V
h : e ∈ G.edgeSet
⊢ Sym2.map
      (fun (x : V) ↦
        (RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) ⋯ :
            (a : W) → V)
          ((RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) ⋯ :
                (a : V) → W)
              x :
            W))
      e =
    e
have h₁ : ∀ x ∈ e,
  (RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) sorry : (a : W) → V)
      ((RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) sorry : (a : V) → W)
          x :
        W) =
    id x
Tactic: convert! congr_fun Sym2.map_id e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v : V
f : G ≃g G'
e : Sym2 W
h : e ∈ G'.edgeSet
⊢ Hom.mapEdgeSet ((RelIso.toRelEmbedding (r := G.Adj) (s := G'.Adj) f).toRelHom (r := G.Adj) (s := G'.Adj))
      (Hom.mapEdgeSet ((RelIso.toRelEmbedding (r := G'.Adj) (s := G.Adj) f.symm).toRelHom (r := G'.Adj) (s := G.Adj))
        (Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) e h)) =
    Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) e h
have simp : Sym2.map
    (fun (x : W) ↦
      (RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) sorry : (a : V) → W)
        ((RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) sorry :
              (a : W) → V)
            x :
          V))
    e =
  e
Tactic: simp only [Hom.mapEdgeSet, RelEmbedding.toRelHom, Sym2.map_map, comp_apply, Subtype.mk.injEq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v : V
f : G ≃g G'
e : Sym2 W
h : e ∈ G'.edgeSet
⊢ Sym2.map
      (fun (x : W) ↦
        (RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) ⋯ : (a : V) → W)
          ((RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) ⋯ :
                (a : W) → V)
              x :
            V))
      e =
    e
have h₁ : ∀ x ∈ e,
  (RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) sorry : (a : V) → W)
      ((RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) sorry :
            (a : W) → V)
          x :
        V) =
    id x
Tactic: convert! congr_fun Sym2.map_id e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
inst : Fintype V
inst_1 : Fintype W
⊢ Fintype.card V = Fintype.card W
have rw : Fintype.card W = Fintype.card W
Tactic: rw [← Fintype.ofEquiv_card f.toEquiv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v : V
inst : Fintype V
n : ℕ
hc : Fintype.card V = n
x y : Fin n
simp_rw simp_rw₁ :
  G.Adj (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) x)
      (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) y) →
    G.Adj (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) y)
      (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) x)
⊢ (fun (x y : Fin n) ↦
        G.Adj (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) x)
          (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) y))
      x y →
    (fun (x y : Fin n) ↦
        G.Adj (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) x)
          (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) y))
      y x
have simp_rw₂ : G.Adj (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) x)
    (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) y) →
  G.Adj (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) x)
    (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) y)
Tactic: simp_rw [adj_comm, imp_self]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v : V
inst : Fintype V
n : ℕ
hc : Fintype.card V = n
⊢ G ≃g G.overFin hc
have map_rel_iff' : ∀ {a b : V},
  (G.overFin hc).Adj ((Fintype.equivFinOfCardEq hc : (a : V) → Fin n) a)
      ((Fintype.equivFinOfCardEq hc : (a : V) → Fin n) b) ↔
    G.Adj a b
Tactic: use Fintype.equivFinOfCardEq hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hvw : M.Adj v w
⊢ h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) =
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) hvw
have rw : Eq (α := (↑M.edgeSet : Type u_1))
  (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet)
    s((↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v sorry) : V),
      Exists.choose (p := fun (x : V) ↦
        (fun (w_1 : V) ↦ M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v sorry) : V) w_1) x ∧
          ∀ (y : V), M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v sorry) : V) y → y = x)
        sorry)
    sorry)
  (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) hvw)
Tactic: rw [IsMatching.toEdge, Subtype.mk_eq_mk, ← h hvw.fst_mem |>.choose_spec.right w hvw]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hvw : M.Adj v w
rw :
  Eq (α := (↑M.edgeSet : Type u_1))
    (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet)
      s((↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V),
        Exists.choose (p := fun (x : V) ↦
          (fun (w_1 : V) ↦ M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V) w_1) x ∧
            ∀ (y : V), M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V) y → y = x)
          ⋯)
      ⋯)
    (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) hvw)
⊢ h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) =
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) hvw
have rw₁ : s((↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v sorry) : V),
    Exists.choose (p := fun (x : V) ↦
      (fun (w_1 : V) ↦ M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v sorry) : V) w_1) x ∧
        ∀ (y : V), M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v sorry) : V) y → y = x)
      sorry) =
  s(v, w)
Tactic: rw [IsMatching.toEdge, Subtype.mk_eq_mk, ← h hvw.fst_mem |>.choose_spec.right w hvw]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hvw : M.Adj v w
rw :
  Eq (α := (↑M.edgeSet : Type u_1))
    (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet)
      s((↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V),
        Exists.choose (p := fun (x : V) ↦
          (fun (w_1 : V) ↦ M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V) w_1) x ∧
            ∀ (y : V), M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V) y → y = x)
          ⋯)
      ⋯)
    (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) hvw)
rw₁ :
  s((↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V),
      Exists.choose (p := fun (x : V) ↦
        (fun (w_1 : V) ↦ M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V) w_1) x ∧
          ∀ (y : V), M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V) y → y = x)
        ⋯) =
    s(v, w)
⊢ h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) =
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) hvw
have rw₂ : s((↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v sorry) : V), w) = s(v, w)
Tactic: rw [IsMatching.toEdge, Subtype.mk_eq_mk, ← h hvw.fst_mem |>.choose_spec.right w hvw]