awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
y : V
hy : Adj (G := G) (⨆ (i : ι), f i) v y
i' : ι
hi' : (f i').Adj v y
heq : ¬i = i'
this : (fun (i j : ι) ↦ Disjoint (f i).support (f j).support) i i'
⊢ ∀ ⦃a : V⦄, a ∈ (f i).support → a ∉ (f i').support

Tactic:
simp only [Set.disjoint_left] at this

Premises used: Set.disjoint_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
y : V
hy : Adj (G := G) (⨆ (i : ι), f i) v y
i' : ι
hi' : (f i').Adj v y
heq : ¬i = i'
this : ∀ ⦃a : V⦄, a ∈ (f i).support → a ∉ (f i').support
⊢ y = w

Tactic:
simpa [(mem_support _).mpr ⟨w, hw.1⟩, (mem_support _).mpr ⟨y, hi'⟩] using @this v

Premises used: Iff.mpr, And.left, Exists.intro, SimpleGraph.Subgraph.mem_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v_1 : V
hv : v_1 ∈ (G.subgraphOfAdj h).verts
⊢ v_1 = v ∨ v_1 = w

Tactic:
rw [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at hv

Premises used: Set.mem_singleton_iff, SimpleGraph.subgraphOfAdj_verts, Set.mem_insert_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v_1 : V
h_1 : v_1 = v
h₁ :
  (fun (w_1 : V) ↦ (G.subgraphOfAdj h).Adj v_1 w_1) w ∧
    ∀ (y : V), (fun (w_1 : V) ↦ (G.subgraphOfAdj h).Adj v_1 w_1) y → y = w
⊢ ∃! w_1 : V, (G.subgraphOfAdj h).Adj v_1 w_1

Tactic:
use w
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v_1 : V
h_1 : v_1 = v
⊢ (fun (w_1 : V) ↦ (G.subgraphOfAdj h).Adj v_1 w_1) w ∧
    ∀ (y : V), (fun (w_1 : V) ↦ (G.subgraphOfAdj h).Adj v_1 w_1) y → y = w

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v_1 : V
h_1 : v_1 = w
h₁ :
  (fun (w_1 : V) ↦ (G.subgraphOfAdj h).Adj v_1 w_1) v ∧
    ∀ (y : V), (fun (w_1 : V) ↦ (G.subgraphOfAdj h).Adj v_1 w_1) y → y = v
⊢ ∃! w_1 : V, (G.subgraphOfAdj h).Adj v_1 w_1

Tactic:
use v
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v_1 : V
h_1 : v_1 = w
⊢ (fun (w_1 : V) ↦ (G.subgraphOfAdj h).Adj v_1 w_1) v ∧
    ∀ (y : V), (fun (w_1 : V) ↦ (G.subgraphOfAdj h).Adj v_1 w_1) y → y = v

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v_1 : V
hv : v_1 = v ∨ v_1 = w
inl : v_1 = v → ∃! w_1 : V, (G.subgraphOfAdj h).Adj v_1 w_1
inr : v_1 = w → ∃! w_1 : V, (G.subgraphOfAdj h).Adj v_1 w_1
⊢ ∃! w_1 : V, (G.subgraphOfAdj h).Adj v_1 w_1

Tactic:
cases hv with
  | inl => use w; aesop
  | inr => use v; aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v : V
hv : v ∈ (Subgraph.coeSubgraph M).verts
obtain :
  ∀ (w : (↑G'.verts : Type u_1))
    (hw :
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) w ∧
        ∀ (y : (↑G'.verts : Type u_1)),
          (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) y → y = w),
    ∃! w : V, (Subgraph.coeSubgraph M).Adj v w
⊢ ∃! w : V, (Subgraph.coeSubgraph M).Adj v w

Tactic:
obtain ⟨w, hw⟩ := hM <| Set.mem_of_mem_image_val <| (Subgraph.verts_coeSubgraph M).symm ▸ hv

Premises used: Set.mem_of_mem_image_val
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v : V
hv : v ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) y → y = w
h :
  (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) (↑w : V) ∧
    ∀ (y : V), (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y → y = (↑w : V)
⊢ ∃! w : V, (Subgraph.coeSubgraph M).Adj v w

Tactic:
use w
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v : V
hv : v ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) y → y = w
⊢ (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) (↑w : V) ∧
    ∀ (y : V), (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y → y = (↑w : V)

Tactic:
⟨?_, fun y hy => ?_⟩

Premises used: And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v : V
hv : v ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) y → y = w
h : (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) (↑w : V)
h₁ : ∀ (y : V) (hy : (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y), y = (↑w : V)
⊢ (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) (↑w : V) ∧
    ∀ (y : V), (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y → y = (↑w : V)

Tactic:
refine ⟨?_, fun y hy => ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v : V
hv : v ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) y → y = w
h : ∀ (v_1 : { x : V // x ∈ G'.verts }) (hv : v_1 ∈ M.verts ∧ (↑v_1 : V) = v), (Subgraph.coeSubgraph M).Adj v (↑w : V)
⊢ (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) (↑w : V)

Tactic:
obtain ⟨v, hv⟩ := (Set.mem_image _ _ _).mp <| (Subgraph.verts_coeSubgraph M).symm ▸ hv

Premises used: Set.mem_image, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v_1 : V
hv_1 : v_1 ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v_1 ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v_1 ⋯) w) y → y = w
v : { x : V // x ∈ G'.verts }
hv : v ∈ M.verts ∧ (↑v : V) = v_1
h : ∃ (h : v_1 ∈ G'.verts), M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v_1 ⋯) w
⊢ (Subgraph.coeSubgraph M).Adj v_1 (↑w : V)

Tactic:
simp only [coeSubgraph_adj, Subtype.coe_eta, Subtype.coe_prop, exists_const]

Premises used: Subtype.coe_prop, Subtype.coe_eta, exists_const, SimpleGraph.Subgraph.coeSubgraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v_1 : V
hv_1 : v_1 ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v_1 ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v_1 ⋯) w) y → y = w
v : { x : V // x ∈ G'.verts }
hv : v ∈ M.verts ∧ (↑v : V) = v_1
⊢ ∃ (h : v_1 ∈ G'.verts), M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v_1 ⋯) w

Tactic:
⟨hv.2 ▸ v.2, hw.1⟩

Premises used: Eq.rec, And.right, And.left, Exists.intro, Subtype.property
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v_1 : V
hv_1 : v_1 ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v_1 ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v_1 ⋯) w) y → y = w
v : { x : V // x ∈ G'.verts }
hv : v ∈ M.verts ∧ (↑v : V) = v_1
⊢ ∃ (h : v_1 ∈ G'.verts), M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v_1 ⋯) w

Tactic:
exact ⟨hv.2 ▸ v.2, hw.1⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v : V
hv : v ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) y → y = w
y : V
hy : (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y
⊢ v ∈ G'.verts

Tactic:
obtain ⟨_, hw', hvw⟩ := (coeSubgraph_adj _ _ _).mp hy

Premises used: Iff.mp, SimpleGraph.Subgraph.coeSubgraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v : V
hv : v ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) y → y = w
y : V
hy : (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y
w₁ : v ∈ G'.verts
⊢ y ∈ G'.verts

Tactic:
obtain ⟨_, hw', hvw⟩ := (coeSubgraph_adj _ _ _).mp hy

Premises used: Iff.mp, SimpleGraph.Subgraph.coeSubgraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v : V
hv : v ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) y → y = w
y : V
hy : (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y
w₁ : v ∈ G'.verts
hw' : y ∈ G'.verts
⊢ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v w₁) (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) y hw')

Tactic:
obtain ⟨_, hw', hvw⟩ := (coeSubgraph_adj _ _ _).mp hy

Premises used: Iff.mp, SimpleGraph.Subgraph.coeSubgraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v : V
hv : v ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) y → y = w
y : V
hy : (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y
w_1 : v ∈ G'.verts
hw' : y ∈ G'.verts
hvw : M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v w_1) (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) y hw')
h h₁ : y = (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) y hw') : V)
⊢ y = (↑w : V)

Tactic:
rw [← hw.2 ⟨y, hw'⟩ hvw]

Premises used: Subtype.mk, And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h_1 : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
v w : V
h :
  (∃ (h : v ∈ s),
      (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) = w) ∨
    ∃ (h : w ∈ s),
      (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v
inl :
  ∀ (hv : v ∈ s),
    G.Adj v (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv)) : V)
inr :
  ∀ (hw : w ∈ s),
    G.Adj (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w hw)) : V) w
⊢ G.Adj v w

Tactic:
obtain (⟨hv, rfl⟩ | ⟨hw, rfl⟩) := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
v : V
hv : v ∈ s
⊢ G.Adj v (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv)) : V)

Tactic:
hadj ⟨v, _⟩

Premises used: Subtype.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
v : V
hv : v ∈ s
⊢ G.Adj v (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv)) : V)

Tactic:
exact hadj ⟨v, _⟩

Premises used: Subtype.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
w : V
hw : w ∈ s
⊢ G.Adj (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w hw)) : V) w

Tactic:
(hadj ⟨w, _⟩).symm

Premises used: SimpleGraph.Adj.symm, Subtype.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
w : V
hw : w ∈ s
⊢ G.Adj (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w hw)) : V) w

Tactic:
exact (hadj ⟨w, _⟩).symm

Premises used: SimpleGraph.Adj.symm, Subtype.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
⊢ ∀ {v w : V},
    ((∃ (h : v ∈ s),
          (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) = w) ∨
        ∃ (h : w ∈ s),
          (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v) →
      v ∈ s ∪ t

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
h₁ :
  verts (G := G)
        { verts := s ∪ t,
          Adj := fun (v w : V) ↦
            (∃ (h : v ∈ s),
                (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) =
                  w) ∨
              ∃ (h : w ∈ s),
                (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v,
          adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ : G.Subgraph } =
      s ∪ t ∧
    IsMatching (G := G)
      { verts := s ∪ t,
        Adj := fun (v w : V) ↦
          (∃ (h : v ∈ s),
              (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) = w) ∨
            ∃ (h : w ∈ s),
              (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v,
        adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
⊢ ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching

Tactic:
use {
    verts := s ∪ t
    Adj := fun v w ↦ (∃ h : v ∈ s, f ⟨v, h⟩ = w) ∨ (∃ h : w ∈ s, f ⟨w, h⟩ = v)
    adj_sub := by
      intro v w h
      obtain (⟨hv, rfl⟩ | ⟨hw, rfl⟩) := h
      · exact hadj ⟨v, _⟩
      · exact (hadj ⟨w, _⟩).symm
    edge_vert := by grind }
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
h₁ :
  ∀ ⦃v : V⦄,
    v ∈ s ∨ v ∈ t →
      ∃! w : V,
        (∃ (h : v ∈ s),
            (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) = w) ∨
          ∃ (h : w ∈ s),
            (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v
⊢ verts (G := G)
        { verts := s ∪ t,
          Adj := fun (v w : V) ↦
            (∃ (h : v ∈ s),
                (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) =
                  w) ∨
              ∃ (h : w ∈ s),
                (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v,
          adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ : G.Subgraph } =
      s ∪ t ∧
    IsMatching (G := G)
      { verts := s ∪ t,
        Adj := fun (v w : V) ↦
          (∃ (h : v ∈ s),
              (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) = w) ∨
            ∃ (h : w ∈ s),
              (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v,
        adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

Tactic:
simp only [Subgraph.IsMatching, Set.mem_union, true_and]

Premises used: Set.mem_union, SimpleGraph.Subgraph.IsMatching, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
v : V
hv : v ∈ s ∨ v ∈ t
h₁ :
  ∀ (hl : v ∈ s),
    ∃! w : V,
      (∃ (h : v ∈ s),
          (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) = w) ∨
        ∃ (h : w ∈ s),
          (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v
h₂ :
  ∀ (hr : v ∈ t),
    ∃! w : V,
      (∃ (h : v ∈ s),
          (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) = w) ∨
        ∃ (h : w ∈ s),
          (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v
⊢ ∃! w : V,
    (∃ (h : v ∈ s),
        (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) = w) ∨
      ∃ (h : w ∈ s),
        (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v

Tactic:
rcases hv with hl | hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
v : V
hl : v ∈ s
h₁ :
  (fun (w : V) ↦
        (∃ (h : v ∈ s),
            (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) = w) ∨
          ∃ (h : w ∈ s),
            (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v)
      (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hl)) : V) ∧
    ∀ (y : V),
      (fun (w : V) ↦
            (∃ (h : v ∈ s),
                (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) =
                  w) ∨
              ∃ (h : w ∈ s),
                (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v)
          y →
        y = (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hl)) : V)
⊢ ∃! w : V,
    (∃ (h : v ∈ s),
        (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) = w) ∨
      ∃ (h : w ∈ s),
        (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v

Tactic:
use f ⟨v, hl⟩

Premises used: Subtype.mk, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
v : V
hl : v ∈ s
h₁ :
  ∀ (y : V),
    ((↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v ⋯)) : V) = y ∨
        ∃ (h : y ∈ s),
          (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) y h)) : V) = v) →
      y = (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hl)) : V)
⊢ (fun (w : V) ↦
        (∃ (h : v ∈ s),
            (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) = w) ∨
          ∃ (h : w ∈ s),
            (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v)
      (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hl)) : V) ∧
    ∀ (y : V),
      (fun (w : V) ↦
            (∃ (h : v ∈ s),
                (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) =
                  w) ∨
              ∃ (h : w ∈ s),
                (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v)
          y →
        y = (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hl)) : V)

Tactic:
simp only [hl, exists_const, true_or, exists_true_left, true_and]

Premises used: true_or, exists_true_left, exists_const, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
v : V
hl : v ∈ s
⊢ Eq.{u_1 + 1} (α := V)
    (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v ⋯)) : V)
    (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hl)) : V)

Tactic:
rfl