mathlib-initiative/mathlib-tactics huggingface dataset:
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:
Generators.ker_eq_ker_aeval_val,

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.span (Set.range (⇑(rename ⇑e.symm) ∘ P.relation ∘ ⇑f)) = RingHom.ker (aeval (P.reindex e).val)
Module: Mathlib.Algebra.Module.Presentation.DirectSum

Goal state before:
pp: A : Type u
inst✝⁷ : Ring A
ι : Type w
inst✝⁶ : DecidableEq ι
relations : ι → Relations A
M : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (M i)
inst✝⁴ : (i : ι) → Module A (M i)
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
solution : (i : ι) → (relations i).Solution (M i)
h : ∀ (i : ι), (solution i).IsPresentation
N✝ : Type w'
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
f✝ f'✝ : (⨁ (i : ι), M i) →ₗ[A] N✝
h' : (directSum solution).postcomp f✝ = (directSum solution).postcomp f'✝
⊢ f✝ = f'✝

Tactic:
ext i : 1

Goal state after:
A : Type u
inst✝⁷ : Ring A
ι : Type w
inst✝⁶ : DecidableEq ι
relations : ι → Relations A
M : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (M i)
inst✝⁴ : (i : ι) → Module A (M i)
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
solution : (i : ι) → (relations i).Solution (M i)
h : ∀ (i : ι), (solution i).IsPresentation
N✝ : Type w'
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
f✝ f'✝ : (⨁ (i : ι), M i) →ₗ[A] N✝
h' : (directSum solution).postcomp f✝ = (directSum solution).postcomp f'✝
i : ι
⊢ f✝ ∘ₗ lof A ι M i = f'✝ ∘ₗ lof A ι M i
Module: Mathlib.Algebra.Module.Presentation.DirectSum

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
pres : Presentation A N
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq N
i : ι
g : pres.G
⊢ (lof A ι (fun x ↦ N) i) (pres.var g) = (Finsupp.single i (pres.var g)).toDFinsupp

Tactic:
Finsupp.toDFinsupp_single

