mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ p ^ k • Submodule.Quotient.mk f1.choose = 0

Tactic:
f1.choose_spec,

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
⊢ p ^ k • f 1 = 0
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.Algebra.MvPolynomial.PDeriv

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

Tactic:
induction p using MvPolynomial.induction_on with

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

Goal state before:
pp: R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : MvPolynomial (σ ⊕ τ) R
f : τ → S
j : σ
⊢ (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)

Tactic:
induction p using MvPolynomial.induction_on with

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
σ : Type u_1
ι : Type u_2
p : MvPolynomial (σ ⊕ ι) R
i : σ
⊢ (pderiv i) ((sumRingEquiv R σ ι) p) = (sumRingEquiv R σ ι) ((pderiv (Sum.inl i)) p)

Tactic:
induction p using MvPolynomial.induction_on with

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

Goal state before:
pp: R : Type u_5
N : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
S : Type u_3
ι : Type u_4
inst✝² : Finite ι
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ IsBaseChange S (baseChangeHom R S (ι → R) N)

Tactic:
have : Fintype ι := Fintype.ofFinite ι

Goal state after:
R : Type u_5
N : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
S : Type u_3
ι : Type u_4
inst✝² : Finite ι
inst✝¹ : CommRing S
inst✝ : Algebra R S
this : Fintype ι
⊢ IsBaseChange S (baseChangeHom R S (ι → R) N)
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case refine_3
R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : FinitePresentation R M
n m : ℕ
f : (Fin n → R) →ₗ[R] M
g : (Fin m → R) →ₗ[R] Fin n → R
hf : Function.Surjective ⇑f
hfg : Function.Exact ⇑g ⇑f
⊢ Function.Exact ⇑(lcomp S (S ⊗[R] N) (baseChange S f)) ⇑(lcomp S (S ⊗[R] N) (baseChange S g))

Tactic:
apply exact_lcomp_of_exact_of_surjective
    · exact lTensor_exact S hfg hf
    · exact LinearMap.lTensor_surjective S hf

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.16
S' : Type ?u.18
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝² : CommRing R''
inst✝¹ : CommRing S''
inst✝ : Algebra R'' S''
P'' : Extension R'' S''
P : Extension R S
x : S
⊢ (algebraMap (P.Ring ⧸ P.ker ^ 2) S) ((⇑(Ideal.Quotient.mk (P.ker ^ 2)) ∘ P.σ) x) = x

Tactic:
by dsimp; exact P.algebraMap_σ 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
ι' : 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 : MvPolynomial ι' S
⊢ ∃ a, (Q.aux P) a = p

