mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝⁵ : CommRing R₁
K : Type u_4
inst✝⁴ : Field K
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : IsDomain R₁
inst✝ : IsNoetherianRing R₁
d : R₁
J : Ideal R₁
left✝ : d ≠ 0
⊢ IsNoetherian R₁ ↥↑↑J

Tactic:
apply isNoetherian_coeIdeal

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

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
I : Ideal R
J : Ideal A
B : Type u_4
inst✝² : CommRing B
inst✝¹ : IsDedekindDomain B
L : Ideal B
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
⊢ ↑{p | p ∣ I} ≃o ↑{p | p ∣ J}

Tactic:
have f_surj : Function.Surjective (f : R ⧸ I →+* A ⧸ J) := f.surjective

Goal state after:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst✝² : CommRing B
inst✝¹ : IsDedekindDomain B
L : Ideal B
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
f_surj : Function.Surjective ⇑↑f
⊢ ↑{p | p ∣ I} ≃o ↑{p | p ∣ J}
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
h : a * b ∈ I ^ (n✝ + 1)
⊢ a ∈ I ∨ b ∈ I ^ (n✝ + 1)

Tactic:
by_cases hI0 : I = ⊥

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
h : a * b ∈ I ^ (n✝ + 1)
hI0 : I = ⊥
⊢ a ∈ I ∨ b ∈ I ^ (n✝ + 1)

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
h : a * b ∈ I ^ (n✝ + 1)
hI0 : ¬I = ⊥
⊢ a ∈ I ∨ b ∈ I ^ (n✝ + 1)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (P i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j
x : ↥s → R
y : R
hy :
  ∀ (i : ι) (hi : i ∈ s), (Ideal.Quotient.mk (P i ^ e i)) y = (Ideal.Quotient.mk (P ↑⟨i, hi⟩ ^ e ↑⟨i, hi⟩)) (x ⟨i, hi⟩)
⊢ ∃ y, ∀ (i : ι) (hi : i ∈ s), y - x ⟨i, hi⟩ ∈ P i ^ e i

Tactic:
exact ⟨y, fun i hi => Ideal.Quotient.eq.mp (hy i hi)⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥l.ker
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : (↥s →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
hf : Function.Surjective ⇑f
this : π.ker ≤ (l ∘ₗ π).ker
⊢ ((l ∘ₗ π).ker ⊓ π.ker).FG

Tactic:
← Submodule.range_subtype (LinearMap.ker _),

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥l.ker
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : (↥s →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
hf : Function.Surjective ⇑f
this : π.ker ≤ (l ∘ₗ π).ker
⊢ ((l ∘ₗ π).ker.subtype.range ⊓ π.ker).FG
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : ¬FiniteMultiplicity a b
⊢ emultiplicity (span {a}) (span {b}) = emultiplicity a b

Tactic:
· suffices ¬FiniteMultiplicity (span ({a} : Set R)) (span ({b} : Set R)) by
      rw [emultiplicity_eq_top.2 h, emultiplicity_eq_top.2 this]
    exact FiniteMultiplicity.not_iff_forall.mpr fun n => by
      rw [span_singleton_pow, span_singleton_dvd_span_singleton_iff_dvd]
      exact FiniteMultiplicity.not_iff_forall.mp h n

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.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
H : ∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG := FinitePresentation.out
n : ℕ := H.choose
f : MvPolynomial (Fin n) R →ₐ[R] S := ⋯.choose
hf : Function.Surjective ⇑f
hf' : (RingHom.ker f).FG
H' : ∃ n_1 s, Submodule.span (MvPolynomial (Fin n) R) (Set.range s) = RingHom.ker f :=
  Submodule.fg_iff_exists_fin_generating_family.mp hf'
m : ℕ := H'.choose
v : Fin m → MvPolynomial (Fin n) R := ⋯.choose
hv : Ideal.span (Set.range v) = RingHom.ker f
⊢ Function.Surjective ⇑(aeval fun x ↦ f (X x))

Tactic:
by convert! hf; ext; simp

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : Unit
⊢ invSelf r = (mvPolynomialQuotientEquiv S r) ((Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (X x))

Tactic:
rw [IsLocalization.Away.mvPolynomialQuotientEquiv_apply, aeval_X]

Goal state after:
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
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx : (aeval (Generators.baseChange T P.toGenerators).val) x = 0
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
⊢ (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm x) = 0

Tactic:
← hx

Goal state after:
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 ι σ
x : MvPolynomial ι T
hx : (aeval (Generators.baseChange T P.toGenerators).val) x = 0
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
⊢ (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm x) =
    (aeval (Generators.baseChange T P.toGenerators).val) x
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
⊢ Function.Surjective ⇑φ

Tactic:
have h₂ : Submodule.span pres.Ring
      (Set.range (fun r ↦ (⟨pres.relation r, by simp⟩ : pres.ker))) = ⊤ := by
    refine Submodule.map_injective_of_injective (f := Submodule.subtype pres.ker)
      Subtype.coe_injective ?_
    rw [Submodule.map_top, Submodule.range_subtype, Submodule.map_span,
      Submodule.coe_subtype, Ideal.submodule_span_eq]
    simp only [← pres.span_range_relation_eq_ker]
    congr
    aesop

Goal state after:
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
h₂ : Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = ⊤
⊢ Function.Surjective ⇑φ
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
P : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
⊢ (IsScalarTower.toAlgHom T (baseChange T P).toExtension.Ring (T ⊗[R] S)).comp ↑(algebraTensorAlgEquiv R T) =
    (IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S)).comp
      (IsScalarTower.toAlgHom T P.toExtension.baseChange.Ring (T ⊗[R] S))

Tactic:
by
    dsimp [Extension.baseChange]
    ext
    simp [RingHom.algebraMap_toAlgebra]

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
P : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
⊢ (IsScalarTower.toAlgHom T P.toExtension.baseChange.Ring (T ⊗[R] S)).comp ↑(algebraTensorAlgEquiv R T).symm =
    (IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S)).comp
      (IsScalarTower.toAlgHom T (baseChange T P).toExtension.Ring (T ⊗[R] S))

Tactic:
by
    dsimp [Extension.baseChange]
    ext
    simp [RingHom.algebraMap_toAlgebra]

Goal state after:
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
⊢ FiniteType R S ↔ ∃ n, Nonempty (Generators R S (Fin n))

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨n, ⟨P⟩⟩ ↦ P.finiteType⟩
  obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp h
  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 a
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 : P.Ring
hx : (algebraMap P.Ring S) x = 0
⊢ x ∈ Ideal.comap (Q.toComp P).toAlgHom (RingHom.ker (Q.ofComp P).toAlgHom)

Tactic:
have : (Q.ofComp P).toAlgHom.comp (Q.toComp P).toAlgHom = IsScalarTower.toAlgHom R _ _ := by
      ext1; simp

Goal state after:
case a
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 : P.Ring
hx : (algebraMap P.Ring S) x = 0
this : (Q.ofComp P).toAlgHom.comp (Q.toComp P).toAlgHom = IsScalarTower.toAlgHom R P.Ring Q.Ring
⊢ x ∈ Ideal.comap (Q.toComp P).toAlgHom (RingHom.ker (Q.ofComp P).toAlgHom)
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: 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
hmn : VanishesTrivially R m n
⊢ ∑ i, m i ⊗ₜ[R] n i = 0

Tactic:
obtain ⟨k, a, y, h₁, h₂⟩ := hmn

Goal state after:
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
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j, a i j • y j
h₂ : ∀ (j : Fin k), ∑ i, a i j • m i = 0
⊢ ∑ i, m i ⊗ₜ[R] n i = 0
Module: Mathlib.RingTheory.Extension.Cotangent.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'
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'
⊢ (↑R Cotangent.mk ∘ₗ f.subToKer g) 1 = 0

Tactic:
ext
    simp [Ideal.toCotangent_eq_zero]

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
p : PrimeSpectrum R
⊢ p ∈ support R M ↔ ∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0

Tactic:
by
  rw [← @not_not (_ ∈ _), notMem_support_iff']
  push Not
  rfl

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (∀ m ∈ s, ∃ x ∉ p.asIdeal, x • m = 0) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0

Tactic:
exact id

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)
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)

Tactic:
by
  have : ⟨p, inferInstance⟩ ∈ (Module.support R M)ᶜ := by
    simpa [Module.notMem_support_iff]
  rw [Module.support_eq_zeroLocus, ← Set.biUnion_of_singleton (Module.annihilator R M : Set R),
    PrimeSpectrum.zeroLocus_iUnion₂, Set.compl_iInter₂, Set.mem_iUnion₂] at this
  obtain ⟨f, hf, hf'⟩ := this
  exact ⟨f, by simpa using hf', subsingleton_iff.mpr
    fun m ↦ ⟨f, Submonoid.mem_powers f, Module.mem_annihilator.mp hf _⟩⟩

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

Goal state before:
pp: R : Type u_1
K : Type u_2
M : Type u_3
E : Type u_4
n : ℕ
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup E
inst✝¹ : Module K E
inst✝ : Free R M
⊢ Free R ↥(⋀[R]^n M)

Tactic:
classical
  have ⟨I, b⟩ := Module.Free.exists_basis R M
  let : LinearOrder I := linearOrderOfSTO WellOrderingRel
  exact Module.Free.of_basis (b.exteriorPower n)

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

Goal state before:
pp: case zero
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ (M.mulMap N) 0 ∈ M * N

Tactic:
rw [map_zero]; exact zero_mem _

Goal state after:
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
hf : Flat R ↥M ∨ Flat R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
⊢ LinearIndependent R fun i ↦ ↑(m i.1) * ↑(n i.2)

Tactic:
rcases hf with _ | _
  · exact H.linearIndependent_mul_of_flat_left hm hn
  · exact H.linearIndependent_mul_of_flat_right hm hn

Goal state after:
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
M' : Submodule R S
h : M' ≤ M
inst✝ : Flat R ↥N
⊢ M'.LinearDisjoint N

Tactic:
let i := mulMap M N ∘ₗ (inclusion h).rTensor N
  have hi : Function.Injective i := H.injective.comp <|
    Module.Flat.rTensor_preserves_injective_linearMap _ <| inclusion_injective h
  have : i = mulMap M' N := by ext; simp [i]
  exact ⟨this ▸ hi⟩

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

Goal state before:
pp: case e_6
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a✝ : ⨂[R]^na M
b✝ : ⨂[R]^nb M
c✝ : ⨂[R]^nc M
mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M :=
  fun n m ↦ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv
e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯
lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
      ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ
    mul na nb
lhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M),
    ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
          (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
        ↑LinearMap.lflip)
      ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
          (mul na (nb + nc)).flip ∘ₗ
        mul nb nc)).flip
rhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
a : Fin na → M
b : Fin nb → M
c : Fin nc → M
j : Fin (na + (nb + nc))
⊢ ((Fin.append a (Fin.append b c) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯) j = Fin.append a (Fin.append b c) j

Tactic:
refine congr_arg (Fin.append a (Fin.append b c)) (Fin.ext ?_)

Goal state after:
case e_6
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a✝ : ⨂[R]^na M
b✝ : ⨂[R]^nb M
c✝ : ⨂[R]^nc M
mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M :=
  fun n m ↦ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv
e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯
lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
      ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ
    mul na nb
lhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M),
    ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
          (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
        ↑LinearMap.lflip)
      ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
          (mul na (nb + nc)).flip ∘ₗ
        mul nb nc)).flip
rhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
a : Fin na → M
b : Fin nb → M
c : Fin nc → M
j : Fin (na + (nb + nc))
⊢ ↑(Fin.cast ⋯ (Fin.cast ⋯ j)) = ↑j
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
na nb nc : ℕ
a : ⨂[R]^na M
b : ⨂[R]^nb M
c : ⨂[R]^nc M
⊢ (cast R M ⋯) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) =
    GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)

Tactic:
by
  let mul : ∀ n m : ℕ, ⨂[R]^n M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M := fun n m =>
    (TensorProduct.mk R _ _).compr₂ ↑(mulEquiv : _ ≃ₗ[R] (⨂[R]^(n + m)) M)
  -- replace `a`, `b`, `c` with `tprod R a`, `tprod R b`, `tprod R c`
  let e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (add_assoc _ _ _)
  let lhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
    (LinearMap.llcomp R _ _ _ ((mul _ nc).compr₂ e.toLinearMap)).comp (mul na nb)
  have lhs_eq : ∀ a b c, lhs a b c = e (a ₜ* b ₜ* c) := fun _ _ _ => rfl
  let rhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
    (LinearMap.llcomp R _ _ _ (LinearMap.lflip (R := R)).toLinearMap <|
        (LinearMap.llcomp R _ _ _ (mul na _).flip).comp (mul nb nc)).flip
  have rhs_eq : ∀ a b c, rhs a b c = a ₜ* (b ₜ* c) := fun _ _ _ => rfl
  suffices lhs = rhs from
    LinearMap.congr_fun (LinearMap.congr_fun (LinearMap.congr_fun this a) b) c
  ext a b c
  -- clean up
  simp only [e, LinearMap.compMultilinearMap_apply, lhs_eq, rhs_eq, tprod_mul_tprod, cast_tprod]
  congr 1 with j
  rw [Fin.append_assoc]
  refine congr_arg (Fin.append a (Fin.append b c)) (Fin.ext ?_)
  rw [Fin.val_cast, Fin.val_cast]

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
y : M
h₃ : ∀ I ∈ {P | ⊥.colon {x} ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ⊥.colon {y}}, ¬⊥.colon {y} < I
l : ⊥.colon {x} ≤ ⊥.colon {y}
h₁ : ⊥.colon {y} ≠ ⊤
a b : R
hab : (a * b) • y ∈ ⊥
ha : a • y ∉ ⊥
c : R
⊢ c ∈ ⊥.colon {y} → c ∈ ⊥.colon {a • y}

Tactic:
hc

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
y : M
h₃ : ∀ I ∈ {P | ⊥.colon {x} ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ⊥.colon {y}}, ¬⊥.colon {y} < I
l : ⊥.colon {x} ≤ ⊥.colon {y}
h₁ : ⊥.colon {y} ≠ ⊤
a b : R
hab : (a * b) • y ∈ ⊥
ha : a • y ∉ ⊥
c : R
hc : c ∈ ⊥.colon {y}
⊢ c ∈ ⊥.colon {a • y}
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e : J = (⊥.colon {(Ideal.Quotient.mkₐ R I) x}).radical
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
y : R
⊢ (algebraMap R (R ⧸ I)) y * (Ideal.Quotient.mk I) x ∈ ⊥ ↔ (Ideal.Quotient.mk I) (y * x) = 0

Tactic:
Ideal.Quotient.algebraMap_eq,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e : J = (⊥.colon {(Ideal.Quotient.mkₐ R I) x}).radical
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
y : R
⊢ (Ideal.Quotient.mk I) y * (Ideal.Quotient.mk I) x ∈ ⊥ ↔ (Ideal.Quotient.mk I) (y * x) = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : g * z ∈ span {g}
c : R
⊢ c ∈ T → x ∣ normalize b * id c

Tactic:
hc

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : g * z ∈ span {g}
c : R
hc : c ∈ T
⊢ x ∣ normalize b * id c
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
⊢ I ∈ (toPrincipalIdeal R K).range ↔ ∃ x, spanSingleton R⁰ x = ↑I

Tactic:
simp only [MonoidHom.mem_range, toPrincipalIdeal_eq_iff]
  constructor <;> rintro ⟨x, hx⟩
  · exact ⟨x, hx⟩
  · refine ⟨Units.mk0 x ?_, hx⟩
    rintro rfl
    simp [I.ne_zero.symm] at hx

Goal state after: