mathlib-initiative/mathlib-tactics huggingface dataset:
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' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹¹ : CommRing R''
inst✝¹⁰ : CommRing S''
inst✝⁹ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra R' R''
inst✝⁶ : Algebra R' S''
inst✝⁵ : Algebra S S'
inst✝⁴ : Algebra S' S''
inst✝³ : Algebra S S''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R' S' S''
inst✝ : IsScalarTower S S' S''
f : P'.Hom P''
g : P.Hom P'
x : ι
⊢ (aeval P''.val) ((aeval f.val) (g.val x)) = (algebraMap S S'') (P.val x)

Tactic:
IsScalarTower.algebraMap_apply S S' S'',

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' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹¹ : CommRing R''
inst✝¹⁰ : CommRing S''
inst✝⁹ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra R' R''
inst✝⁶ : Algebra R' S''
inst✝⁵ : Algebra S S'
inst✝⁴ : Algebra S' S''
inst✝³ : Algebra S S''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R' S' S''
inst✝ : IsScalarTower S S' S''
f : P'.Hom P''
g : P.Hom P'
x : ι
⊢ (aeval P''.val) ((aeval f.val) (g.val x)) = (algebraMap S' S'') ((algebraMap S S') (P.val x))
Module: Mathlib.RingTheory.Extension.Generators

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

Tactic:
| add p q hp hq =>

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

Goal state before:
pp: case mul_X
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 : MvPolynomial ι' S
i : ι'
hp : ∃ a, (Q.ofComp P).toAlgHom a = p
⊢ ∃ a, (Q.ofComp P).toAlgHom a = p * X i

Tactic:
obtain ⟨(p : MvPolynomial (ι' ⊕ ι) R), rfl⟩ := hp

Goal state after:
case mul_X
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 ι
i : ι'
p : MvPolynomial (ι' ⊕ ι) R
⊢ ∃ a, (Q.ofComp P).toAlgHom a = (Q.ofComp P).toAlgHom p * X i
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case a.convert_4.monomial
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 (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
v : ι' ⊕ ι →₀ ℕ
a : R
⊢ (∑ᶠ (i_1 : (ι' →₀ ℕ) × (ι →₀ ℕ)),
      if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) ((monomial v) a))) else 0) =
    coeff i ((Q.ofComp P).toAlgHom ((monomial v) a))

Tactic:
rw [finsum_eq_sum_of_support_subset _ (this _), ← Finset.sum_filter]

Goal state after:
case a.convert_4.monomial
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 (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
v : ι' ⊕ ι →₀ ℕ
a : R
⊢ ∑ a_1 ∈ Finset.map (↑e).toEmbedding ((monomial v) a).support with a_1.1 = i,
      (aeval P.val) ((monomial a_1.2) (coeff (e.symm a_1) ((monomial v) a))) =
    coeff i ((Q.ofComp P).toAlgHom ((monomial v) a))
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
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
⊢ ∃ k a y, x = y ∘ₗ a ∧ a f = 0

Tactic:
let f' : Fin l → R := f

Goal state after:
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 := ⇑f
⊢ ∃ k a y, x = y ∘ₗ a ∧ a f = 0
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case a.convert_4.add
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 (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
p q : MvPolynomial (ι' ⊕ ι) R
hp :
  (∑ᶠ (i_1 : (ι' →₀ ℕ) × (ι →₀ ℕ)), if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) p)) else 0) =
    coeff i ((Q.ofComp P).toAlgHom p)
hq :
  (∑ᶠ (i_1 : (ι' →₀ ℕ) × (ι →₀ ℕ)), if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) q)) else 0) =
    coeff i ((Q.ofComp P).toAlgHom q)
⊢ (∑ᶠ (i_1 : (ι' →₀ ℕ) × (ι →₀ ℕ)),
      if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) (p + q))) else 0) =
    coeff i ((Q.ofComp P).toAlgHom (p + q))

Tactic:
| add p q hp hq =>

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

Goal state before:
pp: case mpr
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.Ring
⊢ x ∈ Q.ker → ∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x

Tactic:
· intro hx
    exact ⟨_, (kerCompPreimage Q P ⟨x, hx⟩).2, ofComp_kerCompPreimage Q P ⟨x, hx⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : Subsingleton (LocalizedModule p.primeCompl M)
this : { asIdeal := p, isPrime := ⋯ } ∈ ⋃ i ∈ ↑(Module.annihilator R M), (zeroLocus {i})ᶜ
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)

Tactic:
Set.mem_iUnion₂

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 : Ideal R
inst✝¹ : p.IsPrime
inst✝ : Subsingleton (LocalizedModule p.primeCompl M)
this : ∃ i, ∃ (_ : i ∈ ↑(Module.annihilator R M)), { asIdeal := p, isPrime := ⋯ } ∈ (zeroLocus {i})ᶜ
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsLocalRing R
fg : N.FG
this : Module.Finite R ↥N := Module.Finite.iff_fg.mpr fg
s : Set (𝓀 ⊗[R] ↥N)
hs₁ : Cardinal.mk ↑s = ⊤.spanRank
hs₂ : span 𝓀 s = ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
ht₁ : ⇑((mk R 𝓀 ↥N) 1) '' t = s
⊢ span R t = ⊤

Tactic:
rwa [← restrictScalars_eq_top_iff R, restrictScalars_span _ _ (by exact residue_surjective),
      ← ht₁, ← map_span, map_tensorProduct_mk_eq_top] at hs₂

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
⊢ ((pairingDual R M n) ((ιMulti R n) (f ∘ ⇑a))) ((ιMulti R n) (x ∘ ⇑b)) = 0

Tactic:
simp only [pairingDual_ιMulti_ιMulti, Function.comp_apply, Matrix.det_apply]

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.sign σ • ∏ i, Matrix.of (fun i j ↦ (f (a j)) (x (b i))) (σ i) i = 0
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 : ↑(powersetCard I n)
this : (Matrix.of fun i j ↦ (b.coord ((ofFinEmbEquiv.symm s) j)) (b ((ofFinEmbEquiv.symm s) i))) = 1
⊢ (Matrix.of fun i j ↦ (b.coord ((ofFinEmbEquiv.symm s) j)) (b ((ofFinEmbEquiv.symm s) i))).det = 1

Tactic:
this,

Goal state after:
R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
this : (Matrix.of fun i j ↦ (b.coord ((ofFinEmbEquiv.symm s) j)) (b ((ofFinEmbEquiv.symm s) i))) = 1
⊢ Matrix.det 1 = 1
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case mp
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
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
hf : Surjective ⇑f
hN : Submodule.map f (Submodule.map ((TensorProduct.mk R k M) 1) N) = Submodule.map f ⊤
⊢ N = ⊤

Tactic:
← Submodule.map_comp,

Goal state after:
case mp
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
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
hf : Surjective ⇑f
hN : Submodule.map (f ∘ₗ (TensorProduct.mk R k M) 1) N = Submodule.map f ⊤
⊢ N = ⊤
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case mp
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
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
hf : Surjective ⇑f
hN : Submodule.map (f ∘ₗ (TensorProduct.mk R k M) 1) N = Submodule.map f ⊤
⊢ N = ⊤

Tactic:
this,

Goal state after:
case mp
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
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
hf : Surjective ⇑f
hN : Submodule.map (𝔪 • ⊤).mkQ N = Submodule.map f ⊤
⊢ N = ⊤
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₁)
x : M₂ ⊗[R] N₁
hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0
this : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) x) = 0
y : M₁ ⊗[R] N₂
hy : (LinearMap.rTensor N₂ f₁) y = (LinearMap.lTensor M₂ g₁) x
⊢ (LinearMap.lTensor M₂ g₂) ((LinearMap.lTensor M₂ g₁) x) = (LinearMap.rTensor N₃ f₁) 0

Tactic:
rw [← LinearMap.comp_apply, ← LinearMap.lTensor_comp, hgexact.linearMap_comp_eq_zero]

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₁
hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0
this : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) x) = 0
y : M₁ ⊗[R] N₂
hy : (LinearMap.rTensor N₂ f₁) y = (LinearMap.lTensor M₂ g₁) x
⊢ (LinearMap.lTensor M₂ 0) x = (LinearMap.rTensor N₃ f₁) 0
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I✝ : Ideal R
hI✝¹ : ¬I✝.minimalPrimes.Finite
I : Ideal R
hI✝ : ¬I.minimalPrimes.Finite
hmax : ∀ (I_1 : Submodule R R), I < I_1 → (Ideal.minimalPrimes I_1).Finite
h1 : ¬I.IsPrime
h2 : I ≠ ⊤
x : R
hx : I < I ⊔ span {x}
y : R
hy : I < I ⊔ span {y}
h : x * y ∈ I
p : Ideal R
x✝ : p ∈ I.minimalPrimes
hp : p.IsPrime
hI : I ≤ p
hmin : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hxp : x ∈ p
⊢ p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes

pp: case inr
R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I✝ : Ideal R
hI✝¹ : ¬I✝.minimalPrimes.Finite
I : Ideal R
hI✝ : ¬I.minimalPrimes.Finite
hmax : ∀ (I_1 : Submodule R R), I < I_1 → (Ideal.minimalPrimes I_1).Finite
h1 : ¬I.IsPrime
h2 : I ≠ ⊤
x : R
hx : I < I ⊔ span {x}
y : R
hy : I < I ⊔ span {y}
h : x * y ∈ I
p : Ideal R
x✝ : p ∈ I.minimalPrimes
hp : p.IsPrime
hI : I ≤ p
hmin : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hyp : y ∈ p
⊢ p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes

Tactic:
· exact Or.inl ⟨⟨hp, sup_le hI (p.span_singleton_le_iff_mem.mpr hxp)⟩,
      fun q hq hqp ↦ hmin ⟨hq.1, hx.le.trans hq.2⟩ hqp⟩

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I✝ : Ideal R
hI✝¹ : ¬I✝.minimalPrimes.Finite
I : Ideal R
hI✝ : ¬I.minimalPrimes.Finite
hmax : ∀ (I_1 : Submodule R R), I < I_1 → (Ideal.minimalPrimes I_1).Finite
h1 : ¬I.IsPrime
h2 : I ≠ ⊤
x : R
hx : I < I ⊔ span {x}
y : R
hy : I < I ⊔ span {y}
h : x * y ∈ I
p : Ideal R
x✝ : p ∈ I.minimalPrimes
hp : p.IsPrime
hI : I ≤ p
hmin : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hyp : y ∈ p
⊢ p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes
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
inst✝¹ : IsNoetherianRing A
inst✝ : Module.Finite A M
N : Submodule A M
hN : N ≠ ⊤
s : RelSeries {(N₁, N₂) | N₁.IsQuotientEquivQuotientPrime N₂}
hs₁ : s.head = ⊥
hs₂ : s.last = N
this✝ : Nontrivial (M ⧸ N)
x : M
hp : (⊥.colon {N.mkQ x}).IsPrime
hxN : x ∉ N
this : N.IsQuotientEquivQuotientPrime (N ⊔ A ∙ x)
⊢ (s.snoc (s.last ⊔ A ∙ x) ⋯).last > N

Tactic:
simpa [hs₂]

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 : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤) → ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}

Tactic:
rintro ⟨x, y, hx, hy, h⟩
    rw [Ideal.mul_top] at h
    rcases Ideal.mem_span_singleton_mul.mp ((Ideal.span_singleton_le_iff_mem _).mp h.ge) with
      ⟨i, _hi, rfl⟩
    rw [← Ideal.span_singleton_mul_span_singleton, Ideal.span_singleton_mul_right_inj hx] at h
    exact ⟨i, by grobner, h⟩

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

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : Ideal R
hI : Submodule.IsPrincipal (I ^ n)
hI0 : I = 0
⊢ Submodule.IsPrincipal I

Tactic:
simp [hI0, bot_isPrincipal]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ (∃ a, ↑(I * J) = R ∙ a) ↔ ∃ x, x ≠ 0 ∧ ↑I * ↑J = Ideal.span {x}

Tactic:
Submonoid.coe_mul

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ (∃ a, ↑I * ↑J = R ∙ a) ↔ ∃ x, x ≠ 0 ∧ ↑I * ↑J = Ideal.span {x}
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x✝ : ∃ a, ↑I * ↑J = R ∙ a
a : R
ha : ↑I * ↑J = R ∙ a
this : a = 0
⊢ False

Tactic:
this,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x✝ : ∃ a, ↑I * ↑J = R ∙ a
a : R
ha : ↑I * ↑J = R ∙ 0
this : a = 0
⊢ False
Module: Mathlib.RingTheory.Localization.Free

Goal state before:
pp: case refine_2
R : Type u_4
M : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁹ : AddCommGroup M'
inst✝⁸ : Module R M'
f : M →ₗ[R] M'
inst✝⁷ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁶ : CommRing Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : IsScalarTower R Rₛ M'
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
I : Type u_6
inst✝ : Finite I
b : Basis I Rₛ M'
this✝ : FinitePresentation R (I →₀ R)
r : R
hr : r ∈ S
e : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r (I →₀ R)
e' : LocalizedModule (Submonoid.powers r) (I →₀ R) ≃ₗ[R] I →₀ Localization (Submonoid.powers r) :=
  IsLocalizedModule.iso (Submonoid.powers r)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (Submonoid.powers r))))
i : I
this : e'.symm (Finsupp.single i 1) = LocalizedModule.mk (Finsupp.single i 1) 1
he :
  (LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯)
      (e'.symm (Finsupp.single i 1)) =
    b.repr ((LocalizedModule.lift (Submonoid.powers r) f ⋯) (e.symm (e'.symm (Finsupp.single i 1))))
⊢ (LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯)
      (e'.symm (Finsupp.single i 1)) =
    Finsupp.single i 1

Tactic:
this,

Goal state after:
case refine_2
R : Type u_4
M : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁹ : AddCommGroup M'
inst✝⁸ : Module R M'
f : M →ₗ[R] M'
inst✝⁷ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁶ : CommRing Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : IsScalarTower R Rₛ M'
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
I : Type u_6
inst✝ : Finite I
b : Basis I Rₛ M'
this✝ : FinitePresentation R (I →₀ R)
r : R
hr : r ∈ S
e : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r (I →₀ R)
e' : LocalizedModule (Submonoid.powers r) (I →₀ R) ≃ₗ[R] I →₀ Localization (Submonoid.powers r) :=
  IsLocalizedModule.iso (Submonoid.powers r)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (Submonoid.powers r))))
i : I
this : e'.symm (Finsupp.single i 1) = LocalizedModule.mk (Finsupp.single i 1) 1
he :
  (LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯)
      (e'.symm (Finsupp.single i 1)) =
    b.repr ((LocalizedModule.lift (Submonoid.powers r) f ⋯) (e.symm (e'.symm (Finsupp.single i 1))))
⊢ (LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯)
      (LocalizedModule.mk (Finsupp.single i 1) 1) =
    Finsupp.single i 1