Tactic:
induction p using MvPolynomial.induction_on with

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 ι σ
⊢ Ideal.comap (↑(sumAlgEquiv R ι' ι)) (Ideal.map C (RingHom.ker (aeval P.val))) =
    Ideal.map (rename Sum.inr) (RingHom.ker (aeval P.val))

Tactic:
change Ideal.comap _ (Ideal.map (IsScalarTower.toAlgHom R (MvPolynomial ι R) _) _) = _

Goal state after:
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 ι σ
⊢ Ideal.comap (↑(sumAlgEquiv R ι' ι))
      (Ideal.map (IsScalarTower.toAlgHom R (MvPolynomial ι R) (MvPolynomial ι' (MvPolynomial ι R)))
        (RingHom.ker (aeval P.val))) =
    Ideal.map (rename Sum.inr) (RingHom.ker (aeval P.val))
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 ι
x : P.Ring
⊢ (algebraMap P.Ring S) x = (aeval P.val) x

Tactic:
by
  simp [algebraMap_eq]

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

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

Tactic:
rw [← top_le_iff, ← h₁, LinearMap.range_eq_map, ← h₂]

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₁ : Extension.Cotangent.mk.range = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = ⊤
⊢ Submodule.map Extension.Cotangent.mk (Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩)) ≤ φ.range
Module: Mathlib.Algebra.Module.Presentation.Free

Goal state before:
pp: case mpr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ (∃ p, IsEmpty p.R) → Free A M

Tactic:
· rintro ⟨p, h⟩
    exact p.toIsPresentation.free

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 ι
p : Q.Ring
⊢ ∃ a, (Q.ofComp P).toAlgHom a = p

Tactic:
induction p using MvPolynomial.induction_on with

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'
f : P.Hom P'
x : S
y : P.Ring
⊢ (x • 1) ⊗ₜ[P'.Ring] (D R' P'.Ring) ((algebraMap P.Ring P'.Ring) y) =
    (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom y)

Tactic:
← Algebra.algebraMap_eq_smul_one

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'
f : P.Hom P'
x : S
y : P.Ring
⊢ (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) ((algebraMap P.Ring P'.Ring) y) =
    (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom y)
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
P : Type u_3
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R P
h₁ : P →ₗ[R] M
w✝ : ℕ
K : Submodule R (Fin w✝ → R)
ϕ : P ≃ₗ[R] (Fin w✝ → R) ⧸ K
hK : K.FG
this✝ : Module.Finite R ↥K
this : (h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w✝ → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ = y ∘ₗ a
ha : a ∘ₗ K.subtype = 0
⊢ K ≤ a.ker

Tactic:
← range_le_ker_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
P : Type u_3
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R P
h₁ : P →ₗ[R] M
w✝ : ℕ
K : Submodule R (Fin w✝ → R)
ϕ : P ≃ₗ[R] (Fin w✝ → R) ⧸ K
hK : K.FG
this✝ : Module.Finite R ↥K
this : (h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w✝ → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ = y ∘ₗ a
ha : K.subtype.range ≤ a.ker
⊢ K ≤ a.ker
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin n
h : Even ↑k
this : NeZero n
⊢ Even k

Tactic:
rw [← Fin.cast_val_eq_self k]

Goal state after:
n : ℕ
k : Fin n
h : Even ↑k
this : NeZero n
⊢ Even ↑↑k
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin n
inst✝ : NeZero n
h : Odd ↑k
⊢ Odd k

Tactic:
rw [← Fin.cast_val_eq_self k]

Goal state after:
n : ℕ
k : Fin n
inst✝ : NeZero n
h : Odd ↑k
⊢ Odd ↑↑k
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
⊢ ∑ x,
      ∑ x_1 ≥ x,
        ((-1) ^ ↑x •
            (-1) ^ ↑x_1 • ((f (v x.castSucc)) (x.castSucc.removeNth v x_1)) (x_1.removeNth (x.castSucc.removeNth v)) +
          (-1) ^ (↑x_1 + 1) •
            (-1) ^ ↑x • ((f (v x_1.succ)) (x_1.succ.removeNth v x)) (x.removeNth (x_1.succ.removeNth v))) =
    ∑ i,
      ∑ j ≥ i,
        (-1) ^ (↑i + ↑j) •
          (((f (v i.castSucc)) (v j.succ)) (j.removeNth (i.castSucc.removeNth v)) -
            ((f (v j.succ)) (v i.castSucc)) (j.removeNth (i.castSucc.removeNth v)))

Tactic:
refine Fintype.sum_congr _ _ fun i ↦ Finset.sum_congr rfl fun j hj ↦ ?_

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : j ∈ Finset.Ici i
⊢ (-1) ^ ↑i • (-1) ^ ↑j • ((f (v i.castSucc)) (i.castSucc.removeNth v j)) (j.removeNth (i.castSucc.removeNth v)) +
      (-1) ^ (↑j + 1) • (-1) ^ ↑i • ((f (v j.succ)) (j.succ.removeNth v i)) (i.removeNth (j.succ.removeNth v)) =
    (-1) ^ (↑i + ↑j) •
      (((f (v i.castSucc)) (v j.succ)) (j.removeNth (i.castSucc.removeNth v)) -
        ((f (v j.succ)) (v i.castSucc)) (j.removeNth (i.castSucc.removeNth v)))
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: case neg
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)
hst : s ≠ t
⊢ (Finsupp.single t 1) s = 0

Tactic:
Finsupp.single_eq_of_ne hst

Goal state after:
case neg
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)
hst : s ≠ t
⊢ 0 = 0
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✝ : Module.Finite R M
p : PrimeSpectrum R
K : Type u_1 := p.asIdeal.ResidueField
e : K ⊗[R] M ≃ₗ[K] K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) :=
  (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) K K M).symm
⊢ Nontrivial (Localization p.asIdeal.primeCompl ⊗[R] M) ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))

Tactic:
← not_iff_not,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
p : PrimeSpectrum R
K : Type u_1 := p.asIdeal.ResidueField
e : K ⊗[R] M ≃ₗ[K] K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) :=
  (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) K K M).symm
⊢ ¬Nontrivial (Localization p.asIdeal.primeCompl ⊗[R] M) ↔
    ¬Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
ι : Type u_1
n : Basis ι R ↥N
H :
  Function.Injective
    ⇑(M.mulMap N ∘ₗ LinearMap.lTensor ↥M ↑n.repr.symm ∘ₗ ↑(TensorProduct.finsuppScalarRight R R (↥M) ι).symm)
⊢ M.LinearDisjoint N

Tactic:
← LinearEquiv.coe_lTensor,

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
ι : Type u_1
n : Basis ι R ↥N
H :
  Function.Injective
    ⇑(M.mulMap N ∘ₗ ↑(LinearEquiv.lTensor (↥M) n.repr.symm) ∘ₗ ↑(TensorProduct.finsuppScalarRight R R (↥M) ι).symm)
⊢ M.LinearDisjoint N
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
n : ℕ
a : ⨂[R]^n M
⊢ (cast R M ⋯) (GradedMonoid.GMul.mul a GradedMonoid.GOne.one) = a

Tactic:
rw [gMul_def, gOne_def]
  induction a using PiTensorProduct.induction_on with
  | smul_tprod r a =>
    rw [← TensorProduct.smul_tmul', map_smul, map_smul, ← gMul_def, tprod_mul_tprod R a _,
      cast_tprod]
    simp
  | add x y hx hy =>
    rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]

Goal state after:
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✝ : Flat R M
ι : Type u
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
s : Finset ι
f : ι → R
hfv : ∑ i ∈ s, f i • v i = 0
i : ι
hi : i ∈ s
⊢ f i = 0

Tactic:
induction s using Finset.induction generalizing v i with

Goal state after:
case insert
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n : ι
s : Finset ι
hn : n ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i ∈ insert n s, f i • v i = 0
i : ι
hi : i ∈ insert n s
⊢ f i = 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
x✝ : DecidableEq ι
f : (i : ι) → s i
i : ι
r : R
x : s i
⊢ tprodCoeff R 1 (update f i (r • x)) = r • tprodCoeff R 1 (update f i x)

Tactic:
rw [smul_tprodCoeff', ← smul_tprodCoeff (1 : R) _ i, update_idem, update_self]

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
smul_tprod : ∀ (r : R) (f : (i : ι) → s i), motive (r • (tprod R) f)
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
⊢ motive z

Tactic:
simp_rw [← tprodCoeff_eq_smul_tprod] at smul_tprod
  exact PiTensorProduct.induction_on' z smul_tprod add

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
h : IsAssociatedPrime J (R ⧸ I)
⊢ J = I.radical

Tactic:
obtain ⟨hJ, x, e⟩ := h

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R ⧸ I
e : J = (⊥.colon {x}).radical
⊢ J = I.radical
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
this : Nontrivial (R ⧸ I)
a : Ideal R
ha : a ∈ associatedPrimes R (R ⧸ I)
⊢ I.radical ∈ associatedPrimes R (R ⧸ I)

Tactic:
exact ha.eq_radical hI ▸ ha

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

Goal state before:
pp: A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
⊢ N₁.IsQuotientEquivQuotientPrime N₂ ↔ ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x

Tactic:
let f := mapQ (N₁.submoduleOf N₂) N₁ N₂.subtype le_rfl
  have hf₁ : ker f = ⊥ := ker_liftQ_eq_bot _ _ _ (by simp [ker_comp, submoduleOf])
  have hf₂ : range f = N₂.map N₁.mkQ := by simp [f, mapQ, range_liftQ, range_comp]
  refine ⟨fun ⟨h, p, ⟨e⟩⟩ ↦ ?_, fun ⟨x, hx, hx'⟩ ↦ ⟨le_sup_left.trans_eq hx'.symm, ⟨_, hx⟩, ?_⟩⟩
  · obtain ⟨⟨x, hx⟩, hx'⟩ := Submodule.mkQ_surjective _ (e.symm 1)
    have hx'' : N₁.mkQ x = f (e.symm 1) := by simp [f, ← hx']
    refine ⟨x, ?_, ?_⟩
    · convert! p.2
      ext r
      simp [hx'', ← map_smul, Algebra.smul_def, show f _ = 0 ↔ _ from congr(_ ∈ $hf₁),
        Ideal.Quotient.eq_zero_iff_mem]
    · 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]
  · have hxN₂ : x ∈ N₂ := (le_sup_right.trans_eq hx'.symm) (mem_span_singleton_self x)
    refine ⟨.symm (.ofBijective (Submodule.mapQ _ _ (toSpanSingleton A _ ⟨x, hxN₂⟩) ?_) ⟨?_, ?_⟩)⟩
    · simp [SetLike.le_def, ← Quotient.mk_smul, submoduleOf]
    · refine ker_eq_bot.mp (ker_liftQ_eq_bot _ _ _ ?_)
      simp [← Quotient.mk_smul, SetLike.le_def, submoduleOf]
    · rw [mapQ, ← range_eq_top, range_liftQ, range_comp]
      have := congr($(hx').submoduleOf N₂)
      rw [submoduleOf_self, submoduleOf_sup_of_le (by simp_all) (by simp_all),
        submoduleOf_span_singleton_of_mem _ hxN₂] at this
      simpa [← span_singleton_eq_range, LinearMap.range_toSpanSingleton] using this.symm

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

Goal state before:
pp: case zero
A : Type u
inst✝³ : CommRing A
inst✝² : IsNoetherianRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x✝ : Module.Finite A M
motive : (N : Type v) → [inst : AddCommGroup N] → [inst_1 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (N₃ : Type v)
    [inst_6 : AddCommGroup N₃] [inst_7 : Module A N₃] [inst_8 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂) (g : N₂ →ₗ[A] N₃),
    Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂),
    motive N₁ → motive N₂
s : RelSeries {(N₁, N₂) | N₁.IsQuotientEquivQuotientPrime N₂}
hs1 : s.head = ⊥
hs2 : s.last = ⊤
h : 0 < s.length + 1
⊢ motive ↥(s.toFun ⟨0, h⟩)

Tactic:
change motive s.head
    rw [hs1]
    exact subsingleton _

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mp
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)ˣ
⊢ (∃ x, spanSingleton R⁰ ↑x = ↑I) → ∃ x, spanSingleton R⁰ x = ↑I

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case mp
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)ˣ
x : Kˣ
hx : spanSingleton R⁰ ↑x = ↑I
⊢ ∃ x, spanSingleton R⁰ x = ↑I
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mpr
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)ˣ
⊢ (∃ x, spanSingleton R⁰ x = ↑I) → ∃ x, spanSingleton R⁰ ↑x = ↑I

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case mpr
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)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mpr
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
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ x = ↑I) →
    ∃ x,
      (∃ x_1, spanSingleton R⁰ x_1 = ↑x) ∧
        (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom x = I

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case mpr
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
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ ∃ x,
    (∃ x_1, spanSingleton R⁰ x_1 = ↑x) ∧
      (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom x = I
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ mk0 ⟨integralRep ↑I, ⋯⟩ = (mk (FractionRing R)) I

Tactic:
← ClassGroup.mk_mk0 (FractionRing R),

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ (mk (FractionRing R)) ((FractionalIdeal.mk0 (FractionRing R)) ⟨integralRep ↑I, ⋯⟩) = (mk (FractionRing R)) I