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

Goal state before:
pp: case refine_4
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x✝ : K
hx✝¹ : x✝ ∈ span R₁ (f '' ↑s)
c : R₁
x : K
hx✝ : x ∈ span R₁ (f '' ↑s)
hx : IsInteger R₁ (↑a' • x)
⊢ IsInteger R₁ (c • ↑a' • x)

Tactic:
exact IsLocalization.isInteger_smul hx

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
y : P
h : y = 0
⊢ spanSingleton S y = 0

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ ∃ P x, ∃ (_ : ∀ p ∈ P, Prime p), ∃ e, DirectSum.IsInternal fun p ↦ torsionBySet R M ↑(↑p ^ e p)

Tactic:
by
  exact ⟨_, _, fun p hp => prime_of_factor p (Multiset.mem_toFinset.mp hp), _,
    isInternal_prime_power_torsion hM⟩

Goal state after:
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₁
x : K
h : x = 0
⊢ 1 / spanSingleton R₁⁰ x = spanSingleton R₁⁰ x⁻¹

Tactic:
simp [h]

Goal state after:
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₁
x : K
h : ¬x = 0
⊢ spanSingleton R₁⁰ x * spanSingleton R₁⁰ x⁻¹ = 1

Tactic:
simp [h]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
I J : FractionalIdeal S P
h : ∀ z ∈ I, x * z ∈ J
z : R
zI : P
hzI : zI ∈ I
⊢ z • x * zI ∈ J

Tactic:
rw [Algebra.smul_mul_assoc]

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
I J : FractionalIdeal S P
h : ∀ z ∈ I, x * z ∈ J
z : R
zI : P
hzI : zI ∈ I
⊢ z • (x * zI) ∈ J
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_5
K : Type u_7
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
x : K
⊢ x ∈ (ringEquivOfRingEquiv K K (RingEquiv.refl R)) I ↔ x ∈ (RingEquiv.refl (FractionalIdeal R⁰ K)) I

Tactic:
simp only [ringEquivOfRingEquiv_apply, RingEquiv.coe_ringHom_refl, RingEquiv.symm_refl,
    val_eq_coe, RingEquiv.refl_apply, ← mem_coe]

Goal state after:
R : Type u_5
K : Type u_7
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
x : K
⊢ x ∈ ↑⟨Submodule.map ↑(semilinearEquivOfRingEquiv K K (RingEquiv.refl R)) ↑I, ⋯⟩ ↔ x ∈ ↑I
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
K : Type u_2
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : IsFractionRing R K
M : Submodule R (ι → K)
inst✝ : IsLattice K M
⊢ Module.rank R ↥M = ↑(Fintype.card ι)

Tactic:
rw [IsLattice.rank' K M]

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
K : Type u_2
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : IsFractionRing R K
M : Submodule R (ι → K)
inst✝ : IsLattice K M
⊢ Module.rank K (ι → K) = ↑(Fintype.card ι)
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u : V →ₗ[K] V₂
v : V₂ →ₗ[K] V₃
u' : V₂ →ₗ[K] V
v' : V₃ →ₗ[K] V₂
hu : u'.IsLeftQuasiInverse u
hv : v'.IsLeftQuasiInverse v
⊢ u' ∘ₗ (v' ∘ₗ v) ∘ₗ u ≈ u' ∘ₗ id ∘ₗ u

Tactic:
grw [hv.equiv]

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
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u : V →ₗ[K] V₂
v : V₂ →ₗ[K] V₃
v' : V₃ →ₗ[K] V₂
w : V₃ →ₗ[K] V
hv : v'.IsLeftQuasiInverse v
hw : w.IsRightQuasiInverse (v ∘ₗ u)
⊢ id ∘ₗ u ∘ₗ w ∘ₗ v ≈ (v' ∘ₗ v) ∘ₗ u ∘ₗ w ∘ₗ v

Tactic:
grw [hv.equiv]

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : CommRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S T : Submodule K V
hST : IsCompl S T
⊢ S.projection T hST ≈ id ↔ IsNoetherian K ↥T

Tactic:
FiniteRangeSetoid.projection_equiv_id_iff_isNoetherian hST

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : CommRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S T : Submodule K V
hST : IsCompl S T
⊢ IsNoetherian K ↥T ↔ IsNoetherian K ↥T
Module: Mathlib.Algebra.Module.LinearMap.Prod

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ IsLinearMap R fun x ↦ x.1 + x.2

Tactic:
apply IsLinearMap.mk
  · intro x y
    simp only [Prod.fst_add, Prod.snd_add]
    abel
  · simp [smul_add]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a x : R
hx : Prime x
n : ℕ
hle : x ^ n ∣ a
hlt : ¬x ^ (n + 1) ∣ a
⊢ (Associates.mk (span {x})).count (Associates.mk (span {a})).factors = n

Tactic:
obtain ⟨q, hq⟩ := hle
  apply count_associates_eq hx _ hq
  contrapose hlt with hdvd
  obtain ⟨q', hq'⟩ := hdvd
  use q'
  rw [hq, hq']
  ring

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
c : Ideal R
hc : c ∈ normalizedFactors (span {b})
hc' : Associated (span {a}) c
⊢ span {a} ∈ normalizedFactors (span {b})

Tactic:
associated_iff_eq.mp hc'

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
c : Ideal R
hc : c ∈ normalizedFactors (span {b})
hc' : Associated (span {a}) c
⊢ c ∈ normalizedFactors (span {b})
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:
ext1
  simp [supportedEquivMvPolynomial, MvPolynomial.algebraMap_eq]

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

Goal state before:
pp: σ : 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
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (mkDerivationₗ R f) ((monomial s) 1 * X i) =
    (monomial s) 1 • (mkDerivationₗ R f) (X i) + X i • (mkDerivationₗ R f) ((monomial s) 1)

Tactic:
simp only [mkDerivationₗ_monomial, X, monomial_mul, one_smul, one_mul]
      rw [Finsupp.sum_add_index'] <;>
        [skip; simp; (intros; simp only [Nat.cast_add, (monomial _).map_add, add_smul])]
      rw [Finsupp.sum_single_index, Finsupp.sum_single_index] <;> [skip; simp; simp]
      rw [tsub_self, add_tsub_cancel_right, Nat.cast_one, ← C_apply, C_1, one_smul, add_comm,
        Finsupp.smul_sum]
      refine congr_arg₂ (· + ·) rfl (Finset.sum_congr rfl fun j hj => ?_); dsimp only
      rw [smul_smul, monomial_mul, one_mul, add_comm s, add_tsub_assoc_of_le]
      rwa [Finsupp.single_le_iff, Nat.succ_le_iff, pos_iff_ne_zero, ← Finsupp.mem_support_iff]

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

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommSemiring R
i j : σ
h : j ≠ i
⊢ (pderiv i) (X j) = 0

Tactic:
simp [h]

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

Goal state before:
pp: case pos
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m n : σ →₀ ℕ
a : R
h : n = m + single i 1
⊢ (if n - single i 1 = m then a * ↑(n i) else 0) = (if n = m + single i 1 then a else 0) * (↑(m i) + 1)

Tactic:
simp [h]

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

Goal state before:
pp: case inr
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p : MvPolynomial σ R
j : σ
eq : (pderiv i) ((map φ) p) = (map φ) ((pderiv i) p)
h : j ≠ i
⊢ (pderiv i) ((map φ) (p * X j)) = (map φ) ((pderiv i) (p * X j))

Tactic:
simp [eq, h]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
d : Derivation R A M
a : A
⊢ ∀ (a_1 b : R[X]),
    { toFun := fun f ↦ (AEval.of R M a) (d ((aeval a) f)), map_add' := ⋯, map_smul' := ⋯ } (a_1 * b) =
      a_1 • { toFun := fun f ↦ (AEval.of R M a) (d ((aeval a) f)), map_add' := ⋯, map_smul' := ⋯ } b +
        b • { toFun := fun f ↦ (AEval.of R M a) (d ((aeval a) f)), map_add' := ⋯, map_smul' := ⋯ } a_1

Tactic:
simp [AEval.of_aeval_smul, -Derivation.map_aeval]

Goal state after:
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
M : Submonoid S
S' : Type u_1
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : IsLocalization M S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R S S'
P : Extension R S
this : Algebra (Localization (Submonoid.comap (algebraMap P.Ring S) M)) S' := ⋯
⊢ algebraMap R S' =
    (algebraMap (Localization (Submonoid.comap (algebraMap P.Ring S) M)) S').comp
      (algebraMap R (Localization (Submonoid.comap (algebraMap P.Ring S) M)))

Tactic:
RingHom.algebraMap_toAlgebra,

Goal state after:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P✝ : Extension R S
M : Submonoid S
S' : Type u_1
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : IsLocalization M S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R S S'
P : Extension R S
this : Algebra (Localization (Submonoid.comap (algebraMap P.Ring S) M)) S' := (IsLocalization.lift ⋯).toAlgebra
⊢ algebraMap R S' = (IsLocalization.lift ⋯).comp (algebraMap R (Localization (Submonoid.comap (algebraMap P.Ring S) M)))
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)
α : ↥LieSubalgebra.root
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : α ∈ J.rootSet
hα_not : (rootSystem H).root α ∉ q
hα_nz : (↑α).IsNonZero
hne : ∀ (χ : Weight K (↥H) L), Weight.toLinear K (↥H) L χ ∈ q → ⇑χ ≠ ⇑↑α
x✝ : { α // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ Weight.toLinear K (↥H) L (-β) ∈ q

Tactic:
Weight.toLinear_neg

Goal state after:
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)
α : ↥LieSubalgebra.root
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : α ∈ J.rootSet
hα_not : (rootSystem H).root α ∉ q
hα_nz : (↑α).IsNonZero
hne : ∀ (χ : Weight K (↥H) L), Weight.toLinear K (↥H) L χ ∈ q → ⇑χ ≠ ⇑↑α
x✝ : { α // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ -Weight.toLinear K (↥H) L β ∈ q
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)
α : ↥LieSubalgebra.root
⊢ α ∈ (invtSubmoduleToLieIdeal q hq).rootSet ↔ (rootSystem H).root α ∈ q

Tactic:
by
  set J := invtSubmoduleToLieIdeal q hq
  constructor
  · intro hα_mem
    by_contra hα_not
    have hα_nz := H.isNonZero_coe_root α
    have hne (χ : Weight K H L) (hχ : ↑χ ∈ q) : (χ : H → K) ≠ ((α : Weight K H L) : H → K) :=
      fun heq ↦ hα_not (by simpa [rootSystem_root_apply] using DFunLike.coe_injective heq ▸ hχ)
    have h_le : J.restr H ≤ ⨆ (χ : H → K) (_ : χ ≠ (α : Weight K H L)), genWeightSpace L χ := by
      refine iSup_le fun ⟨β, hβ_mem, hβ_nz⟩ ↦ ?_
      rw [sl2SubmoduleOfRoot_eq_sup]
      refine sup_le (sup_le ?_ ?_) ?_
      · exact le_iSup₂_of_le _ (hne β hβ_mem) le_rfl
      · have : ↑(-β) ∈ q := by rw [Weight.toLinear_neg]; exact q.neg_mem hβ_mem
        exact le_iSup₂_of_le _ (hne (-β) this) le_rfl
      · apply (LieSubmodule.map_incl_le.trans (rootSpace_zero_eq K L H).symm.le).trans
        exact le_iSup₂_of_le 0 (fun h ↦ hα_nz h.symm) le_rfl
    have h_disj := ((iSupIndep_genWeightSpace K H L _).mono_right h_le).mono_right hα_mem
    exact (α : Weight K H L).genWeightSpace_ne_bot L (disjoint_self.mp h_disj)
  · intro hα
    calc rootSpace H (α : Weight K H L)
        ≤ sl2SubmoduleOfRoot (H.isNonZero_coe_root α) := by
          rw [sl2SubmoduleOfRoot_eq_sup]; exact le_sup_of_le_left le_sup_left
      _ ≤ ⨆ x : {β : Weight K H L // ↑β ∈ q ∧ β.IsNonZero}, sl2SubmoduleOfRoot x.2.2 :=
          le_iSup_of_le ⟨↑α, hα, H.isNonZero_coe_root α⟩ le_rfl
      _ = J.restr H := (restr_invtSubmoduleToLieIdeal_eq_iSup q hq).symm

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

Goal state before:
pp: case mpr
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
x : MvPolynomial ι' S
⊢ x ∈ Set.range Q.relation → x ∈ ⇑(Q.aux P) '' Set.range (Q.compRelationAux P)

Tactic:
rintro ⟨y, rfl⟩

Goal state after:
case mpr
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
y : σ'
⊢ Q.relation y ∈ ⇑(Q.aux P) '' Set.range (Q.compRelationAux P)
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 ι
r : R
inst✝ : IsLocalization.Away r S
s : S
⊢ (aeval fun x ↦ IsLocalization.Away.invSelf r)
      (C (IsLocalization.Away.sec r s).1 * X () ^ (IsLocalization.Away.sec r s).2) =
    s

Tactic:
by
    rw [map_mul, algHom_C, map_pow, aeval_X]
    simp only [← IsLocalization.Away.sec_spec, map_pow, IsLocalization.Away.invSelf]
    rw [← IsLocalization.mk'_pow, one_pow, ← IsLocalization.mk'_one (M := Submonoid.powers r) S r]
    rw [← IsLocalization.mk'_pow, one_pow, mul_assoc, ← IsLocalization.mk'_mul]
    rw [mul_one, one_mul, IsLocalization.mk'_pow]
    simp

Goal state after:
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✝ : Module A N✝
f✝ f'✝ : (relations.G →₀ A) →ₗ[A] N✝
h : relations.solutionFinsupp.postcomp f✝ = relations.solutionFinsupp.postcomp f'✝
⊢ f✝ = f'✝

Tactic:
by ext; apply Solution.congr_var h

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

Goal state before:
pp: case 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
b : B
w : presM.R →₀ B
a✝¹ : r ∉ w.support
a✝ : b ≠ 0
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
⊢ Finsupp.single r b ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
obtain ⟨β, rfl⟩ := presB.surjective_π b

Goal state after:
case 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
⊢ Finsupp.single r (presB.π β) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
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 (ι' →₀ ℕ)
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
this :
  ∑ v ∈ Finset.map (↑e).toEmbedding (support x), (monomial (e.symm v)) (coeff (e.symm v) x) ∈
    Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
⊢ x ∈ Ideal.map (Q.toComp P).toAlgHom P.ker

Tactic:
simpa only [AlgHom.toRingHom_eq_coe, Finset.sum_map, Equiv.coe_toEmbedding,
        EquivLike.coe_coe, AddEquiv.symm_apply_apply, support_sum_monomial_coeff] using! this

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

Goal state before:
pp: case tmul.tmul
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''
f : P.Hom P'
g : P'.Hom P''
x : S
x✝ y✝ : P.Ring
⊢ (CotangentSpace.map (g.comp f)) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ ⊗ₜ[R] y✝)) =
    (↑S (CotangentSpace.map g) ∘ₗ CotangentSpace.map f) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ ⊗ₜ[R] y✝))

Tactic:
| tmul =>

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

Goal state before:
pp: case tmul
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''
f : P.Hom P'
g : P'.Hom P''
x : S
y : P.Ring ⊗[R] P.Ring
⊢ (CotangentSpace.map (g.comp f)) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo y) =
    (↑S (CotangentSpace.map g) ∘ₗ CotangentSpace.map f) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo y)

Tactic:
induction y with
    | zero => simp only [map_zero, tmul_zero]
    | add => simp only [map_add, tmul_add, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
      Function.comp_apply, *]
    | tmul => simp only [Derivation.tensorProductTo_tmul, tmul_smul, smul_tmul', map_tmul,
        Hom.toAlgHom_apply, Hom.comp_toRingHom, RingHom.coe_comp, Function.comp_apply,
        LinearMap.coe_comp, LinearMap.coe_restrictScalars,
        ← IsScalarTower.algebraMap_apply S S' S'']

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

Goal state before:
pp: case tmul.tmul
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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : S
x✝ y✝ : P.Ring
⊢ (CotangentSpace.map f - CotangentSpace.map g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ ⊗ₜ[R] y✝)) =
    (↑S P'.cotangentComplex ∘ₗ f.sub g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ ⊗ₜ[R] y✝))

Tactic:
| tmul =>

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 ι
⊢ Ideal.map (Q.ofComp P).toAlgHom (Q.comp P).ker = Q.ker

Tactic:
by
  ext x
  rw [Ideal.mem_map_iff_of_surjective _ (toAlgHom_ofComp_surjective Q P)]
  constructor
  · rintro ⟨x, hx, rfl⟩
    simp only [ker_eq_ker_aeval_val,
      RingHom.mem_ker] at hx ⊢
    rw [← hx, Hom.algebraMap_toAlgHom, algebraMap_self_apply]
  · intro hx
    exact ⟨_, (kerCompPreimage Q P ⟨x, hx⟩).2, ofComp_kerCompPreimage Q P ⟨x, hx⟩⟩

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 q : PrimeSpectrum R
H : p ≤ q
hp : ∃ m, (R ∙ m).annihilator ≤ p.asIdeal
⊢ ∃ m, (R ∙ m).annihilator ≤ q.asIdeal

Tactic:
exact ⟨_, hp.choose_spec.trans H⟩

Goal state after: