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

Goal state before:
pp: case mpr
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f)).range
g : N →ₗ[R] M
s : ↥I.primeCompl
⊢ ↑R ((LocalizedModule.map I.primeCompl) (f ∘ₗ g)) =
    ↑R
      (((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
            (LocalizedModule I.primeCompl N))
          ((LocalizedModule.map I.primeCompl) f))
        ((LocalizedModule.map I.primeCompl) g))

Tactic:
apply IsLocalizedModule.ext I.primeCompl (LocalizedModule.mkLinearMap I.primeCompl N)

Goal state after:
case mpr.map_unit
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f)).range
g : N →ₗ[R] M
s : ↥I.primeCompl
⊢ ∀ (x : ↥I.primeCompl), IsUnit ((algebraMap R (Module.End R (LocalizedModule I.primeCompl N))) ↑x)

case mpr.h
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f)).range
g : N →ₗ[R] M
s : ↥I.primeCompl
⊢ ↑R ((LocalizedModule.map I.primeCompl) (f ∘ₗ g)) ∘ₗ LocalizedModule.mkLinearMap I.primeCompl N =
    ↑R
        (((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
              (LocalizedModule I.primeCompl N))
            ((LocalizedModule.map I.primeCompl) f))
          ((LocalizedModule.map I.primeCompl) g)) ∘ₗ
      LocalizedModule.mkLinearMap I.primeCompl N
Module: Mathlib.RingTheory.Localization.Free

Goal state before:
pp: case refine_2
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)
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))))
i : I
this : e'.symm (Finsupp.single i 1) = LocalizedModule.mk (Finsupp.single i 1) 1
he :
  (LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯)
      (e'.symm (Finsupp.single i 1)) =
    b.repr ((LocalizedModule.lift (Submonoid.powers r) f ⋯) (e.symm (e'.symm (Finsupp.single i 1))))
⊢ (LocalizedModule.lift (Submonoid.powers r) f ⋯) (e.symm (e'.symm (Finsupp.single i 1))) = b i

Tactic:
apply b.repr.injective

Goal state after:
case refine_2
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)
e' : LocalizedModule (Submonoid.powers r) (I →₀ R) ≃ₗ[R] I →₀ Localization (Submonoid.powers r) := ⋯
i : I
this : e'.symm (Finsupp.single i 1) = LocalizedModule.mk (Finsupp.single i 1) 1
he :
  (LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯)
      (e'.symm (Finsupp.single i 1)) =
    b.repr ((LocalizedModule.lift (Submonoid.powers r) f ⋯) (e.symm (e'.symm (Finsupp.single i 1))))
⊢ b.repr ((LocalizedModule.lift (Submonoid.powers r) f ⋯) (e.symm (e'.symm (Finsupp.single i 1)))) = b.repr (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
N : ι → Type u_4
inst✝⁵ : (i : ι) → AddCommMonoid (N i)
inst✝⁴ : (i : ι) → Module R (N i)
P : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (P i)
inst✝² : (i : ι) → Module R (P i)
inst✝¹ : (i : ι) → Module S (P i)
inst✝ : ∀ (i : ι), IsScalarTower R S (P i)
ε : (i : ι) → N i →ₗ[R] P i
ibc : ∀ (i : ι), IsBaseChange S (ε i)
⊢ IsBaseChange S (lmap ε)

Tactic:
apply of_equiv <| directSumRight R S S N ≪≫ₗ congrLinearEquiv fun i ↦ (ibc i).equiv

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
N : ι → Type u_4
inst✝⁵ : (i : ι) → AddCommMonoid (N i)
inst✝⁴ : (i : ι) → Module R (N i)
P : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (P i)
inst✝² : (i : ι) → Module R (P i)
inst✝¹ : (i : ι) → Module S (P i)
inst✝ : ∀ (i : ι), IsScalarTower R S (P i)
ε : (i : ι) → N i →ₗ[R] P i
ibc : ∀ (i : ι), IsBaseChange S (ε i)
⊢ ∀ (x : ⨁ (i : ι), N i), (directSumRight R S S N ≪≫ₗ congrLinearEquiv fun i ↦ ⋯.equiv) (1 ⊗ₜ[R] x) = (lmap ε) x
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case refine_2
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
S : Finset (Dual R M × M)
hS : (linearEquiv R M).symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
f : Dual R M
m : M
left✝ : (f, m) ∈ S
hr : (f, m).1 (f, m).2 ∈ Finset.image (fun i ↦ i.1 i.2) S
f' : Dual (Localization.Away (f m)) (LocalizedModule.Away (f m) M) :=
  LinearMap.extendScalarsOfIsLocalization (Submonoid.powers (f m)) (Localization.Away (f m))
    ((IsLocalizedModule.map (Submonoid.powers (f m)) (LocalizedModule.mkLinearMap (Submonoid.powers (f m)) M)
        (Algebra.linearMap R (Localization.Away (f m))))
      f)
⊢ Free (Localization.Away ((f, m).1 (f, m).2)) (LocalizedModule.Away ((f, m).1 (f, m).2) M)

Tactic:
have surj : Function.Surjective f' := LinearMap.range_eq_top.mp <| Ideal.eq_top_of_isUnit_mem
    _ ⟨_, IsLocalizedModule.map_apply ..⟩ (IsLocalization.Away.algebraMap_isUnit (f m))

Goal state after:
case refine_2
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
S : Finset (Dual R M × M)
hS : (linearEquiv R M).symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
f : Dual R M
m : M
left✝ : (f, m) ∈ S
hr : (f, m).1 (f, m).2 ∈ Finset.image (fun i ↦ i.1 i.2) S
f' : Dual (Localization.Away (f m)) (LocalizedModule.Away (f m) M) :=
  LinearMap.extendScalarsOfIsLocalization (Submonoid.powers (f m)) (Localization.Away (f m))
    ((IsLocalizedModule.map (Submonoid.powers (f m)) (LocalizedModule.mkLinearMap (Submonoid.powers (f m)) M)
        (Algebra.linearMap R (Localization.Away (f m))))
      f)
surj : Function.Surjective ⇑f'
⊢ Free (Localization.Away ((f, m).1 (f, m).2)) (LocalizedModule.Away ((f, m).1 (f, m).2) M)
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hx : eval₂ ιEE' x h = 0
f_root : eval₂ ιEE' (ιEE' γ - ιEE' (ιFE c) * x) (Polynomial.map ιFE f) = 0
⊢ ιEE' γ - ιEE' (ιFE c) * x ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots

Tactic:
eval₂_map

Goal state after:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hx : eval₂ ιEE' x h = 0
f_root : eval₂ (ιEE'.comp ιFE) (ιEE' γ - ιEE' (ιFE c) * x) f = 0
⊢ ιEE' γ - ιEE' (ιFE c) * x ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots
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
α : ↥K
h : F⟮α⟯ = ⊤
⊢ ∃ α, F⟮α⟯ = K

Tactic:
exact ⟨α, by simpa only [lift_adjoin_simple, lift_top] using congr_arg lift h⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X

Tactic:
inter_eq_self_of_subset_left hX

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ M.IsBasis I X ↔ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hX : X ⊆ M.E
⊢ ∃ J, M.IsBasis J X ∧ I ⊆ J

Tactic:
obtain ⟨J, hJ, hJmax⟩ := M.maximality X hX I hI hIX
  exact ⟨J, ⟨hJmax, hX⟩, hJ⟩

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

Goal state before:
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 I B'' ∧ e ∉ B''

Tactic:
and_iff_left heB''

Goal state after:
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 I B''
Module: Mathlib.Combinatorics.Matroid.Constructions

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

Tactic:
by
  rw [eq_freeOn_iff, and_iff_right M.restrict_ground_eq, restrict_indep_iff,
    and_iff_left Subset.rfl]

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
⊢ (∀ (J_1 : Finset α), ↑J_1 ⊆ J → Indep J_1) →
    J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ ∀ (J : Finset α), ↑J ⊆ insert e I → Indep J

Tactic:
hJ

Goal state after:
α : 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
⊢ J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ ∀ (J : Finset α), ↑J ⊆ insert e I → Indep J
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

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

Tactic:
exact fun I ↦ Indep.subset_ground

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.IsRkFinite M.E ↔ M.RankFinite

Tactic:
by
  rw [IsRkFinite, restrict_ground_eq_self]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
⊢ M.Indep J → ¬insert (f e) (f '' I) = f '' J

Tactic:
hJ

Goal state after:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
hJ : M.Indep J
⊢ ¬insert (f e) (f '' I) = f '' J
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (M.IsBase (M.E \ B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).IsBase (f '' B)

Tactic:
map_image_isBase_iff (show B ⊆ M✶.E from hB),

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (M.IsBase (M.E \ B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ M✶.IsBase B
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C R : Set α
hCR : C ⊆ R
hC : (¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ M.E → D ⊆ C → D = C
⊢ (¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ R → D ⊆ C → D = C

Tactic:
exact ⟨⟨hC.1.1, hCR⟩, fun I hI _ hIC ↦ hC.2 hI (hIC.trans hC.1.2) hIC⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∈ X
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e

Tactic:
exact fun b hbX h ↦ h _ (singleton_subset_iff.2 heX) Subset.rfl

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

Goal state before:
pp: α : Type u_1
M : Matroid α
E : Set α
h : M.loops = E
h' : M.E = E
⊢ M.closure ∅ = M.E

Tactic:
← loops,

Goal state after:
α : Type u_1
M : Matroid α
E : Set α
h : M.loops = E
h' : M.E = E
⊢ M.loops = M.E
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
E : Set α
x✝ : M.loops = E ∧ M.E = E
h : M.loops = E
h' : M.E = E
⊢ M.closure ∅ = M.E

Tactic:
← loops,

Goal state after:
α : Type u_1
M : Matroid α
E : Set α
x✝ : M.loops = E ∧ M.E = E
h : M.loops = E
h' : M.E = E
⊢ M.loops = M.E
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hcl : z ∈ M.closure ((⋃ i, I i) ∪ J \ {z})
⊢ z ∉ (⋃ i, I i) ∪ J \ {z}

Tactic:
simp [hzI]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk X ≤ M.eRk M.E

Tactic:
← eRk_inter_ground

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk (X ∩ M.E) ≤ M.eRk M.E
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case refine_1
α : 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 {e, f} ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})

Tactic:
suffices ¬ M.Indep {e, f} by simpa [pair_sdiff_left hef, hf, pair_sdiff_right hef, he]

Goal state after:
case refine_1
α : 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 {e, f}
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ X ∩ M.E ⊆ M.loops ↔ X ⊆ M.loops

Tactic:
inter_eq_self_of_subset_left hX

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ X ⊆ M.loops ↔ X ⊆ M.loops
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ z ∈ M.closure ((range x ∪ ⋃ i, I i) ∪ J \ {z})

Tactic:
union_right_comm

Goal state after:
case inr
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ z ∈ M.closure (range x ∪ J \ {z} ∪ ⋃ i, I i)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ z ∈ M.closure ((⋃ i, I i) ∪ J \ {z})

Tactic:
rw [closure_union_congr_left <| closure_iUnion_congr _ _ hC',
    iUnion_insert_eq_range_union_iUnion, union_right_comm]

Goal state after:
case inr
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ z ∈ M.closure (range x ∪ J \ {z} ∪ ⋃ i, I i)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ I.Infinite ↔ ¬M.IsRkFinite X

Tactic:
← hI.finite_iff_isRkFinite,

Goal state after:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ I.Infinite ↔ ¬I.Finite
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
J : Set α
hr : J.encard ≤ I.encard
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ M.closure X = M.closure Y

Tactic:
rw [← closure_inter_ground, ← M.closure_inter_ground Y,
    ← hI.isBasis_inter_ground.closure_eq_closure,
    ← hJ.isBasis_inter_ground.closure_eq_closure, Finite.eq_of_subset_of_encard_le
      (hI.indep.finite_of_subset_isRkFinite hI.subset hX) hIJ hr]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.Indep I
⊢ M.eRk I = I.encard

Tactic:
rw [h.eRk_eq_encard]

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

Goal state before:
pp: case refine_2
α : 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
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
h : ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ False

Tactic:
simpa [hC.mem_closure_sdiff_singleton_of_mem heC] using h (C \ {e})

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ ⋂₀ {F | M.IsFlat F ∧ X ∩ M.E ⊆ F} = ⋂₀ {F | M.IsFlat F ∧ X ⊆ F}

Tactic:
inter_eq_self_of_subset_left hX

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ ⋂₀ {F | M.IsFlat F ∧ X ⊆ F} = ⋂₀ {F | M.IsFlat F ∧ X ⊆ F}
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
⊢ M.cRk M.E = M.cRank

Tactic:
by
  rw [cRk, restrict_ground_eq_self]

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

Goal state before:
pp: α✝ : Type u_1
M✝ : Matroid α✝
e✝ : α✝
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
heR : e ∈ R
⊢ (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R

Tactic:
rw [isColoop_iff_forall_notMem_isCircuit heR, mem_closure_iff_exists_isCircuit (by simp)]

Goal state after:
α✝ : Type u_1
M✝ : Matroid α✝
e✝ : α✝
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
heR : e ∈ R
⊢ (∀ ⦃C : Set α⦄, (M ↾ R).IsCircuit C → e ∉ C) ↔ (¬∃ C ⊆ insert e (R \ {e}), M.IsCircuit C ∧ e ∈ C) ∧ e ∈ R
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case refine_2
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ lift.{v, u} #↑I ≤ lift.{u, v} (⨆ B, #↑↑B)

Tactic:
rw [← mk_image_eq_of_injOn_lift _ _ (hf.mono hI.indep.subset_ground), lift_le]

Goal state after:
case refine_2
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ #↑(f '' I) ≤ ⨆ B, #↑↑B
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E \ M.closure (B \ {e})
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
⊢ M.Spanning (M.E \ X)

Tactic:
rw [subset_sdiff] at hXss

Goal state after:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
⊢ M.Spanning (M.E \ X)