awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
W₁ : Type u_2
W₂ : Type u_3
v : W₁ ⊕ W₂
val : W₁
h : s(Sum.inl val, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
refine_1 :
  ∀ (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)
⊢ 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, v)
have refine_1₁ : ∀ (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: cases v
Cleared hypotheses: v, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
W₁ : Type u_2
W₂ : Type u_3
v : W₁ ⊕ W₂
val : W₂
h : s(Sum.inr val, v) ∈ (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, v)
have 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)
Tactic: cases v
Cleared hypotheses: v, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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)
⊢ 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)
have 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)
Tactic: cases v
Cleared hypotheses: v, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
W₁ : Type u_2
W₂ : Type u_3
⊢ (completeBipartiteGraph W₁ W₂).edgeSet.encard = ENat.card W₁ * ENat.card W₂
have 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
Tactic: rw [edgeSet_completeBipartiteGraph, ← ENat.card_prod, ← Set.encard_univ, ← Set.image_univ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
hG : G.IsBipartiteWith s t
⊢ G.edgeSet.encard ≤ s.encard * t.encard
have 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
Tactic: grw [hG.edgeSetEmbeddingCompleteBipartiteGraph.encard_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
hG : G.IsBipartiteWith s t
⊢ G.edgeSet.encard ≤ s.encard * t.encard
have 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
Tactic: classical
  grw [hG.edgeSetEmbeddingCompleteBipartiteGraph.encard_le]
  simp [encard_edgeSet_completeBipartiteGraph]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsBipartite
⊢ 4 * G.edgeSet.encard ≤ HPow.hPow (β := ℕ) (ENat.card V) 2
have hv : Finite V
Tactic: refine finite_or_infinite V |>.elim (fun hv ↦ ?_) (fun _ ↦ by simp)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsBipartite
hv : Finite V
⊢ 4 * G.edgeSet.encard ≤ HPow.hPow (β := ℕ) (ENat.card V) 2
have have : ∀ (s t : Set V) (h : G.IsBipartiteWith s t), 4 * G.edgeSet.encard ≤ HPow.hPow (β := ℕ) (ENat.card V) 2
Tactic: have ⟨s, t, h⟩ := h.exists_isBipartiteWith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h_1 : G.IsBipartite
hv : Finite V
s t : Set V
h : G.IsBipartiteWith s t
⊢ 4 * G.edgeSet.encard ≤ HPow.hPow (β := ℕ) (ENat.card V) 2
have grw : 4 * (s.encard * t.encard) ≤ HPow.hPow (β := ℕ) (ENat.card V) 2
Tactic: grw [h.encard_edgeSet_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h_1 : G.IsBipartite
hv : Finite V
s t : Set V
h : G.IsBipartiteWith s t
⊢ 4 * (s.encard * t.encard) ≤ HPow.hPow (β := ℕ) (ENat.card V) 2
have this : s.encard + t.encard ≤ ENat.card V
Tactic: have := Set.encard_union_eq h.disjoint ▸ Set.encard_le_card
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ 4 * (s.encard * t.encard) ≤ HPow.hPow (β := ℕ) (ENat.card V) 2
have rw : ∀ (this : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞) ≤ (↑(Nat.card V) : ℕ∞)),
  4 * HMul.hMul (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞) ≤ HPow.hPow (α := ℕ∞) (β := ℕ) (↑(Nat.card V) : ℕ∞) 2
Tactic: rw [ENat.card_eq_coe_natCard, ← s.toFinite.cast_ncard_eq, ← t.toFinite.cast_ncard_eq] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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) : ℕ∞)
⊢ 4 * HMul.hMul (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞) ≤ HPow.hPow (α := ℕ∞) (β := ℕ) (↑(Nat.card V) : ℕ∞) 2
have norm_cast : ∀ (this : s.ncard + t.ncard ≤ Nat.card V), 4 * (s.ncard * t.ncard) ≤ HPow.hPow (β := ℕ) (Nat.card V) 2
Tactic: norm_cast at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ #G.bipartiteDoubleCover.edgeFinset = 2 * #G.edgeFinset
have 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
Tactic: rw [two_mul_card_edgeFinset, eq_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ 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
have 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
Tactic: apply card_bij (fun (v, w) _ ↦ s(.inl v, .inr w))
    (fun _ h ↦ by simpa using h) (by grind) (fun e he ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ ∃ (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
have 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)
Tactic: induction e with | _ v w
Cleared hypotheses: e, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
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
⊢ ∃ (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)
have he₁ : G.bipartiteDoubleCover.Adj v w
Tactic: rw [mem_edgeFinset, mem_edgeSet] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
⊢ completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G
have have : ∀ (this : Fintype α), completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G
Tactic: have : Fintype α := .ofFinite α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this : Fintype α
⊢ completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G
have have : ∀ (this : Fintype β), completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G
Tactic: have : Fintype β := .ofFinite β
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
⊢ completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G
have simp_rw : (∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))) ↔
  ∃ (left : Finset V) (right : Finset V),
    #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
