awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
simp :
  ∀ (a : ι) (b : α a),
    Sigma.mk (β := fun (a : ι) ↦ α a) a b ∈ B₁ →
      Sigma.mk (β := fun (a : ι) ↦ α a) a b ∉ B₂ →
        ∃ (a_3 : ι) (b_1 : α a_3),
          (Sigma.mk (β := fun (a : ι) ↦ α a) a_3 b_1 ∈ B₂ ∧ Sigma.mk (β := fun (a : ι) ↦ α a) a_3 b_1 ∉ B₁) ∧
            ∀ (i : ι),
              (M i).IsBase
                (Sigma.mk (β := α) i ⁻¹'
                  insert (Sigma.mk (β := fun (a : ι) ↦ α a) a_3 b_1) (B₁ \ {Sigma.mk (β := fun (a : ι) ↦ α a) a b}))
⊢ ∀ a ∈ B₁ \ B₂,
    ∃ b ∈ B₂ \ B₁,
      (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) (insert b (B₁ \ {a}))

Tactic:
simp only [mem_diff, Sigma.exists, and_imp, Sigma.forall]

Premises used: Sigma.exists, and_imp, Sigma.forall, Set.mem_diff
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
⊢ e ∉ Sigma.mk (β := α) i ⁻¹' B₂

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
⊢ ∃ y ∈ Sigma.mk (β := α) i ⁻¹' B₂ \ Sigma.mk (β := α) i ⁻¹' B₁,
    (M i).IsBase (insert y (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))

Tactic:
have hf_ex := (h₁ i).exchange (h₂ i) ⟨he₁, by simpa⟩
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
hf_ex :
  ∃ y ∈ Sigma.mk (β := α) i ⁻¹' B₂ \ Sigma.mk (β := α) i ⁻¹' B₁,
    (M i).IsBase (insert y (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
obtain :
  ∀ (f : α i) (hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))) (hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂)
    (hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁),
    ∃ (a : ι) (b : α a),
      (Sigma.mk (β := fun (a : ι) ↦ α a) a b ∈ B₂ ∧ Sigma.mk (β := fun (a : ι) ↦ α a) a b ∉ B₁) ∧
        ∀ (i_1 : ι),
          (M i_1).IsBase
            (Sigma.mk (β := α) i_1 ⁻¹'
              insert (Sigma.mk (β := fun (a : ι) ↦ α a) a b) (B₁ \ {Sigma.mk (β := fun (a : ι) ↦ α a) i e}))
⊢ ∃ (a : ι) (b : α a),
    (Sigma.mk (β := fun (a : ι) ↦ α a) a b ∈ B₂ ∧ Sigma.mk (β := fun (a : ι) ↦ α a) a b ∉ B₁) ∧
      ∀ (i_1 : ι),
        (M i_1).IsBase
          (Sigma.mk (β := α) i_1 ⁻¹'
            insert (Sigma.mk (β := fun (a : ι) ↦ α a) a b) (B₁ \ {Sigma.mk (β := fun (a : ι) ↦ α a) i e}))

Tactic:
obtain ⟨f, ⟨hf₁, hf₂⟩, hfB⟩ := hf_ex
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
⊢ ∃ (a : ι) (b : α a),
    (Sigma.mk (β := fun (a : ι) ↦ α a) a b ∈ B₂ ∧ Sigma.mk (β := fun (a : ι) ↦ α a) a b ∉ B₁) ∧
      ∀ (i_1 : ι),
        (M i_1).IsBase
          (Sigma.mk (β := α) i_1 ⁻¹'
            insert (Sigma.mk (β := fun (a : ι) ↦ α a) a b) (B₁ \ {Sigma.mk (β := fun (a : ι) ↦ α a) i e}))

Tactic:
⟨i, f, ⟨hf₁, hf₂⟩, fun j ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
refine :
  ∀ (j : ι),
    (M j).IsBase
      (Sigma.mk (β := α) j ⁻¹'
        insert (Sigma.mk (β := fun (a : ι) ↦ α a) i f) (B₁ \ {Sigma.mk (β := fun (a : ι) ↦ α a) i e}))
⊢ ∃ (a : ι) (b : α a),
    (Sigma.mk (β := fun (a : ι) ↦ α a) a b ∈ B₂ ∧ Sigma.mk (β := fun (a : ι) ↦ α a) a b ∉ B₁) ∧
      ∀ (i_1 : ι),
        (M i_1).IsBase
          (Sigma.mk (β := α) i_1 ⁻¹'
            insert (Sigma.mk (β := fun (a : ι) ↦ α a) a b) (B₁ \ {Sigma.mk (β := fun (a : ι) ↦ α a) i e}))

Tactic:
refine ⟨i, f, ⟨hf₁, hf₂⟩, fun j ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
j : ι
rw :
  (M j).IsBase
    (Sigma.mk (β := α) j ⁻¹' B₁ \ Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i e} ∪
      Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i f})
⊢ (M j).IsBase
    (Sigma.mk (β := α) j ⁻¹'
      insert (Sigma.mk (β := fun (a : ι) ↦ α a) i f) (B₁ \ {Sigma.mk (β := fun (a : ι) ↦ α a) i e}))

Tactic:
rw [← union_singleton, preimage_union, preimage_diff]

Premises used: Set.preimage_union, Set.union_singleton, Set.preimage_diff
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
j : ι
inl :
  (M i).IsBase
    (Sigma.mk (β := α) i ⁻¹' B₁ \ Sigma.mk (β := α) i ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i e} ∪
      Sigma.mk (β := α) i ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i f})
inr :
  ∀ (hne : i ≠ j),
    (M j).IsBase
      (Sigma.mk (β := α) j ⁻¹' B₁ \ Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i e} ∪
        Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i f})
⊢ (M j).IsBase
    (Sigma.mk (β := α) j ⁻¹' B₁ \ Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i e} ∪
      Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i f})

Tactic:
obtain (rfl | hne) := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
⊢ ∀ (x : ?m.254 i),
    Eq.{max (u_1 + 1) (?u.2855 + 1)} (α := Set.{max u_1 ?u.2855} (Sigma ?m.254))
      (singleton.{max u_1 ?u.2855, max u_1 ?u.2855} (Sigma.mk (β := ?m.254) i x))
      (image.{?u.2855, max u_1 ?u.2855} (Sigma.mk (β := ?m.254) i) {x})

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
⊢ (M i).IsBase
    (Sigma.mk (β := α) i ⁻¹' B₁ \ Sigma.mk (β := α) i ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i e} ∪
      Sigma.mk (β := α) i ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i f})

Tactic:
simpa only [show ∀ x, {⟨i,x⟩} = Sigma.mk i '' {x} by simp,
        preimage_image_eq _ sigma_mk_injective, union_singleton]

Premises used: Set.preimage_image_eq, Set.union_singleton, sigma_mk_injective
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
j : ι
hne : i ≠ j
⊢ Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ range (Sigma.mk (β := α) j)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
j : ι
hne : i ≠ j
⊢ Sigma.mk (β := fun (a : ι) ↦ α a) i f ∉ range (Sigma.mk (β := α) j)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
j : ι
hne : i ≠ j
inr : (M j).IsBase (Sigma.mk (β := α) j ⁻¹' B₁)
⊢ (M j).IsBase
    (Sigma.mk (β := α) j ⁻¹' B₁ \ Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i e} ∪
      Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i f})

Tactic:
rw [preimage_singleton_eq_empty.2 (by simpa), preimage_singleton_eq_empty.2 (by simpa),
      diff_empty, union_empty]

Premises used: Iff.mpr, Set.union_empty, Set.diff_empty, Set.preimage_singleton_eq_empty
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
j : ι
hne : i ≠ j
⊢ (M j).IsBase (Sigma.mk (β := α) j ⁻¹' B₁)

Tactic:
h₁ j
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
j : ι
hne : i ≠ j
⊢ (M j).IsBase (Sigma.mk (β := α) j ⁻¹' B₁)

Tactic:
exact h₁ j
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
choose :
  ∀ (Js : (i : ι) → Set (α i))
    (hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i),
    ∃ (J : Set ((i : ι) × α i)),
      I ⊆ J ∧
        Maximal
          (fun (K : Set ((i : ι) × α i)) ↦
            (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) K ∧ K ⊆ X)
          J
⊢ ∃ (J : Set ((i : ι) × α i)),
    I ⊆ J ∧
      Maximal
        (fun (K : Set ((i : ι) × α i)) ↦
          (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) K ∧ K ⊆ X)
        J

Tactic:
choose Js hJs using
      fun i ↦ (hI i).subset_isBasis'_of_subset (preimage_mono (f := Sigma.mk i) hIX)

Premises used: Matroid.Indep.subset_isBasis'_of_subset, Set.preimage_mono
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h_1 : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
h :
  I ⊆ Set.sigma (α := α) univ Js ∧
    Maximal
      (fun (K : Set ((i : ι) × α i)) ↦
        (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) K ∧ K ⊆ X)
      (Set.sigma (α := α) univ Js)
⊢ ∃ (J : Set ((i : ι) × α i)),
    I ⊆ J ∧
      Maximal
        (fun (K : Set ((i : ι) × α i)) ↦
          (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) K ∧ K ⊆ X)
        J

Tactic:
use univ.sigma Js

Premises used: Set.univ, Set.sigma
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h_1 : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
h :
  I ⊆ Set.sigma (α := α) univ Js ∧
    ((∀ (i : ι), (M i).Indep (Js i)) ∧ Set.sigma (α := α) univ Js ⊆ X) ∧
      ∀ ⦃t : Set ((i : ι) × α i)⦄,
        (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) →
          t ⊆ X → Set.sigma (α := α) univ Js ⊆ t → t ⊆ Set.sigma (α := α) univ Js
⊢ I ⊆ Set.sigma (α := α) univ Js ∧
    Maximal
      (fun (K : Set ((i : ι) × α i)) ↦
        (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) K ∧ K ⊆ X)
      (Set.sigma (α := α) univ Js)

Tactic:
simp only [maximal_subset_iff', mem_univ, mk_preimage_sigma, and_imp]

Premises used: and_imp, Set.mk_preimage_sigma, Set.mem_univ, maximal_subset_iff'
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
⊢ I ⊆ Set.sigma (α := α) univ Js ∧
    ((∀ (i : ι), (M i).Indep (Js i)) ∧ Set.sigma (α := α) univ Js ⊆ X) ∧
      ∀ ⦃t : Set ((i : ι) × α i)⦄,
        (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) →
          t ⊆ X → Set.sigma (α := α) univ Js ⊆ t → t ⊆ Set.sigma (α := α) univ Js

Tactic:
⟨?_, ⟨fun i ↦ (hJs i).1.indep, ?_⟩, fun S hS hSX hJS ↦ ?_⟩

Premises used: Matroid.IsBasis'.indep, And.left, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h_1 : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
h : I ⊆ Set.sigma (α := α) univ Js
h₁ : Set.sigma (α := α) univ Js ⊆ X
h₂ :
  ∀ (S : Set ((i : ι) × α i)) (hS : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' S)) (hSX : S ⊆ X)
    (hJS : Set.sigma (α := α) univ Js ⊆ S), S ⊆ Set.sigma (α := α) univ Js
⊢ I ⊆ Set.sigma (α := α) univ Js ∧
    ((∀ (i : ι), (M i).Indep (Js i)) ∧ Set.sigma (α := α) univ Js ⊆ X) ∧
      ∀ ⦃t : Set ((i : ι) × α i)⦄,
        (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) →
          t ⊆ X → Set.sigma (α := α) univ Js ⊆ t → t ⊆ Set.sigma (α := α) univ Js

Tactic:
refine ⟨?_, ⟨fun i ↦ (hJs i).1.indep, ?_⟩, fun S hS hSX hJS ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h_1 : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
h :
  (Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' I) ⊆
    Set.sigma (α := α) univ Js
⊢ I ⊆ Set.sigma (α := α) univ Js

Tactic:
rw [← univ_sigma_preimage_mk I]

Premises used: Set.univ_sigma_preimage_mk
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
⊢ (Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' I) ⊆
    Set.sigma (α := α) univ Js

Tactic:
sigma_mono rfl.subset fun i ↦ (hJs i).2

Premises used: Eq.subset, And.right, Set.sigma_mono, rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
⊢ (Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' I) ⊆
    Set.sigma (α := α) univ Js

Tactic:
exact sigma_mono rfl.subset fun i ↦ (hJs i).2

Premises used: Eq.subset, And.right, Set.sigma_mono, rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h_1 : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
h :
  Set.sigma (α := α) univ Js ⊆
    Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' X
⊢ Set.sigma (α := α) univ Js ⊆ X

Tactic:
rw [← univ_sigma_preimage_mk X]

Premises used: Set.univ_sigma_preimage_mk
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
⊢ Set.sigma (α := α) univ Js ⊆
    Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' X

Tactic:
sigma_mono rfl.subset fun i ↦ (hJs i).1.subset

Premises used: Eq.subset, And.left, Matroid.IsBasis'.subset, Set.sigma_mono, rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
⊢ Set.sigma (α := α) univ Js ⊆
    Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' X

Tactic:
exact sigma_mono rfl.subset fun i ↦ (hJs i).1.subset

Premises used: Eq.subset, And.left, Matroid.IsBasis'.subset, Set.sigma_mono, rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h_1 : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' S)
hSX : S ⊆ X
hJS : Set.sigma (α := α) univ Js ⊆ S
h :
  (Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' S) ⊆
    Set.sigma (α := α) univ Js
⊢ S ⊆ Set.sigma (α := α) univ Js

Tactic:
rw [← univ_sigma_preimage_mk S]

Premises used: Set.univ_sigma_preimage_mk