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

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type ?u.13
N' : Type ?u.18
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝³ : IsLocalizedModule S f
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FinitePresentation R M
⊢ Module.FinitePresentation A (A ⊗[R] M)

Tactic:
obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
  have inst := Module.finitePresentation_of_projective A (A ⊗[R] (Fin n → R))
  apply Module.finitePresentation_of_surjective (f.baseChange A)
    (LinearMap.lTensor_surjective A hf)
  have : Function.Exact ((LinearMap.ker f).subtype.baseChange A) (f.baseChange A) :=
    lTensor_exact A f.exact_subtype_ker_map hf
  rw [LinearMap.exact_iff] at this
  rw [this]
  have : Module.Finite R (LinearMap.ker f) :=
    .of_fg (Module.FinitePresentation.fg_ker f hf)
  exact Submodule.fg_range _

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
x : R
⊢ (supportedEquivMvPolynomial s).symm (C x) = (algebraMap R ↥(supported R s)) x

Tactic:
by
  ext1
  simp [supportedEquivMvPolynomial, MvPolynomial.algebraMap_eq]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: σ : Type u_1
s : Set σ
R : Type u_2
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : ↑F.vars ⊆ s
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (aeval x) F

Tactic:
rw [← mem_supported, supported_eq_range_rename, AlgHom.mem_range] at hF

Goal state after:
σ : Type u_1
s : Set σ
R : Type u_2
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : ∃ x, (rename Subtype.val) x = F
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (aeval x) F
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
s : M → ↥S
hs : ∀ (x : M), s x • g₁ x = s x • g₂ x
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
⊢ σ.prod s • g₁ = σ.prod s • g₂

Tactic:
rw [← sub_eq_zero, ← LinearMap.ker_eq_top, ← top_le_iff, ← hσ, Submodule.span_le]

Goal state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
s : M → ↥S
hs : ∀ (x : M), s x • g₁ x = s x • g₂ x
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
⊢ ↑σ ⊆ ↑(σ.prod s • g₁ - σ.prod s • g₂).ker
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: case add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)
hC : ∀ (r : R), D (C r) = 0
i : σ
p q : MvPolynomial σ R
hp : D (p * X i) = p • D (X i) + X i • D p
hq : D (q * X i) = q • D (X i) + X i • D q
⊢ p • D (X i) + X i • D p + D (q * X i) = (p + q) • D (X i) + X i • (D p + D q)

Tactic:
hq,

Goal state after:
case add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)
hC : ∀ (r : R), D (C r) = 0
i : σ
p q : MvPolynomial σ R
hp : D (p * X i) = p • D (X i) + X i • D p
hq : D (q * X i) = q • D (X i) + X i • D q
⊢ p • D (X i) + X i • D p + (q • D (X i) + X i • D q) = (p + q) • D (X i) + X i • (D p + D q)
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z
f1 : ∃ a, Submodule.Quotient.mk a = f 1
this : p ^ k • f1.choose ∈ R ∙ z
a : R
ha : p ^ k • f1.choose = p ^ k • a • z
⊢ p ^ k • f1.choose - p ^ k • a • z = 0

Tactic:
sub_eq_zero,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z
f1 : ∃ a, Submodule.Quotient.mk a = f 1
this : p ^ k • f1.choose ∈ R ∙ z
a : R
ha : p ^ k • f1.choose = p ^ k • a • z
⊢ p ^ k • f1.choose = p ^ k • a • z
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z
⊢ ∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1

Tactic:
by
  have f1 := mk_surjective (R ∙ z) (f 1)
  have : p ^ k • f1.choose ∈ R ∙ z := by
    rw [← Quotient.mk_eq_zero, mk_smul, f1.choose_spec, ← f.map_smul]
    convert! f.map_zero; change _ • Submodule.Quotient.mk _ = _
    rw [← mk_smul, Quotient.mk_eq_zero, smul_eq_mul, mul_one]
    exact Submodule.mem_span_singleton_self _
  obtain ⟨a, ha⟩ := p_pow_smul_lift hp hM hz this
  refine ⟨f1.choose - a • z, by rw [smul_sub, sub_eq_zero, ha], ?_⟩
  rw [mk_sub, mk_smul, (Quotient.mk_eq_zero _).mpr <| Submodule.mem_span_singleton_self _,
    smul_zero, sub_zero, f1.choose_spec]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case mul_X.inl
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : σ
⊢ (aeval (Sum.elim X (⇑C ∘ f))) p * (aeval (Sum.elim X (⇑C ∘ f))) (Pi.single (Sum.inl j) 1 (Sum.inl val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inl val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p) =
    (aeval (Sum.elim X (⇑C ∘ f))) p * (pderiv j) (Sum.elim X (⇑C ∘ f) (Sum.inl val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inl val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)

Tactic:
simp [Pi.single_apply]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case mul_X.inr
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : τ
⊢ (aeval (Sum.elim X (⇑C ∘ f))) p * (aeval (Sum.elim X (⇑C ∘ f))) (Pi.single (Sum.inl j) 1 (Sum.inr val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inr val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p) =
    (aeval (Sum.elim X (⇑C ∘ f))) p * (pderiv j) (Sum.elim X (⇑C ∘ f) (Sum.inr val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inr val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)

Tactic:
simp [Pi.single_apply]

Goal state after:
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
inst✝ : IsLocalization M S
a : R
m : ↥M
⊢ C (IsLocalization.mk' S a m) * (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) (C ↑m) =
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) (C a)

Tactic:
algebraMap_def,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
m : ↥M
⊢ C (IsLocalization.mk' S a m) * (map (algebraMap R S)) (C ↑m) = (map (algebraMap R S)) (C a)
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
inst✝ : IsLocalization M S
a : R
m : ↥M
⊢ C (IsLocalization.mk' S a m) * (map (algebraMap R S)) (C ↑m) = (map (algebraMap R S)) (C a)

Tactic:
map_C,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
m : ↥M
⊢ C (IsLocalization.mk' S a m) * C ((algebraMap R S) ↑m) = C ((algebraMap R S) a)
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Extension R S
R₀ : Type u_1
inst✝⁹ : CommRing R₀
inst✝⁸ : Algebra R₀ R
inst✝⁷ : Algebra R₀ S
inst✝⁶ : IsScalarTower R₀ R S
R₁ : Type u_2
inst✝⁵ : CommRing R₁
inst✝⁴ : Algebra R₁ R
inst✝³ : Algebra R₁ S
inst✝² : IsScalarTower R₁ R S
inst✝¹ : Algebra R₀ R₁
inst✝ : IsScalarTower R₀ R₁ R
⊢ (algebraMap R P.Ring).comp (algebraMap R₀ R) = (algebraMap R₁ P.Ring).comp (algebraMap R₀ R₁)

Tactic:
IsScalarTower.algebraMap_eq R₁ R,

Goal state after:
R : Type u
S : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Extension R S
R₀ : Type u_1
inst✝⁹ : CommRing R₀
inst✝⁸ : Algebra R₀ R
inst✝⁷ : Algebra R₀ S
inst✝⁶ : IsScalarTower R₀ R S
R₁ : Type u_2
inst✝⁵ : CommRing R₁
inst✝⁴ : Algebra R₁ R
inst✝³ : Algebra R₁ S
inst✝² : IsScalarTower R₁ R S
inst✝¹ : Algebra R₀ R₁
inst✝ : IsScalarTower R₀ R₁ R
⊢ (algebraMap R P.Ring).comp (algebraMap R₀ R) = ((algebraMap R P.Ring).comp (algebraMap R₁ R)).comp (algebraMap R₀ R₁)
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
x m : L
hm : m ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier
hx : x ∈ ⨆ χ, genWeightSpace L ⇑χ
⊢ ⁅x, m⁆ ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier

Tactic:
induction hx using LieSubmodule.iSup_induction' with

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.RestrictScalars

Goal state before:
pp: case single_add.single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝¹ : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝ : presB.π β ≠ 0
⊢ ∀ (a : presB.G) (b : A) (f : presB.G →₀ A),
    a ∉ f.support →
      b ≠ 0 →
        Finsupp.single r (presB.π f) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
          Finsupp.single r (presB.π (Finsupp.single a b + f)) ∈
            Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
intro g a f _ _ hf
          rw [map_add, Finsupp.single_add]
          refine Submodule.add_mem _ ?_ hf
          rw [← Finsupp.smul_single_one, ← Finsupp.smul_single_one,
            map_smul, Relations.Solution.π_single, smul_assoc]
          exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨⟨g, r⟩, rfl⟩)

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

Goal state before:
pp: case e'_5
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 ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ ∑ i ∈ Finset.map (↑e).toEmbedding (support x) with i.1 = i, (monomial (e.symm i)) (coeff (e.symm i) x) =
    (monomial (e.symm (i, 0))) 1 *
      (Q.toComp P).toAlgHom.toRingHom
        (∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i, (monomial j.2) (coeff (e.symm j) x))

Tactic:
rw [map_sum, Finset.mul_sum]
      refine Finset.sum_congr rfl fun j hj ↦ ?_
      obtain rfl := (Finset.mem_filter.mp hj).2
      obtain ⟨i, j⟩ := j
      clear hj hi
      have : (Q.toComp P).toAlgHom (monomial j (coeff (e.symm (i, j)) x)) =
          monomial (e.symm (0, j)) (coeff (e.symm (i, j)) x) :=
        toComp_toAlgHom_monomial ..
      simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
          this]
      rw [monomial_mul, ← map_add, Prod.mk_add_mk, add_zero, zero_add, one_mul]

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

Goal state before:
pp: 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 ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
a : R
v : (ι' →₀ ℕ) × (ι →₀ ℕ)
| coeff i ((Q.ofComp P).toAlgHom ((monomial (e.symm v)) a))

Tactic:
simp only [e, Finsupp.sumFinsuppAddEquivProdFinsupp,
          Finsupp.sumFinsuppEquivProdFinsupp, AddEquiv.symm_mk, AddEquiv.coe_mk,
          Equiv.coe_fn_symm_mk, ofComp_toAlgHom_monomial_sumElim]

Goal state after:
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 ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
a : R
v : (ι' →₀ ℕ) × (ι →₀ ℕ)
| coeff i ((monomial v.1) ((aeval P.val) ((monomial v.2) a)))
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Extension R S
A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra S A
inst✝¹ : Algebra P.Ring A
inst✝ : IsScalarTower P.Ring S A
⊢ LinearMap.baseChange A P.cotangentComplex =
    ↑(AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]).symm ∘ₗ
      cotangentComplexBaseChange R S P.Ring A ∘ₗ
        ↑((AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker).symm ≪≫ₗ
              LinearEquiv.baseChange S A (S ⊗[P.Ring] ↥P.ker) P.Cotangent P.cotangentEquiv).symm

Tactic:
apply LinearMap.coe_injective
  dsimp
  rw [LinearEquiv.eq_symm_comp, ← LinearEquiv.comp_symm_eq]
  exact congr(($(cotangentComplexBaseChange_eq_lTensor_cotangentComplex P A) : _ → _)).symm

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case refine_2
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 : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ (rTensor N G).ker
exact_ker_subtype : Exact ⇑G.ker.subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N G.ker.subtype) ⇑(rTensor N G)
ma : Finset (↥G.ker × N)
hkn : (rTensor N G.ker.subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en
⊢ ∀ (j : ↥ma),
    ∑ i,
        (match j with
          | ⟨(kj, snd), property⟩ => ↑kj i) •
          m i =
      0

Tactic:
· rintro ⟨⟨⟨k, hk⟩, _⟩, _⟩
    simpa only [hG, linearCombination_apply, zero_smul, implies_true, Finsupp.sum_fintype] using
      mem_ker.mp hk

Goal state after:
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✝ : Module.Finite R M
p : PrimeSpectrum R
K : Type u_1 := p.asIdeal.ResidueField
e : K ⊗[R] M ≃ₗ[K] K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) :=
  (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) K K M).symm
⊢ Nontrivial (LocalizedModule p.asIdeal.primeCompl M) ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))

Tactic:
(LocalizedModule.equivTensorProduct p.asIdeal.primeCompl M).nontrivial_congr,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
p : PrimeSpectrum R
K : Type u_1 := p.asIdeal.ResidueField
e : K ⊗[R] M ≃ₗ[K] K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) :=
  (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) K K M).symm
⊢ Nontrivial (Localization p.asIdeal.primeCompl ⊗[R] M) ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)
x : M₂ ⊗[R] N₁
hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0
this : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) x) = 0
y : M₁ ⊗[R] N₂
hy : (LinearMap.rTensor N₂ f₁) y = (LinearMap.lTensor M₂ g₁) x
⊢ (LinearMap.lTensor M₂ g₂ ∘ₗ LinearMap.lTensor M₂ g₁) x = (LinearMap.rTensor N₃ f₁) 0

Tactic:
← LinearMap.lTensor_comp,

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)
x : M₂ ⊗[R] N₁
hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0
this : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) x) = 0
y : M₁ ⊗[R] N₂
hy : (LinearMap.rTensor N₂ f₁) y = (LinearMap.lTensor M₂ g₁) x
⊢ (LinearMap.lTensor M₂ (g₂ ∘ₗ g₁)) x = (LinearMap.rTensor N₃ f₁) 0
Module: Mathlib.LinearAlgebra.LinearDisjoint

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
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
⊢ x = y

Tactic:
by
  obtain ⟨N', hN, hFG, h⟩ :=
    TensorProduct.exists_finite_submodule_right_of_setFinite' {x, y} (Set.toFinite _)
  rw [Module.Finite.iff_fg] at hFG
  obtain ⟨x', hx'⟩ := h (show x ∈ {x, y} by simp)
  obtain ⟨y', hy'⟩ := h (show y ∈ {x, y} by simp)
  rw [← hx', ← hy']; congr
  exact (H N' hN hFG).injective (by simp [← mulMap_comp_lTensor _ hN, hx', hy', hxy])

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i ↦ ⨂[R]^i M
⊢ (cast R M ⋯) (GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r) * x).snd =
    (x * GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r)).snd

Tactic:
by
    have := (algebraMap₀_mul r x.snd).trans (mul_algebraMap₀ r x.snd).symm
    rw [← LinearEquiv.eq_symm_apply, cast_symm]
    rw [← LinearEquiv.eq_symm_apply, cast_symm, cast_cast] at this
    exact this

Goal state after:
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)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
f : (i : ι) → s i →ₗ[R] t i →ₗ[R] t' i
a : (i : ι) → s i
b : (i : ι) → t i
⊢ ((piTensorHomMap₂ ((tprod R) f)) ((tprod R) a)) ((tprod R) b) = ⨂ₜ[R] (i : ι), ((f i) (a i)) (b i)

Tactic:
by
  simp [piTensorHomMapFun₂, piTensorHomMap₂]

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

Goal state before:
pp: case insert.inr
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 : ∀ 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⁻¹
hi : i ∈ s
⊢ f i = 0

Tactic:
exact ih i hi

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
l' : N →ₗ[R] M
hl : l' ∘ₗ l = LinearMap.id
⊢ LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l = LinearMap.id

Tactic:
← LinearMap.lTensor_comp,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
l' : N →ₗ[R] M
hl : l' ∘ₗ l = LinearMap.id
⊢ LinearMap.lTensor k (l' ∘ₗ l) = LinearMap.id