awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h :
  (∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X) ∧
    (∀ (x : ι) ⦃t : Set (α x)⦄,
        (M x).Indep t → t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t) ∧
      ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E
hIX : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X
h' :
  ∀ (x : ι) ⦃t : Set (α x)⦄,
    (M x).Indep t → t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t
h'' : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E
refine_4 :
  ∀ (J : Set ((i : ι) × α i)) (hJ : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' J)) (hJX : J ⊆ X) (hIJ : I ⊆ J)
    (x : (i : ι) × α i) (i : ι) (x : α i) (hx : Sigma.mk (β := fun (i : ι) ↦ α i) i x ∈ J),
    Sigma.mk (β := fun (i : ι) ↦ α i) i x ∈ I
⊢ ∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t

Tactic:
refine fun J hJ hJX hIJ ↦ hIJ.antisymm fun ⟨i,x⟩ hx ↦ ?_
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h :
  (∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X) ∧
    (∀ (x : ι) ⦃t : Set (α x)⦄,
        (M x).Indep t → t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t) ∧
      ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E
hIX : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X
h' :
  ∀ (x : ι) ⦃t : Set (α x)⦄,
    (M x).Indep t → t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t
h'' : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E
J : Set ((i : ι) × α i)
hJ : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' J)
hJX : J ⊆ X
hIJ : I ⊆ J
x_1 : (i : ι) × α i
i : ι
x : α i
hx : Sigma.mk (β := fun (i : ι) ↦ α i) i x ∈ J
⊢ Sigma.mk (β := fun (i : ι) ↦ α i) i x ∈ I

Tactic:
simpa using (h' i (hJ i) (preimage_mono hJX) (preimage_mono hIJ)).symm.subset hx

Premises used: Eq.subset, Set.preimage_mono, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h :
  (∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X) ∧
    (∀ (x : ι) ⦃t : Set (α x)⦄,
        (M x).Indep t → t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t) ∧
      ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E
hIX : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X
h' :
  ∀ (x : ι) ⦃t : Set (α x)⦄,
    (M x).Indep t → t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t
h'' : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E
x_1 : (i : ι) × α i
i : ι
x : α i
hx : Sigma.mk (β := fun (i : ι) ↦ α i) i x ∈ X
⊢ Membership.mem (γ := Set ((i : ι) × α i)) (Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E)
    (Sigma.mk (β := fun (i : ι) ↦ α i) i x)

Tactic:
simpa using h'' i hx
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h :
  (∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X) ∧
    (∀ (x : ι) ⦃t : Set (α x)⦄,
        (M x).Indep t → t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t) ∧
      ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E
hIX : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X
h' :
  ∀ (x : ι) ⦃t : Set (α x)⦄,
    (M x).Indep t → t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t
h'' : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E
⊢ X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E

Tactic:
exact fun ⟨i,x⟩ hx ↦ by simpa using h'' i hx
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
⊢ (Matroid.sigma (α := α) M).Finitary

Tactic:
⟨fun I hI ↦ ?_⟩

Premises used: Matroid.Finitary.mk
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
refine :
  ∀ (I : Set ((i : ι) × α i)) (hI : ∀ J ⊆ I, J.Finite → (Matroid.sigma (α := α) M).Indep J),
    (Matroid.sigma (α := α) M).Indep I
⊢ (Matroid.sigma (α := α) M).Finitary

Tactic:
refine ⟨fun I hI ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → (Matroid.sigma (α := α) M).Indep J
⊢ ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' J)

Tactic:
simp only [sigma_indep_iff] at hI ⊢

Premises used: Matroid.sigma_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' J)
i : ι
h₁ : ∀ J ⊆ Sigma.mk (β := α) i ⁻¹' I, J.Finite → (M i).Indep J
⊢ (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)

Tactic:
apply indep_of_forall_finite_subset_indep

Premises used: Matroid.indep_of_forall_finite_subset_indep
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' J)
i : ι
J : Set (α i)
hJI : J ⊆ Sigma.mk (β := α) i ⁻¹' I
hJ : J.Finite
⊢ Sigma.mk (β := fun (i : ι) ↦ α i) i '' J ⊆ I

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' J)
i : ι
J : Set (α i)
hJI : J ⊆ Sigma.mk (β := α) i ⁻¹' I
hJ : J.Finite
h₁ : J = Sigma.mk (β := α) i ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' J
⊢ (M i).Indep J

Tactic:
convert! hI (Sigma.mk i '' J) (by simpa) (hJ.image _) i

Premises used: Set.Finite.image, Set.image, Sigma.mk
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' J)
i : ι
J : Set (α i)
hJI : J ⊆ Sigma.mk (β := α) i ⁻¹' I
hJ : J.Finite
h₁ h₂ : J = J
⊢ J = Sigma.mk (β := α) i ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' J

Tactic:
rw [sigma_mk_preimage_image_eq_self]

Premises used: sigma_mk_preimage_image_eq_self
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
simp :
  (∀ (i : ι),
      (M i).Indep
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I))) ↔
    ∀ (i : ι), (M i).Indep (Prod.mk i ⁻¹' I)
⊢ (Matroid.sum' M).Indep I ↔ ∀ (i : ι), (M i).Indep (Prod.mk i ⁻¹' I)

Tactic:
simp only [Matroid.sum', mapEquiv_indep_iff, Equiv.sigmaEquivProd_symm_apply, sigma_indep_iff]

Premises used: Matroid.sum', Equiv.sigmaEquivProd_symm_apply, Matroid.mapEquiv_indep_iff, Matroid.sigma_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
⊢ (∀ (i : ι),
      (M i).Indep
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I))) ↔
    ∀ (i : ι),
      (M i).Indep
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I))

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
h :
  ∀ (a : ι),
    Prod.mk a ⁻¹' I =
      preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
        ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I)
⊢ (∀ (i : ι),
      (M i).Indep
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I))) ↔
    ∀ (i : ι), (M i).Indep (Prod.mk i ⁻¹' I)

Tactic:
convert! Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
a : ι
h :
  ∀ (x : α),
    x ∈ Prod.mk a ⁻¹' I ↔
      Membership.mem (γ := Set α)
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
            ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I) :
          Set α)
        x
⊢ Prod.mk a ⁻¹' I =
    preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
      ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I)

Tactic:
ext
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
a : ι
x : α
⊢ x ∈ Prod.mk a ⁻¹' I ↔
    Membership.mem (γ := Set α)
      (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I) :
        Set α)
      x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : ∀ (x : ι × α), x ∈ (Matroid.sum' M).E ↔ Membership.mem (γ := Set (ι × α)) (⋃ (i : ι), Prod.mk i '' (M i).E) x
⊢ (Matroid.sum' M).E = ⋃ (i : ι), Prod.mk i '' (M i).E

Tactic:
ext
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
x : ι × α
⊢ x ∈ (Matroid.sum' M).E ↔ Membership.mem (γ := Set (ι × α)) (⋃ (i : ι), Prod.mk i '' (M i).E) x

Tactic:
simp [Matroid.sum']

Premises used: Matroid.sum'
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
simp :
  (∀ (i : ι),
      (M i).IsBase
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' B))) ↔
    ∀ (i : ι), (M i).IsBase (Prod.mk i ⁻¹' B)
⊢ (Matroid.sum' M).IsBase B ↔ ∀ (i : ι), (M i).IsBase (Prod.mk i ⁻¹' B)

Tactic:
simp only [Matroid.sum', mapEquiv_isBase_iff, Equiv.sigmaEquivProd_symm_apply, sigma_isBase_iff]

Premises used: Matroid.sum', Equiv.sigmaEquivProd_symm_apply, Matroid.sigma_isBase_iff, Matroid.mapEquiv_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
⊢ (∀ (i : ι),
      (M i).IsBase
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' B))) ↔
    ∀ (i : ι),
      (M i).IsBase
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' B))

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
h :
  ∀ (a : ι),
    Prod.mk a ⁻¹' B =
      preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
        ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' B)
⊢ (∀ (i : ι),
      (M i).IsBase
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' B))) ↔
    ∀ (i : ι), (M i).IsBase (Prod.mk i ⁻¹' B)

Tactic:
convert! Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
a : ι
h :
  ∀ (x : α),
    x ∈ Prod.mk a ⁻¹' B ↔
      Membership.mem (γ := Set α)
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
            ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' B) :
          Set α)
        x
⊢ Prod.mk a ⁻¹' B =
    preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
      ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' B)

Tactic:
ext
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
a : ι
x : α
⊢ x ∈ Prod.mk a ⁻¹' B ↔
    Membership.mem (γ := Set α)
      (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' B) :
        Set α)
      x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
simp :
  (∀ (i : ι),
      (M i).IsBasis
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I))
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' X))) ↔
    ∀ (i : ι), (M i).IsBasis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)
⊢ (Matroid.sum' M).IsBasis I X ↔ ∀ (i : ι), (M i).IsBasis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)

Tactic:
simp only [Matroid.sum', mapEquiv_isBasis_iff, Equiv.sigmaEquivProd_symm_apply, sigma_isBasis_iff]

Premises used: Matroid.sigma_isBasis_iff, Matroid.sum', Equiv.sigmaEquivProd_symm_apply, Matroid.mapEquiv_isBasis_iff
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
⊢ (∀ (i : ι),
      (M i).IsBasis
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I))
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' X))) ↔
    ∀ (i : ι),
      (M i).IsBasis
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I))
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' X))

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
h :
  ∀ (a : ι),
    Prod.mk a ⁻¹' I =
      preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
        ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I)
h₁ :
  ∀ (a : ι),
    Prod.mk a ⁻¹' X =
      preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
        ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' X)
⊢ (∀ (i : ι),
      (M i).IsBasis
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I))
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' X))) ↔
    ∀ (i : ι), (M i).IsBasis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)

Tactic:
convert! Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
a : ι
⊢ ∀ (x : α),
    x ∈ Prod.mk a ⁻¹' I ↔
      Membership.mem (γ := Set α)
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
            ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I) :
          Set α)
        x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
a : ι
⊢ Prod.mk a ⁻¹' I =
    preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
      ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I)

Tactic:
exact ext <| by simp

Premises used: Set.ext
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
a : ι
⊢ ∀ (x : α),
    x ∈ Prod.mk a ⁻¹' X ↔
      Membership.mem (γ := Set α)
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
            ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' X) :
          Set α)
        x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
a : ι
⊢ Prod.mk a ⁻¹' X =
    preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
      ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' X)

Tactic:
exact ext <| by simp

Premises used: Set.ext
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : ∀ (i : ι), (M i).Finitary
⊢ (Matroid.sigma (α := fun (i : ι) ↦ α) M).Finitary

Tactic:
have := Finitary.sigma h
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : ∀ (i : ι), (M i).Finitary
this : (Matroid.sigma (α := fun (i : ι) ↦ α) M).Finitary
⊢ ((Matroid.sigma (α := fun (i : ι) ↦ α) M).mapEquiv (Equiv.sigmaEquivProd ι α)).Finitary

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise.{u_2} (α := ι) (Function.onFun.{u_2 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (M i).E)
h₁ : ∀ (x : α), x ∈ (Matroid.disjointSigma M h).E ↔ Membership.mem (γ := Set α) (⋃ (i : ι), (M i).E) x
⊢ (Matroid.disjointSigma M h).E = ⋃ (i : ι), (M i).E

Tactic:
ext
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise.{u_2} (α := ι) (Function.onFun.{u_2 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (M i).E)
x : α
⊢ x ∈ (Matroid.disjointSigma M h).E ↔ Membership.mem (γ := Set α) (⋃ (i : ι), (M i).E) x

Tactic:
simp [Matroid.disjointSigma, mapEmbedding, restrictSubtype]

Premises used: Matroid.mapEmbedding, Matroid.disjointSigma, Matroid.restrictSubtype
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise.{u_2} (α := ι) (Function.onFun.{u_2 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (M i).E)
I : Set α
⊢ (Matroid.disjointSigma M h).Indep I ↔ (∀ (i : ι), (M i).Indep (I ∩ (M i).E)) ∧ I ⊆ ⋃ (i : ι), (M i).E

Tactic:
simp [Matroid.disjointSigma, (Function.Embedding.sigmaSet_preimage h)]

Premises used: Matroid.disjointSigma, Function.Embedding.sigmaSet_preimage
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise.{u_2} (α := ι) (Function.onFun.{u_2 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (M i).E)
B : Set α
⊢ (Matroid.disjointSigma M h).IsBase B ↔ (∀ (i : ι), (M i).IsBase (B ∩ (M i).E)) ∧ B ⊆ ⋃ (i : ι), (M i).E

Tactic:
simp [Matroid.disjointSigma, (Function.Embedding.sigmaSet_preimage h)]

Premises used: Matroid.disjointSigma, Function.Embedding.sigmaSet_preimage
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise.{u_2} (α := ι) (Function.onFun.{u_2 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (M i).E)
I X : Set α
⊢ (Matroid.disjointSigma M h).IsBasis I X ↔
    (∀ (i : ι), (M i).IsBasis (I ∩ (M i).E) (X ∩ (M i).E)) ∧ I ⊆ X ∧ X ⊆ ⋃ (i : ι), (M i).E

Tactic:
simp [Matroid.disjointSigma, Function.Embedding.sigmaSet_preimage h]

Premises used: Matroid.disjointSigma, Function.Embedding.sigmaSet_preimage
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
⊢ (M.sum N).E = Sum.inl '' M.E ∪ Sum.inr '' N.E

Tactic:
simp [Matroid.sum, Set.ext_iff, mapEquiv, mapEmbedding, Equiv.ulift, Equiv.sumEquivSigmaBool]

Premises used: Matroid.mapEmbedding, Matroid.mapEquiv, Equiv.ulift, Set.ext_iff, Equiv.sumEquivSigmaBool, Matroid.sum
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : Set (α ⊕ β)
simp :
  M.Indep
        (image (α := bif false then ULift.{u, v} β else ULift.{v, u} α)
          (fun (a : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
            ((Equiv.ulift : (a : bif false then ULift.{u, v} β else ULift.{v, u} α) → α) a : α))
          (preimage (β := (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
              (Sigma.mk (β := fun (i : Bool) ↦ bif i then ULift.{u, v} β else ULift.{v, u} α) false)
              ((fun (a : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                  (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β) :
                      (a : ULift.{v, u} α ⊕ ULift.{u, v} β) →
                        (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
                    a) ''
                (fun (a : α ⊕ β) ↦
                    Sum.map (⇑(Equiv.symm Equiv.ulift) : (a : α) → ULift.{v, u} α)
                      (⇑(Equiv.symm Equiv.ulift) : (a : β) → ULift.{u, v} β) a) ''
                  I) :
            Set (bif false then ULift.{u, v} β else ULift.{v, u} α))) ∧
      N.Indep
        (image (α := bif true then ULift.{u, v} β else ULift.{v, u} α)
          (fun (a : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
            ((Equiv.ulift : (a : bif true then ULift.{u, v} β else ULift.{v, u} α) → β) a : β))
          (preimage (β := (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
              (Sigma.mk (β := fun (i : Bool) ↦ bif i then ULift.{u, v} β else ULift.{v, u} α) true)
              ((fun (a : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                  (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β) :
                      (a : ULift.{v, u} α ⊕ ULift.{u, v} β) →
                        (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
                    a) ''
                (fun (a : α ⊕ β) ↦
                    Sum.map (⇑(Equiv.symm Equiv.ulift) : (a : α) → ULift.{v, u} α)
                      (⇑(Equiv.symm Equiv.ulift) : (a : β) → ULift.{u, v} β) a) ''
                  I) :
            Set (bif true then ULift.{u, v} β else ULift.{v, u} α))) ↔
    M.Indep (Sum.inl ⁻¹' I) ∧ N.Indep (Sum.inr ⁻¹' I)
⊢ (M.sum N).Indep I ↔ M.Indep (Sum.inl ⁻¹' I) ∧ N.Indep (Sum.inr ⁻¹' I)

Tactic:
simp only [Matroid.sum, mapEquiv_indep_iff, Equiv.sumCongr_symm, Equiv.sumCongr_apply,
    Equiv.symm_symm, sigma_indep_iff, Bool.forall_bool]

Premises used: Equiv.symm_symm, Bool.forall_bool, Equiv.sumCongr_apply, Equiv.sumCongr_symm, Matroid.mapEquiv_indep_iff, Matroid.sigma_indep_iff, Matroid.sum
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : Set (α ⊕ β)
⊢ Sum.inl ⁻¹' I =
    image (α := bif false then ULift.{u, v} β else ULift.{v, u} α)
      (fun (a : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
        ((Equiv.ulift : (a : bif false then ULift.{u, v} β else ULift.{v, u} α) → α) a : α))
      (preimage (β := (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
          (Sigma.mk (β := fun (i : Bool) ↦ bif i then ULift.{u, v} β else ULift.{v, u} α) false)
          ((fun (a : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
              (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β) :
                  (a : ULift.{v, u} α ⊕ ULift.{u, v} β) → (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
                a) ''
            (fun (a : α ⊕ β) ↦
                Sum.map (⇑(Equiv.symm Equiv.ulift) : (a : α) → ULift.{v, u} α)
                  (⇑(Equiv.symm Equiv.ulift) : (a : β) → ULift.{u, v} β) a) ''
              I) :
        Set (bif false then ULift.{u, v} β else ULift.{v, u} α))

Tactic:
simp [Set.ext_iff, Equiv.ulift, Equiv.sumEquivSigmaBool]

Premises used: Equiv.ulift, Set.ext_iff, Equiv.sumEquivSigmaBool