mathlib-initiative/mathlib-tactics huggingface dataset:
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
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((TensorProduct.mk R k M) 1) N = ⊤
this✝¹ : Module k (M ⧸ 𝔪 • ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this✝ : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := map_tensorProduct_mk_eq_top._proof_1_9
f : k ⊗[R] M →ₗ[R] M ⧸ 𝔪 • ⊤ :=
  AlgebraTensorModule.lift (↑R ((LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ 𝔪 • ⊤)).symm (𝔪 • ⊤).mkQ))
this : f ∘ₗ (TensorProduct.mk R k M) 1 = (𝔪 • ⊤).mkQ
⊢ Surjective ⇑f

Tactic:
intro x

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((TensorProduct.mk R k M) 1) N = ⊤
this✝¹ : Module k (M ⧸ 𝔪 • ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this✝ : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := map_tensorProduct_mk_eq_top._proof_1_9
f : k ⊗[R] M →ₗ[R] M ⧸ 𝔪 • ⊤ :=
  AlgebraTensorModule.lift (↑R ((LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ 𝔪 • ⊤)).symm (𝔪 • ⊤).mkQ))
this : f ∘ₗ (TensorProduct.mk R k M) 1 = (𝔪 • ⊤).mkQ
x : M ⧸ 𝔪 • ⊤
⊢ ∃ a, f a = x
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)
⊢ ∀ (a : M₃ ⊗[R] N₁), (LinearMap.lTensor M₃ g₁) a = 0 → a = 0

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)
x : M₃ ⊗[R] N₁
⊢ (LinearMap.lTensor M₃ g₁) x = 0 → x = 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✝¹ : 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)
⊢ ∀ (y : k ⊗[R] ↥i.ker), y = 0

Tactic:
intro x

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
this : Surjective ⇑(LinearMap.baseChange k i)
hi' : Function.Bijective ⇑(LinearMap.baseChange k i)
x : k ⊗[R] ↥i.ker
⊢ x = 0
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) := ⋯
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
⊢ Function.Injective ⇑i.ker.subtype

Tactic:
exact Subtype.val_injective

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
a b : GradedMonoid fun n ↦ ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : (cast R M h) a.snd = b.snd
⊢ (reindex R (fun x ↦ M) (Equiv.cast ⋯)) a.snd = b.snd

Tactic:
rw [cast] at h2

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n ↦ ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : (reindex R (fun x ↦ M) (finCongr h)) a.snd = b.snd
⊢ (reindex R (fun x ↦ M) (Equiv.cast ⋯)) a.snd = b.snd
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 GradedMonoid.GOne.one a) = a

Tactic:
by
  rw [gMul_def, gOne_def]
  induction a using PiTensorProduct.induction_on with
  | smul_tprod r a =>
    rw [TensorProduct.tmul_smul, map_smul, map_smul, ← gMul_def, tprod_mul_tprod, cast_tprod]
    congr 2 with i
    rw [Fin.elim0_append]
    refine congr_arg a (Fin.ext ?_)
    simp
  | add x y hx hy =>
    rw [TensorProduct.tmul_add, map_add, map_add, hx, hy]

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
tprodCoeff : ∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R r f)
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
h₁ : motive (PiTensorProduct.tprodCoeff R 0 0)
⊢ motive 0

Tactic:
rwa [zero_tprodCoeff] at h₁

Goal state after:
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✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ 1 • tprodCoeff R r f = tprodCoeff R r f

Tactic:
rw [smul_tprodCoeff', one_smul]

Goal state after:
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✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
x z y : ⨂[R] (i : ι), s i
ihz : 1 • z = z
ihy : 1 • y = y
⊢ 1 • z + 1 • y = z + y

Tactic:
ihz,

Goal state after:
ι : 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✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
x z y : ⨂[R] (i : ι), s i
ihz : 1 • z = z
ihy : 1 • y = y
⊢ z + 1 • y = z + y
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✝⁶ : Monoid R₁
inst✝⁵ : DistribMulAction R₁ R
inst✝⁴ : SMulCommClass R₁ R R
inst✝³ : Monoid R₂
inst✝² : DistribMulAction R₂ R
inst✝¹ : SMulCommClass R₂ R R
inst✝ : SMulCommClass R₁ R₂ R
r' : R₁
r'' : R₂
x z y : ⨂[R] (i : ι), s i
ihz : r' • r'' • z = r'' • r' • z
ihy : r' • r'' • y = r'' • r' • y
⊢ r' • r'' • z + r' • r'' • y = r'' • r' • z + r'' • r' • y

Tactic:
ihz,

Goal state after:
ι : 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✝⁶ : Monoid R₁
inst✝⁵ : DistribMulAction R₁ R
inst✝⁴ : SMulCommClass R₁ R R
inst✝³ : Monoid R₂
inst✝² : DistribMulAction R₂ R
inst✝¹ : SMulCommClass R₂ R R
inst✝ : SMulCommClass R₁ R₂ R
r' : R₁
r'' : R₂
x z y : ⨂[R] (i : ι), s i
ihz : r' • r'' • z = r'' • r' • z
ihy : r' • r'' • y = r'' • r' • y
⊢ r'' • r' • z + r' • r'' • y = r'' • r' • z + r'' • r' • y
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✝⁷ : Monoid R₁
inst✝⁶ : DistribMulAction R₁ R
inst✝⁵ : SMulCommClass R₁ R R
inst✝⁴ : Monoid R₂
inst✝³ : DistribMulAction R₂ R
inst✝² : SMulCommClass R₂ R R
inst✝¹ : SMul R₁ R₂
inst✝ : IsScalarTower R₁ R₂ R
r' : R₁
r'' : R₂
x z y : ⨂[R] (i : ι), s i
ihz : (r' • r'') • z = r' • r'' • z
ihy : (r' • r'') • y = r' • r'' • y
⊢ (r' • r'') • z + (r' • r'') • y = r' • r'' • z + r' • r'' • y

Tactic:
ihz,

Goal state after:
ι : 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✝⁷ : Monoid R₁
inst✝⁶ : DistribMulAction R₁ R
inst✝⁵ : SMulCommClass R₁ R R
inst✝⁴ : Monoid R₂
inst✝³ : DistribMulAction R₂ R
inst✝² : SMulCommClass R₂ R R
inst✝¹ : SMul R₁ R₂
inst✝ : IsScalarTower R₁ R₂ R
r' : R₁
r'' : R₂
x z y : ⨂[R] (i : ι), s i
ihz : (r' • r'') • z = r' • r'' • z
ihy : (r' • r'') • y = r' • r'' • y
⊢ r' • r'' • z + (r' • r'') • y = r' • r'' • z + r' • r'' • y
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: case refine_2
ι : 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)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ : MultilinearMap R s E
r : R
x z y : ⨂[R] (i : ι), s i
ihz : (liftAux φ) (r • z) = r • (liftAux φ) z
ihy : (liftAux φ) (r • y) = r • (liftAux φ) y
⊢ (liftAux φ) (r • z) + (liftAux φ) (r • y) = r • (liftAux φ) (z + y)

Tactic:
ihz,

Goal state after:
case refine_2
ι : 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)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ : MultilinearMap R s E
r : R
x z y : ⨂[R] (i : ι), s i
ihz : (liftAux φ) (r • z) = r • (liftAux φ) z
ihy : (liftAux φ) (r • y) = r • (liftAux φ) y
⊢ r • (liftAux φ) z + (liftAux φ) (r • y) = r • (liftAux φ) (z + y)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Colon

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
n : ℕ
hn0 : n ≠ 0
h : ann.minimalPrimes.Finite
hn : I ^ n * (h.toFinset.erase I).inf id ^ n ≤ ann
⊢ ¬(h.toFinset.erase I).inf id ^ n ≤ I

Tactic:
have (K : Ideal R) (hKI : K ≤ I) (hK : K ∈ ann.minimalPrimes) : K = I :=
      le_antisymm hKI (hI.2 hK.1 hKI)

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
n : ℕ
hn0 : n ≠ 0
h : ann.minimalPrimes.Finite
hn : I ^ n * (h.toFinset.erase I).inf id ^ n ≤ ann
this : ∀ K ≤ I, K ∈ ann.minimalPrimes → K = I
⊢ ¬(h.toFinset.erase I).inf id ^ n ≤ I
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: case refine_1
ι : 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
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
inst✝ : IsEmpty ι
x : ⨂[R] (i : ι), s i
⊢ ∀ (r : R) (f : (i : ι) → s i),
    (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) (r • (tprod R) f)) = r • (tprod R) f

Tactic:
intro x

Goal state after:
case refine_1
ι : 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
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
inst✝ : IsEmpty ι
x✝ : ⨂[R] (i : ι), s i
x : R
⊢ ∀ (f : (i : ι) → s i),
    (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) (x • (tprod R) f)) = x • (tprod R) f
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: case refine_2
ι : 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
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
inst✝ : IsEmpty ι
x : ⨂[R] (i : ι), s i
⊢ ∀ (x y : ⨂[R] (i : ι), s i),
    (lift (constOfIsEmpty R s 1)) x • (tprod R) isEmptyElim = x →
      (lift (constOfIsEmpty R s 1)) y • (tprod R) isEmptyElim = y →
        (lift (constOfIsEmpty R s 1)) (x + y) • (tprod R) isEmptyElim = x + y

Tactic:
intro x

Goal state after:
case refine_2
ι : 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
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
inst✝ : IsEmpty ι
x✝ x : ⨂[R] (i : ι), s i
⊢ ∀ (y : ⨂[R] (i : ι), s i),
    (lift (constOfIsEmpty R s 1)) x • (tprod R) isEmptyElim = x →
      (lift (constOfIsEmpty R s 1)) y • (tprod R) isEmptyElim = y →
        (lift (constOfIsEmpty R s 1)) (x + y) • (tprod R) isEmptyElim = x + y
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsNoetherianRing R
⊢ {r | ∃ x, x ≠ 0 ∧ r • x = 0} = (↑(nonZeroDivisors R))ᶜ

Tactic:
by
    ext; simp [← nonZeroDivisorsLeft_eq_nonZeroDivisors, and_comm]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
I : Ideal R
hI : ↑I * (↑I)⁻¹ = 1
a : R
K : Ideal R
ha0 : a ≠ 0
ha0' :
  spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * (spanSingleton R⁰ ((algebraMap R (FractionRing R)) a))⁻¹ = 1
h :
  spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * ↑I *
      (spanSingleton R⁰ ((algebraMap R (FractionRing R)) a)⁻¹ * ↑K) =
    spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * ↑I * (↑I)⁻¹
⊢ ↑I * ↑K = spanSingleton R⁰ ((algebraMap R (FractionRing R)) a)

Tactic:
mul_mul_mul_comm,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
I : Ideal R
hI : ↑I * (↑I)⁻¹ = 1
a : R
K : Ideal R
ha0 : a ≠ 0
ha0' :
  spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * (spanSingleton R⁰ ((algebraMap R (FractionRing R)) a))⁻¹ = 1
h :
  spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * spanSingleton R⁰ ((algebraMap R (FractionRing R)) a)⁻¹ *
      (↑I * ↑K) =
    spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * ↑I * (↑I)⁻¹
⊢ ↑I * ↑K = spanSingleton R⁰ ((algebraMap R (FractionRing R)) a)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
⊢ ∀ (y : ClassGroup R), y = 1

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
x : ClassGroup R
⊢ x = 1
Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
⊢ p₁ ≤ p₂

Tactic:
intro x

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
⊢ x ∈ p₁.asIdeal → x ∈ p₂.asIdeal
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: case mpr
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
⊢ ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f))
      (IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) g s) ∈
    Submodule.localized₀ I.primeCompl (LocalizedModule.map I.primeCompl) ((llcomp R N M N) f).range

Tactic:
refine ⟨f.comp g, ⟨g, rfl⟩, s, ?_⟩

Goal state after:
case mpr
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
⊢ IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) (f ∘ₗ g) s =
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f))
      (IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) g s)
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case refine_2
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)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = R ∙ x
hx' : ↑I = spanSingleton R⁰ x
⊢ spanSingleton R⁰ ↑(Units.mk0 x ⋯) = ↑I

Tactic:
simp [hx']

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

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max u_1 uM) := ↥s →₀ R
f : N →ₗ[R] M := Finsupp.linearCombination R Subtype.val
⊢ f.range = ⊤

Tactic:
Finsupp.range_linearCombination,

Goal state after:
R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max u_1 uM) := ↥s →₀ R
f : N →ₗ[R] M := Finsupp.linearCombination R Subtype.val
⊢ Submodule.span R (Set.range Subtype.val) = ⊤