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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁹ : AddCommGroup M'
inst✝⁸ : Module R M'
f : M →ₗ[R] M'
inst✝⁷ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁶ : CommRing Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : IsScalarTower R Rₛ M'
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
I : Type u_6
inst✝ : Finite I
b : Basis I Rₛ M'
this : FinitePresentation R (I →₀ R)
r : R
hr : r ∈ S
e : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r (I →₀ R)
he :
  LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯ ∘ₗ ↑R ↑e =
    ↑(LinearEquiv.restrictScalars R b.repr) ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
⊢ ∃ r, ∃ (hr : r ∈ S), ∃ b', ∀ (i : I), (LocalizedModule.lift (Submonoid.powers r) f ⋯) (b' i) = b i

Tactic:
let e' := IsLocalizedModule.iso (.powers r) (Finsupp.mapRange.linearMap (α := I)
    (Algebra.linearMap R (Localization (.powers r))))

Goal state after:
R : Type u_4
M : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁹ : AddCommGroup M'
inst✝⁸ : Module R M'
f : M →ₗ[R] M'
inst✝⁷ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁶ : CommRing Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : IsScalarTower R Rₛ M'
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
I : Type u_6
inst✝ : Finite I
b : Basis I Rₛ M'
this : FinitePresentation R (I →₀ R)
r : R
hr : r ∈ S
e : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r (I →₀ R)
he :
  LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯ ∘ₗ ↑R ↑e =
    ↑(LinearEquiv.restrictScalars R b.repr) ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
e' : LocalizedModule (Submonoid.powers r) (I →₀ R) ≃ₗ[R] I →₀ Localization (Submonoid.powers r) :=
  IsLocalizedModule.iso (Submonoid.powers r)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (Submonoid.powers r))))
⊢ ∃ r, ∃ (hr : r ∈ S), ∃ b', ∀ (i : I), (LocalizedModule.lift (Submonoid.powers r) f ⋯) (b' i) = b i
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module S M'
inst✝ : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
x : ι →₀ M
⊢ (LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ ⋯.equiv ≪≫ₗ
        (finsuppLEquivDirectSum S M' ι).symm)
      (1 ⊗ₜ[R] x) =
    (Finsupp.mapRange.linearMap ε) x

Tactic:
rw [LinearEquiv.trans_apply, Finsupp.mapRange.linearMap_apply,
    LinearEquiv.symm_apply_eq]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module S M'
inst✝ : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
x : ι →₀ M
⊢ (LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ ⋯.equiv) (1 ⊗ₜ[R] x) =
    (finsuppLEquivDirectSum S M' ι) (Finsupp.mapRange ⇑ε ⋯ x)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: case e_f
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
x✝ : Localization p.primeCompl
⊢ (algebraMap (Localization p.primeCompl) (Localization (algebraMapSubmonoid S p.primeCompl))) x✝ =
    ((↑(Localization.tensorLeftAlgEquiv p.primeCompl S).toRingEquiv).comp ↑includeRight) x✝

Tactic:
simp [Localization.tensorLeftAlgEquiv_apply_one_tmul p.primeCompl]

Goal state after:
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
h✝¹ : Nontrivial R
N : Type u_1
w✝³ : AddCommGroup N
w✝² : Module R N
w✝¹ : Module.Finite R N
w✝ : Free R N
h✝ : Free R (M × N)
n : ℕ := finrank R N
⊢ finrank R (M × N) = n + 1

Tactic:
let 𝔭 : PrimeSpectrum R := Nonempty.some inferInstance

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
h✝¹ : Nontrivial R
N : Type u_1
w✝³ : AddCommGroup N
w✝² : Module R N
w✝¹ : Module.Finite R N
w✝ : Free R N
h✝ : Free R (M × N)
n : ℕ := finrank R N
𝔭 : PrimeSpectrum R := ⋯.some
⊢ finrank R (M × N) = n + 1
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝² : Group G
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G' m = ⊥
⊢ IsSolvable G

Tactic:
refine ⟨⟨n + m, le_bot_iff.mp (Subgroup.map_bot f ▸ hm ▸ ?_)⟩⟩

Goal state after:
G : Type u_1
inst✝² : Group G
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G' m = ⊥
⊢ derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
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
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
e : M ⊗[R] N ≃ₗ[R] R
x✝ : P →ₗ[R] Q
⊢ (LinearEquiv.congrLeft Q R (rightCancelEquiv P e))
      ((rightCancelEquiv Q e).congrRight ((LinearMap.rTensorHom N) ((LinearMap.rTensorHom M) x✝))) =
    x✝

Tactic:
← LinearEquiv.eq_symm_apply

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
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
e : M ⊗[R] N ≃ₗ[R] R
x✝ : P →ₗ[R] Q
⊢ (rightCancelEquiv Q e).congrRight ((LinearMap.rTensorHom N) ((LinearMap.rTensorHom M) x✝)) =
    (LinearEquiv.congrLeft Q R (rightCancelEquiv P e)).symm x✝
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
⊢ Function.Injective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑f

Tactic:
by
  refine ⟨fun h ↦ ?_, Flat.lTensor_preserves_injective_linearMap _⟩
  rw [← leftCancelEquiv_comp_lTensor_comp_symm (linearEquiv R M) f]
  simpa using Flat.lTensor_preserves_injective_linearMap _ h

Goal state after:
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : Algebra.IsAlgebraic F K
h : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
L' : Type u_4
inst✝¹ : Field L'
inst✝ : Algebra F L'
⊢ Nonempty (↥(⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L')) →ₐ[F] L)

Tactic:
rw [← gc.l_iSup]
      refine nonempty_algHom_adjoin_of_splits fun x hx ↦ ?_
      obtain ⟨y, hx⟩ := Set.mem_iUnion.mp hx
      refine ⟨isAlgebraic_iff_isIntegral.mp (isAlgebraic_of_mem_rootSet hx), ?_⟩
      by_cases iy : IsIntegral F y
      · exact (h y).of_dvd (map_ne_zero (minpoly.ne_zero iy))
          ((map_dvd_map' _).mpr (minpoly.dvd F x (mem_rootSet.mp hx).2))
      · simp [minpoly.eq_zero iy] at hx

Goal state after:
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case refine_1
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F L
f : ↥K →ₐ[F] L
⊢ f.fieldRange ≤ ⨆ f, map f K

Tactic:
exact le_iSup_of_le (f.liftNormal L) (fun b ⟨a, h⟩ ↦ ⟨a, a.2, h ▸ f.liftNormal_commutes L a⟩)

Goal state after:
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
⊢ Normal F E

Tactic:
by
  rcases eq_or_ne p 0 with (rfl | hp)
  · have := hFEp.adjoin_rootSet
    rw [rootSet_zero, Algebra.adjoin_empty] at this
    exact Normal.of_algEquiv
      (AlgEquiv.ofBijective (Algebra.ofId F E) (Algebra.bijective_algebraMap_iff.2 this.symm))
  refine normal_iff.mpr fun x ↦ ?_
  have : FiniteDimensional F E := IsSplittingField.finiteDimensional E p
  have hx := IsIntegral.of_finite F x
  let L := (p * minpoly F x).SplittingField
  have hL := SplittingField.splits (p * minpoly F x)
  rw [Polynomial.map_mul, splits_mul _ (map_ne_zero (minpoly.ne_zero hx))] at hL
  · obtain ⟨hL1, hL2⟩ := hL
    let j : E →ₐ[F] L := IsSplittingField.lift E p hL1
    rw [← j.comp_algebraMap, ← Polynomial.map_map] at hL2
    refine ⟨hx, Splits.of_splits_map (j : E →+* L) hL2 fun a ha ↦ ?_⟩
    rw [Polynomial.map_map, j.comp_algebraMap] at ha
    let : Algebra F⟮x⟯ L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toRingHom.toAlgebra
    let j' : E →ₐ[F⟮x⟯] L := IsSplittingField.lift E (p.map (algebraMap F F⟮x⟯)) ?_
    · change a ∈ j.range
      rw [← IsSplittingField.adjoin_rootSet_eq_range E p j,
            IsSplittingField.adjoin_rootSet_eq_range E p (j'.restrictScalars F)]
      exact ⟨x, (j'.commutes _).trans (algHomAdjoinIntegralEquiv_symm_apply_gen F hx _)⟩
    · rwa [Polynomial.map_map, ← IsScalarTower.algebraMap_eq]
  · exact Polynomial.map_ne_zero hp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
h : M.RankFinite
⊢ ¬¬M.RankFinite

Tactic:
simpa

Goal state after:
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)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ ∀ (I : Set α),
    (∀ J ⊆ I,
        J.Finite →
          (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).matroid.Indep
            J) →
      (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).matroid.Indep I

Tactic:
simpa

Goal state after:
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:
apply induction_on_adjoin (fun K ↦ ∃ α : E, F⟮α⟯ = K) ⟨0, adjoin_zero⟩

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
⊢ ∀ (K : IntermediateField F E) (x : E), (∃ α, F⟮α⟯ = K) → ∃ α, F⟮α⟯ = IntermediateField.restrictScalars F (↥K)⟮x⟯
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
x✝ : Set α
⊢ Indep x✝ ↔ ∃ B, IsBase B ∧ x✝ ⊆ B

Tactic:
hI,

Goal state after:
α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
x✝ : Set α
⊢ M.Indep x✝ ↔ ∃ B, IsBase B ∧ x✝ ⊆ B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : e ∉ ⋃ i, I i
i : ι
hes : e ∈ X i
⊢ M.Dep (insert e (⋃ i, I i))

Tactic:
mem_iUnion,

Goal state after:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : ¬∃ i, e ∈ I i
i : ι
hes : e ∈ X i
⊢ M.Dep (insert e (⋃ i, I i))
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R✝ I✝ X Y : Set α
inst✝ : M.Finitary
R I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J ∧ J ⊆ R
e : α
heI : e ∈ I
⊢ {e} ⊆ I

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
E B I✝ X R J I : Set α
h : ∀ J ⊆ I, J.Finite → J ⊆ E
e : α
heI : e ∈ I
⊢ {e} ⊆ I

Tactic:
simpa

Goal state after:
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
⊢ ∀ (I : Set α),
    (∀ J ⊆ I,
        J.Finite →
          (IndepMatroid.ofFinitaryCardAugment E Indep indep_empty indep_subset indep_aug indep_compact
                  subset_ground).matroid.Indep
            J) →
      (IndepMatroid.ofFinitaryCardAugment E Indep indep_empty indep_subset indep_aug indep_compact
              subset_ground).matroid.Indep
        I

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
E B I X R J K : Set α
hK : ∀ J ⊆ K, J.Finite → J ⊆ I ∩ E
e : α
heK : e ∈ K
⊢ {e} ⊆ K

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
hB : (N ↾ range f).IsBase (f '' I)
⊢ (N ↾ range f).Indep (f '' I')

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
h₂ : (N ↾ range f).IsBase (f '' B)
⊢ (N ↾ range f).Indep (f '' I)

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
⊢ (N ↾ range f).Indep (f '' I)

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I J : Set α
hI : ∀ (J : Finset α), ↑J ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), ↑J_1 ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset.card < hJfin.toFinset.card
e : α
heJ : e ∈ J
heI : e ∉ I
hi : Indep (insert e hIfin.toFinset)
K : Finset α
hK : ↑K ⊆ insert e I
⊢ ↑K ⊆ ↑(insert e hIfin.toFinset)

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I : Set α
hI : ∀ (J : Finset α), ↑J ⊆ I → Indep J
x : α
hxI : x ∈ I
⊢ ↑{x} ⊆ I

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
⊢ (Matroid.ofExistsFiniteIsBase E IsBase ⋯ isBase_exchange subset_ground).IsBase B

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ (∃ B, M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X) ∧ X ⊆ M.E ↔ ∃ B, M.IsBase B ∧ X ⊆ M.E ∧ Disjoint X B

Tactic:
exact ⟨fun ⟨⟨B, hB, _, hBX⟩, hX⟩ ↦ ⟨B, hB, hX, hBX.symm⟩,
    fun ⟨B, hB, hXE, hXB⟩ ↦ ⟨⟨B, hB, hB.subset_ground, hXB.symm⟩, hXE⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ BijOn f E N✶.E

Tactic:
simpa

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
h : M.IsRkFinite X
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
⊢ M.IsBasis' (↑hIfin.toFinset) X

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ B ⊆ E

Tactic:
simpa

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
x✝ : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
⊢ C = insert e I

Tactic:
hI,

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
x✝ : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
⊢ C = insert e (C \ {e})
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ I ∈ {J | J ⊆ I ∧ e ∈ M.closure J}

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N : Matroid β
inst✝ : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
e : β
he : e ∈ I
⊢ {e} ⊆ I

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
⊢ I ∈ {J | J ⊆ I ∧ e ∈ M.closure J}

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ I ∈ {J | J ⊆ I ∧ e ∈ M.closure J}

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.Indep I
⊢ M.Indep (⇑f.symm '' ⇑f '' I)

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f.symm '' I)

Tactic:
exact ⟨by rintro ⟨I, hI, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.Dep I
⊢ M.Dep (⇑f.symm '' ⇑f '' I)

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
D : Set β
⊢ (∃ D₀, M.Dep D₀ ∧ D = ⇑f '' D₀) ↔ M.Dep (⇑f.symm '' D)

Tactic:
exact ⟨by rintro ⟨I, hI, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.IsBase I
⊢ M.IsBase (⇑f.symm '' ⇑f '' I)

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = ⇑f '' B₀) ↔ M.IsBase (⇑f.symm '' B)

Tactic:
exact ⟨by rintro ⟨I, hI, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
h : ¬M.Indep {e} ∧ e ∈ M.E
B : Set α
hB : M.IsBase B
heB : e ∈ B
⊢ {e} ⊆ B

Tactic:
simpa

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

Goal state before:
pp: α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set α
hIX : M.IsBasis I X
⊢ M.IsBasis (⇑f.symm '' ⇑f '' I) (⇑f.symm '' ⇑f '' X)

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
X I : Set α
M : Matroid α
hIX : I ⊆ X
⊢ I ⊆ range Subtype.val

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ {e} ⊆ R

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
⊢ M.IsBasis ∅ X

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
he : e ∉ X
x✝ : ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C
C : Set α
hCX : C ⊆ insert e X
hC : M.IsCircuit C
heC : e ∈ C
⊢ C \ {e} ⊆ X

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ M.Indep {f}

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ e ∉ {f}

Tactic:
simpa

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ Ii.encard + M.eRk (IX ∪ IY) ≤ (IX ∪ IY).encard + (IX ∩ IY).encard

Tactic:
add_comm

Goal state after:
α : Type u_1
M : Matroid α
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ M.eRk (IX ∪ IY) + Ii.encard ≤ (IX ∪ IY).encard + (IX ∩ IY).encard
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
h : M.IsCocircuit {e}
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ C ∩ {e} = {e}

Tactic:
simpa

Goal state after: