awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
W₁ : Type u_2
W₂ : Type u_3
v : W₁ ⊕ W₂
val : W₂
h : s(Sum.inr val, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
refine_1 :
  ∀ (val_1 : W₁) (h : s(Sum.inr val, Sum.inl val_1) ∈ (completeBipartiteGraph W₁ W₂).edgeSet),
    Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2))
      s(Sum.inr val, Sum.inl val_1)
refine_1₁ :
  ∀ (val_1 : W₂) (h : s(Sum.inr val, Sum.inr val_1) ∈ (completeBipartiteGraph W₁ W₂).edgeSet),
    Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2))
      s(Sum.inr val, Sum.inr val_1)
⊢ Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2))
    s(Sum.inr val, v)

Tactic:
cases v
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
W₁ : Type u_2
W₂ : Type u_3
val val_1 : W₁
h : s(Sum.inl val, Sum.inl val_1) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2))
    s(Sum.inl val, Sum.inl val_1)

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
W₁ : Type u_2
W₂ : Type u_3
val : W₁
val_1 : W₂
h : s(Sum.inl val, Sum.inr val_1) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2))
    s(Sum.inl val, Sum.inr val_1)

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
W₁ : Type u_2
W₂ : Type u_3
val : W₂
val_1 : W₁
h : s(Sum.inr val, Sum.inl val_1) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2))
    s(Sum.inr val, Sum.inl val_1)

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
W₁ : Type u_2
W₂ : Type u_3
val val_1 : W₂
h : s(Sum.inr val, Sum.inr val_1) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2))
    s(Sum.inr val, Sum.inr val_1)

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
W₁ : Type u_2
W₂ : Type u_3
u v : W₁ ⊕ W₂
h : Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2)) s(u, v)
a : W₁
b : W₂
z : (fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2)) (a, b) = s(u, v)
⊢ s(u, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet

Tactic:
grind [completeBipartiteGraph_adj, mem_edgeSet]

Premises used: completeBipartiteGraph_adj, SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
W₁ : Type u_2
W₂ : Type u_3
rw :
  Set.encard (α := Sym2 (W₁ ⊕ W₂)) ((fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2)) '' Set.univ) =
    Set.encard (α := W₁ × W₂) Set.univ
⊢ (completeBipartiteGraph W₁ W₂).edgeSet.encard = ENat.card W₁ * ENat.card W₂

Tactic:
rw [edgeSet_completeBipartiteGraph, ← ENat.card_prod, ← Set.encard_univ, ← Set.image_univ]

Premises used: Set.image_univ, ENat.card_prod, SimpleGraph.edgeSet_completeBipartiteGraph, Set.encard_univ
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
W₁ : Type u_2
W₂ : Type u_3
⊢ Function.Injective (β := Sym2 (W₁ ⊕ W₂)) fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2)

Tactic:
grind [Function.Injective]

Premises used: Function.Injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
W₁ : Type u_2
W₂ : Type u_3
⊢ Set.encard (α := Sym2 (W₁ ⊕ W₂)) ((fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2)) '' Set.univ) =
    Set.encard (α := W₁ × W₂) Set.univ

Tactic:
exact Function.Injective.encard_image (by grind [Function.Injective]) Set.univ

Premises used: Set.univ, Function.Injective.encard_image
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
W₁ : Type u_2
W₂ : Type u_3
inst : DecidableRel fun (x1 : V) (x2 : Set V) ↦ x1 ∈ x2
hG : G.IsBipartiteWith s t
x : (↑G.edgeSet : Type u_1)
e : Sym2 V
he : e ∈ G.edgeSet
x_1 x_2 : V
⊢ (s(x_1, x_2) ∈ G.edgeSet) = (s(x_2, x_1) ∈ G.edgeSet)

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
W₁ : Type u_2
W₂ : Type u_3
inst : DecidableRel fun (x1 : V) (x2 : Set V) ↦ x1 ∈ x2
hG : G.IsBipartiteWith s t
x : (↑G.edgeSet : Type u_1)
e : Sym2 V
he : e ∈ G.edgeSet
x_1 x_2 : V
⊢ ∀ (a : s(x_1, x_2) ∈ G.edgeSet) (a' : s(x_2, x_1) ∈ G.edgeSet),
    a ≍ a' →
      HEq.{u_1 + 1} (α := (↑(edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) : Type u_1))
        (⋯.by_cases
          (fun (h : (x_1, x_2).1 ∈ s ∧ (x_1, x_2).2 ∈ t) ↦
            Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
              Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
                (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
              s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) x_1 ⋯),
                Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x_2 ⋯))
              ⋯)
          fun (h : (x_1, x_2).1 ∈ t ∧ (x_1, x_2).2 ∈ s) ↦
          Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
            Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
              (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
            s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) x_2 ⋯),
              Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x_1 ⋯))
            ⋯)
        (β := (↑(edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) : Type u_1))
        (⋯.by_cases
          (fun (h : (x_2, x_1).1 ∈ s ∧ (x_2, x_1).2 ∈ t) ↦
            Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
              Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
                (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
              s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) x_2 ⋯),
                Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x_1 ⋯))
              ⋯)
          fun (h : (x_2, x_1).1 ∈ t ∧ (x_2, x_1).2 ∈ s) ↦
          Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
            Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
              (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
            s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) x_1 ⋯),
              Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x_2 ⋯))
            ⋯)

Tactic:
grind [Or.by_cases, hG.disjoint]

Premises used: SimpleGraph.IsBipartiteWith.disjoint, Or.by_cases
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
W₁ : Type u_2
W₂ : Type u_3
inst : DecidableRel fun (x1 : V) (x2 : Set V) ↦ x1 ∈ x2
hG : G.IsBipartiteWith s t
val : Sym2 V
a : V × V
property : Quot.mk (Sym2.Rel V) a ∈ G.edgeSet
val_1 : Sym2 V
a_1 : V × V
property_1 : Quot.mk (Sym2.Rel V) a_1 ∈ G.edgeSet
⊢ Eq.{u_1 + 1} (α := (↑(edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) : Type u_1))
      (if x : (a.1, a.2).1 ∈ s ∧ (a.1, a.2).2 ∈ t then
        Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
          Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
            (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
          s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) a.1 ⋯),
            Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) a.2 ⋯))
          ⋯
      else
        Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
          Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
            (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
          s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) a.2 ⋯),
            Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) a.1 ⋯))
          ⋯)
      (if x : (a_1.1, a_1.2).1 ∈ s ∧ (a_1.1, a_1.2).2 ∈ t then
        Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
          Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
            (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
          s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) a_1.1 ⋯),
            Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) a_1.2 ⋯))
          ⋯
      else
        Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
          Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
            (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
          s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) a_1.2 ⋯),
            Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) a_1.1 ⋯))
          ⋯) →
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a) property =
      Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a_1) property_1

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
hG : G.IsBipartiteWith s t
grw :
  Set.encard.{u_1} (α := Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1)))
      (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) ≤
    s.encard * t.encard
⊢ G.edgeSet.encard ≤ s.encard * t.encard

Tactic:
grw [hG.edgeSetEmbeddingCompleteBipartiteGraph.encard_le]

Premises used: Function.Embedding.encard_le, SimpleGraph.IsBipartiteWith.edgeSetEmbeddingCompleteBipartiteGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
hG : G.IsBipartiteWith s t
⊢ Set.encard.{u_1} (α := Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1)))
      (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) ≤
    s.encard * t.encard

Tactic:
simp [encard_edgeSet_completeBipartiteGraph]

Premises used: SimpleGraph.encard_edgeSet_completeBipartiteGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
hG : G.IsBipartiteWith s t
grw grw₁ grw₂ :
  Set.encard.{u_1} (α := Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1)))
      (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) ≤
    s.encard * t.encard
⊢ G.edgeSet.encard ≤ s.encard * t.encard

Tactic:
classical
  grw [hG.edgeSetEmbeddingCompleteBipartiteGraph.encard_le]
  simp [encard_edgeSet_completeBipartiteGraph]

Premises used: SimpleGraph.encard_edgeSet_completeBipartiteGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsBipartite
h_1 : Infinite V
⊢ 4 * G.edgeSet.encard ≤ HPow.hPow (β := ℕ) (ENat.card V) 2

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsBipartite
⊢ Finite V

Tactic:
refine finite_or_infinite V |>.elim (fun hv ↦ ?_) (fun _ ↦ by simp)

Premises used: finite_or_infinite, Or.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsBipartite
hv : Finite V
have : ∀ (s t : Set V) (h : G.IsBipartiteWith s t), 4 * G.edgeSet.encard ≤ HPow.hPow (β := ℕ) (ENat.card V) 2
⊢ 4 * G.edgeSet.encard ≤ HPow.hPow (β := ℕ) (ENat.card V) 2

Tactic:
have ⟨s, t, h⟩ := h.exists_isBipartiteWith
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
h_1 : G.IsBipartite
hv : Finite V
s t : Set V
h : G.IsBipartiteWith s t
grw : 4 * (s.encard * t.encard) ≤ HPow.hPow (β := ℕ) (ENat.card V) 2
⊢ 4 * G.edgeSet.encard ≤ HPow.hPow (β := ℕ) (ENat.card V) 2

Tactic:
grw [h.encard_edgeSet_le]

Premises used: SimpleGraph.IsBipartiteWith.encard_edgeSet_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
h_1 : G.IsBipartite
hv : Finite V
s t : Set V
h : G.IsBipartiteWith s t
⊢ s.encard + t.encard ≤ ENat.card V

Tactic:
have := Set.encard_union_eq h.disjoint ▸ Set.encard_le_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
h_1 : G.IsBipartite
hv : Finite V
s t : Set V
h : G.IsBipartiteWith s t
this : s.encard + t.encard ≤ ENat.card V
rw :
  ∀ (this : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞) ≤ (↑(Nat.card V) : ℕ∞)),
    4 * HMul.hMul (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞) ≤ HPow.hPow (α := ℕ∞) (β := ℕ) (↑(Nat.card V) : ℕ∞) 2
⊢ 4 * (s.encard * t.encard) ≤ HPow.hPow (β := ℕ) (ENat.card V) 2

Tactic:
rw [ENat.card_eq_coe_natCard, ← s.toFinite.cast_ncard_eq, ← t.toFinite.cast_ncard_eq] at this ⊢

Premises used: Set.toFinite, Set.Finite.cast_ncard_eq, ENat.card_eq_coe_natCard
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
h_1 : G.IsBipartite
hv : Finite V
s t : Set V
h : G.IsBipartiteWith s t
this : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞) ≤ (↑(Nat.card V) : ℕ∞)
norm_cast : ∀ (this : s.ncard + t.ncard ≤ Nat.card V), 4 * (s.ncard * t.ncard) ≤ HPow.hPow (β := ℕ) (Nat.card V) 2
⊢ 4 * HMul.hMul (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞) ≤ HPow.hPow (α := ℕ∞) (β := ℕ) (↑(Nat.card V) : ℕ∞) 2

Tactic:
norm_cast at this ⊢
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
h_1 : G.IsBipartite
hv : Finite V
s t : Set V
h : G.IsBipartiteWith s t
this : s.ncard + t.ncard ≤ Nat.card V
⊢ 4 * (s.ncard * t.ncard) ≤ HPow.hPow (β := ℕ) (Nat.card V) 2

Tactic:
grind [Nat.pow_le_pow_left this 2, four_mul_le_sq_add s.ncard t.ncard]

Premises used: four_mul_le_sq_add, Set.ncard, OfNat.ofNat, Nat.pow_le_pow_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v w : V
G_1 : SimpleGraph V
s t : Set V
G : SimpleGraph V
x x_1 : V ⊕ V
⊢ (fun (x x_2 : V ⊕ V) ↦
        (match (motive := V ⊕ V → V ⊕ V → Prop) x, x_2 with
          | Sum.inl v', Sum.inr w' => G.Adj v' w'
          | Sum.inr v', Sum.inl w' => G.Adj v' w'
          | x, x_3 => False :
          Prop))
      x x_1 →
    (fun (x x_2 : V ⊕ V) ↦
        (match (motive := V ⊕ V → V ⊕ V → Prop) x, x_2 with
          | Sum.inl v', Sum.inr w' => G.Adj v' w'
          | Sum.inr v', Sum.inl w' => G.Adj v' w'
          | x, x_3 => False :
          Prop))
      x_1 x

Tactic:
grind [adj_symm]

Premises used: SimpleGraph.adj_symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
v w : V ⊕ V
val val_1 : V
hadj : G.bipartiteDoubleCover.Adj (Sum.inl val) (Sum.inr val_1)
⊢ (completeBipartiteGraph V V).Adj (Sum.inl val) (Sum.inr val_1)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
v w : V ⊕ V
val val_1 : V
hadj : G.bipartiteDoubleCover.Adj (Sum.inr val) (Sum.inl val_1)
⊢ (completeBipartiteGraph V V).Adj (Sum.inr val) (Sum.inl val_1)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
v w : V ⊕ V
val val_1 : V
hadj : G.bipartiteDoubleCover.Adj (Sum.inl val) (Sum.inl val_1)
⊢ (completeBipartiteGraph V V).Adj (Sum.inl val) (Sum.inl val_1)

Tactic:
simp at hadj
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
v w : V ⊕ V
val val_1 : V
hadj : G.bipartiteDoubleCover.Adj (Sum.inr val) (Sum.inr val_1)
⊢ (completeBipartiteGraph V V).Adj (Sum.inr val) (Sum.inr val_1)

Tactic:
simp at hadj
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
rw :
  Finset.card.{u_1} (α := V × V)
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (x, y) => G.Adj x y} =
    #G.bipartiteDoubleCover.edgeFinset
⊢ #G.bipartiteDoubleCover.edgeFinset = 2 * #G.edgeFinset

Tactic:
rw [two_mul_card_edgeFinset, eq_comm]

Premises used: SimpleGraph.two_mul_card_edgeFinset, eq_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
x : V × V
h :
  Membership.mem (γ := Finset (V × V))
    {x : V × V |
      match (motive := V × V → Prop) x with
      | (x, y) => G.Adj x y}
    x
⊢ (fun (x : V × V)
          (x_1 :
            Membership.mem (γ := Finset (V × V))
              {x : V × V |
                match (motive := V × V → Prop) x with
                | (x, y) => G.Adj x y}
              x) ↦
        (match (motive :=
            (x : V × V) →
              Membership.mem (γ := Finset (V × V))
                  {x : V × V |
                    match (motive := V × V → Prop) x with
                    | (x, y) => G.Adj x y}
                  x →
                Sym2 (V ⊕ V))
            x, x_1 with
          | (v, w), x => s(Sum.inl v, Sum.inr w) :
          Sym2 (V ⊕ V)))
      x h ∈
    G.bipartiteDoubleCover.edgeFinset

Tactic:
simpa using h
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ ∀ (a₁ : V × V)
    (ha₁ :
      Membership.mem (γ := Finset (V × V))
        {x : V × V |
          match (motive := V × V → Prop) x with
          | (x, y) => G.Adj x y}
        a₁)
    (a₂ : V × V)
    (ha₂ :
      Membership.mem (γ := Finset (V × V))
        {x : V × V |
          match (motive := V × V → Prop) x with
          | (x, y) => G.Adj x y}
        a₂),
    Eq.{u_1 + 1} (α := Sym2 (V ⊕ V))
        ((fun (x : V × V)
              (x_1 :
                Membership.mem (γ := Finset (V × V))
                  {x : V × V |
                    match (motive := V × V → Prop) x with
                    | (x, y) => G.Adj x y}
                  x) ↦
            (match (motive :=
                (x : V × V) →
                  Membership.mem (γ := Finset (V × V))
                      {x : V × V |
                        match (motive := V × V → Prop) x with
                        | (x, y) => G.Adj x y}
                      x →
                    Sym2 (V ⊕ V))
                x, x_1 with
              | (v, w), x => s(Sum.inl v, Sum.inr w) :
              Sym2 (V ⊕ V)))
          a₁ ha₁)
        ((fun (x : V × V)
              (x_1 :
                Membership.mem (γ := Finset (V × V))
                  {x : V × V |
                    match (motive := V × V → Prop) x with
                    | (x, y) => G.Adj x y}
                  x) ↦
            (match (motive :=
                (x : V × V) →
                  Membership.mem (γ := Finset (V × V))
                      {x : V × V |
                        match (motive := V × V → Prop) x with
                        | (x, y) => G.Adj x y}
                      x →
                    Sym2 (V ⊕ V))
                x, x_1 with
              | (v, w), x => s(Sum.inl v, Sum.inr w) :
              Sym2 (V ⊕ V)))
          a₂ ha₂) →
      a₁ = a₂

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
apply :
  ∀ (e : Sym2 (V ⊕ V)) (he : e ∈ G.bipartiteDoubleCover.edgeFinset),
    ∃ (a : V × V) (ha :
      Membership.mem (γ := Finset (V × V))
        {x : V × V |
          match (motive := V × V → Prop) x with
          | (x, y) => G.Adj x y}
        a),
      (fun (x : V × V)
              (x_1 :
                Membership.mem (γ := Finset (V × V))
                  {x : V × V |
                    match (motive := V × V → Prop) x with
                    | (x, y) => G.Adj x y}
                  x) ↦
            (match (motive :=
                (x : V × V) →
                  Membership.mem (γ := Finset (V × V))
                      {x : V × V |
                        match (motive := V × V → Prop) x with
                        | (x, y) => G.Adj x y}
                      x →
                    Sym2 (V ⊕ V))
                x, x_1 with
              | (v, w), x => s(Sum.inl v, Sum.inr w) :
              Sym2 (V ⊕ V)))
          a ha =
        e
⊢ Finset.card.{u_1} (α := V × V)
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (x, y) => G.Adj x y} =
    #G.bipartiteDoubleCover.edgeFinset

Tactic:
apply card_bij (fun (v, w) _ ↦ s(.inl v, .inr w))
    (fun _ h ↦ by simpa using h) (by grind) (fun e he ↦ ?_)

Premises used: Finset.card_bij
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
e : Sym2 (V ⊕ V)
he : e ∈ G.bipartiteDoubleCover.edgeFinset
h :
  ∀ (v w : V ⊕ V) (he : s(v, w) ∈ G.bipartiteDoubleCover.edgeFinset),
    ∃ (a : V × V) (ha :
      Membership.mem (γ := Finset (V × V))
        {x : V × V |
          match (motive := V × V → Prop) x with
          | (x, y) => G.Adj x y}
        a),
      (fun (x : V × V)
              (x_1 :
                Membership.mem (γ := Finset (V × V))
                  {x : V × V |
                    match (motive := V × V → Prop) x with
                    | (x, y) => G.Adj x y}
                  x) ↦
            (match (motive :=
                (x : V × V) →
                  Membership.mem (γ := Finset (V × V))
                      {x : V × V |
                        match (motive := V × V → Prop) x with
                        | (x, y) => G.Adj x y}
                      x →
                    Sym2 (V ⊕ V))
                x, x_1 with
              | (v, w), x => s(Sum.inl v, Sum.inr w) :
              Sym2 (V ⊕ V)))
          a ha =
        s(v, w)
⊢ ∃ (a : V × V) (ha :
    Membership.mem (γ := Finset (V × V))
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (x, y) => G.Adj x y}
      a),
    (fun (x : V × V)
            (x_1 :
              Membership.mem (γ := Finset (V × V))
                {x : V × V |
                  match (motive := V × V → Prop) x with
                  | (x, y) => G.Adj x y}
                x) ↦
          (match (motive :=
              (x : V × V) →
                Membership.mem (γ := Finset (V × V))
                    {x : V × V |
                      match (motive := V × V → Prop) x with
                      | (x, y) => G.Adj x y}
                    x →
                  Sym2 (V ⊕ V))
              x, x_1 with
            | (v, w), x => s(Sum.inl v, Sum.inr w) :
            Sym2 (V ⊕ V)))
        a ha =
      e

Tactic:
induction e with | _ v w
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v w : V ⊕ V
he : s(v, w) ∈ G.bipartiteDoubleCover.edgeFinset
⊢ G.bipartiteDoubleCover.Adj v w

Tactic:
rw [mem_edgeFinset, mem_edgeSet] at he

Premises used: SimpleGraph.mem_edgeFinset, SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v w : V ⊕ V
val val_1 : V
he : G.bipartiteDoubleCover.Adj (Sum.inl val) (Sum.inr val_1)
⊢ ∃ (a : V × V) (ha :
    Membership.mem (γ := Finset (V × V))
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (x, y) => G.Adj x y}
      a),
    (fun (x : V × V)
            (x_1 :
              Membership.mem (γ := Finset (V × V))
                {x : V × V |
                  match (motive := V × V → Prop) x with
                  | (x, y) => G.Adj x y}
                x) ↦
          (match (motive :=
              (x : V × V) →
                Membership.mem (γ := Finset (V × V))
                    {x : V × V |
                      match (motive := V × V → Prop) x with
                      | (x, y) => G.Adj x y}
                    x →
                  Sym2 (V ⊕ V))
              x, x_1 with
            | (v, w), x => s(Sum.inl v, Sum.inr w) :
            Sym2 (V ⊕ V)))
        a ha =
      s(Sum.inl val, Sum.inr val_1)

Tactic:
simpa using he