awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (goal)
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
x_1 : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
pos :
  ∀ (hx : x ∈ s),
    (fun (n : Fin (Fintype.card X)) ↦
          (if hn : (↑n : ℕ) < #s then
              (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s) (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card.{u_1} ↥s))) : X)
            else (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ) ⟨(↑n : ℕ) - #s, ⋯⟩) : X) :
            X))
        ((fun (x : X) ↦
            (if hx : x ∈ s then
                Fin.castLE (n := Fintype.card.{u_1} ↥s) ⋯
                  ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
              else
                Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) ⋯
                  (Fin.addNat ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x ⋯))
                    #s) :
              Fin (Fintype.card X)))
          x) =
      x
⊢ (fun (n : Fin (Fintype.card X)) ↦
        (if hn : (↑n : ℕ) < #s then
            (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s) (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card.{u_1} ↥s))) : X)
          else (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ) ⟨(↑n : ℕ) - #s, ⋯⟩) : X) :
          X))
      ((fun (x : X) ↦
          (if hx : x ∈ s then
              Fin.castLE (n := Fintype.card.{u_1} ↥s) ⋯
                ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
            else
              Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) ⋯
                (Fin.addNat ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x ⋯))
                  #s) :
            Fin (Fintype.card X)))
        x) =
    x
have neg : ∀ (hx : x ∉ s),
  (fun (n : Fin (Fintype.card X)) ↦
        (if hn : (↑n : ℕ) < #s then
            (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s) (⟨(↑n : ℕ), sorry⟩ : Fin (Fintype.card.{u_1} ↥s))) : X)
          else (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ) ⟨(↑n : ℕ) - #s, sorry⟩) : X) :
          X))
      ((fun (x : X) ↦
          (if hx : x ∈ s then
              Fin.castLE (n := Fintype.card.{u_1} ↥s) sorry
                ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
            else
              Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) sorry
                (Fin.addNat ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x sorry))
                  #s) :
            Fin (Fintype.card X)))
        x) =
    x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (hypothesis)
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
x_1 : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
hx : x ∈ s
⊢ (fun (n : Fin (Fintype.card X)) ↦
        (if hn : (↑n : ℕ) < #s then
            (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s) (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card.{u_1} ↥s))) : X)
          else (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ) ⟨(↑n : ℕ) - #s, ⋯⟩) : X) :
          X))
      ((fun (x : X) ↦
          (if hx : x ∈ s then
              Fin.castLE (n := Fintype.card.{u_1} ↥s) ⋯
                ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
            else
              Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) ⋯
                (Fin.addNat ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x ⋯))
                  #s) :
            Fin (Fintype.card X)))
        x) =
    x
have this : (↑((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx)) : ℕ) < #s
Tactic: have : g ⟨x, hx⟩ < #s := by simpa using (g ⟨x, hx⟩).2
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (goal)
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
x : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
⊢ (fun (x : X) ↦
        (if hx : x ∈ s then
            Fin.castLE (n := Fintype.card.{u_1} ↥s) ⋯
              ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
          else
            Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) ⋯
              (Fin.addNat ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x ⋯)) #s) :
          Fin (Fintype.card X)))
      ((fun (n : Fin (Fintype.card X)) ↦
          (if hn : (↑n : ℕ) < #s then
              (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s) (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card.{u_1} ↥s))) : X)
            else (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ) ⟨(↑n : ℕ) - #s, ⋯⟩) : X) :
            X))
        n) =
    n
have inl : ∀ (hns : (↑n : ℕ) < #s),
  (fun (x : X) ↦
        (if hx : x ∈ s then
            Fin.castLE (n := Fintype.card.{u_1} ↥s) sorry
              ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
          else
            Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) sorry
              (Fin.addNat ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x sorry)) #s) :
          Fin (Fintype.card X)))
      ((fun (n : Fin (Fintype.card X)) ↦
          (if hn : (↑n : ℕ) < #s then
              (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s) (⟨(↑n : ℕ), sorry⟩ : Fin (Fintype.card.{u_1} ↥s))) : X)
            else (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ) ⟨(↑n : ℕ) - #s, sorry⟩) : X) :
            X))
        n) =
    n
Tactic: obtain hns | hsn := lt_or_ge n.1 #s
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (goal)
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
x : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
inl :
  ∀ (hns : (↑n : ℕ) < #s),
    (fun (x : X) ↦
          (if hx : x ∈ s then
              Fin.castLE (n := Fintype.card.{u_1} ↥s) ⋯
                ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
            else
              Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) ⋯
                (Fin.addNat ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x ⋯))
                  #s) :
            Fin (Fintype.card X)))
        ((fun (n : Fin (Fintype.card X)) ↦
            (if hn : (↑n : ℕ) < #s then
                (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s) (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card.{u_1} ↥s))) : X)
              else (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ) ⟨(↑n : ℕ) - #s, ⋯⟩) : X) :
              X))
          n) =
      n
⊢ (fun (x : X) ↦
        (if hx : x ∈ s then
            Fin.castLE (n := Fintype.card.{u_1} ↥s) ⋯
              ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
          else
            Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) ⋯
              (Fin.addNat ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x ⋯)) #s) :
          Fin (Fintype.card X)))
      ((fun (n : Fin (Fintype.card X)) ↦
          (if hn : (↑n : ℕ) < #s then
              (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s) (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card.{u_1} ↥s))) : X)
            else (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ) ⟨(↑n : ℕ) - #s, ⋯⟩) : X) :
            X))
        n) =
    n
have inr : ∀ (hsn : #s ≤ (↑n : ℕ)),
  (fun (x : X) ↦
        (if hx : x ∈ s then
            Fin.castLE (n := Fintype.card.{u_1} ↥s) sorry
              ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
          else
            Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) sorry
              (Fin.addNat ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x sorry)) #s) :
          Fin (Fintype.card X)))
      ((fun (n : Fin (Fintype.card X)) ↦
          (if hn : (↑n : ℕ) < #s then
              (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s) (⟨(↑n : ℕ), sorry⟩ : Fin (Fintype.card.{u_1} ↥s))) : X)
            else (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ) ⟨(↑n : ℕ) - #s, sorry⟩) : X) :
            X))
        n) =
    n
Tactic: obtain hns | hsn := lt_or_ge n.1 #s
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (goal)
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
x_1 : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
⊢ x ∈ s ↔
    (↑((({
                  toFun := fun (x : X) ↦
                    if hx : x ∈ s then
                      Fin.castLE (n := Fintype.card.{u_1} ↥s) ⋯
                        ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
                    else
                      Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) ⋯
                        (Fin.addNat
                          ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x ⋯)) #s),
                  invFun := fun (n : Fin (Fintype.card X)) ↦
                    if hn : (↑n : ℕ) < #s then
                      (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s)
                            (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card.{u_1} ↥s))) :
                        X)
                    else
                      (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ)
                            (⟨(↑n : ℕ) - #s, ⋯⟩ : Fin (Fintype.card.{u_1} ↥sᶜ))) :
                        X),
                  left_inv := ⋯, right_inv := ⋯ } :
                X ≃ Fin (Fintype.card X)) :
              (a : X) → Fin (Fintype.card X))
            x) :
        ℕ) <
      #s
have mp : x ∈ s →
  (↑((({
                toFun := fun (x : X) ↦
                  if hx : x ∈ s then
                    Fin.castLE (n := Fintype.card.{u_1} ↥s) sorry
                      ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
                  else
                    Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) sorry
                      (Fin.addNat
                        ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x sorry)) #s),
                invFun := fun (n : Fin (Fintype.card X)) ↦
                  if hn : (↑n : ℕ) < #s then
                    (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s)
                          (⟨(↑n : ℕ), sorry⟩ : Fin (Fintype.card.{u_1} ↥s))) :
                      X)
                  else
                    (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ)
                          (⟨(↑n : ℕ) - #s, sorry⟩ : Fin (Fintype.card.{u_1} ↥sᶜ))) :
                      X),
                left_inv := sorry, right_inv := sorry } :
              X ≃ Fin (Fintype.card X)) :
            (a : X) → Fin (Fintype.card X))
          x) :
      ℕ) <
    #s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (goal)
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
x_1 : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
⊢ (↑((({
                  toFun := fun (x : X) ↦
                    if hx : x ∈ s then
                      Fin.castLE (n := Fintype.card.{u_1} ↥s) ⋯
                        ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
                    else
                      Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) ⋯
                        (Fin.addNat
                          ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x ⋯)) #s),
                  invFun := fun (n : Fin (Fintype.card X)) ↦
                    if hn : (↑n : ℕ) < #s then
                      (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s)
                            (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card.{u_1} ↥s))) :
                        X)
                    else
                      (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ)
                            (⟨(↑n : ℕ) - #s, ⋯⟩ : Fin (Fintype.card.{u_1} ↥sᶜ))) :
                        X),
                  left_inv := ⋯, right_inv := ⋯ } :
                X ≃ Fin (Fintype.card X)) :
              (a : X) → Fin (Fintype.card X))
            x) :
        ℕ) <
      #s →
    x ∈ s
have pos : ∀ (hx : x ∈ s),
  (↑((({
                  toFun := fun (x : X) ↦
                    if hx : x ∈ s then
                      Fin.castLE (n := Fintype.card.{u_1} ↥s) sorry
                        ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
                    else
                      Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) sorry
                        (Fin.addNat
                          ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x sorry)) #s),
                  invFun := fun (n : Fin (Fintype.card X)) ↦
                    if hn : (↑n : ℕ) < #s then
                      (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s)
                            (⟨(↑n : ℕ), sorry⟩ : Fin (Fintype.card.{u_1} ↥s))) :
                        X)
                    else
                      (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ)
                            (⟨(↑n : ℕ) - #s, sorry⟩ : Fin (Fintype.card.{u_1} ↥sᶜ))) :
                        X),
                  left_inv := sorry, right_inv := sorry } :
                X ≃ Fin (Fintype.card X)) :
              (a : X) → Fin (Fintype.card X))
            x) :
        ℕ) <
      #s →
    x ∈ s
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (goal)
Goal:
X : Type u_1
inst : Fintype X
s t : Finset X
inst_1 : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
⊢ Disjoint (α := Finset (Numbering X)) (prefixed s) (prefixed t)
have simp : ∀ ⦃a : Numbering X⦄, a.IsPrefix s → ¬a.IsPrefix t
Tactic: simp only [Finset.disjoint_left, mem_prefixed]
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (goal)
Goal:
X : Type u_1
inst : Fintype X
s t : Finset X
inst_1 : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
hs : f.IsPrefix s
ht : f.IsPrefix t
⊢ False
have inl : ∀ (hst' : #s ≤ #t), False
Tactic: obtain hst' | hts' := Nat.le_total #s #t
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (goal)
Goal:
X : Type u_1
inst : Fintype X
s t : Finset X
inst_1 : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
hs : f.IsPrefix s
ht : f.IsPrefix t
inl : ∀ (hst' : #s ≤ #t), False
⊢ False
have inr : ∀ (hts' : #t ≤ #s), False
Tactic: obtain hst' | hts' := Nat.le_total #s #t
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M_1 M : Matroid α
inst : M.RankPos
⊢ M.Nonempty
have obtain : ∀ (B : Set α) (hB : M.IsBase B), M.Nonempty
Tactic: obtain ⟨B, hB⟩ := M.exists_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M_1 M : Matroid α
inst : M.RankPos
B : Set α
hB : M.IsBase B
⊢ M.Nonempty
have inl : ∀ (hB : M.IsBase ∅), M.Nonempty
Tactic: obtain rfl | ⟨e, heB⟩ := B.eq_empty_or_nonempty
Cleared hypotheses: B, hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M_1 M : Matroid α
inst : M.RankPos
B : Set α
hB : M.IsBase B
inl : ∀ (hB : M.IsBase ∅), M.Nonempty
⊢ M.Nonempty
have inr : ∀ (e : α) (heB : e ∈ B), M.Nonempty
Tactic: obtain rfl | ⟨e, heB⟩ := B.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
have inl : ∀ (he : B₂ \ B₁ = ∅), (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
Tactic: obtain (he | hinf | ⟨e, he, hcard⟩) :=
    (B₂ \ B₁).eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
inl : ∀ (he : B₂ \ B₁ = ∅), (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
have inr : ∀ (hinf : (B₂ \ B₁).encard = ⊤), (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
Tactic: obtain (he | hinf | ⟨e, he, hcard⟩) :=
    (B₂ \ B₁).eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
inl : ∀ (he : B₂ \ B₁ = ∅), (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
inr : ∀ (hinf : (B₂ \ B₁).encard = ⊤), (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
have inr₁ : ∀ (e : α) (he : e ∈ B₂ \ B₁) (hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard), (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
Tactic: obtain (he | hinf | ⟨e, he, hcard⟩) :=
    (B₂ \ B₁).eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
he : B₂ \ B₁ = ∅
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
have inl : (B₁ \ B₁).encard ≤ (B₁ \ B₁).encard
Tactic: rw [exch.antichain hB₂ hB₁ (diff_eq_empty.mp he)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
have inr : ∀ (f : α) (hf : f ∈ B₁ \ B₂) (hB' : IsBase (insert f (B₂ \ {e}))), (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
Tactic: obtain ⟨f, hf, hB'⟩ := exch B₂ B₁ hB₂ hB₁ e he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
have this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard
Tactic: have : encard (insert f (B₂ \ {e}) \ B₁) < encard (B₂ \ B₁) := by
    rw [insert_diff_of_mem _ hf.1, diff_diff_comm]; exact hcard
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
have hencard : (B₁ \ insert f (B₂ \ {e})).encard ≤ (insert f (B₂ \ {e}) \ B₁).encard
Tactic: have hencard := encard_diff_le_aux exch hB₁ hB'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard
hencard : (B₁ \ insert f (B₂ \ {e})).encard ≤ (insert f (B₂ \ {e}) \ B₁).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
have hencard₁ : ((B₁ \ B₂) \ {f}).encard ≤ ((B₂ \ B₁) \ {e}).encard
Tactic: rw [insert_diff_of_mem _ hf.1, diff_diff_comm, ← union_singleton, ← diff_diff, diff_diff_right,
    inter_singleton_eq_empty.mpr he.2, union_empty] at hencard
Cleared hypotheses: hencard
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard
hencard : ((B₁ \ B₂) \ {f}).encard ≤ ((B₂ \ B₁) \ {e}).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
have inr : ((B₁ \ B₂) \ {f}).encard + 1 ≤ ((B₂ \ B₁) \ {e}).encard + 1
Tactic: rw [← encard_diff_singleton_add_one he, ← encard_diff_singleton_add_one hf]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
⊢ B₁.encard = B₂.encard
have rw : (B₁ \ B₂).encard + (B₁ ∩ B₂).encard = B₂.encard
Tactic: rw [← encard_diff_add_encard_inter B₁ B₂, exch.encard_diff_eq hB₁ hB₂, inter_comm,
    encard_diff_add_encard_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
rw : (B₁ \ B₂).encard + (B₁ ∩ B₂).encard = B₂.encard
⊢ B₁.encard = B₂.encard
have rw₁ : (B₂ \ B₁).encard + (B₁ ∩ B₂).encard = B₂.encard
Tactic: rw [← encard_diff_add_encard_inter B₁ B₂, exch.encard_diff_eq hB₁ hB₂, inter_comm,
    encard_diff_add_encard_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
rw : (B₁ \ B₂).encard + (B₁ ∩ B₂).encard = B₂.encard
rw₁ : (B₂ \ B₁).encard + (B₁ ∩ B₂).encard = B₂.encard
⊢ B₁.encard = B₂.encard
have rw₂ : (B₂ \ B₁).encard + (B₂ ∩ B₁).encard = B₂.encard
Tactic: rw [← encard_diff_add_encard_inter B₁ B₂, exch.encard_diff_eq hB₁ hB₂, inter_comm,
    encard_diff_add_encard_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
rw : (B₁ \ B₂).encard + (B₁ ∩ B₂).encard = B₂.encard
rw₁ : (B₂ \ B₁).encard + (B₁ ∩ B₂).encard = B₂.encard
rw₂ : (B₂ \ B₁).encard + (B₂ ∩ B₁).encard = B₂.encard
⊢ B₁.encard = B₂.encard
have rw₃ : B₂.encard = B₂.encard
Tactic: rw [← encard_diff_add_encard_inter B₁ B₂, exch.encard_diff_eq hB₁ hB₂, inter_comm,
    encard_diff_add_encard_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ (B₁ \ B₂).ncard = (B₂ \ B₁).ncard
have rw : (B₁ \ B₂).encard.toNat = (B₂ \ B₁).ncard
Tactic: rw [ncard_def, hB₁.encard_diff_comm hB₂, ← ncard_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
rw : (B₁ \ B₂).encard.toNat = (B₂ \ B₁).ncard
⊢ (B₁ \ B₂).ncard = (B₂ \ B₁).ncard
have rw₁ : (B₂ \ B₁).encard.toNat = (B₂ \ B₁).ncard
Tactic: rw [ncard_def, hB₁.encard_diff_comm hB₂, ← ncard_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
rw : (B₁ \ B₂).encard.toNat = (B₂ \ B₁).ncard
rw₁ : (B₂ \ B₁).encard.toNat = (B₂ \ B₁).ncard
⊢ (B₁ \ B₂).ncard = (B₂ \ B₁).ncard
have rw₂ : (B₂ \ B₁).ncard = (B₂ \ B₁).ncard
Tactic: rw [ncard_def, hB₁.encard_diff_comm hB₂, ← ncard_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ B₁.encard = B₂.encard
have rw : B₂.encard = B₂.encard
Tactic: rw [M.isBase_exchange.encard_isBase_eq hB₁ hB₂]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ B₁.ncard = B₂.ncard
have rw : B₁.encard.toNat = B₂.ncard
Tactic: rw [ncard_def B₁, hB₁.encard_eq_encard_of_isBase hB₂, ← ncard_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
rw : B₁.encard.toNat = B₂.ncard
⊢ B₁.ncard = B₂.ncard
have rw₁ : B₂.encard.toNat = B₂.ncard
Tactic: rw [ncard_def B₁, hB₁.encard_eq_encard_of_isBase hB₂, ← ncard_def]