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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
s : S
⊢ (auxHom S r) ((auxInv S r) s) = s

Tactic:
simpa using congrFun (congrArg DFunLike.coe <| auxHom_auxInv S r) s

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : Subsingleton (LocalizedModule p.primeCompl M)
⊢ { asIdeal := p, isPrime := ⋯ } ∈ (Module.support R M)ᶜ

Tactic:
simpa [Module.notMem_support_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
this : LinearOrder (Free.ChooseBasisIndex R M) := linearOrderOfSTO WellOrderingRel
B : Basis (↑(powersetCard (Free.ChooseBasisIndex R M) n)) R ↥(⋀[R]^n M) := Basis.exteriorPower n (Free.chooseBasis R M)
⊢ (Nat.card (Free.ChooseBasisIndex R M)).choose n = (Fintype.card (Free.ChooseBasisIndex R M)).choose n

Tactic:
Fintype.card_eq_nat_card

Goal state after:
R : Type u_1
M : Type u_3
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
this : LinearOrder (Free.ChooseBasisIndex R M) := linearOrderOfSTO WellOrderingRel
B : Basis (↑(powersetCard (Free.ChooseBasisIndex R M) n)) R ↥(⋀[R]^n M) := Basis.exteriorPower n (Free.chooseBasis R M)
⊢ (Nat.card (Free.ChooseBasisIndex R M)).choose n = (Nat.card (Free.ChooseBasisIndex R M)).choose n
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ Function.Surjective ⇑(M.mulMap' N)

Tactic:
simp_rw [mulMap', LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.comp_surjective,
    LinearMap.surjective_rangeRestrict]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: case smul_tprod
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
⊢ r • (cast R M ⋯) (GradedMonoid.GMul.mul ((tprod R) a) ((tprod R) Fin.elim0)) = r • (tprod R) a

Tactic:
tprod_mul_tprod R a _,

Goal state after:
case smul_tprod
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
⊢ r • (cast R M ⋯) ((tprod R) (Fin.append a Fin.elim0)) = r • (tprod R) a
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective
    (⇑(M.mulMap N) ∘
      ⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)) ∘ ⇑(TensorProduct.finsuppScalarLeft R (↥N) ι).symm)

Tactic:
← Function.comp_assoc,

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective
    ((⇑(M.mulMap N) ∘ ⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m))) ∘
      ⇑(TensorProduct.finsuppScalarLeft R (↥N) ι).symm)
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥M
ι : Type u_1
n : ι → ↥N
hn : LinearIndependent R n
⊢ Function.Injective
    (⇑(M.mulMap N) ∘
      ⇑(LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)) ∘ ⇑(TensorProduct.finsuppScalarRight R R (↥M) ι).symm)

Tactic:
← Function.comp_assoc,

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥M
ι : Type u_1
n : ι → ↥N
hn : LinearIndependent R n
⊢ Function.Injective
    ((⇑(M.mulMap N) ∘ ⇑(LinearMap.lTensor (↥M) (Finsupp.linearCombination R n))) ∘
      ⇑(TensorProduct.finsuppScalarRight R R (↥M) ι).symm)
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
this : ∀ (j : Fin l), ¬IsUnit (a n j)
⊢ v n✝ ∈ 𝔪 • ⊤

Tactic:
show v n = _ from hay n

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
this : ∀ (j : Fin l), ¬IsUnit (a n j)
⊢ ∑ j, a n j • y j ∈ 𝔪 • ⊤
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hn : ⟨↑b, ⋯⟩ = 0 ∧ ⟨↑a, ⋯⟩ = 0
⊢ False

Tactic:
rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hn

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hn : b = 0 ∧ ⟨↑a, ⋯⟩ = 0
⊢ False
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hn : b = 0 ∧ ⟨↑a, ⋯⟩ = 0
⊢ False

Tactic:
rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hn

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hn : b = 0 ∧ a = 0
⊢ False
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I✝ : Ideal R
hI✝ : ¬I✝.minimalPrimes.Finite
I : Ideal R
hI : ¬I.minimalPrimes.Finite
hmax : ∀ (I_1 : Submodule R R), I < I_1 → (Ideal.minimalPrimes I_1).Finite
⊢ ¬I.IsPrime

