mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x : Aˣ
x✝ : A
⊢ x✝ ∈ (LinearMap.toSpanSingleton R A ↑x).range ↔ x✝ ∈ ↑((Units.map ↑(spanSingleton R)) x)

Tactic:
;

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x : Aˣ
x✝ : A
⊢ x✝ ∈ (LinearMap.toSpanSingleton R A ↑x).range ↔ x✝ ∈ ↑((Units.map ↑(spanSingleton R)) x)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
I : Set α
M : Matroid α
h : I = ∅
⊢ M.IsBasis ∅ ∅

Tactic:
;

Goal state after:
α : Type u_1
I : Set α
M : Matroid α
h : I = ∅
⊢ M.IsBasis ∅ ∅
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
b : α
hb : b ∈ B₀ \ I
⊢ ∃ Ib ⊆ I, Ib.Finite ∧ ¬Indep (insert (↑⟨b, hb⟩) Ib)

Tactic:
;

Goal state after:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
b : α
hb : b ∈ B₀ \ I
⊢ ∃ Ib ⊆ I, Ib.Finite ∧ ¬Indep (insert (↑⟨b, hb⟩) Ib)
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X B : Set α
hB : M.IsBase B
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
B'' : Set α
hB'' : M.IsBase B''
hIE : B''ᶜ ∩ M.E ⊆ M.E
hIB : Disjoint (B''ᶜ ∩ M.E) B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E)
hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))
hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X B : Set α
hB : M.IsBase B
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
B'' : Set α
hB'' : M.IsBase B''
hIE : B''ᶜ ∩ M.E ⊆ M.E
hIB : Disjoint (B''ᶜ ∩ M.E) B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E)
hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))
hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ
⊢ False
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X B : Set α
hB : M.IsBase B
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := ⋯
hB' : M.IsBase B'
hX : B' = M.E \ X
B'' : Set α
hB'' : M.IsBase B''
hIE : B''ᶜ ∩ M.E ⊆ M.E
hIB : Disjoint (B''ᶜ ∩ M.E) B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E)
hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))
hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ
⊢ M.IsBase (M.E \ (B''ᶜ ∩ M.E))

Tactic:
;

Goal state after:
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X B : Set α
hB : M.IsBase B
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := ⋯
hB' : M.IsBase B'
hX : B' = M.E \ X
B'' : Set α
hB'' : M.IsBase B''
hIE : B''ᶜ ∩ M.E ⊆ M.E
hIB : Disjoint (B''ᶜ ∩ M.E) B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E)
hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))
hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ
⊢ M.IsBase (M.E \ (B''ᶜ ∩ M.E))
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X B : Set α
hB : M.IsBase B
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
B'' : Set α
hB'' : M.IsBase B''
hIE : B''ᶜ ∩ M.E ⊆ M.E
hIB : Disjoint (B''ᶜ ∩ M.E) B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E)
hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))
hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ
⊢ M.E \ (B''ᶜ ∩ M.E) = B''

Tactic:
;

Goal state after:
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X B : Set α
hB : M.IsBase B
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
B'' : Set α
hB'' : M.IsBase B''
hIE : B''ᶜ ∩ M.E ⊆ M.E
hIB : Disjoint (B''ᶜ ∩ M.E) B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E)
hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))
hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ
⊢ M.E \ (B''ᶜ ∩ M.E) = B''
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ I
⊢ M.IsBasis I I

Tactic:
;

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ I
⊢ M.IsBasis I I
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
A : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
x✝¹ : ↥⊤
x✝ : ↥(submoduleAlgebra e)
⊢ ((AlgebraTensorModule.curry (⊤.mulMap (submoduleAlgebra e))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry
          ↑(LinearEquiv.rTensor (↥(submoduleAlgebra e)) Submodule.topEquiv ≪≫ₗ
              LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)))
        x✝¹)
      x✝

Tactic:
;

Goal state after:
R : Type u
M : Type v
A : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
x✝¹ : ↥⊤
x✝ : ↥(submoduleAlgebra e)
⊢ ((AlgebraTensorModule.curry (⊤.mulMap (submoduleAlgebra e))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry
          ↑(LinearEquiv.rTensor (↥(submoduleAlgebra e)) Submodule.topEquiv ≪≫ₗ
              LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)))
        x✝¹)
      x✝
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis J Y ∧ M.IsBasis I X

Tactic:
;

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis J Y ∧ M.IsBasis I X
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
I : Submodule R A
⊢ (I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e) =
    ↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) ∘ₗ
      LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype

Tactic:
;

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
I : Submodule R A
⊢ (I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e) =
    ↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) ∘ₗ
      LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
I : Submodule R A
x✝¹ : ↥I
x✝ : ↥(submoduleAlgebra e)
⊢ ((AlgebraTensorModule.curry ((I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry
          (↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) ∘ₗ
            LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype))
        x✝¹)
      x✝

Tactic:
;

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
I : Submodule R A
x✝¹ : ↥I
x✝ : ↥(submoduleAlgebra e)
⊢ ((AlgebraTensorModule.curry ((I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry
          (↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) ∘ₗ
            LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype))
        x✝¹)
      x✝
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
⊢ M ∈ (unitsToPic R A).range ↔ M ∈ relPic R A

Tactic:
;

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
⊢ M ∈ (unitsToPic R A).range ↔ M ∈ relPic R A
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.Indep I

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case h.refine_1
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
heX : e ∉ X
⊢ e ∈ M.E \ X

Tactic:
;

Goal state after:
case h.refine_1
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
heX : e ∉ X
⊢ e ∈ M.E \ X
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
hE : M.E.Finite
⊢ M ∈ {M_1 | M_1.E ⊆ M.E}

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
hE : M.E.Finite
⊢ M ∈ {M_1 | M_1.E ⊆ M.E}
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α✝ : Type u_1
M : Matroid α✝
E B I X R J : Set α✝
α : Type u_2
Y✝ : Set α
⊢ (fun x ↦ x = ∅) Y✝ → ∀ a ∈ ∅ \ Y✝, ∃ b ∈ Y✝ \ ∅, (fun x ↦ x = ∅) (insert b (∅ \ {a}))

Tactic:
;

Goal state after:
α✝ : Type u_1
M : Matroid α✝
E B I X R J : Set α✝
α : Type u_2
Y✝ : Set α
⊢ (fun x ↦ x = ∅) Y✝ → ∀ a ∈ ∅ \ Y✝, ∃ b ∈ Y✝ \ ∅, (fun x ↦ x = ∅) (insert b (∅ \ {a}))
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α✝ : Type u_1
M : Matroid α✝
E B I X R J : Set α✝
α : Type u_2
X✝ : Set α
a✝ : X✝ ⊆ ∅
⊢ ∃ J, ∅ ⊆ J ∧ Maximal (fun K ↦ (fun x ↦ x = ∅) K ∧ K ⊆ X✝) J

Tactic:
;

Goal state after:
α✝ : Type u_1
M : Matroid α✝
E B I X R J : Set α✝
α : Type u_2
X✝ : Set α
a✝ : X✝ ⊆ ∅
⊢ ∃ J, ∅ ⊆ J ∧ Maximal (fun K ↦ (fun x ↦ x = ∅) K ∧ K ⊆ X✝) J
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
⊢ (emptyOn α)✶.E = ∅

Tactic:
;

Goal state after:
α : Type u_1
⊢ (emptyOn α)✶.E = ∅
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E : Set α
⊢ ∅ ⊆ E

Tactic:
;

Goal state after:
α : Type u_1
E : Set α
⊢ ∅ ⊆ E
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
h : ∀ X ⊆ M.E, M.Indep X → X = ∅
hIE : ∅ ⊆ M.E
⊢ M.Indep ∅

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
h : ∀ X ⊆ M.E, M.Indep X → X = ∅
hIE : ∅ ⊆ M.E
⊢ M.Indep ∅
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E X : Set α
hX : X ⊆ E
⊢ (loopyOn E).IsBasis ∅ X

Tactic:
;

Goal state after:
α : Type u_1
E X : Set α
hX : X ⊆ E
⊢ (loopyOn E).IsBasis ∅ X
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E X : Set α
hX : X ⊆ E
⊢ (loopyOn E).Indep ∅ ∧ ∅ ⊆ X ∧ ∀ (J : Set α), (loopyOn E).Indep J → ∅ ⊆ J → J ⊆ X → ∅ = J

Tactic:
;

Goal state after:
α : Type u_1
E X : Set α
hX : X ⊆ E
⊢ (loopyOn E).Indep ∅ ∧ ∅ ⊆ X ∧ ∀ (J : Set α), (loopyOn E).Indep J → ∅ ⊆ J → J ⊆ X → ∅ = J
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R X : Set α
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
R X : Set α
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ ∀ ⦃I : Set α⦄, I ⊆ (M ↾ M.E).E → ((M ↾ M.E).Indep I ↔ M.Indep I)

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
⊢ ∀ ⦃I : Set α⦄, I ⊆ (M ↾ M.E).E → ((M ↾ M.E).Indep I ↔ M.Indep I)
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.IsBase ∅ ∨ M.RankPos

Tactic:
rankPos_iff

Goal state after:
α : Type u_1
M : Matroid α
⊢ M.IsBase ∅ ∨ ¬M.IsBase ∅
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.IsBase ∅ ∨ ¬M.IsBase ∅

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
⊢ M.IsBase ∅ ∨ ¬M.IsBase ∅
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: case refine_1
α : Type u_1
E : Set α
⊢ (freeOn E).E = E ∧ (freeOn E).Indep E

Tactic:
;

Goal state after:
case refine_1
α : Type u_1
E : Set α
⊢ (freeOn E).E = E ∧ (freeOn E).Indep E
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_4.inr
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
B₁ : Set α
hB₁ hB' : M.IsBase B₁
hI : M.IsBasis (B₁ \ X) (M.E \ X)
hIB' : B₁ \ X ⊆ B₁
hB'IB : B₁ ⊆ B₁ \ X ∪ B
hXJ : X \ B₁ ∩ M.E ⊆ J
hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B₁ \ X
hdj' : ¬Disjoint J B₁
e : α
heJ : e ∈ J
heB' : e ∈ B₁
heX : e ∉ X
⊢ False

Tactic:
exact heX (hJX heJ)

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I E B : Set α
hB : B ⊆ E
h : B = E \ I
⊢ E \ (E \ I) = E ∩ I

Tactic:
;

Goal state after:
α : Type u_1
I E B : Set α
hB : B ⊆ E
h : B = E \ I
⊢ E \ (E \ I) = E ∩ I
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R = M
⊢ R = (M ↾ R).E

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R = M
⊢ R = (M ↾ R).E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α✝ : Type u_1
M : Matroid α✝
R✝ I X Y : Set α✝
N : Matroid α✝
α : Type u_2
M₁ M₂ : Matroidᵣ α
R : Set α
h : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR : R ⊆ R'
hR' : R' ⊆ R
h' : M₂.toMatroid = M₁.toMatroid ↾ R'
⊢ M₁ = M₂

Tactic:
rw [← Matroidᵣ.coe_inj, h, h', hR.antisymm hR', restrict_idem]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
⊢ M ↾ (M ↾ R).E = M ↾ R

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
R : Set α
⊢ M ↾ (M ↾ R).E = M ↾ R
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).E ⊆ M.E

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).E ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
R R' : Set α
M : Matroid α
h : R ⊆ R'
⊢ M ↾ R' ↾ R ≤r M ↾ R'

Tactic:
;

Goal state after:
α : Type u_1
R R' : Set α
M : Matroid α
h : R ⊆ R'
⊢ M ↾ R' ↾ R ≤r M ↾ R'
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: case mpr
α : Type u_1
M N : Matroid α
⊢ (∃ R ⊆ M.E, N = M ↾ R) → N ≤r M

Tactic:
;

Goal state after:
case mpr
α : Type u_1
M N : Matroid α
⊢ (∃ R ⊆ M.E, N = M ↾ R) → N ≤r M
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: case mpr
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R ≤r M

Tactic:
;

Goal state after:
case mpr
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R ≤r M
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
N : Matroid α
h : N <r N
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
N : Matroid α
h : N <r N
⊢ False
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
N : Matroid α
h : { toMatroid := N } < { toMatroid := N }
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
N : Matroid α
h : { toMatroid := N } < { toMatroid := N }
⊢ False
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.Finite
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R ∈ (fun R ↦ M ↾ R) '' {b | b ⊆ M.E}

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
inst✝ : M.Finite
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R ∈ (fun R ↦ M ↾ R) '' {b | b ⊆ M.E}
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I R : Set α
hI : (M ↾ R).Indep I
⊢ M.Indep I

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
I R : Set α
hI : (M ↾ R).Indep I
⊢ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
R : Set α
hIN : I ⊆ (M ↾ R).E
⊢ (M ↾ R).Indep I

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
R : Set α
hIN : I ⊆ (M ↾ R).E
⊢ (M ↾ R).Indep I
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
R : Set α
hR : R ⊆ M.E
hX : X ⊆ (M ↾ R).E
⊢ (M ↾ R).IsBasis I X

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
R : Set α
hR : R ⊆ M.E
hX : X ⊆ (M ↾ R).E
⊢ (M ↾ R).IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBasis I X
⊢ M.IsBasis I X

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
I X R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBasis I X
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBase I
⊢ M.IsBasis I (M ↾ R).E

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
I R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBase I
⊢ M.IsBasis I (M ↾ R).E
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
E : Set β
⊢ ((loopyOn E).comap f).E = f ⁻¹' E ∧ ∀ X ⊆ ((loopyOn E).comap f).E, ((loopyOn E).comap f).Indep X → X = ∅

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
E : Set β
⊢ ((loopyOn E).comap f).E = f ⁻¹' E ∧ ∀ X ⊆ ((loopyOn E).comap f).E, ((loopyOn E).comap f).Indep X → X = ∅
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
h : M✶.RankPos
hB : M.IsBase M.E
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
h : M✶.RankPos
hB : M.IsBase M.E
⊢ False
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
Indep : Set α → Prop
M : Matroid α
h : ∀ (I : Set α), M.Indep I ↔ Indep I
⊢ ∃ M_1, M.E = M_1.E ∧ M_1.Indep = Indep

Tactic:
;

Goal state after:
α : Type u_1
Indep : Set α → Prop
M : Matroid α
h : ∀ (I : Set α), M.Indep I ↔ Indep I
⊢ ∃ M_1, M.E = M_1.E ∧ M_1.Indep = Indep
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
M : Matroid α
hM : ∃ M_1, E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ M.Indep ∅

Tactic:
;

Goal state after:
α : Type u_1
E : Set α
M : Matroid α
hM : ∃ M_1, E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ M.Indep ∅
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
h : M✶.RankPos
hI : M.Indep I
B : Set α
hB : M.IsBase B ∧ I ⊆ B
⊢ I ⊂ M.E

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
h : M✶.RankPos
hI : M.Indep I
B : Set α
hB : M.IsBase B ∧ I ⊆ B
⊢ I ⊂ M.E
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
M : Matroid α
hM : ∃ M_1, E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ ⦃I J : Set α⦄, M.Indep J → I ⊆ J → M.Indep I

Tactic:
;

Goal state after:
α : Type u_1
E : Set α
M : Matroid α
hM : ∃ M_1, E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ ⦃I J : Set α⦄, M.Indep J → I ⊆ J → M.Indep I
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
R : Set α
hXE : X ⊆ (M ↾ R).E
⊢ (M ↾ R).Dep X

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
R : Set α
hXE : X ⊆ (M ↾ R).E
⊢ (M ↾ R).Dep X
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
M : Matroid α
hM : ∃ M_1, E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ ⦃I B : Set α⦄, M.Indep I → ¬Maximal M.Indep I → Maximal M.Indep B → ∃ x ∈ B \ I, M.Indep (insert x I)

Tactic:
;

Goal state after:
α : Type u_1
E : Set α
M : Matroid α
hM : ∃ M_1, E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ ⦃I B : Set α⦄, M.Indep I → ¬Maximal M.Indep I → Maximal M.Indep B → ∃ x ∈ B \ I, M.Indep (insert x I)