Goal state after:
A : Type u
inst✝⁴ : Ring A
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
pres : Presentation A N
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq N
i : ι
g : pres.G
⊢ (lof A ι (fun x ↦ N) i) (pres.var g) = DFinsupp.single i (pres.var g)
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 R R'
inst✝ : Algebra S S'
f : P.Hom P'
v : ι →₀ ℕ
r : R
⊢ ((algebraMap R P'.Ring) r * v.prod fun i k ↦ f.val i ^ k) = r • v.prod fun x1 x2 ↦ f.val x1 ^ x2

Tactic:
Algebra.smul_def

Goal state after:
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 R R'
inst✝ : Algebra S S'
f : P.Hom P'
v : ι →₀ ℕ
r : R
⊢ ((algebraMap R P'.Ring) r * v.prod fun i k ↦ f.val i ^ k) =
    (algebraMap R P'.Ring) r * v.prod fun x1 x2 ↦ f.val x1 ^ x2
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case C
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 ι
a : S
⊢ ∃ a_1, (Q.ofComp P).toAlgHom a_1 = C a

Tactic:
use MvPolynomial.rename Sum.inr (P.σ a)
      simp only [Hom.toAlgHom, ofComp, Generators.comp, MvPolynomial.aeval_rename,
        Sum.elim_comp_inr]
      simp_rw [Function.comp_def, ← MvPolynomial.algebraMap_eq, ← IsScalarTower.toAlgHom_apply R,
        ← MvPolynomial.comp_aeval]
      simp

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

Goal state before:
pp: case e'_5
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
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
j : (ι' →₀ ℕ) × (ι →₀ ℕ)
hj : j ∈ {j ∈ Finset.map e.toEmbedding (support x) | j.1 = i}
⊢ (monomial (e.symm j)) (coeff (e.symm j) x) =
    (monomial (e.symm (i, 0))) 1 * (Q.toComp P).toAlgHom.toRingHom ((monomial j.2) (coeff (e.symm j) x))

Tactic:
obtain rfl := (Finset.mem_filter.mp hj).2

Goal state after:
case e'_5
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
j : (ι' →₀ ℕ) × (ι →₀ ℕ)
hi : j.1 ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
hj : j ∈ {j_1 ∈ Finset.map e.toEmbedding (support x) | j_1.1 = j.1}
⊢ (monomial (e.symm j)) (coeff (e.symm j) x) =
    (monomial (e.symm (j.1, 0))) 1 * (Q.toComp P).toAlgHom.toRingHom ((monomial j.2) (coeff (e.symm j) x))
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.comp P).Ring
hx : (Q.ofComp P).toAlgHom x = 0
⊢ x ∈ (Q.comp P).ker

Tactic:
Generators.ker_eq_ker_aeval_val,

Goal state after:
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.comp P).Ring
hx : (Q.ofComp P).toAlgHom x = 0
⊢ x ∈ RingHom.ker (aeval (Q.comp P).val)
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
inst✝ : FinitePresentation R S
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this : FiniteType R P.toExtension.Ring
⊢ P.toExtension.toKaehler.ker.FG

Tactic:
LinearMap.exact_iff.mp P.toExtension.exact_cotangentComplex_toKaehler,

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this : FiniteType R P.toExtension.Ring
⊢ P.toExtension.cotangentComplex.range.FG
Module: Mathlib.RingTheory.QuotSMulTop

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ (map r) f ∘ₗ (r • ⊤).mkQ = (r • ⊤).mkQ ∘ₗ f

Tactic:
by
  ext; rfl

Goal state after:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
replace hx : _ ∈ y' • Submodule.span R (s : Set S') := Set.smul_mem_smul_set hx

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
hx : y' • (algebraMap S S') x ∈ y' • Submodule.span R ↑s
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
⊢ p ∈ support R M ↔ annihilator R M ≤ p.asIdeal

Tactic:
obtain ⟨s, hs⟩ := ‹Module.Finite R M›
  refine ⟨annihilator_le_of_mem_support, fun H ↦ (mem_support_iff_of_span_eq_top hs).mpr ?_⟩
  simp only [SetLike.le_def, Submodule.mem_annihilator_span_singleton] at H ⊢
  contrapose! H
  choose x hx hx' using Subtype.forall'.mp H
  refine ⟨s.attach.prod x, ?_, ?_⟩
  · rw [← Submodule.annihilator_top, ← hs, Submodule.mem_annihilator_span]
    intro m
    obtain ⟨k, hk⟩ := Finset.dvd_prod_of_mem x (Finset.mem_attach _ m)
    rw [hk, mul_comm, mul_smul, hx, smul_zero]
  · exact p.asIdeal.primeCompl.prod_mem (fun x _ ↦ hx' x)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
hσ : Monotone ⇑σ
hσ' : Monotone ⇑(Equiv.symm σ)
⊢ σ = 1

Tactic:
ext i : 1

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
hσ : Monotone ⇑σ
hσ' : Monotone ⇑(Equiv.symm σ)
i : Fin n
⊢ σ i = 1 i
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: case pos
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
⊢ ((Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) t)) t = (ιMultiDual R n b t) (ιMulti_family R n (⇑b) t)

Tactic:
ιMultiDual_apply_diag,

Goal state after:
case pos
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
⊢ ((Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) t)) t = 1
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).repr (ιMulti_family R n (⇑b) s)) t = (Finsupp.single s 1) t

Tactic:
by_cases hst : s = t

Goal state after:
case pos
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
⊢ ((Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) s)) t = (Finsupp.single s 1) t

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
⊢ ((Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) s)) t = (Finsupp.single s 1) t
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
y : R
n : ↥N
⊢ ((Subalgebra.toSubmodule ⊥).mulMap N) ((algebraMap R ↥⊥) y ⊗ₜ[R] n) = y • ↑n

Tactic:
Algebra.smul_def

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
y : R
n : ↥N
⊢ ((Subalgebra.toSubmodule ⊥).mulMap N) ((algebraMap R ↥⊥) y ⊗ₜ[R] n) = (algebraMap R S) y * ↑n
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
m : ↥M
⊢ M.rTensorOne' (m ⊗ₜ[R] 1) = m

Tactic:
simpa using rTensorOne'_tmul 1 m

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
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) := ⋯
this✝² : Finite ι
this✝¹ : Fintype ι := ⋯
i : (ι →₀ R) →ₗ[R] M := ⋯
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.baseChange k i) ((LinearMap.lTensor (R ⧸ 𝔪) i.ker.subtype) x) =
    (LinearMap.baseChange k i) ((LinearMap.lTensor (R ⧸ 𝔪) i.ker.subtype) 0)

Tactic:
rw [LinearMap.baseChange_eq_ltensor]

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 k i) ((LinearMap.lTensor (R ⧸ 𝔪) i.ker.subtype) x) =
    (LinearMap.lTensor k i) ((LinearMap.lTensor (R ⧸ 𝔪) i.ker.subtype) 0)
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: case refine_2.refine_3
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✝ : ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
x : M
hx : (⊥.colon {N₁.mkQ x}).IsPrime
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
this : N₂.submoduleOf N₂ = (N₁ ⊔ A ∙ x).submoduleOf N₂
⊢ map (N₁.submoduleOf N₂).mkQ (toSpanSingleton A ↥N₂ ⟨x, hxN₂⟩).range = ⊤

Tactic:
submoduleOf_self,

Goal state after:
case refine_2.refine_3
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✝ : ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
x : M
hx : (⊥.colon {N₁.mkQ x}).IsPrime
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
this : ⊤ = (N₁ ⊔ A ∙ x).submoduleOf N₂
⊢ map (N₁.submoduleOf N₂).mkQ (toSpanSingleton A ↥N₂ ⟨x, hxN₂⟩).range = ⊤
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝¹ : CommRing A
inst✝ : IsNoetherianRing A
I : Ideal A
h : Disjoint ↑I ↑(nonZeroDivisors A)
x : A
hP : I ≤ ⊥.colon {x}
prime : (⊥.colon {x}).IsPrime
⊢ ∀ n ∈ I, x • n = 0

Tactic:
simpa only [smul_eq_mul, mul_comm x, SetLike.le_def, Submodule.mem_colon_singleton] using! hP

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

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
⊢ (∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = J) →
    ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'

Tactic:
rintro ⟨x, rfl⟩
    rw [Units.val_mul, hI, coe_toPrincipalIdeal, mul_comm,
      spanSingleton_mul_coeIdeal_eq_coeIdeal] at hJ
    exact ⟨_, _, sec_fst_ne_zero x.ne_zero,
      sec_snd_ne_zero (R := R) le_rfl (x : FractionRing R), hJ⟩

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: case mpr.h
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f)).range
g : N →ₗ[R] M
s : ↥I.primeCompl
x✝ : N
⊢ (↑R ((LocalizedModule.map I.primeCompl) (f ∘ₗ g)) ∘ₗ LocalizedModule.mkLinearMap I.primeCompl N) x✝ =
    (↑R
          (((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
                (LocalizedModule I.primeCompl N))
              ((LocalizedModule.map I.primeCompl) f))
            ((LocalizedModule.map I.primeCompl) g)) ∘ₗ
        LocalizedModule.mkLinearMap I.primeCompl N)
      x✝

Tactic:
simp only [coe_comp, coe_restrictScalars, Function.comp_apply,
        LocalizedModule.mkLinearMap_apply, LocalizedModule.map_mk, llcomp_apply]

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✝ : IsPrincipalIdealRing R
⊢ ∀ (x : ClassGroup R), x ∈ {1}

Tactic:
by
    refine ClassGroup.induction (R := R) (FractionRing R) (fun I => ?_)
    rw [Finset.mem_singleton]
    exact ClassGroup.mk_eq_one_iff.mpr (I : FractionalIdeal R⁰ (FractionRing R)).isPrincipal

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
g : Y → Z
s : Set Z
⊢ IsOpen[inst✝] (g ∘ f ⁻¹' s)

Tactic:
rw [Set.preimage_comp]
  exact hf _

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
hfs : Function.Surjective f.toFun
⊢ Function.Injective (comap f)

Tactic:
by
  intro a b h
  ext y
  obtain ⟨x, hx⟩ := hfs y
  simpa [← hx] using LocallyConstant.congr_fun h x

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S✝
inst✝⁶ : Algebra R S✝
S : Submonoid R
ι : Type u_3
inst✝⁵ : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → AddCommMonoid (M' i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → Module R (M' i)
f : (i : ι) → M i →ₗ[R] M' i
inst✝ : ∀ (i : ι), IsLocalizedModule S (f i)
⊢ IsLocalizedModule S (LinearMap.pi fun i ↦ f i ∘ₗ LinearMap.proj i)

Tactic:
by
  let (i : ι) : Module (Localization S) (M' i) := IsLocalizedModule.module S (f i)
  rw [isLocalizedModule_iff_isBaseChange S (Localization S)]
  apply IsBaseChange.pi
  intro i
  rw [← isLocalizedModule_iff_isBaseChange S]
  infer_instance

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this✝ : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : p ∈ freeLocus R M
hp : ⟨p, hp''⟩ ∈ Subtype.val ⁻¹' ↑(basicOpen f)
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
⊢ rankAtStalk M ↑⟨p, hp''⟩ = rankAtStalk M ↑⟨x, hx⟩

Tactic:
have : IsScalarTower R (Localization.Away f) Rₚ :=
    IsLocalization.localization_isScalarTower_of_submonoid_le ..

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this✝¹ : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : p ∈ freeLocus R M
hp : ⟨p, hp''⟩ ∈ Subtype.val ⁻¹' ↑(basicOpen f)
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this✝ : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
this : IsScalarTower R (Localization.Away f) Rₚ
⊢ rankAtStalk M ↑⟨p, hp''⟩ = rankAtStalk M ↑⟨x, hx⟩