mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case refine_3
R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : FinitePresentation R M
n m : ℕ
f : (Fin n → R) →ₗ[R] M
g : (Fin m → R) →ₗ[R] Fin n → R
hf : Function.Surjective ⇑f
hfg : Function.Exact ⇑g ⇑f
⊢ Function.Exact ⇑(lcomp S (S ⊗[R] N) (baseChange S f)) ⇑(lcomp S (S ⊗[R] N) (baseChange S g))

Tactic:
apply exact_lcomp_of_exact_of_surjective

Goal state after:
case refine_3.exac
R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : FinitePresentation R M
n m : ℕ
f : (Fin n → R) →ₗ[R] M
g : (Fin m → R) →ₗ[R] Fin n → R
hf : Function.Surjective ⇑f
hfg : Function.Exact ⇑g ⇑f
⊢ Function.Exact ⇑(baseChange S g) ⇑(baseChange S f)

case surj
R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : FinitePresentation R M
n m : ℕ
f : (Fin n → R) →ₗ[R] M
g : (Fin m → R) →ₗ[R] Fin n → R
hf : Function.Surjective ⇑f
hfg : Function.Exact ⇑g ⇑f
⊢ Function.Surjective ⇑(baseChange S f)
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case C
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
a : T
⊢ (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S))
      ((algebraTensorAlgEquiv R T).symm ((algebraMap T (MvPolynomial ι T)) a)) =
    a ⊗ₜ[R] 1

Tactic:
AlgEquiv.commutes

Goal state after:
case C
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
a : T
⊢ (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) ((algebraMap T (T ⊗[R] MvPolynomial ι R)) a) =
    a ⊗ₜ[R] 1
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : f.toRingHom ↑x ∈ P'.ker ^ 2
⊢ mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))

Tactic:
eq_map,

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : f.toRingHom ↑x ∈ Ideal.map f.toRingHom P.ker ^ 2
⊢ mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P✝ P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
⊢ Ideal.span (⇑(rename ⇑e.symm) '' P.relation '' Set.range ⇑f) =
    Ideal.comap (rename ⇑e) (Ideal.span (Set.range P.relation))

Tactic:
Equiv.range_eq_univ,

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P✝ P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
⊢ Ideal.span (⇑(rename ⇑e.symm) '' P.relation '' Set.univ) = Ideal.comap (rename ⇑e) (Ideal.span (Set.range P.relation))
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P✝ P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
hf : Function.Bijective ⇑(rename ⇑e.symm)
⊢ Ideal.comap (rename ⇑e.symm) (Ideal.map (rename ⇑e.symm) (Ideal.span (Set.range P.relation))) =
    Ideal.comap (rename (⇑e ∘ ⇑e.symm)) (Ideal.span (Set.range P.relation))

Tactic:
Equiv.self_comp_symm

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P✝ P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
hf : Function.Bijective ⇑(rename ⇑e.symm)
⊢ Ideal.comap (rename ⇑e.symm) (Ideal.map (rename ⇑e.symm) (Ideal.span (Set.range P.relation))) =
    Ideal.comap (rename _root_.id) (Ideal.span (Set.range P.relation))
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case tmul
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T✝ : Type ?u.18
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
T : Type ?u.24
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
a : T
b : S
X : P.Ring := P.σ b
⊢ ∃ a_1, (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) a_1 = a ⊗ₜ[R] b

Tactic:
use a • MvPolynomial.map (algebraMap R T) X

Goal state after:
case h
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T✝ : Type ?u.18
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
T : Type ?u.24
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
a : T
b : S
X : P.Ring := ⋯
⊢ (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) (a • (MvPolynomial.map (algebraMap R T)) X) = a ⊗ₜ[R] b
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
y : P.Ring
y_in : y ∈ RingHom.ker f.toRingHom
y_in' : y ∈ P.ker
hy : y - ↑x ∈ P.ker ^ 2
⊢ f.toRingHom ↑x ∈ P'.ker ^ 2

Tactic:
eq_map,

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
y : P.Ring
y_in : y ∈ RingHom.ker f.toRingHom
y_in' : y ∈ P.ker
hy : y - ↑x ∈ P.ker ^ 2
⊢ f.toRingHom ↑x ∈ Ideal.map f.toRingHom P.ker ^ 2
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ ∃ n, Nonempty (Generators R S (Fin n))

Tactic:
exact ⟨n, ⟨.ofSurjective (fun i ↦ f (X i)) <| by rwa [aeval_unique f] at hf⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case h
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
a : S
⊢ (aeval fun x ↦ (IsScalarTower.toAlgHom R S (MvPolynomial ι' S)) (P.val x)) (P.σ a) =
    (IsScalarTower.toAlgHom R S (MvPolynomial ι' S)) a

Tactic:
← MvPolynomial.comp_aeval

Goal state after:
case h
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
a : S
⊢ ((IsScalarTower.toAlgHom R S (MvPolynomial ι' S)).comp (aeval P.val)) (P.σ a) =
    (IsScalarTower.toAlgHom R S (MvPolynomial ι' S)) a
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case e'_1
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)
m' : ι → ↥(span R (Set.range m)) := Subtype.coind m mem_M'
m'_eq : m' = Subtype.coind m mem_M'
hm' : span R (Set.range m') = ⊤
hm'n : ∑ i, m' i ⊗ₜ[R] n i = 0
this : ∃ k a y, (∀ (i : ι), n i = ∑ j, a i j • y j) ∧ ∀ (j : Fin k), ∑ i, a i j • m' i = 0
κ : ℕ
x✝ : ι → Fin κ → R
a : Fin κ → N
y : Fin κ
⊢ ∑ i, x✝ i y • m i = (span R (Set.range m)).subtype (∑ i, x✝ i y • m' i)

Tactic:
simp [m'_eq]

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
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
⊢ ∃ r ∉ x.asIdeal, r • m = 0

Tactic:
obtain ⟨r, hr, e₁⟩ := H₂ (g m)

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
e₁ : r • g m = 0
⊢ ∃ r ∉ x.asIdeal, r • m = 0
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
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : p ∈ zeroLocus ↑I
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl (M ⧸ I • ⊤)
Mₚ'' : Type (max u_1 u_2) := Mₚ ⧸ Ideal.map (algebraMap R Rₚ) I • ⊤
e : Mₚ' ≃ₗ[Rₚ] Mₚ'' :=
  (localizedQuotientEquiv p.asIdeal.primeCompl (I • ⊤)).symm ≪≫ₗ
    (Submodule.localized p.asIdeal.primeCompl (I • ⊤)).quotEquivOfEq (Ideal.map (algebraMap R Rₚ) I • ⊤) ⋯
⊢ Ideal.map (algebraMap R Rₚ) I ≤ Ideal.map (algebraMap R (Localization.AtPrime p.asIdeal)) p.asIdeal

Tactic:
exact Ideal.map_mono hp₂

Goal state after:
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin n
⊢ Even k ↔ Even n → Even ↑k

Tactic:
rw [imp_iff_not_or, Nat.not_even_iff_odd]
  exact even_iff

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
inst✝⁴ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst✝³ : SMul R₁ R
inst✝² : IsScalarTower R₁ R R
inst✝¹ : SMul R₁ (s i)
inst✝ : IsScalarTower R₁ R (s i)
⊢ r • z = r • 1 * z

Tactic:
smul_mul_assoc,

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
inst✝⁴ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst✝³ : SMul R₁ R
inst✝² : IsScalarTower R₁ R R
inst✝¹ : SMul R₁ (s i)
inst✝ : IsScalarTower R₁ R (s i)
⊢ r • z = r • (1 * z)
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
⊢ (cast R M ⋯) (mulEquiv ((tprod R) Fin.elim0 ⊗ₜ[R] (r • (tprod R) a))) = r • (tprod R) a

Tactic:
TensorProduct.tmul_smul,

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
⊢ (cast R M ⋯) (mulEquiv (r • (tprod R) Fin.elim0 ⊗ₜ[R] (tprod R) a)) = r • (tprod R) a
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
⊢ p ∈ x.lifts ↔ (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i) (FreeAddMonoid.toList p)).sum = x

Tactic:
by
  simp only [lifts, Set.mem_ofPred_eq, FreeAddMonoid.toPiTensorProduct]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case e'_4
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
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
x✝ : ι
⊢ (⇑((TensorProduct.mk R k M) 1) ∘ (v + fun x ↦ c x • v ↑n)) x✝ =
    (⇑((TensorProduct.mk R k M) 1) ∘ v + fun x ↦
        (⇑(Ideal.Quotient.mk 𝔪) ∘ c) x • (⇑((TensorProduct.mk R k M) 1) ∘ v) ↑n)
      x✝

Tactic:
simp [tmul_add]

Goal state after:
case e'_4
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
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
x✝ : ι
⊢ c x✝ • 1 ⊗ₜ[R] v ↑n = (Ideal.Quotient.mk 𝔪) (c x✝) • 1 ⊗ₜ[R] v ↑n
Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
x : PrimeSpectrum (S ⊗[R] T)
hx₁ : a ⊗ₜ[R] 1 ∉ x.asIdeal
hx₂ : 1 ⊗ₜ[R] t ∉ x.asIdeal
hx₃ : f ∈ x.asIdeal
⊢ 1 ⊗ₜ[R] (r • t) * f ∈ ↑x.asIdeal

Tactic:
exact x.asIdeal.mul_mem_left _ hx₃

Goal state after:
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
⊢ IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) (f ∘ₗ g) s =
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f))
      (IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) g s)

Tactic:
apply ((Module.End.isUnit_iff _).mp <| IsLocalizedModule.map_units
         (LocalizedModule.map I.primeCompl) s).injective

Goal state after:
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
⊢ ((algebraMap R
          (Module.End R (LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)))
        ↑s)
      (IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) (f ∘ₗ g) s) =
    ((algebraMap R
          (Module.End R (LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)))
        ↑s)
      (((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
            (LocalizedModule I.primeCompl N))
          ((LocalizedModule.map I.primeCompl) f))
        (IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) g s))
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ₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
e : Rₚ P ≃+* Localization.AtPrime P :=
  (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv
m : Mₚ P
r : R
s : ↥P.primeCompl
⊢ ↑s •
      (IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))
        (IsLocalization.mk' (Rₚ P) r s • m) =
    ↑s •
      (IsLocalization.map (Localization.AtPrime P) (RingHom.id R) ⋯) (IsLocalization.mk' (Rₚ P) r s) •
        (IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) m

Tactic:
simp only [← map_smul, ← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul,
      IsLocalization.map_id_mk']

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
n : ℕ
hn : derivedSeries G n = ⊥
⊢ _root_.commutator G ≠ ⊤

Tactic:
contrapose! hn

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
n : ℕ
hn : _root_.commutator G = ⊤
⊢ derivedSeries G n ≠ ⊥
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case inr
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).comp (algebraMap F E)) (minpoly F x)).Splits
⊢ IsIntegral F x ∧ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits

Tactic:
← Polynomial.map_map

Goal state after:
case inr
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
⊢ IsIntegral F x ∧ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits
Module: Mathlib.RingTheory.AlgebraicIndependent.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ AlgebraicIndependent R Subtype.val

Tactic:
simpa using hx.comp _ (rangeSplitting_injective x)

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

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : (B' \ B).encard = ∅.encard
hfB : f ∈ B'
h : B \ B' = ∅
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
encard_empty,

Goal state after:
case inl
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : (B' \ B).encard = 0
hfB : f ∈ B'
h : B \ B' = ∅
⊢ M.IsBase (insert f (B \ {e}))