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

Goal state before:
pp: case mp.refine_2
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
⊢ ∃ c, c * (↑e 1).1 = 1

Tactic:
·

Goal state after:
case mp.refine_2
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
⊢ ∃ c, c * (↑e 1).1 = 1
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case inl
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Finite F
⊢ ∃ α, F⟮α⟯ = K

pp: case inr
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
⊢ ∃ α, F⟮α⟯ = K

Tactic:
·

Goal state after:
case inl
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Finite F
⊢ ∃ α, F⟮α⟯ = K
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case inr
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
⊢ ∃ α, F⟮α⟯ = K

Tactic:
·

Goal state after:
case inr
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
⊢ ∃ α, F⟮α⟯ = K
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mpr
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h : I ∈ (Units.map ↑(spanSingleton R)).range
⊢ I ∈ (unitsToPic R A).ker

Tactic:
·

Goal state after:
case mpr
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h : I ∈ (Units.map ↑(spanSingleton R)).range
⊢ I ∈ (unitsToPic R A).ker
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case hPQ
α : Type u_1
M : Matroid α
I X : Set α
⊢ ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X ∩ M.E → M.Indep x ∧ x ⊆ X

pp: case h
α : Type u_1
M : Matroid α
I X : Set α
⊢ ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X → ∃ y, x ⊆ y ∧ M.Indep y ∧ y ⊆ X ∩ M.E

Tactic:
·

Goal state after:
case hPQ
α : Type u_1
M : Matroid α
I X : Set α
⊢ ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X ∩ M.E → M.Indep x ∧ x ⊆ X
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
⊢ Function.Injective ⇑(toAlgebra e)

Tactic:
simpa [toAlgebra] using
    Flat.rTensor_preserves_injective_linearMap _ (FaithfulSMul.algebraMap_injective R A)

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

Goal state before:
pp: case pos
α : 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
⊢ ∃ x ∈ B \ I, Indep (insert x I)

pp: case neg
α : 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
⊢ ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
·

Goal state after:
case pos
α : 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
⊢ ∃ x ∈ B \ I, Indep (insert x I)
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
this : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra
⊢ ∃ x, ∀ (y : E →ₐ[↥F⟮α⟯] A), y = x

pp: F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
this : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra
⊢ ∀ (x : E), (Polynomial.map (algebraMap (↥F⟮α⟯) A) (minpoly (↥F⟮α⟯) x)).Splits

Tactic:
·

Goal state after:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
this : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra
⊢ ∃ x, ∀ (y : E →ₐ[↥F⟮α⟯] A), y = x
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
this : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra
⊢ ∀ (x : E), (Polynomial.map (algebraMap (↥F⟮α⟯) A) (minpoly (↥F⟮α⟯) x)).Splits

Tactic:
·

Goal state after:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
this : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra
⊢ ∀ (x : E), (Polynomial.map (algebraMap (↥F⟮α⟯) A) (minpoly (↥F⟮α⟯) x)).Splits
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 (insert e I)

pp: case refine_2
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ {x | M.IsBasis I (insert x I)} \ I
hu : M.Indep (insert e I)
⊢ e ∈ 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 (insert e I)
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)
⊢ ∀ (i : Bool), M.IsBasis (bif i then I else J) (bif i then X else Y)

pp: case refine_2
α : 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.Indep (⋃ i, bif i then I else J)

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)
⊢ ∀ (i : Bool), M.IsBasis (bif i then I else J) (bif i then X else Y)
Module: Mathlib.RingTheory.PicardGroup

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

pp: case mpr
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
h : M ∈ relPic R A
⊢ M ∈ (unitsToPic R A).range

Tactic:
·

Goal state after:
case mp
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
h : M ∈ (unitsToPic R A).range
⊢ M ∈ relPic R A
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 ∈ B'

pp: case h.refine_2
α : 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
⊢ Disjoint (insert e I) B''

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 ∈ B'
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B X : Set α
M : Matroid α
⊢ ∀ ⦃I B : Set α⦄,
    (I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) →
      ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I →
        Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) B →
          ∃ x ∈ B \ I, insert x I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert x I) B

Tactic:
by
    rintro I X ⟨hIE, B, hB, hIB⟩ hI_not_max hX_max
    have hXE := hX_max.1.1
    have hB' := (isBase_compl_iff_maximal_disjoint_isBase hXE).mpr hX_max
    set B' := M.E \ X with hX
    have hI := (not_iff_not.mpr (isBase_compl_iff_maximal_disjoint_isBase)).mpr hI_not_max
    obtain ⟨B'', hB'', hB''₁, hB''₂⟩ := (hB'.indep.sdiff I).exists_isBase_subset_union_isBase hB
    rw [← compl_subset_compl, ← hIB.sdiff_eq_right, ← union_sdiff_distrib, sdiff_eq, compl_inter,
      compl_compl, union_subset_iff, compl_subset_compl] at hB''₂
    have hssu := (subset_inter (hB''₂.2) hIE).ssubset_of_ne
      (by { rintro rfl; apply hI; convert! hB''; simp [hB''.subset_ground] })
    obtain ⟨e, ⟨(heB'' : e ∉ _), heE⟩, heI⟩ := exists_of_ssubset hssu
    use e
    simp_rw [mem_sdiff, insert_subset_iff, and_iff_left heI, and_iff_right heE, and_iff_right hIE]
    refine ⟨by_contra (fun heX ↦ heB'' (hB''₁ ⟨?_, heI⟩)), ⟨B'', hB'', ?_⟩⟩
    · rw [hX]; exact ⟨heE, heX⟩
    rw [← union_singleton, disjoint_union_left, disjoint_singleton_left, and_iff_left heB'']
    exact disjoint_of_subset_left hB''₂.2 disjoint_compl_left

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

Goal state before:
pp: case refine_1
α : 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
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ I' ⊆ X \ B' ∩ M.E

pp: case refine_2
α : 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
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ ∃ B, M.IsBase B ∧ Disjoint (X \ B' ∩ M.E) B

pp: case refine_3
α : 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
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ X \ B' ∩ M.E ⊆ X

pp: case refine_4
α : 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
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint t B) ∧ t ⊆ X → X \ B' ∩ M.E ⊆ t → t ⊆ X \ B' ∩ M.E

Tactic:
·

Goal state after:
case refine_1
α : 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
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ I' ⊆ X \ B' ∩ M.E
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_2
α : 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
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ ∃ B, M.IsBase B ∧ Disjoint (X \ B' ∩ M.E) B

pp: case refine_3
α : 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
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ X \ B' ∩ M.E ⊆ X

pp: case refine_4
α : 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
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint t B) ∧ t ⊆ X → X \ B' ∩ M.E ⊆ t → t ⊆ X \ B' ∩ M.E

Tactic:
·

Goal state after:
case refine_2
α : 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
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ ∃ B, M.IsBase B ∧ Disjoint (X \ B' ∩ M.E) B
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_3
α : 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
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ X \ B' ∩ M.E ⊆ X

pp: case refine_4
α : 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
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint t B) ∧ t ⊆ X → X \ B' ∩ M.E ⊆ t → t ⊆ X \ B' ∩ M.E

Tactic:
·

Goal state after:
case refine_3
α : 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
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ X \ B' ∩ M.E ⊆ X
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_4
α : 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
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ ∀ ⦃t : Set α⦄,
    t ⊆ M.E → ∀ (x : Set α), M.IsBase x → Disjoint t x → t ⊆ X → X \ B' ∩ M.E ⊆ t → (t ⊆ X ∧ Disjoint t B') ∧ t ⊆ M.E

Tactic:
refine fun J hJE B'' hB'' hdj hJX hXJ ↦ ⟨⟨hJX, ?_⟩, hJE⟩

Goal state after:
case refine_4
α : 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
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ Disjoint J B'
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
R₁ R₂ : Set α
M : Matroid α
hR : R₂ ⊆ R₁
⊢ M ↾ R₁ ↾ R₂ = M ↾ R₂

Tactic:
by
  refine ext_indep rfl ?_
  simp only [restrict_ground_eq, restrict_indep_iff, and_congr_left_iff, and_iff_left_iff_imp]
  exact fun _ h _ _ ↦ h.trans hR

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

Goal state before:
pp: α : Type u_1
M : Matroid α
E : Set α
⊢ M = freeOn E ↔ M.E = E ∧ M.Indep E

Tactic:
refine ⟨?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
E : Set α
⊢ M = freeOn E → M.E = E ∧ M.Indep E

case refine_2
α : Type u_1
M : Matroid α
E : Set α
h : M.E = E ∧ M.Indep E
⊢ M = freeOn E
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
E : Set α
⊢ M = freeOn E → M.E = E ∧ M.Indep E

pp: case refine_2
α : Type u_1
M : Matroid α
E : Set α
h : M.E = E ∧ M.Indep E
⊢ M = freeOn E

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
E : Set α
⊢ M = freeOn E → M.E = E ∧ M.Indep E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: case refine_1
α : Type u_1
M M' : Matroid α
X : Set α
h : M ↾ X = M' ↾ X
I : Set α
hIX : I ⊆ X
⊢ M.Indep I ↔ M'.Indep I

pp: case refine_2
α : Type u_1
M M' : Matroid α
X : Set α
h : ∀ I ⊆ X, M.Indep I ↔ M'.Indep I
I : Set α
hI : I ⊆ X
⊢ (M ↾ X).Indep I ↔ (M' ↾ X).Indep I

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
M M' : Matroid α
X : Set α
h : M ↾ X = M' ↾ X
I : Set α
hIX : I ⊆ X
⊢ M.Indep I ↔ M'.Indep I
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_4.inl
α : 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₁
heB'' : e ∈ B''
⊢ False

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:
·

Goal state after:
case refine_4.inl
α : 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₁
heB'' : e ∈ B''
⊢ False
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: case refine_1
α : Type u_1
M M' : Matroid α
X : Set α
h : M ↾ X = M' ↾ X
I : Set α
hIX : I ⊆ X
⊢ M.Indep I ↔ M'.Indep I

Tactic:
← and_iff_left (a := (M.Indep I)) hIX,

Goal state after:
case refine_1
α : Type u_1
M M' : Matroid α
X : Set α
h : M ↾ X = M' ↾ X
I : Set α
hIX : I ⊆ X
⊢ M.Indep I ∧ I ⊆ X ↔ M'.Indep I
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 B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
B : Set α
n : ℕ
hn : ∀ (I : Set α), Indep I → I.encard ≤ ↑n
hB : (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground ⋯).matroid.IsBase B
⊢ Indep B

Tactic:
by simpa using hB.indep

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
⊢ M✶.Indep (M.E \ B ∩ (M.E \ X))

pp: case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : e ∈ (M.E \ X) \ (M.E \ B ∩ (M.E \ X))
⊢ M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
⊢ M✶.Indep (M.E \ B ∩ (M.E \ X))
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : ¬N.Indep (f '' I)
hIE : I ⊆ f ⁻¹' N.E
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

pp: case inr
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : ¬N.Indep (f '' I)
hIE : I ⊆ f ⁻¹' N.E
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
⊢ N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X

pp: case refine_2
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
⊢ (N.comap f).IsBasis I X

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
⊢ N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X