awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : Set (α ⊕ β)
⊢ Sum.inr ⁻¹' I =
    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} α))

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

Premises used: Equiv.ulift, Set.ext_iff, Equiv.sumEquivSigmaBool
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
simp :
  M.IsBase
        (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) ''
                  B) :
            Set (bif false then ULift.{u, v} β else ULift.{v, u} α))) ∧
      N.IsBase
        (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) ''
                  B) :
            Set (bif true then ULift.{u, v} β else ULift.{v, u} α))) ↔
    M.IsBase (Sum.inl ⁻¹' B) ∧ N.IsBase (Sum.inr ⁻¹' B)
⊢ (M.sum N).IsBase B ↔ M.IsBase (Sum.inl ⁻¹' B) ∧ N.IsBase (Sum.inr ⁻¹' B)

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

Premises used: Equiv.symm_symm, Bool.forall_bool, Equiv.sumCongr_apply, Equiv.sumCongr_symm, Matroid.sigma_isBase_iff, Matroid.mapEquiv_isBase_iff, Matroid.sum
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ Sum.inl ⁻¹' B =
    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) ''
              B) :
        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
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ Sum.inr ⁻¹' B =
    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) ''
              B) :
        Set (bif true 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
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ ∀ (x : α),
    x ∈ Sum.inl ⁻¹' I ↔
      Membership.mem (γ := Set α)
        (image (α := bif false then ULift.{u, v} β else ULift.{v, u} α)
          (fun (a : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦ a.down)
          (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 (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                  Sum.elim
                    (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
                    (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
                    s) ''
                (fun (a : α ⊕ β) ↦
                    Sum.map
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : α) → ULift.{v, u} α)
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : β) → ULift.{u, v} β)
                      a) ''
                  I) :
            Set (bif false then ULift.{u, v} β else ULift.{v, u} α)))
        x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : 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} α) ↦ a.down)
      (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 (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
              Sum.elim
                (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                  Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
                (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                  Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
                s) ''
            (fun (a : α ⊕ β) ↦
                Sum.map
                  (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                    (a : α) → ULift.{v, u} α)
                  (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                    (a : β) → ULift.{u, v} β)
                  a) ''
              I) :
        Set (bif false then ULift.{u, v} β else ULift.{v, u} α))

Tactic:
exact ext <| by simp

Premises used: Set.ext
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ ∀ (x : α),
    x ∈ Sum.inl ⁻¹' X ↔
      Membership.mem (γ := Set α)
        (image (α := bif false then ULift.{u, v} β else ULift.{v, u} α)
          (fun (a : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦ a.down)
          (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 (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                  Sum.elim
                    (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
                    (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
                    s) ''
                (fun (a : α ⊕ β) ↦
                    Sum.map
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : α) → ULift.{v, u} α)
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : β) → ULift.{u, v} β)
                      a) ''
                  X) :
            Set (bif false then ULift.{u, v} β else ULift.{v, u} α)))
        x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ Sum.inl ⁻¹' X =
    image (α := bif false then ULift.{u, v} β else ULift.{v, u} α)
      (fun (a : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦ a.down)
      (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 (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
              Sum.elim
                (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                  Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
                (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                  Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
                s) ''
            (fun (a : α ⊕ β) ↦
                Sum.map
                  (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                    (a : α) → ULift.{v, u} α)
                  (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                    (a : β) → ULift.{u, v} β)
                  a) ''
              X) :
        Set (bif false then ULift.{u, v} β else ULift.{v, u} α))

Tactic:
exact ext <| by simp

Premises used: Set.ext
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ ∀ (x : β),
    x ∈ Sum.inr ⁻¹' I ↔
      Membership.mem (γ := Set β)
        (image (α := bif true then ULift.{u, v} β else ULift.{v, u} α)
          (fun (a : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦ a.down)
          (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 (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                  Sum.elim
                    (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
                    (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
                    s) ''
                (fun (a : α ⊕ β) ↦
                    Sum.map
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : α) → ULift.{v, u} α)
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : β) → ULift.{u, v} β)
                      a) ''
                  I) :
            Set (bif true then ULift.{u, v} β else ULift.{v, u} α)))
        x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ Sum.inr ⁻¹' I =
    image (α := bif true then ULift.{u, v} β else ULift.{v, u} α)
      (fun (a : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦ a.down)
      (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 (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
              Sum.elim
                (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                  Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
                (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                  Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
                s) ''
            (fun (a : α ⊕ β) ↦
                Sum.map
                  (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                    (a : α) → ULift.{v, u} α)
                  (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                    (a : β) → ULift.{u, v} β)
                  a) ''
              I) :
        Set (bif true then ULift.{u, v} β else ULift.{v, u} α))

Tactic:
exact ext <| by simp

Premises used: Set.ext
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ ∀ (x : β),
    x ∈ Sum.inr ⁻¹' X ↔
      Membership.mem (γ := Set β)
        (image (α := bif true then ULift.{u, v} β else ULift.{v, u} α)
          (fun (a : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦ a.down)
          (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 (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                  Sum.elim
                    (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
                    (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
                    s) ''
                (fun (a : α ⊕ β) ↦
                    Sum.map
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : α) → ULift.{v, u} α)
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : β) → ULift.{u, v} β)
                      a) ''
                  X) :
            Set (bif true then ULift.{u, v} β else ULift.{v, u} α)))
        x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ Sum.inr ⁻¹' X =
    image (α := bif true then ULift.{u, v} β else ULift.{v, u} α)
      (fun (a : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦ a.down)
      (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 (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
              Sum.elim
                (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                  Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
                (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                  Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
                s) ''
            (fun (a : α ⊕ β) ↦
                Sum.map
                  (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                    (a : α) → ULift.{v, u} α)
                  (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                    (a : β) → ULift.{u, v} β)
                  a) ''
              X) :
        Set (bif true then ULift.{u, v} β else ULift.{v, u} α))

Tactic:
exact ext <| by simp

Premises used: Set.ext
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
⊢ (M.disjointSum N h).E = M.E ∪ N.E

Tactic:
simp [disjointSum, restrictSubtype, mapEmbedding]

Premises used: Matroid.disjointSum, Matroid.mapEmbedding, Matroid.restrictSubtype
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
⊢ (M.disjointSum N h).Indep I ↔ M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E

Tactic:
simp [disjointSum, and_assoc]

Premises used: Matroid.disjointSum, and_assoc
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
⊢ (M.disjointSum N h).IsBase B ↔ M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E

Tactic:
simp [disjointSum, and_assoc]

Premises used: Matroid.disjointSum, and_assoc
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I X : Set α
⊢ (M.disjointSum N h).IsBasis I X ↔
    M.IsBasis (I ∩ M.E) (X ∩ M.E) ∧ N.IsBasis (I ∩ N.E) (X ∩ N.E) ∧ I ⊆ X ∧ X ⊆ M.E ∪ N.E

Tactic:
simp [disjointSum, and_assoc]

Premises used: Matroid.disjointSum, and_assoc
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
hE : ∀ (x : α), x ∈ (M.disjointSum N h).E ↔ x ∈ (N.disjointSum M ⋯).E
h₁ : ∀ ⦃I : Set α⦄, I ⊆ (M.disjointSum N h).E → ((M.disjointSum N h).Indep I ↔ (N.disjointSum M ⋯).Indep I)
⊢ M.disjointSum N h = N.disjointSum M ⋯

Tactic:
ext
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
x : α
⊢ x ∈ (M.disjointSum N h).E ↔ x ∈ (N.disjointSum M ⋯).E

Tactic:
simp [union_comm]

Premises used: Set.union_comm
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
h_1 : I ⊆ (M.disjointSum N h).E
⊢ (M.disjointSum N h).Indep I ↔ (N.disjointSum M ⋯).Indep I

Tactic:
simpa [union_comm] using ⟨fun ⟨m, n, h⟩ ↦ ⟨n, m, M.E.union_comm N.E ▸ h⟩,
    fun ⟨n, m, h⟩ ↦ ⟨m, n, M.E.union_comm N.E ▸ h⟩⟩

Premises used: Set.union_comm
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
h_1 : I ⊆ (M.disjointSum N h).E
⊢ (M.disjointSum N h).Indep I ↔ (N.disjointSum M ⋯).Indep I

Tactic:
repeat simpa [union_comm] using ⟨fun ⟨m, n, h⟩ ↦ ⟨n, m, M.E.union_comm N.E ▸ h⟩,
    fun ⟨n, m, h⟩ ↦ ⟨m, n, M.E.union_comm N.E ▸ h⟩⟩

Premises used: Set.union_comm
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : (M.disjointSum N h).Indep I
⊢ M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E

Tactic:
rw [disjointSum_indep_iff] at hI

Premises used: Matroid.disjointSum_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ ∃ (IM : Set α) (IN : Set α), M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN

Tactic:
⟨_, _, hI.1, hI.2.1, h.mono inter_subset_right inter_subset_right, ?_⟩

Premises used: And.right, And.left, And.intro, Exists.intro, Disjoint.mono, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
refine : I = I ∩ M.E ∪ I ∩ N.E
⊢ ∃ (IM : Set α) (IN : Set α), M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN

Tactic:
refine ⟨_, _, hI.1, hI.2.1, h.mono inter_subset_right inter_subset_right, ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
rw : I = I ∩ (M.E ∪ N.E)
rw₁ rw₂ : I = I
⊢ I = I ∩ M.E ∪ I ∩ N.E

Tactic:
rw [← inter_union_distrib_left, inter_eq_self_of_subset_left hI.2.2]

Premises used: And.right, Set.inter_union_distrib_left, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : (M.disjointSum N h).IsBase B
⊢ M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E

Tactic:
rw [disjointSum_isBase_iff] at hB

Premises used: Matroid.disjointSum_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
⊢ ∃ (BM : Set α) (BN : Set α), M.IsBase BM ∧ N.IsBase BN ∧ Disjoint BM BN ∧ B = BM ∪ BN

Tactic:
⟨_, _, hB.1, hB.2.1, h.mono inter_subset_right inter_subset_right, ?_⟩

Premises used: And.right, And.left, And.intro, Exists.intro, Disjoint.mono, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
refine : B = B ∩ M.E ∪ B ∩ N.E
⊢ ∃ (BM : Set α) (BN : Set α), M.IsBase BM ∧ N.IsBase BN ∧ Disjoint BM BN ∧ B = BM ∪ BN

Tactic:
refine ⟨_, _, hB.1, hB.2.1, h.mono inter_subset_right inter_subset_right, ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
rw : B = B ∩ (M.E ∪ N.E)
rw₁ rw₂ : B = B
⊢ B = B ∩ M.E ∪ B ∩ N.E

Tactic:
rw [← inter_union_distrib_left, inter_eq_self_of_subset_left hB.2.2]

Premises used: And.right, Set.inter_union_distrib_left, Set.inter_eq_self_of_subset_left