Tactic: simp_rw [completeBipartiteGraph_isContained_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
⊢ (∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
      #left = Fintype.card α ∧
        #right = Fintype.card β ∧
          G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))) ↔
    ∃ (left : Finset V) (right : Finset V),
      #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
have refine_1 : (∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))) →
  ∀ (left right : Finset (V ⊕ V)) (card_left : #left = Fintype.card α) (card_right : #right = Fintype.card β)
    (h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))),
    ∃ (left : Finset V) (right : Finset V),
      #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
Tactic: refine ⟨fun ⟨left, right, card_left, card_right, h⟩ ↦ ?_,
    fun ⟨left, right, card_left, card_right, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
refine_1 :
  (∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
      #left = Fintype.card α ∧
        #right = Fintype.card β ∧
          G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))) →
    ∀ (left right : Finset (V ⊕ V)) (card_left : #left = Fintype.card α) (card_right : #right = Fintype.card β)
      (h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))),
      ∃ (left : Finset V) (right : Finset V),
        #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
⊢ (∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
      #left = Fintype.card α ∧
        #right = Fintype.card β ∧
          G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))) ↔
    ∃ (left : Finset V) (right : Finset V),
      #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
have refine_2 : (∃ (left : Finset V) (right : Finset V),
    #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)) →
  ∀ (left right : Finset V) (card_left : #left = Fintype.card α) (card_right : #right = Fintype.card β)
    (h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)),
    ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
      #left = Fintype.card α ∧
        #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
Tactic: refine ⟨fun ⟨left, right, card_left, card_right, h⟩ ↦ ?_,
    fun ⟨left, right, card_left, card_right, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
⊢ ∃ (left : Finset V) (right : Finset V),
    #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
have refine_1 : ∃ (left_1 : Finset V) (right_1 : Finset V),
  #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)
Tactic: simp_rw [← card_left, ← card_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
⊢ ∃ (left_1 : Finset V) (right_1 : Finset V),
    #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)
have refine_1 : ∀ (l : V ⊕ V) (hl : l ∈ left),
  ∃ (left_1 : Finset V) (right_1 : Finset V),
    #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)
Tactic: obtain ⟨l, hl⟩ : left.Nonempty := card_pos.mp <| card_pos.trans_le card_left.ge
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V ⊕ V
hl : l ∈ left
⊢ ∃ (left_1 : Finset V) (right_1 : Finset V),
    #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)
have refine_1 : ∀ (r : V ⊕ V) (hr : r ∈ right),
  ∃ (left_1 : Finset V) (right_1 : Finset V),
    #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)
Tactic: obtain ⟨r, hr⟩ : right.Nonempty := card_pos.mp <| card_pos.trans_le card_right.ge
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V ⊕ V
hl : l ∈ left
r : V ⊕ V
hr : r ∈ right
l' : V ⊕ V
hl' : l' ∈ left
⊢ (l.isLeft = true → l'.isLeft = true) ∧ (l.isRight = true → l'.isRight = true)
have inl : ∀ (l : V) (hl : Sum.inl l ∈ left),
  (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
Tactic: rcases l with l | l
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V ⊕ V
hl : l ∈ left
r : V ⊕ V
hr : r ∈ right
l' : V ⊕ V
hl' : l' ∈ left
inl :
  ∀ (l : V) (hl : Sum.inl l ∈ left),
    (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
⊢ (l.isLeft = true → l'.isLeft = true) ∧ (l.isRight = true → l'.isRight = true)
have inr : ∀ (l : V) (hl : Sum.inr l ∈ left),
  (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
Tactic: rcases l with l | l
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
r : V ⊕ V
hr : r ∈ right
l' : V ⊕ V
hl' : l' ∈ left
l : V
hl : Sum.inl l ∈ left
⊢ (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
have inl : ∀ (r : V) (hr : Sum.inl r ∈ right),
  (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
Tactic: rcases r with r | r
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
r : V ⊕ V
hr : r ∈ right
l' : V ⊕ V
hl' : l' ∈ left
l : V
hl : Sum.inl l ∈ left
inl :
  ∀ (r : V) (hr : Sum.inl r ∈ right),
    (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
⊢ (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
have inl₁ : ∀ (r : V) (hr : Sum.inr r ∈ right),
  (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
Tactic: rcases r with r | r
Cleared hypotheses: r, hr