mathlib-initiative/mathlib-tactics huggingface dataset:
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
V : Type u_3
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Module R V
inst✝⁶ : IsScalarTower R K V
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Module.Finite K V
inst✝² : IsFractionRing R K
M N : Submodule R V
inst✝¹ : IsLattice K M
inst✝ : IsLattice K N
this : IsNoetherian R ↥(M ⊓ N)
⊢ (M ⊓ N).FG

Tactic:
← Module.Finite.iff_fg

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
K : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
V : Type u_3
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Module R V
inst✝⁶ : IsScalarTower R K V
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Module.Finite K V
inst✝² : IsFractionRing R K
M N : Submodule R V
inst✝¹ : IsLattice K M
inst✝ : IsLattice K N
this : IsNoetherian R ↥(M ⊓ N)
⊢ Module.Finite R ↥(M ⊓ N)
Module: Mathlib.RingTheory.Finiteness.Cofinite

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ f.range.FG ↔ f.ker.CoFG

Tactic:
← Module.Finite.iff_fg

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ Module.Finite R ↥f.range ↔ f.ker.CoFG
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁵ : CommRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : IsNoetherianRing K
u v : V →ₗ[K] V₂
⊢ u ≈ v ↔ (u - v).HasFiniteRange

Tactic:
by
  rw [equiv_iff_hasNoetherianRange, hasNoetherianRange_iff_hasFiniteRange]

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✝⁴ : CommRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
u v : V →ₗ[K] V₂
⊢ (u - v).HasNoetherianRange ↔ IsNoetherian K (V ⧸ u.eqLocus v)

Tactic:
hasNoetherianRange_iff_quotient_ker,

Goal state after:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁴ : CommRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
u v : V →ₗ[K] V₂
⊢ IsNoetherian K (V ⧸ (u - v).ker) ↔ IsNoetherian K (V ⧸ u.eqLocus v)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case e_a
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ ↑n
⊢ emultiplicity J I < ⊤

Tactic:
apply hn.trans_lt

Goal state after:
case e_a
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ ↑n
⊢ ↑n < ⊤
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case hp
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
⊢ Irreducible (span {x})

Tactic:
exact (prime_span_singleton_iff.mpr hx).irreducible

Goal state after:
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

Goal state after:
case map_add
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (x y : M × M), (x + y).1 + (x + y).2 = x.1 + x.2 + (y.1 + y.2)

case map_smul
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (c : R) (x : M × M), (c • x).1 + (c • x).2 = c • (x.1 + x.2)
Module: Mathlib.Algebra.Module.LinearMap.Prod

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

Tactic:
apply IsLinearMap.mk

Goal state after:
case map_add
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (x y : M × M), (x + y).1 - (x + y).2 = x.1 - x.2 + (y.1 - y.2)

case map_smul
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (c : R) (x : M × M), (c • x).1 - (c • x).2 = c • (x.1 - x.2)
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case hs2
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
⊢ l.ker.FG

Tactic:
← Module.Finite.iff_fg

Goal state after:
case hs2
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
⊢ Module.Finite R ↥l.ker
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 ⋯
⊢ (linearCombination R Subtype.val).ker.FG

Tactic:
have e : π ∘ₗ Submodule.subtype _ = Submodule.subtype _ ∘ₗ f := by ext; rfl

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
⊢ (linearCombination R Subtype.val).ker.FG
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 ≠ ⊥
⊢ ∃ a, f a = { asIdeal := Ideal.comap (algebraMap R A) P, isPrime := isPrime✝, ne_bot := hp }

Tactic:
exact ⟨⟨P, hP, by aesop⟩, rfl⟩

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

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
hs : ↑p.vars ⊆ s
⊢ ∃ x, (rename Subtype.val) x = p

Tactic:
exact exists_rename_eq_of_vars_subset_range p ((↑) : s → σ) Subtype.val_injective (by simpa)

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

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

Tactic:
refine ⟨f1.choose - a • z, by rw [smul_sub, sub_eq_zero, ha], ?_⟩

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

Goal state before:
pp: case h_add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ∀ (a : σ) (b₁ b₂ : ℕ),
    (monomial (s + Finsupp.single i 1 - Finsupp.single a 1)) ↑(b₁ + b₂) • f a =
      (monomial (s + Finsupp.single i 1 - Finsupp.single a 1)) ↑b₁ • f a +
        (monomial (s + Finsupp.single i 1 - Finsupp.single a 1)) ↑b₂ • f a

Tactic:
intros; simp only [Nat.cast_add, (monomial _).map_add, add_smul]

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

Goal state before:
pp: case add
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 ι σ
p q : MvPolynomial ι' S
hp : ∃ a, (Q.aux P) a = p
hq : ∃ a, (Q.aux P) a = q
⊢ ∃ a, (Q.aux P) a = p + q

Tactic:
obtain ⟨a, rfl⟩ := hp

Goal state after:
case add
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 : MvPolynomial ι' S
hq : ∃ a, (Q.aux P) a = q
a : MvPolynomial (ι' ⊕ ι) R
⊢ ∃ a_1, (Q.aux P) a_1 = (Q.aux P) a + q
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 : σ' ≃ σ
⊢ Ideal.span (Set.range (⇑(rename ⇑e.symm) ∘ P.relation ∘ ⇑f)) = (P.reindex e).ker

Tactic:
rw [Generators.ker_eq_ker_aeval_val, Generators.reindex_val, ← aeval_comp_rename,
      ← AlgHom.comap_ker, ← P.ker_eq_ker_aeval_val, ← P.span_range_relation_eq_ker,
      Set.range_comp, Set.range_comp, Equiv.range_eq_univ, Set.image_univ,
      ← Ideal.map_span (rename ⇑e.symm)]

Goal state after:
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 : σ' ≃ σ
⊢ Ideal.map (rename ⇑e.symm) (Ideal.span (Set.range P.relation)) =
    Ideal.comap (rename ⇑e) (Ideal.span (Set.range P.relation))
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
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'
f : P.Hom P'
x : S
y : Ω[P.Ring⁄R]
⊢ (CotangentSpace.map f) (x ⊗ₜ[P.Ring] y) =
    (algebraMap S S') x ⊗ₜ[P'.Ring] (KaehlerDifferential.map R R' P.Ring P'.Ring) y

Tactic:
by
  rw [CotangentSpace.map, LinearMap.liftBaseChange_tmul, LinearMap.coe_comp, Function.comp_apply,
    LinearMap.restrictScalars_apply, mk_apply, smul_tmul', Algebra.smul_def, mul_one]

Goal state after:
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: case h.right
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
h₄ : ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
l : ℕ
f : Fin l →₀ R
x : (Fin l →₀ R) →ₗ[R] M
hfx : x f = 0
f' : Fin l → R := ⋯
x' : Fin l → M := ⋯
this : ∑ i, f' i • x' i = 0
k : ℕ
a' : Fin l → Fin k → R
y' : Fin k → M
ha'y' : ∀ (i : Fin l), x' i = ∑ j, a' i j • y' j
ha' : ∀ (j : Fin k), ∑ i, f' i * a' i j = 0
⊢ (linearCombination R fun i ↦ equivFunOnFinite.symm (a' i)) f = 0

Tactic:
ext j
      simp only [linearCombination_apply, zero_smul, implies_true, sum_fintype, finsetSum_apply]
      exact ha' j

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 ι
x : ↥Q.ker
⊢ (Q.ofComp P).toAlgHom ↑(Q.kerCompPreimage P x) = ↑x

Tactic:
conv_rhs => rw [← x.1.support_sum_monomial_coeff]
  rw [kerCompPreimage, map_finsuppSum, Finsupp.sum]
  refine Finset.sum_congr rfl fun j _ ↦ ?_
  simp only [map_mul, Hom.toAlgHom_monomial]
  rw [one_smul, Finsupp.prod_mapDomain_index_inj Sum.inl_injective]
  rw [rename_eq_aeval, ← AlgHom.comp_apply, comp_aeval]
  simp only [ofComp_val, Sum.elim_inr, Function.comp_apply,
    Sum.elim_inl, monomial_eq, Hom.toAlgHom_X]
  congr 1
  rw [aeval_def, IsScalarTower.algebraMap_eq R S, ← MvPolynomial.algebraMap_eq,
    ← coe_eval₂Hom, ← map_aeval, P.aeval_val_σ]
  simp [coeff]

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
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 : P.Cotangent
⊢ ((map f - map g) x).val = ((f.sub g ∘ₗ P.cotangentComplex) x).val

Tactic:
obtain ⟨x, rfl⟩ := mk_surjective x

Goal state after:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Extension R S
R' : Type u'
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 : ↥P.ker
⊢ ((map f - map g) (mk x)).val = ((f.sub g ∘ₗ P.cotangentComplex) (mk x)).val
Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
⊢ Surjective ⇑(LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ I i) M) 1)

Tactic:
by
  have := rTensor_surjective M (pi_mkQ_surjective hI)
  classical rw [pi_mkQ_rTensor] at this
  simpa using this

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
ι : Type w
P : Generators R S ι
R' : Type u'
S' : Type v'
ι' : Type w'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators 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 : P.Hom P'
i : ι
j : ι'
⊢ (P'.cotangentSpaceBasis.repr ((CotangentSpace.map f.toExtensionHom) (P.cotangentSpaceBasis i))) j =
    (aeval P'.val) ((pderiv j) (f.val i))

Tactic:
rw [cotangentSpaceBasis_apply]

Goal state after:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
ι : Type w
P : Generators R S ι
R' : Type u'
S' : Type v'
ι' : Type w'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators 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 : P.Hom P'
i : ι
j : ι'
⊢ (P'.cotangentSpaceBasis.repr ((CotangentSpace.map f.toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)))) j =
    (aeval P'.val) ((pderiv j) (f.val 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
ι : Type w
P : Generators R S ι
i : ι
⊢ P.toExtension.toKaehler (P.cotangentSpaceBasis i) = (D R S) (P.val i)

Tactic:
rw [cotangentSpaceBasis_apply]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type w
P : Generators R S ι
i : ι
⊢ P.toExtension.toKaehler (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)) = (D R S) (P.val i)
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
⊢ (∃ m, ∀ r ∉ p.asIdeal, ¬r • m = 0) ↔ RingHom.ker (algebraMap R A) ≤ p.asIdeal

Tactic:
refine ⟨fun ⟨m, hm⟩ x hx ↦ not_not.mp fun hx' ↦ ?_, fun H ↦ ⟨1, fun r hr e ↦ ?_⟩⟩

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
x✝ : ∃ m, ∀ r ∉ p.asIdeal, ¬r • m = 0
x : R
hx : x ∈ RingHom.ker (algebraMap R A)
m : A
hm : ∀ r ∉ p.asIdeal, ¬r • m = 0
hx' : x ∉ p.asIdeal
⊢ False

case refine_2
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
H : RingHom.ker (algebraMap R A) ≤ p.asIdeal
r : R
hr : r ∉ p.asIdeal
e : r • 1 = 0
⊢ False
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: K : Type u_2
E : Type u_4
n : ℕ
inst✝³ : Field K
inst✝² : AddCommGroup E
inst✝¹ : Module K E
I : Type u_5
inst✝ : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
b : Basis I K ↥W
hb : v = ⇑W.subtype ∘ ⇑b
⊢ LinearIndependent (ι := ↑(powersetCard I n)) K (ιMulti_family K n (⇑W.subtype ∘ ⇑b))

Tactic:
← map_comp_ιMulti_family

Goal state after:
K : Type u_2
E : Type u_4
n : ℕ
inst✝³ : Field K
inst✝² : AddCommGroup E
inst✝¹ : Module K E
I : Type u_5
inst✝ : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
b : Basis I K ↥W
hb : v = ⇑W.subtype ∘ ⇑b
⊢ LinearIndependent (ι := ↑(powersetCard I n)) K (⇑(map n W.subtype) ∘ ιMulti_family K n ⇑b)
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
r✝ r' : R₁
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ tprodCoeff R (r✝ • r + r' • r) f = tprodCoeff R (r✝ • r) f + tprodCoeff R (r' • r) f

Tactic:
add_tprodCoeff'

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
this : (cast R M ⋯) (GradedMonoid.GMul.mul (algebraMap₀ r) (algebraMap₀ s)) = algebraMap₀ (r * s)
⊢ (GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom (r * s))).snd =
    (cast R M ⋯).symm
      (GradedMonoid.mk (0 + 0)
          (GradedMonoid.GMul.mul ((↑algebraMap₀).toAddMonoidHom r) ((↑algebraMap₀).toAddMonoidHom s))).snd

Tactic:
exact this.symm

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

Goal state before:
pp: case refine_1.refine_2
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : (↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ p.asIdeal
x : M
hx : x ∈ N₂
hx' : (N₁.submoduleOf N₂).mkQ ⟨x, hx⟩ = e.symm 1
hx'' : N₁.mkQ x = f (e.symm 1)
⊢ N₂ = N₁ ⊔ A ∙ x

Tactic:
refine le_antisymm ?_ (sup_le h ((span_singleton_le_iff_mem _ _).mpr hx))
      have : (span A {x}).map N₁.mkQ = ((span A {1}).map e.symm.toLinearMap).map f := by
        simp only [map_span, Set.image_singleton, hx'', LinearEquiv.coe_coe]
      rw [← N₁.ker_mkQ, sup_comm, ← comap_map_eq, ← map_le_iff_le_comap, this]
      simp [hf₂, Ideal.Quotient.span_singleton_one]

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

Goal state before:
pp: A : Type u
inst✝² : CommRing A
inst✝¹ : IsNoetherianRing A
I : Ideal A
inst✝ : FaithfulSMul A ↥I
this : ↑I ∩ ↑(nonZeroDivisors A) = ∅
⊢ Module.annihilator A ↥I = ⊥

Tactic:
by rwa [Module.annihilator_eq_bot]

Goal state after:
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
inst✝¹ : IsDomain R
inst✝ : Subsingleton (ClassGroup R)
I : (FractionalIdeal R⁰ K)ˣ
⊢ (mk K) I = 1

Tactic:
Subsingleton.elim (ClassGroup.mk K I) 1

Goal state after:
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : Subsingleton (ClassGroup R)
I : (FractionalIdeal R⁰ K)ˣ
⊢ 1 = 1
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
f : K →ₐ[F] L
x✝¹ : L
x✝ : x✝¹ ∈ f.fieldRange
x : K
hx : f.toRingHom x = x✝¹
⊢ (aeval (↑f x)) (minpoly F x) = 0

Tactic:
AlgHom.coe_toRingHom,

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
f : K →ₐ[F] L
x✝¹ : L
x✝ : x✝¹ ∈ f.fieldRange
x : K
hx : f.toRingHom x = x✝¹
⊢ (aeval (f x)) (minpoly F x) = 0
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case refine_1
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
S : Finset (Dual R M × M)
hS : (linearEquiv R M).symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ Ideal.span ↑(Finset.image (fun i ↦ i.1 i.2) S) = ⊤

Tactic:
simpa [Ideal.eq_top_iff_one, (LinearEquiv.symm_apply_eq _).mp hS, linearEquiv]
      using Ideal.sum_mem _ fun i hi ↦ Ideal.subset_span (Finset.mem_image_of_mem _ hi)

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ mapRingHom (algebraMap R A) = mapAlgebra R A

Tactic:
mapRingHom,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ mapAlgebra R A = mapAlgebra R A
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type u_7
T : Type u_8
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* S
g : S →+* T
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
⊢ (mapRingHom g).comp (mapRingHom f) = mapRingHom (g.comp f)

Tactic:
mapRingHom,

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Type u_7
T : Type u_8
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* S
g : S →+* T
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
⊢ (mapAlgebra S T).comp (mapAlgebra R S) = mapAlgebra R T