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

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
this : IsUnit (mk' (FractionRing R) x ⟨y, ⋯⟩)
⊢ ↑((toPrincipalIdeal R (FractionRing R)) this.unit * I) = ↑J

Tactic:
Units.val_mul,

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
this : IsUnit (mk' (FractionRing R) x ⟨y, ⋯⟩)
⊢ ↑((toPrincipalIdeal R (FractionRing R)) this.unit) * ↑I = ↑J
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
⊢ Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{uM', uM} (Module.rank R M)

Tactic:
by
  apply Cardinal.lift_injective.{max uM' uR'}
  have := (algebraMap R Rₛ).domain_nontrivial
  have := (IsLocalizedModule.isBaseChange S Rₛ f).equiv.lift_rank_eq.symm
  simp only [rank_tensorProduct, rank_self,
    Cardinal.lift_one, one_mul, Cardinal.lift_lift] at this ⊢
  convert! this
  exact Cardinal.lift_umax

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max u_1 uM) := ↥s →₀ R
⊢ Projective R M

Tactic:
let f : N →ₗ[R] M := Finsupp.linearCombination R (Subtype.val : s → M)

Goal state after:
R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max u_1 uM) := ↥s →₀ R
f : N →ₗ[R] M := Finsupp.linearCombination R Subtype.val
⊢ Projective R M
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)
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))))
i : I
this : e'.symm (Finsupp.single i 1) = LocalizedModule.mk (Finsupp.single i 1) 1
⊢ (LocalizedModule.lift (Submonoid.powers r) f ⋯) (e.symm (e'.symm (Finsupp.single i 1))) = b i

Tactic:
replace he := LinearMap.congr_fun he (e.symm (e'.symm (Finsupp.single i 1)))

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) :=
  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ₛ)) ⋯ ∘ₗ ↑R ↑e)
      (e.symm (e'.symm (Finsupp.single i 1))) =
    (↑(LinearEquiv.restrictScalars R 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
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_1
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
e : M ≃ₗ[R] M'
p : PrimeSpectrum R
⊢ p ∈ freeLocus R M ↔ p ∈ freeLocus R M'

Tactic:
exact mem_freeLocus_of_isLocalization _ _ _
    (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M' ∘ₗ e.toLinearMap)

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
hp : p ∈ comap (algebraMap R A) ⁻¹' freeLocus R M
Rₚ : Type uR := Localization.AtPrime (comap (algebraMap R A) p).asIdeal
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
⊢ p ∈ freeLocus A (A ⊗[R] M)

Tactic:
Set.mem_preimage,

Goal state after:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
hp : comap (algebraMap R A) p ∈ freeLocus R M
Rₚ : Type uR := Localization.AtPrime (comap (algebraMap R A) p).asIdeal
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
⊢ p ∈ freeLocus A (A ⊗[R] M)
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝⁴ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝³ : IsScalarTower R (Localization S) Rₚ
this✝² : IsLocalization.AtPrime Rₚ p.asIdeal
this✝¹ : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this✝ : IsScalarTower R (Localization S) Mₚ
this : IsScalarTower (Localization S) Rₚ Mₚ
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ comap (algebraMap R (Localization S)) p ∈ freeLocus R M

Tactic:
let l := (IsLocalizedModule.liftOfLE _ _ hp' (LocalizedModule.mkLinearMap S M)
    (LocalizedModule.mkLinearMap p'.primeCompl M)).extendScalarsOfIsLocalization S
    (Localization S)

Goal state after:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝⁴ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝³ : IsScalarTower R (Localization S) Rₚ
this✝² : IsLocalization.AtPrime Rₚ p.asIdeal
this✝¹ : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this✝ : IsScalarTower R (Localization S) Mₚ
this : IsScalarTower (Localization S) Rₚ Mₚ
l : LocalizedModule S M →ₗ[Localization S] LocalizedModule p'.primeCompl M :=
  LinearMap.extendScalarsOfIsLocalization S (Localization S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ comap (algebraMap R (Localization S)) p ∈ freeLocus R M
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : derivedSeries G (n✝ + 1) = ⊥
⊢ ∀ (a b : G), a * b = b * a

Tactic:
rw [IsSimpleGroup.derivedSeries_succ] at hn

Goal state after:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
⊢ ∀ (a b : G), a * b = b * a
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
e : M ⊗[R] N ≃ₗ[R] R
⊢ Function.Bijective ⇑(contractLeft R N)

Tactic:
show contractLeft R N = ((linearEquivDual e).rTensor N).symm ≪≫ₗ e by
      rw [LinearEquiv.coe_trans, LinearEquiv.eq_comp_toLinearMap_symm]; ext; rfl

Goal state after:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
e : M ⊗[R] N ≃ₗ[R] R
⊢ Function.Bijective ⇑↑((LinearEquiv.rTensor N (linearEquivDual e)).symm ≪≫ₗ e)
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.rTensor M f) ↔ Function.Injective ⇑f

Tactic:
← LinearMap.lTensor_inj_iff_rTensor_inj,

Goal state after:
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
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 ⇑f ∧ Function.Surjective ⇑(LinearMap.rTensor M f) ↔ Function.Injective ⇑f ∧ Function.Surjective ⇑f

Tactic:
rTensor_surjective_iff

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

Goal state before:
pp: case inr.refine_2
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
hp : p ≠ 0
x : E
this✝ : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : (Polynomial.map (↑j) (Polynomial.map (algebraMap F E) (minpoly F x))).Splits
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra (↥F⟮x⟯) L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toAlgebra
j' : E →ₐ[↥F⟮x⟯] L := IsSplittingField.lift E (Polynomial.map (algebraMap F ↥F⟮x⟯) p) ?inr.refine_1
⊢ a ∈ j.range

Tactic:
rw [← IsSplittingField.adjoin_rootSet_eq_range E p j,
            IsSplittingField.adjoin_rootSet_eq_range E p (j'.restrictScalars F)]

Goal state after:
case inr.refine_2
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
hp : p ≠ 0
x : E
this✝ : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : (Polynomial.map (↑j) (Polynomial.map (algebraMap F E) (minpoly F x))).Splits
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra (↥F⟮x⟯) L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toAlgebra
j' : E →ₐ[↥F⟮x⟯] L := IsSplittingField.lift E (Polynomial.map (algebraMap F ↥F⟮x⟯) p) ?inr.refine_1
⊢ a ∈ (AlgHom.restrictScalars F j').range
Module: Mathlib.RingTheory.AlgebraicIndependent.Defs

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
e : ι ≃ ι'
f : ι' → A
⊢ IsTranscendenceBasis R (f ∘ ⇑e) ↔ IsTranscendenceBasis R f

Tactic:
simp_rw [IsTranscendenceBasis, algebraicIndependent_equiv, EquivLike.range_comp]

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

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
hf : f ∈ B' \ B
x : α
he : x ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {x})
hfB : M.Indep (insert f (B \ {x}))
hnot : ¬Maximal M.Indep (insert f (B \ {x}))
hxB : x ∈ B \ insert f (B \ {x})
hind : M.Indep (insert x (insert f (B \ {x})))
⊢ B ⊂ insert f B

Tactic:
exact ssubset_insert hf.2

Goal state after:
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
⊢ ∃ B, IsBase B

Tactic:
simp_rw [hB]

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
⊢ ∃ B, M.IsBase B
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I X : Set α
⊢ (freeOn E).IsBasis I X ↔ I = X ∧ X ⊆ E

Tactic:
use fun h ↦ ⟨(freeOn_indep h.subset_ground).eq_of_isBasis h, h.subset_ground⟩
  rintro ⟨rfl, hIE⟩
  exact (freeOn_indep hIE).isBasis_self

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

Goal state before:
pp: α : Type u_1
I E B : Set α
hB : B ⊆ E
⊢ (uniqueBaseOn (I ∩ E) E)✶.IsBase B ↔ (uniqueBaseOn (E \ I) E).IsBase B

Tactic:
dual_isBase_iff,

Goal state after:
α : Type u_1
I E B : Set α
hB : B ⊆ E
⊢ (uniqueBaseOn (I ∩ E) E).IsBase ((uniqueBaseOn (I ∩ E) E).E \ B) ↔ (uniqueBaseOn (E \ I) E).IsBase B
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M✶.IsBase B ↔ M.IsBase (M.E \ B) ∧ B ⊆ M.E

Tactic:
dual_isBase_iff,

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M.IsBase (M.E \ B) ↔ M.IsBase (M.E \ B) ∧ B ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M✶✶.IsBase B ↔ M.IsBase B

Tactic:
dual_isBase_iff,

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M✶.IsBase (M✶.E \ B) ↔ M.IsBase B
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M✶.IsBase (M✶.E \ B) ↔ M.IsBase B

Tactic:
dual_isBase_iff,

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M.IsBase (M.E \ (M✶.E \ B)) ↔ M.IsBase B
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
h : M.IsBase B
⊢ M✶.IsBase (M.E \ B)

Tactic:
dual_isBase_iff,

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
h : M.IsBase B
⊢ M.IsBase (M.E \ (M.E \ B))
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N <r M
⊢ N.E ⊂ M.E

Tactic:
obtain ⟨R, -, rfl⟩ := h.1

Goal state after:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R <r M
⊢ (M ↾ R).E ⊂ M.E
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase B ↔ M✶.IsBase (M.E \ B)

Tactic:
dual_isBase_iff,

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase B ↔ M.IsBase (M.E \ (M.E \ B))
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
h : ¬M✶.IsBase ∅
⊢ ¬M.IsBase M.E

Tactic:
dual_isBase_iff,

Goal state after:
α : Type u_1
M : Matroid α
h : ¬M.IsBase (M.E \ ∅)
⊢ ¬M.IsBase M.E
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

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

Tactic:
obtain ⟨M, -, rfl⟩ := hex

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.IndepAxioms

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

Tactic:
obtain ⟨M, -, rfl⟩ := hex

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.IndepAxioms

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

Tactic:
obtain ⟨M, -, rfl⟩ := hex

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)
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
⊢ (N.comapOn E f)✶.IsBase B ↔ N✶.IsBase (f '' B) ∧ B ⊆ E

Tactic:
dual_isBase_iff,

Goal state after:
α : 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
⊢ (N.comapOn E f).IsBase ((N.comapOn E f).E \ B) ↔ N✶.IsBase (f '' B) ∧ B ⊆ E
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
f : α
heI : f ∉ I
he : f ∈ M.closure I
h : ∀ f_1 ∈ I, f ∉ M.closure (I \ {f_1})
⊢ M.Indep (insert f I \ {f})

Tactic:
simpa [heI]

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

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

Tactic:
simp +contextual [closure_empty]

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

Goal state before:
pp: case neg
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : ¬M.IsRkFinite X
⊢ ⊤ = M.eRk Y

Tactic:
eRk_eq_top_iff.2 (mt (fun h ↦ h.subset hXY) hX)

Goal state after:
case neg
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : ¬M.IsRkFinite X
⊢ ⊤ = ⊤
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
⊢ M.eRk {e} = 1

Tactic:
← he.indep.isBasis_self.encard_eq_eRk,

Goal state after:
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
⊢ {e}.encard = 1
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ ∀ t' ∈ {F | M.IsFlat F ∧ I ∩ M.E ⊆ F}, F ⊆ t'

Tactic:
rintro F' ⟨hF', hIF'⟩ e (he : M.IsBasis I (insert e I))
    rw [inter_eq_left.mpr (hIF.subset.trans hIF.subset_ground)] at hIF'
    obtain ⟨J, hJ, hIJ⟩ := hI.subset_isBasis_of_subset hIF' hF'.2
    exact (hF'.1 hJ (he.isBasis_union_of_subset hJ.indep hIJ)) (Or.inr (mem_insert _ _))

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

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
⊢ e ∈ M.closure I ↔ M.Dep (insert e I)

Tactic:
by
  rw [hI.insert_dep_iff, mem_sdiff, and_iff_left heI]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ X = X'

Tactic:
rwa [hf.image_eq_image_iff hX hIX.subset_ground] at hXX'

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ M✶.IsCocircuit C ↔ M.IsCircuit C

Tactic:
rw [isCocircuit_def, dual_dual]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
this : (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ x, M.IsCircuit x ∧ x.Subsingleton
⊢ M.Loopless ↔ ∀ (C : Set α), M.IsCircuit C → C.Nontrivial

Tactic:
rw [loopless_iff_forall_not_isLoop]

Goal state after:
α : Type u_1
M : Matroid α
this : (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ x, M.IsCircuit x ∧ x.Subsingleton
⊢ (∀ e ∈ M.E, ¬M.IsLoop e) ↔ ∀ (C : Set α), M.IsCircuit C → C.Nontrivial
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
I J X : Set α
inst✝ : M.InvariantCardinalRank
hIX : M.IsBasis I X
hJX : M.IsBasis J X
⊢ #↑(I \ J) + #↑(I ∩ J) = #↑J

Tactic:
hIX.cardinalMk_sdiff_comm hJX,

Goal state after:
α : Type u
M : Matroid α
I J X : Set α
inst✝ : M.InvariantCardinalRank
hIX : M.IsBasis I X
hJX : M.IsBasis J X
⊢ #↑(J \ I) + #↑(I ∩ J) = #↑J
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ ¬M✶.IsBase ∅ ↔ ∃ C, M.IsCircuit C

Tactic:
dual_isBase_iff,

Goal state after:
α : Type u_1
M : Matroid α
⊢ ¬M.IsBase (M.E \ ∅) ↔ ∃ C, M.IsCircuit C
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ Transcendental R f

Tactic:
· rw [← transcendental_polynomial_aeval_X_iff R i]
    refine h.restrictScalars fun _ _ heq ↦ MvPolynomial.C_injective σ R ?_
    simp_rw [← MvPolynomial.algebraMap_eq]
    exact congr($(heq).1)

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i ↦ (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i ↦ x ↑i
i : ι
hi : i ∉ t
a✝ : ι
h : a✝ ∈ t
⊢ a✝ ∈ x ⁻¹' ↑(supported R t)

Tactic:
rw [Set.mem_preimage]

Goal state after:
ι : Type u_1
R : Type u_3
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i ↦ (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i ↦ x ↑i
i : ι
hi : i ∉ t
a✝ : ι
h : a✝ ∈ t
⊢ x a✝ ∈ ↑(supported R t)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S I : Set α
hI : M.Indep I
hS : M.Spanning S
hIS : I ⊆ S
B : Set α
hB : M.IsBasis B S ∧ I ⊆ B
⊢ ∃ B, M.IsBase B ∧ I ⊆ B ∧ B ⊆ S

Tactic:
exact ⟨B, hB.1.isBase_of_spanning hS, hB.2, hB.1.subset⟩

Goal state after:
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: case zero
F : Type u_1
inst✝¹ : Field F
f g : F[X]
inst✝ : CharZero F
hf : HasSeparableContraction 1 f
left✝ : g.Separable
m : ℕ
hm : g = f
⊢ g.natDegree = hf.degree

Tactic:
rw [hf.eq_degree, hm]

Goal state after: