awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
have refine_5 : C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x
Tactic: refine ⟨C', hC'ss.trans ?_, hC', hzC'⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x
have refine_5 : ∀ (i : ι), Disjoint (C i \ {x i}) (range x)
Tactic: refine union_subset (diff_subset_diff_left subset_union_left)
      (iUnion_subset fun i ↦ subset_diff.2
        ⟨diff_subset.trans (subset_union_of_subset_right (subset_iUnion ..) _), ?_⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
i : ι
⊢ Disjoint (C i \ {x i}) (range x)
have refine_5 : ∀ ⦃a : α⦄, a ∈ C i \ {x i} → ∀ ⦃b : α⦄, b ∈ range x → a ≠ b
Tactic: rw [disjoint_iff_forall_ne]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
i j : ι
he : x j ∈ C i \ {x i}
⊢ False
have he₁ : x j ∈ C j \ {x j}
Tactic: obtain rfl : j = i := h_unique he.1
Cleared hypotheses: i, he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
⊢ M.IsCircuit (C₀ \ range x ∪ range x)
have refine_2 : range x ⊆ C₀
Tactic: rwa [diff_union_self, union_eq_self_of_subset_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
⊢ ∀ (i : ι), z ∉ (fun (i : ι) ↦ C i \ {x i}) i
have refine_4 : ∀ (i : ι), z ∈ C i → z = x i
Tactic: simp only [mem_diff, mem_singleton_iff, not_and, not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hX : ∀ x ∈ X, ∃ C ∈ S, C ∩ X = {x}
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
have choose! : ∀ (C : (x : α) → Set α) (hC : ∀ x ∈ X, C x ∈ S ∧ C x ∩ X = {x}), ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
Tactic: choose! C hC using hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : (x : α) → Set α
hC : ∀ x ∈ X, C x ∈ S ∧ C x ∩ X = {x}
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
have hC₁ : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
Tactic: simp only [forall_and] at hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
have refine_6 : ∀
  (hwin :
    ∃
      C' ⊆
        (C₀ ∪ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) \
          range fun (x : (↑X : Type u_1)) ↦ (↑x : α),
      M.IsCircuit C' ∧ z ∈ C'),
  ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
Tactic: have hwin := hC₀.strong_multi_elimination (fun x : X ↦ x) (fun x ↦ C x) z ?_ ?_ ?_ ?_ hzC₀ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
refine_6 :
  ∀
    (hwin :
      ∃
        C' ⊆
          (C₀ ∪ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) \
            range fun (x : (↑X : Type u_1)) ↦ (↑x : α),
        M.IsCircuit C' ∧ z ∈ C'),
    ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
have refine_1 : ∀ (i : (↑X : Type u_1)), M.IsCircuit ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i)
Tactic: have hwin := hC₀.strong_multi_elimination (fun x : X ↦ x) (fun x ↦ C x) z ?_ ?_ ?_ ?_ hzC₀ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
refine_6 :
  ∀
    (hwin :
      ∃
        C' ⊆
          (C₀ ∪ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) \
            range fun (x : (↑X : Type u_1)) ↦ (↑x : α),
        M.IsCircuit C' ∧ z ∈ C'),
    ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
refine_1 : ∀ (i : (↑X : Type u_1)), M.IsCircuit ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i)
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
have refine_2 : ∀ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i ∈ C₀
Tactic: have hwin := hC₀.strong_multi_elimination (fun x : X ↦ x) (fun x ↦ C x) z ?_ ?_ ?_ ?_ hzC₀ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
refine_6 :
  ∀
    (hwin :
      ∃
        C' ⊆
          (C₀ ∪ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) \
            range fun (x : (↑X : Type u_1)) ↦ (↑x : α),
        M.IsCircuit C' ∧ z ∈ C'),
    ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
refine_1 : ∀ (i : (↑X : Type u_1)), M.IsCircuit ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i)
refine_2 : ∀ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i ∈ C₀
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
have refine_3 : ∀ (i : (↑X : Type u_1)),
  Membership.mem (γ := Set α) ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) ((fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i)
Tactic: have hwin := hC₀.strong_multi_elimination (fun x : X ↦ x) (fun x ↦ C x) z ?_ ?_ ?_ ?_ hzC₀ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
refine_6 :
  ∀
    (hwin :
      ∃
        C' ⊆
          (C₀ ∪ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) \
            range fun (x : (↑X : Type u_1)) ↦ (↑x : α),
        M.IsCircuit C' ∧ z ∈ C'),
    ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
refine_1 : ∀ (i : (↑X : Type u_1)), M.IsCircuit ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i)
refine_2 : ∀ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i ∈ C₀
refine_3 :
  ∀ (i : (↑X : Type u_1)),
    Membership.mem (γ := Set α) ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) ((fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i)
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
have refine_4 : ∀ ⦃i i' : (↑X : Type u_1)⦄,
  Membership.mem (γ := Set α) ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i') ((fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i) →
    i = i'
Tactic: have hwin := hC₀.strong_multi_elimination (fun x : X ↦ x) (fun x ↦ C x) z ?_ ?_ ?_ ?_ hzC₀ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
refine_6 :
  ∀
    (hwin :
      ∃
        C' ⊆
          (C₀ ∪ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) \
            range fun (x : (↑X : Type u_1)) ↦ (↑x : α),
        M.IsCircuit C' ∧ z ∈ C'),
    ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
refine_1 : ∀ (i : (↑X : Type u_1)), M.IsCircuit ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i)
refine_2 : ∀ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i ∈ C₀
refine_3 :
  ∀ (i : (↑X : Type u_1)),
    Membership.mem (γ := Set α) ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) ((fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i)
refine_4 :
  ∀ ⦃i i' : (↑X : Type u_1)⦄,
    Membership.mem (γ := Set α) ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i')
        ((fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i) →
      i = i'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
have refine_5 : ∀ (i : (↑X : Type u_1)), z ∉ (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i
Tactic: have hwin := hC₀.strong_multi_elimination (fun x : X ↦ x) (fun x ↦ C x) z ?_ ?_ ?_ ?_ hzC₀ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
hwin :
  ∃
    C' ⊆
      (C₀ ∪ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) \
        range fun (x : (↑X : Type u_1)) ↦ (↑x : α),
    M.IsCircuit C' ∧ z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
have refine_6 : ∀ (C' : Set α)
  (hC'ss :
    C' ⊆
      (C₀ ∪ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) \
        range fun (x : (↑X : Type u_1)) ↦ (↑x : α))
  (hC' : M.IsCircuit C') (hz : z ∈ C'), ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
Tactic: obtain ⟨C', hC'ss, hC', hz⟩ := hwin
Cleared hypotheses: hwin
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz_1 : ∀ C ∈ S, z ∉ C
C : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
C' : Set α
hC'ss :
  C' ⊆
    (C₀ ∪ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) \
      range fun (x : (↑X : Type u_1)) ↦ (↑x : α)
hC' : M.IsCircuit C'
hz : z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
have refine_6 : ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i ⊆ ⋃₀ S
Tactic: refine ⟨C', hC'ss.trans (diff_subset_diff (union_subset_union_right _ ?_) (by simp)), hC', hz⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
⊢ ∀ (i : (↑X : Type u_1)),
    Membership.mem (γ := Set α) ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) ((fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i)
have refine_3 : ∀ (a : α) (b : a ∈ X), {a} ⊆ C a
Tactic: simp only [Subtype.forall, ← singleton_subset_iff (s := C _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
⊢ ∀ ⦃i i' : (↑X : Type u_1)⦄,
    Membership.mem (γ := Set α) ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i')
        ((fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i) →
      i = i'
have refine_4 : ∀ (a : α) (b : a ∈ X) (a_1 : α) (b : a_1 ∈ X), a ∈ C a_1 → a = a_1
Tactic: simp only [Subtype.forall, Subtype.mk.injEq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C ∧ f ∈ C
have obtain : ∀ (C : Set α) (hCs : C ⊆ (C₁ ∪ ⋃ (i : Unit), C₂) \ range fun (i : Unit) ↦ e) (hC : M.IsCircuit C) (hfC : f ∈ C),
  ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C ∧ f ∈ C
Tactic: obtain ⟨C, hCs, hC, hfC⟩ := hC₁.strong_multi_elimination (fun i : Unit ↦ e) (fun _ ↦ C₂) f
    (by simpa) (by simpa) (by simpa) (by simp) (by simpa) (by simpa)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
have hnss : ¬C₁ ⊆ C₂
Tactic: have hnss : ¬ (C₁ ⊆ C₂) := fun hss ↦ h <| hC₁.eq_of_subset_isCircuit hC₂ hss
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
have obtain : ∀ (f : α) (hf₁ : f ∈ C₁) (hf₂ : f ∉ C₂), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
Tactic: obtain ⟨f, hf₁, hf₂⟩ := not_subset.1 hnss
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
have pos : ∀ (he₁ : e ∈ C₁), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
Tactic: by_cases he₁ : e ∈ C₁
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
pos : ∀ (he₁ : e ∈ C₁), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
have neg : ∀ (he₁ : e ∉ C₁), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
Tactic: by_cases he₁ : e ∈ C₁
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
have pos : ∀ (he₂ : e ∈ C₂), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
Tactic: by_cases he₂ : e ∈ C₂
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
pos : ∀ (he₂ : e ∈ C₂), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
have neg : ∀ (he₂ : e ∉ C₂), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
Tactic: by_cases he₂ : e ∈ C₂
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
he₂ : e ∈ C₂
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
have pos : ∀ (C : Set α) (hC : C ⊆ (C₁ ∪ C₂) \ {e}) (hC' : M.IsCircuit C), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
Tactic: obtain ⟨C, hC, hC', -⟩ := hC₁.strong_elimination hC₂ he₁ he₂ hf₁ hf₂
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
C : Set α
inst : M.Finitary
hC : M.IsCircuit C
⊢ C.Finite
have hi : ¬M.Indep C
Tactic: have hi := hC.dep.not_indep
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
C : Set α
inst : M.Finitary
hC : M.IsCircuit C
hi : ¬M.Indep C
⊢ C.Finite
have hi₁ : ¬∀ J ⊆ C, J.Finite → M.Indep J
Tactic: rw [indep_iff_forall_finite_subset_indep] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
C : Set α
inst : M.Finitary
hC : M.IsCircuit C
hi : ¬∀ J ⊆ C, J.Finite → M.Indep J
⊢ C.Finite
have hi₁ : ∃ J ⊆ C, J.Finite ∧ ¬M.Indep J
Tactic: push Not at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
inst : M.Finitary
hC : M.IsCircuit C
hi : ∃ J ⊆ C, J.Finite ∧ ¬M.Indep J
⊢ C.Finite
have obtain : ∀ (J : Set α) (hJC : J ⊆ C) (hJfin : J.Finite) (hJ : ¬M.Indep J), C.Finite
Tactic: obtain ⟨J, hJC, hJfin, hJ⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.Finitary ↔ ∀ (C : Set α), M.IsCircuit C → C.Finite
have refine_1 : ∀ (h : ∀ (C : Set α), M.IsCircuit C → C.Finite) (I : Set α) (hI : ∀ J ⊆ I, J.Finite → M.Indep J) (hd : M.Dep I), False
Tactic: refine ⟨fun _ _ ↦ IsCircuit.finite, fun h ↦
    ⟨fun I hI ↦ indep_iff_not_dep.2 ⟨fun hd ↦ ?_,fun x hx ↦ ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
refine_1 :
  ∀ (h : ∀ (C : Set α), M.IsCircuit C → C.Finite) (I : Set α) (hI : ∀ J ⊆ I, J.Finite → M.Indep J) (hd : M.Dep I), False
⊢ M.Finitary ↔ ∀ (C : Set α), M.IsCircuit C → C.Finite
have refine_2 : ∀ (h : ∀ (C : Set α), M.IsCircuit C → C.Finite) (I : Set α) (hI : ∀ J ⊆ I, J.Finite → M.Indep J) (x : α) (hx : x ∈ I),
  x ∈ M.E
Tactic: refine ⟨fun _ _ ↦ IsCircuit.finite, fun h ↦
    ⟨fun I hI ↦ indep_iff_not_dep.2 ⟨fun hd ↦ ?_,fun x hx ↦ ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
⊢ False
have refine_1 : ∀ (C : Set α) (hCI : C ⊆ I) (hC : M.IsCircuit C), False
Tactic: obtain ⟨C, hCI, hC⟩ := hd.exists_isCircuit_subset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst : M.Finitary
he : e ∈ M.closure X
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
have pos : ∀ (heY : e ∈ X), ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
Tactic: by_cases heY : e ∈ X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst : M.Finitary
he : e ∈ M.closure X
pos : ∀ (heY : e ∈ X), ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
have neg : ∀ (heY : e ∉ X), ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
Tactic: by_cases heY : e ∈ X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
have pos : ∀ (J : Set α) (hJ : M.IsBasis J {e}), ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
Tactic: obtain ⟨J, hJ⟩ := M.exists_isBasis {e}
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst : M.Finitary
he : e ∈ M.closure X
heY : e ∉ X
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
have neg : ∀ (C : Set α) (hCs : C ⊆ insert e X) (hC : M.IsCircuit C) (heC : e ∈ C), ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
Tactic: obtain ⟨C, hCs, hC, heC⟩ := exists_isCircuit_of_mem_closure he heY
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
inst : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
aux : ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I
have obtain : ∀ (T : Set α) (hT : T ⊆ Y) (hTfin : T.Finite) (hXT : X ⊆ M.closure T), ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I
Tactic: obtain ⟨T, hT, hTfin, hXT⟩ := aux
Cleared hypotheses: aux
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
inst : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
T : Set α
hT : T ⊆ Y
hTfin : T.Finite
hXT : X ⊆ M.closure T
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I
have obtain : ∀ (I : Set α) (hI : M.IsBasis' I T), ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis' T
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
inst : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I
have suffices : ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T
Tactic: suffices aux : ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T by
    obtain ⟨T, hT, hTfin, hXT⟩ := aux
    obtain ⟨I, hI⟩ := M.exists_isBasis' T
    exact ⟨_, hI.subset.trans hT, hTfin.subset hI.subset, hI.indep, by rwa [hI.closure_eq_closure]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
inst : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
⊢ ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T
have refine : ∀ {e : α} {Z : Set α} (heX : e ∈ X),
  Z ⊆ X →
    ∀ (heZ : e ∉ Z),
      (∃ T ⊆ Y, T.Finite ∧ Z ⊆ M.closure T) →
        ∀ (T : Set α) (hTY : T ⊆ Y) (hTfin : T.Finite) (hT : Z ⊆ M.closure T),
          ∃ T ⊆ Y, T.Finite ∧ insert e Z ⊆ M.closure T
Tactic: refine Finite.induction_on_subset X hX ⟨∅, by simp⟩ (fun {e Z} heX _ heZ ⟨T, hTY, hTfin, hT⟩ ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
inst : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
e : α
Z : Set α
heX : e ∈ X
h : Z ⊆ X
heZ : e ∉ Z
h_1 : ∃ T ⊆ Y, T.Finite ∧ Z ⊆ M.closure T
T : Set α
hTY : T ⊆ Y
hTfin : T.Finite
hT : Z ⊆ M.closure T
⊢ ∃ T ⊆ Y, T.Finite ∧ insert e Z ⊆ M.closure T
have obtain : ∀ (S : Set α) (hSY : S ⊆ Y) (hSfin : S.Finite) (heS : e ∈ M.closure S), ∃ T ⊆ Y, T.Finite ∧ insert e Z ⊆ M.closure T
Tactic: obtain ⟨S, hSY, hSfin, -, heS⟩ := exists_mem_finite_closure_of_mem_closure (hXY heX)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ M✶.IsCocircuit C
have rwa : M✶✶.IsCircuit C
Tactic: rwa [isCocircuit_def, dual_dual]