Tactic:
contrapose hI

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I✝ : Ideal R
hI✝ : ¬I✝.minimalPrimes.Finite
I : Ideal R
hmax : ∀ (I_1 : Submodule R R), I < I_1 → (Ideal.minimalPrimes I_1).Finite
hI : I.IsPrime
⊢ I.minimalPrimes.Finite
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I✝ : Ideal R
hI✝ : ¬I✝.minimalPrimes.Finite
I : Ideal R
hI : ¬I.minimalPrimes.Finite
hmax : ∀ (I_1 : Submodule R R), I < I_1 → (Ideal.minimalPrimes I_1).Finite
h1 : ¬I.IsPrime
⊢ I ≠ ⊤

Tactic:
contrapose hI

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I✝ : Ideal R
hI✝ : ¬I✝.minimalPrimes.Finite
I : Ideal R
hmax : ∀ (I_1 : Submodule R R), I < I_1 → (Ideal.minimalPrimes I_1).Finite
h1 : ¬I.IsPrime
hI : I = ⊤
⊢ I.minimalPrimes.Finite
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hn : b = 0 ∧ a = 0
⊢ False

Tactic:
rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hn

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hn : b = 0 ∧ a = 0
⊢ False
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Colon

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : span R ↑s = ⊤
z : R := ∏ y ∈ s, f y
hz : z ∉ I
hz' : K ≤ N.colon {z • x}
⊢ False

Tactic:
replace hz' : K * Ideal.span {z} ≤ ann := by
    rw [mul_comm, Ideal.span_singleton_mul_le_iff]
    intro i hi
    simpa only [ann, mem_colon_singleton, mul_comm, mul_smul] using hz' hi

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : span R ↑s = ⊤
z : R := ∏ y ∈ s, f y
hz : z ∉ I
hz' : K * Ideal.span {z} ≤ ann
⊢ False
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x ↦ x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) ⋯
⊢ ∀ (x : ↑C₀) (hx : x ∈ Subtype.val ⁻¹' C₁ ∩ Subtype.val ⁻¹' C₂),
    (comap { toFun := C₁.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₁) ⟨x, ⋯⟩ =
      (comap { toFun := C₂.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₂) ⟨x, ⋯⟩

Tactic:
by
      rintro ⟨x, hx₀⟩ ⟨hx₁ : x ∈ C₁, hx₂ : x ∈ C₂⟩
      simpa using hf x ⟨hx₁, hx₂⟩

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
inst✝ : FinitePresentation R M
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this✝³ : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : p ∈ freeLocus R M
hp : ⟨p, hp''⟩ ∈ Subtype.val ⁻¹' ↑(basicOpen f)
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this✝² : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
this✝¹ : IsScalarTower R (Localization.Away f) Rₚ
this✝ : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
this : IsScalarTower R (Localization.Away f) Mₚ
⊢ rankAtStalk M ↑⟨p, hp''⟩ = rankAtStalk M ↑⟨x, hx⟩

Tactic:
have : IsScalarTower (Localization.Away f) Rₚ Mₚ :=
    ⟨fun r r' m ↦ show _ = algebraMap _ Rₚ r • r' • m by rw [← mul_smul, ← Algebra.smul_def]⟩

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this✝⁴ : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : p ∈ freeLocus R M
hp : ⟨p, hp''⟩ ∈ Subtype.val ⁻¹' ↑(basicOpen f)
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this✝³ : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
this✝² : IsScalarTower R (Localization.Away f) Rₚ
this✝¹ : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
this✝ : IsScalarTower R (Localization.Away f) Mₚ
this : IsScalarTower (Localization.Away f) Rₚ Mₚ
⊢ rankAtStalk M ↑⟨p, hp''⟩ = rankAtStalk M ↑⟨x, hx⟩
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case right
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
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : ↥(⨆ f, f.fieldRange)
x✝ : x ∈ ⊤
⊢ (⨆ f, f.fieldRange).val.toRingHom x ∈ ⇑(⨆ f, f.fieldRange).val.toRingHom '' ↑(⨆ f, f.fieldRange)

Tactic:
rw [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, coe_val, ← IntermediateField.coe_val,
    ← IntermediateField.coe_map, IntermediateField.map_iSup]

Goal state after:
case right
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
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : ↥(⨆ f, f.fieldRange)
x✝ : x ∈ ⊤
⊢ (⨆ f, f.fieldRange).val x ∈ ↑(⨆ i, IntermediateField.map (⨆ f, f.fieldRange).val i.fieldRange)
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case inl
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
hFEp : IsSplittingField F E 0
this : ⊥ = ⊤
⊢ Normal F E

Tactic:
exact Normal.of_algEquiv
      (AlgEquiv.ofBijective (Algebra.ofId F E) (Algebra.bijective_algebraMap_iff.2 this.symm))

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

Goal state before:
pp: case refine_2
F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨅ i, t i)
⊢ (Polynomial.map (algebraMap F ↥(⨅ i, t i)) (minpoly F x)).Splits

Tactic:
have hx : ∀ i, Splits ((minpoly F x).map (algebraMap F (t i))) := by
      intro i
      rw [← minpoly.algHom_eq (inclusion (iInf_le t i)) (inclusion (iInf_le t i)).injective]
      exact (h i).splits' (inclusion (iInf_le t i) x)

Goal state after:
case refine_2
F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨅ i, t i)
hx : ∀ (i : ι), (Polynomial.map (algebraMap F ↥(t i)) (minpoly F x)).Splits
⊢ (Polynomial.map (algebraMap F ↥(⨅ i, t i)) (minpoly F x)).Splits
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 α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)

Tactic:
by_contra! ⟨I, e, -, hIe, h⟩

Goal state after:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I : Set α
e : α
hIe : ¬Indep (insert e I)
h : ∀ I₀ ⊆ I, I₀.Finite → Indep (insert e I₀)
⊢ False
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : 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
⊢ B'' ∩ X ∪ B' \ X ⊆ B'

Tactic:
rw [union_subset_iff, and_iff_left sdiff_subset, ← union_sdiff_cancel hJX,
        inter_union_distrib_left, hdj.symm.inter_eq, empty_union, sdiff_eq, ← inter_assoc,
        ← sdiff_eq, sdiff_subset_comm, sdiff_eq, inter_assoc, ← sdiff_eq, inter_comm]

Goal state after:
α : 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
⊢ X \ B' ∩ B'' ⊆ J
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 ∈ f '' X \ f '' I, (M.map f hf).Dep (insert e (f '' I))

Tactic:
rintro _ ⟨⟨e, he, rfl⟩, he'⟩

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
⊢ (M.map f hf).Dep (insert (f e) (f '' I))
Module: Mathlib.Combinatorics.Matroid.Circuit

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

Tactic:
restrict_dep_iff,

Goal state after:
α : Type u_1
M : Matroid α
C R : Set α
hCR : C ⊆ R
hC : M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C
⊢ (¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D ∧ D ⊆ R → D ⊆ C → D = C
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ ((M ↾ R).Dep C ∧ ∀ ⦃D : Set α⦄, (M ↾ R).Dep D → D ⊆ C → D = C) →
    (M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C) ∧ C ⊆ R

Tactic:
restrict_dep_iff,

Goal state after:
α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ ((¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D ∧ D ⊆ R → D ⊆ C → D = C) →
    (M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C) ∧ C ⊆ R
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
e : α
f : α → β
hf : InjOn f M.E
he : e ∈ M.E
⊢ f e ∈ (M.map f hf).loops ↔ M.IsLoop e

Tactic:
map_loops,

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
e : α
f : α → β
hf : InjOn f M.E
he : e ∈ M.E
⊢ f e ∈ f '' M.loops ↔ M.IsLoop e
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
F : ↑(Iic M.E)
⊢ M.subtypeClosure.IsClosed F ↔ M.IsFlat ↑F

Tactic:
by
  simp [subtypeClosure]

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

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

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

Goal state after:
α : Type u_1
M : Matroid α
e : α
h : M.eRk {e} = 1
⊢ M.IsNonloop e
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case neg
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∉ C₁
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
exact ⟨C₁, subset_sdiff_singleton subset_union_left he₁, hC₁⟩

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

Goal state before:
pp: α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
aux : ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
⊢ (M ↾ X).cRk Y = M.cRk Y

Tactic:
simp_rw [le_antisymm_iff, cRk_le_iff]

Goal state after:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
aux : ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
⊢ (∀ ⦃I : Set α⦄, (M ↾ X).IsBasis' I Y → #↑I ≤ M.cRk Y) ∧ ∀ ⦃I : Set α⦄, M.IsBasis' I Y → #↑I ≤ (M ↾ X).cRk Y
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
rwa [hI.closure_eq_setOfPred_isBasis_insert, mem_ofPred, isBasis_insert_iff]

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

Goal state before:
pp: case e'_2
α : Type u_1
M : Matroid α
K✝ K : Set α
⊢ (∀ (x : Set α), M.IsBase x ∧ x ⊆ M.E → (x ∩ K).Nonempty) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty

Tactic:
and_iff_left_of_imp IsBase.subset_ground,

Goal state after:
case e'_2
α : Type u_1
M : Matroid α
K✝ K : Set α
⊢ (∀ (x : Set α), M.IsBase x → (x ∩ K).Nonempty) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty