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

Goal state before:
pp: M : Type u_1
inst✝⁶ : CommMonoidWithZero M
inst✝⁵ : IsCancelMulZero M
N : Type u_2
inst✝⁴ : CommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
⊢ Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)

Tactic:
rw [mkFactorOrderIsoOfFactorDvdEquiv_apply_coe]

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

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
J : FractionalIdeal R₁⁰ K
h : J ≠ 0
⊢ ↑J⁻¹ = IsLocalization.coeSubmodule K ⊤ / ↑J

Tactic:
simp_rw [inv_of_ne_zero _ h, coe_one, coe_mk, IsLocalization.coeSubmodule_top]

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

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : K
hx : x ≠ 0
⊢ spanSingleton R₁⁰ x * (spanSingleton R₁⁰ x)⁻¹ = 1

Tactic:
by
  rw [spanSingleton_inv, spanSingleton_mul_spanSingleton, mul_inv_cancel₀ hx, spanSingleton_one]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case a
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
⊢ ⨆ α, ⨆ (_ : rootSpace H ⇑↑α ≤ LieSubmodule.restr I H), rootSpace H ⇑↑α ≤ ⨆ α ∈ I.rootSet, sl2SubmoduleOfRoot ⋯

Tactic:
exact iSup₂_le fun α hα ↦ le_iSup₂_of_le α hα
        (by rw [sl2SubmoduleOfRoot_eq_sup]; exact le_sup_of_le_left le_sup_left)

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

Goal state before:
pp: case h
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 : R₁
I : FractionalIdeal R₁⁰ K
hI : ∀ J ≤ I, (↑J).FG
hx : ¬x = 0
h_gx : (algebraMap R₁ K) x ≠ 0
h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0
J : FractionalIdeal R₁⁰ K
hJ : J * spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≤ I
s : Finset K
hs : span R₁ ↑s = ↑(J * spanSingleton R₁⁰ ((algebraMap R₁ K) x))
⊢ span R₁ (↑s * ↑{((algebraMap R₁ K) x)⁻¹}) = ↑J

Tactic:
Finset.coe_singleton,

Goal state after:
case h
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 : R₁
I : FractionalIdeal R₁⁰ K
hI : ∀ J ≤ I, (↑J).FG
hx : ¬x = 0
h_gx : (algebraMap R₁ K) x ≠ 0
h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0
J : FractionalIdeal R₁⁰ K
hJ : J * spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≤ I
s : Finset K
hs : span R₁ ↑s = ↑(J * spanSingleton R₁⁰ ((algebraMap R₁ K) x))
⊢ span R₁ (↑s * {((algebraMap R₁ K) x)⁻¹}) = ↑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
⊢ ringEquivOfRingEquiv K K (RingEquiv.refl R) = RingEquiv.refl (FractionalIdeal R⁰ K)

Tactic:
by
  ext I x
  simp only [ringEquivOfRingEquiv_apply, RingEquiv.coe_ringHom_refl, RingEquiv.symm_refl,
    val_eq_coe, RingEquiv.refl_apply, ← mem_coe]
  simp [semilinearEquivOfRingEquiv]

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

Goal state before:
pp: ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
⊢ M ≃ₗ[A] ⨁ (i : ιM), ↥(𝓜 i)

Tactic:
by
  letI h := isModule 𝓐 𝓜
  refine ⟨⟨(DirectSum.decomposeAddEquiv 𝓜).toAddHom, ?_⟩,
    (DirectSum.decomposeAddEquiv 𝓜).symm.toFun, (DirectSum.decomposeAddEquiv 𝓜).left_inv,
    (DirectSum.decomposeAddEquiv 𝓜).right_inv⟩
  intro x y
  classical
  rw [AddHom.toFun_eq_coe, ← DirectSum.sum_support_decompose 𝓐 x, map_sum, Finset.sum_smul,
    AddEquiv.coe_toAddHom, map_sum, Finset.sum_smul]
  refine Finset.sum_congr rfl (fun i _hi => ?_)
  rw [RingHom.id_apply, ← DirectSum.sum_support_decompose 𝓜 y, map_sum, Finset.smul_sum, map_sum,
    Finset.smul_sum]
  refine Finset.sum_congr rfl (fun j _hj => ?_)
  rw [show (decompose 𝓐 x i : A) • (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j) : (⨁ i, 𝓜 i)) =
    DirectSum.Gmodule.smulAddMonoidHom _ _ (decompose 𝓐 ↑(decompose 𝓐 x i))
    (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j)) from DirectSum.Gmodule.smul_def _ _ _ _]
  simp only [decomposeAddEquiv_apply, decompose_coe, Gmodule.smulAddMonoidHom_apply_of_of]
  convert! DirectSum.decompose_coe 𝓜 _
  rfl

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

Goal state before:
pp: T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
⊢ (replicate n J ∩ normalizedFactors I).prod = J ^ min n (count J (normalizedFactors I))

Tactic:
replicate_inter,

Goal state after:
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
⊢ (replicate (min n (count J (normalizedFactors I))) J).prod = J ^ min n (count J (normalizedFactors I))
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✝⁸ : DivisionRing k
inst✝⁷ : Module k M
inst✝⁶ : Module k N
f : M →ₗ[k] N
P : Type u_4
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module k P
g : N →ₗ[k] P
inst✝³ : FiniteDimensional k ↥f.ker
inst✝² : FiniteDimensional k ↥g.ker
inst✝¹ : FiniteDimensional k (N ⧸ f.range)
inst✝ : FiniteDimensional k (P ⧸ g.range)
aux : f.range ≤ comap g (g ∘ₗ f).range
f₀ : ↥f.ker →ₗ[k] ↥(g ∘ₗ f).ker := inclusion ⋯
f₁ : ↥(g ∘ₗ f).ker →ₗ[k] ↥g.ker := f.restrict ⋯
f₂ : ↥g.ker →ₗ[k] N ⧸ f.range := f.range.mkQ ∘ₗ g.ker.subtype
f₃ : N ⧸ f.range →ₗ[k] P ⧸ (g ∘ₗ f).range := f.range.mapQ (g ∘ₗ f).range g aux
f₄ : P ⧸ (g ∘ₗ f).range →ₗ[k] P ⧸ g.range := factor ⋯
h₀ : Injective ⇑f₀
h₁ : Exact ⇑f₀ ⇑f₁
⊢ (g ∘ₗ f).index = g.index + f.index

Tactic:
have h₂ : Exact f₁ f₂ := by rw [exact_iff]; simp [f₁, f₂, ker_comp, map_comap_eq]

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : AddCommGroup N
k : Type u_3
inst✝⁸ : DivisionRing k
inst✝⁷ : Module k M
inst✝⁶ : Module k N
f : M →ₗ[k] N
P : Type u_4
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module k P
g : N →ₗ[k] P
inst✝³ : FiniteDimensional k ↥f.ker
inst✝² : FiniteDimensional k ↥g.ker
inst✝¹ : FiniteDimensional k (N ⧸ f.range)
inst✝ : FiniteDimensional k (P ⧸ g.range)
aux : f.range ≤ comap g (g ∘ₗ f).range
f₀ : ↥f.ker →ₗ[k] ↥(g ∘ₗ f).ker := inclusion ⋯
f₁ : ↥(g ∘ₗ f).ker →ₗ[k] ↥g.ker := f.restrict ⋯
f₂ : ↥g.ker →ₗ[k] N ⧸ f.range := f.range.mkQ ∘ₗ g.ker.subtype
f₃ : N ⧸ f.range →ₗ[k] P ⧸ (g ∘ₗ f).range := f.range.mapQ (g ∘ₗ f).range g aux
f₄ : P ⧸ (g ∘ₗ f).range →ₗ[k] P ⧸ g.range := factor ⋯
h₀ : Injective ⇑f₀
h₁ : Exact ⇑f₀ ⇑f₁
h₂ : Exact ⇑f₁ ⇑f₂
⊢ (g ∘ₗ f).index = g.index + f.index
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a x : R
hx : Prime x
n : ℕ
q : R
hq : a = x ^ n * q
q' : R
hq' : q = x * q'
⊢ x ^ n * q = x ^ (n + 1) * q'

Tactic:
hq'

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a x : R
hx : Prime x
n : ℕ
q : R
hq : a = x ^ n * q
q' : R
hq' : q = x * q'
⊢ x ^ n * (x * q') = x ^ (n + 1) * q'
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
e : ι → ℕ
f : ι → HeightOneSpectrum R
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
i : ι
hi : i ∈ ↑s
j : ι
⊢ j ∈ ↑s → i ≠ j → Function.onFun IsCoprime (fun i ↦ (f i).asIdeal ^ e i) i j

Tactic:
hj

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
e : ι → ℕ
f : ι → HeightOneSpectrum R
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
⊢ i ≠ j → Function.onFun IsCoprime (fun i ↦ (f i).asIdeal ^ e i) i j
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (f i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
i : ι
hi : i ∈ ↑s
j : ι
⊢ j ∈ ↑s → i ≠ j → Function.onFun IsCoprime (fun i ↦ f i ^ e i) i j

Tactic:
hj

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (f i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
⊢ i ≠ j → Function.onFun IsCoprime (fun i ↦ f i ^ e i) i j
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: case mp
σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
h : supported R s ≤ supported R t
i : σ
⊢ i ∈ s → i ∈ t

Tactic:
simpa using @h (X i)

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

Goal state before:
pp: case monomial
σ : 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 : σ
s : σ →₀ ℕ
r : R
⊢ D ((monomial s) r * X i) = (monomial s) r • D (X i) + X i • D ((monomial s) r)

Tactic:
| monomial s r =>

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

Goal state before:
pp: case h.succ.refine_3.refine_2.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this✝ : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
this :
  ∀ (i : Fin d),
    ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
i : Fin d
⊢ f (Submodule.Quotient.mk ⋯.choose) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) (Submodule.Quotient.mk 1)

Tactic:
Ideal.Quotient.mk_eq_mk,

Goal state after:
case h.succ.refine_3.refine_2.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this✝ : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
this :
  ∀ (i : Fin d),
    ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
i : Fin d
⊢ f (Submodule.Quotient.mk ⋯.choose) =
    (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) ((Ideal.Quotient.mk (R ∙ p ^ k i)) 1)
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case mul_X
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h : (pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)
⊢ (pderiv (f x)) ((rename f) (p * X a)) = (rename f) ((pderiv x) (p * X a))

Tactic:
simp only [map_mul, MvPolynomial.rename_X, Derivation.leibniz, MvPolynomial.pderiv_X,
      Pi.single_apply, hf.eq_iff, smul_eq_mul, mul_ite, mul_one, mul_zero, h, map_add]

Goal state after:
case mul_X
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h : (pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)
⊢ (if a = x then (rename f) p else 0) + X (f a) * (rename f) ((pderiv x) p) =
    (rename f) (if a = x then p else 0) + X (f a) * (rename f) ((pderiv x) p)
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: case single
R : Type u
inst✝ : CommRing R
σ : Type u_1
a b : MvPolynomial σ R
⊢ (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential.toFun
        ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) (Finsupp.single a b))) =
    (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) (Finsupp.single a b)

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Finsupp.linearCombination_single,
        map_smul, Derivation.liftKaehlerDifferential_comp_D]

Goal state after:
case single
R : Type u
inst✝ : CommRing R
σ : Type u_1
a b : MvPolynomial σ R
⊢ b •
      (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
        ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1) a) =
    b • (D R (MvPolynomial σ R)) a
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₁ q₂ : Submodule K (Dual K ↥H)
hq₁ : ∀ (i : ↥LieSubalgebra.root), q₁ ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
hq₂ : ∀ (i : ↥LieSubalgebra.root), q₂ ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
h : q₁ ≤ q₂
⊢ LieSubmodule.restr (invtSubmoduleToLieIdeal q₁ hq₁) H ≤ LieSubmodule.restr (invtSubmoduleToLieIdeal q₂ hq₂) H

Tactic:
exact iSup_le fun ⟨α, hα_mem, hα_nz⟩ ↦ le_iSup_of_le ⟨α, h hα_mem, hα_nz⟩ le_rfl

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
ι' : 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 ι σ
⊢ ⇑(Q.aux P) '' Set.range (Q.compRelationAux P) = Set.range Q.relation

Tactic:
by
  ext x
  constructor
  · rintro ⟨y, ⟨a, rfl⟩, rfl⟩
    exact ⟨a, (Q.compRelationAux_map P a).symm⟩
  · rintro ⟨y, rfl⟩
    use Q.compRelationAux P y
    simp only [Set.mem_range, exists_apply_eq_apply, true_and, compRelationAux_map]

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
R' : Type u_1
S' : Type u_2
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
R'' : Type u_4
S'' : Type u_5
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''
f : P.Hom P'
g : P'.Hom P''
x : ↥P.ker
⊢ ((map (g.comp f)) (mk x)).val = ((↑S (map g) ∘ₗ map f) (mk x)).val

Tactic:
simp only [map_mk, Hom.toAlgHom_apply, Hom.comp_toRingHom, RingHom.coe_comp, Function.comp_apply,
    val_mk, LinearMap.coe_comp, LinearMap.coe_restrictScalars]

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

Goal state before:
pp: case refine_3
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u_3
inst✝⁴ : CommRing T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ (rename Sum.inr) (P.σ g) * (monomial (Finsupp.mapDomain Sum.inl (Finsupp.single () 1))) 1 +
      (rename Sum.inr) (P.σ (-1)) * (monomial (Finsupp.mapDomain Sum.inl 0)) 1 =
    (rename Sum.inr) (P.σ g) * X (Sum.inl ()) + C (-1)

Tactic:
· simp [h1, ← X_pow_eq_monomial]

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 ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝³ : CommRing R'
inst✝² : CommRing S'
inst✝¹ : Algebra R' S'
P' : Generators R' S' ι'
inst✝ : Algebra S S'
f : P.Hom P'
⊢ (Hom.id P').comp f = f

Tactic:
by
  ext; simp [Hom.id, aeval_X_left]

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

Goal state before:
pp: case e_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 ι
x : ↥Q.ker
j : ι' →₀ ℕ
x✝ : j ∈ support ↑x
⊢ (algebraMap S Q.Ring) ((↑x).coeff j) = (algebraMap S (MvPolynomial ι' S)) (coeff j ↑x)

Tactic:
simp [coeff]

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 : p ∈ support R M
⊢ q ∈ support R M

Tactic:
by
  rw [Module.mem_support_iff_exists_annihilator] at hp ⊢
  exact ⟨_, hp.choose_spec.trans H⟩

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 g : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
x✝ : Fin (n + 1) → M
⊢ (alternatizeUncurryFin (f + g)) x✝ = (alternatizeUncurryFin f + alternatizeUncurryFin g) x✝

Tactic:
simp [alternatizeUncurryFin_apply, Finset.sum_add_distrib]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s t : ↑(powersetCard I n)
⊢ ((Basis.exteriorPower n b).coord s) (ιMulti_family R n (⇑b) t) = (ιMultiDual R n b s) (ιMulti_family R n (⇑b) t)

Tactic:
rw [Basis.coord_apply]

Goal state after:
R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s t : ↑(powersetCard I n)
⊢ ((Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) t)) s = (ιMultiDual R n b s) (ιMulti_family R n (⇑b) t)
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✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝¹ : Finite ι
this✝ : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this : Module.Finite R ↥i.ker
⊢ Subsingleton ↥i.ker

Tactic:
← IsLocalRing.subsingleton_tensorProduct (R := R),

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝¹ : Finite ι
this✝ : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this : Module.Finite R ↥i.ker
⊢ Subsingleton (k ⊗[R] ↥i.ker)
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝² : Finite ι
this✝¹ : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this✝ : Module.Finite R ↥i.ker
this : Surjective ⇑(LinearMap.baseChange k i)
hi' : Function.Bijective ⇑(LinearMap.baseChange k i)
x : k ⊗[R] ↥i.ker
⊢ Function.Injective ⇑(LinearMap.lTensor R i.ker.subtype)

pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝² : Finite ι
this✝¹ : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this✝ : Module.Finite R ↥i.ker
this : Surjective ⇑(LinearMap.baseChange k i)
hi' : Function.Bijective ⇑(LinearMap.baseChange k i)
x : k ⊗[R] ↥i.ker
⊢ (LinearMap.lTensor (R ⧸ 𝔪) i.ker.subtype) x = (LinearMap.lTensor (R ⧸ 𝔪) i.ker.subtype) 0

Tactic:
· apply Module.Flat.lTensor_preserves_injective_linearMap
      exact Subtype.val_injective

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝² : Finite ι
this✝¹ : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this✝ : Module.Finite R ↥i.ker
this : Surjective ⇑(LinearMap.baseChange k i)
hi' : Function.Bijective ⇑(LinearMap.baseChange k i)
x : k ⊗[R] ↥i.ker
⊢ (LinearMap.lTensor (R ⧸ 𝔪) i.ker.subtype) x = (LinearMap.lTensor (R ⧸ 𝔪) i.ker.subtype) 0
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁰ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁹ : (i : ι) → AddCommMonoid (s i)
inst✝⁸ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
E : Type u_9
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
F : Type u_10
inst✝³ : AddCommMonoid F
inst✝² : Semiring R₁
inst✝¹ : Module R₁ R
inst✝ : SMulCommClass R₁ R R
x✝ x y : ⨂[R] (i : ι), s i
ihx : 0 • x = 0
ihy : 0 • y = 0
⊢ 0 • (x + y) = 0

Tactic:
simp_rw [PiTensorProduct.smul_add, ihx, ihy, add_zero]

Goal state after: