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

Goal state before:
pp: R : Type u_1
A : Type u_2
K✝ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K✝
inst✝ : IsFractionRing A K✝
I : { x // 0 < x }
J K : Ideal A
e : (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) I J) ((fun x y ↦ ↑x * y) I K)
⊢ J ≤ K

Tactic:
rwa [← FractionalIdeal.coeIdeal_le_coeIdeal (FractionRing A),
      ← mul_le_mul_iff_right₀ (α := FractionalIdeal A⁰ (FractionRing A)) (a := I.1)
        (by simpa [pos_iff_ne_zero] using I.2.ne'),
      ← FractionalIdeal.coeIdeal_mul, ← FractionalIdeal.coeIdeal_mul,
      FractionalIdeal.coeIdeal_le_coeIdeal]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
a : A
⊢ Prime (span {a}) ↔ Prime a

Tactic:
by
  rcases eq_or_ne a 0 with rfl | ha
  · rw [Set.singleton_zero, span_zero, ← zero_eq_bot, ← not_iff_not]
    simp only [not_prime_zero, not_false_eq_true]
  · have ha' : span {a} ≠ ⊥ := by simpa only [ne_eq, span_singleton_eq_bot] using ha
    rw [prime_iff_isPrime ha', span_singleton_prime ha]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case pos
A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : I = 0
⊢ I * ⨅ i, J i = ⨅ i, I * J i

Tactic:
simp [hI]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁵ : Ring K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : IsNoetherianRing K
u : V →ₗ[K] V₂
h : u.HasFiniteRange
⊢ u.HasNoetherianRange

Tactic:
rw [HasNoetherianRange]
  have := Finite.of_fg h.fg_range
  infer_instance

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ I ≤ J ^ (Associates.mk J).count (Associates.mk I).factors

Tactic:
rw [← dvd_iff_le, ← Associates.mk_dvd_mk, Associates.mk_pow]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ Associates.mk J ^ (Associates.mk J).count (Associates.mk I).factors ∣ Associates.mk I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ ¬I ≤ J ^ ((Associates.mk J).count (Associates.mk I).factors + 1)

Tactic:
rw [← dvd_iff_le, ← Associates.mk_dvd_mk, Associates.mk_pow]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ ¬Associates.mk J ^ ((Associates.mk J).count (Associates.mk I).factors + 1) ∣ Associates.mk I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case hI
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ ¬a₀ = 0

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Index

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
k : Type u_3
inst✝² : Field k
inst✝¹ : Module k M
inst✝ : Module k N
f : M →ₗ[k] N
t : k
ht : t ≠ 0
⊢ (t • f).index = f.index

Tactic:
by
  rw [index_eq_finrank_sub, index_eq_finrank_sub, ker_smul _ _ ht, range_smul _ _ ht]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : IsDomain A
inst✝ : IsTorsionFree A B
P : Ideal B
⊢ P ∈ primesOverFinset p B ↔ P ∈ p.primesOver B

Tactic:
← Finset.mem_coe,

Goal state after:
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : IsDomain A
inst✝ : IsTorsionFree A B
P : Ideal B
⊢ P ∈ ↑(primesOverFinset p B) ↔ P ∈ p.primesOver B
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case neg
A : Type u_4
inst✝⁶ : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst✝⁵ : CommRing B
inst✝⁴ : IsDedekindDomain B
inst✝³ : Algebra A B
inst✝² : IsDomain A
inst✝¹ : IsTorsionFree A B
inst✝ : Algebra.IsIntegral A B
hpb : ¬p = ⊥
⊢ (↑(primesOverFinset p B)).Finite

Tactic:
exact (primesOverFinset p B).finite_toSet

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Algebra R A
inst✝² : FaithfulSMul R A
inst✝¹ : Algebra.IsIntegral R A
inst✝ : Nontrivial (HeightOneSpectrum R)
this : IsDomain R
f : HeightOneSpectrum A → HeightOneSpectrum R := fun p ↦ HeightOneSpectrum.under R p
x✝ : HeightOneSpectrum R
P : Ideal A
hP : P.IsPrime
isPrime✝ : (Ideal.comap (algebraMap R A) P).IsPrime
hp : Ideal.comap (algebraMap R A) P ≠ ⊥
⊢ P ≠ ⊥

Tactic:
aesop

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

Goal state before:
pp: A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (pres₂.cokernelRelations data).Solution N✝
⊢ (pres₂.cokernelSolution data).postcomp
      (f.range.liftQ (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ }) ⋯) =
    s

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
⊢ (map S f g) l' = (s • LinearMap.id) ∘ₗ ↑l

Tactic:
apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
⊢ (map S f g) l' ∘ₗ f = ((s • LinearMap.id) ∘ₗ ↑l) ∘ₗ f
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
inst✝ : Module.Finite R M
m : ℕ
ι : Type u
w✝ : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
e : M ≃ₗ[R] (Fin m →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ n i
x : R
h :
  e.symm
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)) =
    0
⊢ x ∈ annihilator R M

Tactic:
e.symm.map_eq_zero_iff,

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
inst✝ : Module.Finite R M
m : ℕ
ι : Type u
w✝ : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
e : M ≃ₗ[R] (Fin m →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ n i
x : R
h : x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1) = 0
⊢ x ∈ annihilator R M
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case surj
R : Type u_3
M : Type u_4
N : Type u_5
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✝
M' : Type u_1
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
f : M →ₗ[R] M'
inst✝⁴ : IsLocalizedModule S f
N' : Type u_2
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g
inst✝ : FinitePresentation R M
h : M' →ₗ[R] N'
h' : M →ₗ[R] N
s : ↥S
e : g ∘ₗ h' = s • h ∘ₗ f
⊢ (h', s).2 • h = (IsLocalizedModule.map S f g) (h', s).1

Tactic:
apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)

Goal state after:
case surj
R : Type u_3
M : Type u_4
N : Type u_5
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✝
M' : Type u_1
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
f : M →ₗ[R] M'
inst✝⁴ : IsLocalizedModule S f
N' : Type u_2
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g
inst✝ : FinitePresentation R M
h : M' →ₗ[R] N'
h' : M →ₗ[R] N
s : ↥S
e : g ∘ₗ h' = s • h ∘ₗ f
⊢ ((h', s).2 • h) ∘ₗ f = (IsLocalizedModule.map S f g) (h', s).1 ∘ₗ f
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 _root_.id) (Ideal.span (Set.range P.relation))

Tactic:
simp [Ideal.comap_map_of_bijective _ hf, rename_id]

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

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
⊢ (Subtype.val '' Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = Set.range pres.relation

Tactic:
aesop

Goal state after:
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
R' : Type ?u.16
S' : Type ?u.18
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝¹⁶ : CommRing R''
inst✝¹⁵ : CommRing S''
inst✝¹⁴ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' R''
inst✝¹¹ : Algebra R' S''
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra S' S''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S'
inst✝⁶ : IsScalarTower R R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : S ⊗[P.Ring] ↥P.ker
hx : (LinearMap.liftBaseChange S Cotangent.mk) x = 0
⊢ x = 0

Tactic:
obtain ⟨x, rfl⟩ := TensorProduct.mk_surjective P.Ring P.ker S P.algebraMap_surjective x

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
R' : Type ?u.16
S' : Type ?u.18
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝¹⁶ : CommRing R''
inst✝¹⁵ : CommRing S''
inst✝¹⁴ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' R''
inst✝¹¹ : Algebra R' S''
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra S' S''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S'
inst✝⁶ : IsScalarTower R R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : ↥P.ker
hx : (LinearMap.liftBaseChange S Cotangent.mk) (((TensorProduct.mk P.Ring S ↥P.ker) 1) x) = 0
⊢ ((TensorProduct.mk P.Ring S ↥P.ker) 1) x = 0
Module: Mathlib.Algebra.Module.Presentation.Free

Goal state before:
pp: A : Type u
inst✝³ : Ring A
relations : Relations A
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsEmpty relations.R
⊢ ∀ {N : Type w} [inst : AddCommGroup N] [inst_1 : Module A N] (s : relations.Solution N),
    relations.solutionFinsupp.postcomp (Finsupp.linearCombination A s.var) = s

Tactic:
aesop

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

Goal state before:
pp: A : Type u
inst✝⁶ : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
relations₁ : Relations A
relations₂ : Relations A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
x✝ : (relations₁.tensor relations₂).Solution N✝
⊢ (solution₁.tensor solution₂).postcomp
      ((uncurry (RingHom.id A) M₁ M₂ N✝)
        (h₁.desc
          { var := fun g₁ ↦ h₂.desc { var := fun g₂ ↦ x✝.var (g₁, g₂), linearCombination_var_relation := ⋯ },
            linearCombination_var_relation := ⋯ })) =
    x✝

Tactic:
aesop

Goal state after:
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✝
P : Type u_2
A : Type u_3
inst✝⁶ : CommRing P
inst✝⁵ : CommRing A
inst✝⁴ : Algebra P S
inst✝³ : Algebra P A
inst✝² : Algebra R P
inst✝¹ : Algebra S A
inst✝ : IsScalarTower P S A
x✝ : P
⊢ x✝ ∈ RingHom.ker (algebraMap P S) → x✝ ∈ RingHom.ker ((algebraMap S A).comp (algebraMap P S))

Tactic:
aesop

Goal state after:
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✝
P : Type u_2
A : Type u_3
inst✝⁶ : CommRing P
inst✝⁵ : CommRing A
inst✝⁴ : Algebra P S
inst✝³ : Algebra P A
inst✝² : Algebra R P
inst✝¹ : Algebra S A
inst✝ : IsScalarTower P S A
a : A
b : ↥(RingHom.ker (algebraMap P S))
⊢ ↑b ∈ RingHom.ker ((algebraMap S A).comp (algebraMap P S))

Tactic:
aesop

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.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
R' : Type u'
S' : Type v'
inst✝²⁰ : CommRing R'
inst✝¹⁹ : CommRing S'
inst✝¹⁸ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁷ : Algebra R R'
inst✝¹⁶ : Algebra S S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹⁰ : Algebra R R''
inst✝⁹ : Algebra S S''
inst✝⁸ : Algebra R S''
inst✝⁷ : IsScalarTower R R'' S''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
this✝³ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
this✝² : IsScalarTower P.Ring S S'
this✝¹ : Algebra P.Ring P'.Ring := f.toAlgHom.toAlgebra
this✝ : IsScalarTower P.Ring P'.Ring S'
this : IsScalarTower R P.Ring S'
⊢ ∀ (a b : P.Ring),
    (↑R Cotangent.mk ∘ₗ f.subToKer g) (a * b) =
      a • (↑R Cotangent.mk ∘ₗ f.subToKer g) b + b • (↑R Cotangent.mk ∘ₗ f.subToKer g) a

Tactic:
intro x y
    ext
    simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply,
      Cotangent.val_mk, Cotangent.val_add, Cotangent.val_smul''', ← map_smul, ← map_add,
      Ideal.toCotangent_eq]
    exact Hom.sub_aux f g x y

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

Goal state before:
pp: case e'_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
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx : ∑ i, ↑(↑(e i)).1 ⊗ₜ[R] (↑(e i)).2 = 0
this :
  ∃ k a y,
    (∀ (i : Fin (Fintype.card ↥s)), (fun i ↦ (↑(e i)).2) i = ∑ j, a i j • y j) ∧
      ∀ (j : Fin k), ∑ i, a i j • (fun i ↦ ↑(↑(e i)).1) i = 0
x✝² : ℕ
x✝¹ : Fin (Fintype.card ↥s) → Fin x✝² → R
x✝ : Fin x✝² → N
a✝ : Fin x✝²
⊢ ∑ i, x✝¹ i a✝ • (fun i ↦ ↑(↑(e i)).1) i = 0 ↔ ∑ i, x✝¹ i a✝ • ((fun i ↦ (↑i).1) ∘ ⇑e) i = 0

Tactic:
convert! (injective_iff_map_eq_zero' _).mp (injective_subtype M') _

Goal state after:
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
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx : ∑ i, ↑(↑(e i)).1 ⊗ₜ[R] (↑(e i)).2 = 0
this :
  ∃ k a y,
    (∀ (i : Fin (Fintype.card ↥s)), (fun i ↦ (↑(e i)).2) i = ∑ j, a i j • y j) ∧
      ∀ (j : Fin k), ∑ i, a i j • (fun i ↦ ↑(↑(e i)).1) i = 0
x✝² : ℕ
x✝¹ : Fin (Fintype.card ↥s) → Fin x✝² → R
x✝ : Fin x✝² → N
a✝ : Fin x✝²
⊢ ∑ i, x✝¹ i a✝ • (fun i ↦ ↑(↑(e i)).1) i = M'.subtype (∑ i, x✝¹ i a✝ • ((fun i ↦ (↑i).1) ∘ ⇑e) i)
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
inst✝ : FinitePresentation R S
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
⊢ FiniteType R P.toExtension.Ring

Tactic:
simp [P]

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
⊢ FiniteType R (Presentation.ofFinitePresentation R S).Ring
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
ι : Type w
ι' : Type u_1
P✝ : Generators R S ι
S' : Type u_2
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R S'
T : Type w
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Algebra S' T
inst✝² : IsScalarTower R S' T
inst✝¹ : FinitePresentation R S
inst✝ : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
⊢ FiniteType R P.toExtension.Ring

Tactic:
simp [P]

Goal state after:
R : Type u
S : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
ι : Type w
ι' : Type u_1
P✝ : Generators R S ι
S' : Type u_2
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R S'
T : Type w
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Algebra S' T
inst✝² : IsScalarTower R S' T
inst✝¹ : FinitePresentation R S
inst✝ : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
⊢ FiniteType R (Presentation.ofFinitePresentation R S).Ring
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
⊢ support R M = ∅ ↔ Subsingleton M

Tactic:
rw [← Set.subset_empty_iff, ← PrimeSpectrum.zeroLocus_singleton_one,
    ← LocalizedModule.subsingleton_iff_support_subset, LocalizedModule.subsingleton_iff,
    subsingleton_iff_forall_eq 0]
  simp only [Submonoid.powers_one, Submonoid.mem_bot, exists_eq_left, one_smul]

Goal state after:
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: case hd
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
fg : N.FG
⊢ Cardinal.lift.{u_2, u_3} N.spanRank < Cardinal.aleph0

Tactic:
simp [Cardinal.lift_lt_aleph0, spanRank_finite_iff_fg.mpr fg]

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
j : Fin (n + 1)
i : Fin n
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ (-1) ^ ↑(j.succAbove i) • f ((j.succAbove i).removeNth v) + (-1) ^ ↑j • f (j.removeNth v) = 0

Tactic:
obtain ⟨m, rfl⟩ : ∃ m, m + 1 = n := by simp [i.pos]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ (-1) ^ ↑(j.succAbove i) • f ((j.succAbove i).removeNth v) + (-1) ^ ↑j • f (j.removeNth v) = 0
Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct

Goal state before:
pp: R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝¹ : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝ : (i : ι₁ ⊕ ι₂) → Module R (N i)
⊢ ∀ (m₁ m₂ : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁) (n : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂),
    (m₁ + m₂).domCoprodDep n = m₁.domCoprodDep n + m₂.domCoprodDep n

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝¹ : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝ : (i : ι₁ ⊕ ι₂) → Module R (N i)
⊢ ∀ (c : R) (m : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁) (n : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂),
    (c • m).domCoprodDep n = c • m.domCoprodDep n

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝¹ : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝ : (i : ι₁ ⊕ ι₂) → Module R (N i)
⊢ ∀ (m : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁) (n₁ n₂ : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂),
    m.domCoprodDep (n₁ + n₂) = m.domCoprodDep n₁ + m.domCoprodDep n₂

Tactic:
aesop

Goal state after: