mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case e'_2.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 ι
j : ι →₀ ℕ
a : R
⊢ (Q.toComp P).toAlgHom = rename ?convert_5

Tactic:
ext f (i₁ | i₂)

Goal state after:
case e'_2.e'_5.mk
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 ι
j : ι →₀ ℕ
a : R
f : ι
toFun✝ : ι' ⊕ ι → ℕ
val✝ : Multiset (ι' ⊕ ι)
i₁ : List (ι' ⊕ ι)
nodup✝ : Multiset.Nodup (Quot.mk (⇑(List.isSetoid (ι' ⊕ ι))) i₁)
mem_support_toFun✝ :
  ∀ (a : ι' ⊕ ι), a ∈ { val := Quot.mk (⇑(List.isSetoid (ι' ⊕ ι))) i₁, nodup := nodup✝ } ↔ toFun✝ a ≠ 0
⊢ coeff
      { support := { val := Quot.mk (⇑(List.isSetoid (ι' ⊕ ι))) i₁, nodup := nodup✝ }, toFun := toFun✝,
        mem_support_toFun := mem_support_toFun✝ }
      ((Q.toComp P).toAlgHom (X f)) =
    coeff
      { support := { val := Quot.mk (⇑(List.isSetoid (ι' ⊕ ι))) i₁, nodup := nodup✝ }, toFun := toFun✝,
        mem_support_toFun := mem_support_toFun✝ }
      ((rename ?convert_5) (X f))
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case e'_3
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 ι
j : ι →₀ ℕ
a : R
⊢ Finsupp.sumElim 0 = Finsupp.mapDomain Sum.inr

Tactic:
ext f (i₁ | i₂)

Goal state after:
case e'_3.inl
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 ι
j : ι →₀ ℕ
a : R
f : ι →₀ ℕ
i₁ : ι'
⊢ (Finsupp.sumElim 0 f) (Sum.inl i₁) = (Finsupp.mapDomain Sum.inr f) (Sum.inl i₁)

case e'_3.inr
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 ι
j : ι →₀ ℕ
a : R
f : ι →₀ ℕ
i₂ : ι
⊢ (Finsupp.sumElim 0 f) (Sum.inr i₂) = (Finsupp.mapDomain Sum.inr f) (Sum.inr i₂)
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)

Goal state after:
case h
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
⊢ (Q.ofComp P).toAlgHom ((rename Sum.inr) (P.σ a)) = C a
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 ι
⊢ P.ker = RingHom.ker (aeval P.val)

Tactic:
simp only [ker, Extension.ker, toExtension_Ring, algebraMap_eq]
  rfl

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

Goal state before:
pp: case a.convert_4
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
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))
⊢ (∑ᶠ (i_1 : (ι' →₀ ℕ) × (ι →₀ ℕ)), if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) x)) else 0) =
    coeff i ((Q.ofComp P).toAlgHom x)

Tactic:
induction x using MvPolynomial.induction_on' with
      | monomial v a =>
        rw [finsum_eq_sum_of_support_subset _ (this _), ← Finset.sum_filter]
        obtain ⟨v, rfl⟩ := e.symm.surjective v
        -- Rewrite `e` in the right-hand side only.
        conv_rhs => simp only [e, Finsupp.sumFinsuppAddEquivProdFinsupp,
          Finsupp.sumFinsuppEquivProdFinsupp, AddEquiv.symm_mk, AddEquiv.coe_mk,
          Equiv.coe_fn_symm_mk, ofComp_toAlgHom_monomial_sumElim]
        classical
        simp only [coeff_monomial, ← e.injective.eq_iff,
          map_zero, AddEquiv.apply_symm_apply, apply_ite]
        rw [← apply_ite, Finset.sum_ite_eq]
        simp only [Finset.mem_filter, Finset.mem_map_equiv, AddEquiv.coe_toEquiv_symm,
          mem_support_iff, coeff_monomial, ↓reduceIte, ne_eq, ite_and, ite_not]
        split
        · simp only [*, map_zero, ite_self]
        · congr
      | add p q hp hq =>
        simp only [coeff_add, map_add, ite_add_zero]
        rw [finsum_add_distrib, hp, hq]
        · refine (((support p).map e).finite_toSet.subset ?_)
          convert! this p
        · refine (((support q).map e).finite_toSet.subset ?_)
          convert! this q

Goal state after:
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin n
⊢ Even k ↔ Odd n ∨ Even ↑k

Tactic:
refine ⟨fun hk ↦ ?_, or_imp.mpr ⟨(even_of_odd · k), even_of_val⟩⟩
  rw [← Nat.not_even_iff_odd, ← imp_iff_not_or]
  exact fun hn ↦ (even_iff_of_even hn).mp hk

Goal state after:
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 R s = ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
ht₁ : ⇑((mk R 𝓀 ↥N) 1) '' t = s
⊢ span R t = ⊤

Tactic:
← ht₁,

Goal state after:
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₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
hs₂ : span R (⇑((mk R 𝓀 ↥N) 1) '' t) = ⊤
ht₁ : ⇑((mk R 𝓀 ↥N) 1) '' t = s
⊢ span R t = ⊤
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
⊢ v i = v j → i ≠ j → (∑ p, (-1) ^ ↑p • LinearMap.uncurryMid p (toMultilinearMapLM ∘ₗ f)).toFun v = 0

Tactic:
hvij

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
⊢ i ≠ j → (∑ p, (-1) ^ ↑p • LinearMap.uncurryMid p (toMultilinearMapLM ∘ₗ f)).toFun v = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: case zero
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ 0 ∈ M * N

Tactic:
exact zero_mem _

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hm : (M.mulRightMap n) m = 0
⊢ False

Tactic:
← LinearMap.mem_ker,

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hm : m ∈ (M.mulRightMap n).ker
⊢ False
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hn : (mulLeftMap N m) n = 0
⊢ False

Tactic:
← LinearMap.mem_ker,

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hn : n ∈ (mulLeftMap N m).ker
⊢ False
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
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
inst✝ : IsEmpty ι
x : ⨂[R] (i : ι), s i
⊢ (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) x) = x

Tactic:
refine x.induction_on ?_ ?_
    · intro x y
      simp only [map_smulₛₗ, RingHom.id_apply, lift.tprod, constOfIsEmpty_apply, const_apply,
        smul_eq_mul, mul_one]
      congr
      aesop
    · simp only
      intro x y hx hy
      rw [map_add, add_smul, hx, hy]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this : Free R (N ⧸ l.range)
⊢ Projective R ↥l.range

Tactic:
have := (Exact.split_tfae (LinearMap.exact_subtype_mkQ (LinearMap.range l))
        Subtype.val_injective (Submodule.mkQ_surjective _)).out 0 1

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝ : Free R (N ⧸ l.range)
this : (∃ l_1, l.range.mkQ ∘ₗ l_1 = LinearMap.id) ↔ ∃ l_1, l_1 ∘ₗ l.range.subtype = LinearMap.id
⊢ Projective R ↥l.range
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝¹ : Free R (N ⧸ l.range)
this✝ : Projective R ↥l.range
l' : M →ₗ[R] ↥l.ker
this : Module.Finite R ↥l.ker
hl' : LinearMap.lTensor k (l' ∘ₗ l.ker.subtype) = LinearMap.lTensor k LinearMap.id
⊢ Function.Injective ⇑(LinearMap.lTensor k l.ker.subtype)

Tactic:
LinearMap.lTensor_comp,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝¹ : Free R (N ⧸ l.range)
this✝ : Projective R ↥l.range
l' : M →ₗ[R] ↥l.ker
this : Module.Finite R ↥l.ker
hl' : LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l.ker.subtype = LinearMap.lTensor k LinearMap.id
⊢ Function.Injective ⇑(LinearMap.lTensor k l.ker.subtype)
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
b : R
x✝ : b ∈ (⊥.colon {g x}).radical
n : ℕ
hb : g (b ^ n • x) = 0
⊢ b ∈ p

Tactic:
← LinearMap.mem_ker,

Goal state after:
case neg.refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
b : R
x✝ : b ∈ (⊥.colon {g x}).radical
n : ℕ
hb : b ^ n • x ∈ g.ker
⊢ b ∈ p
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
b : R
x✝ : b ∈ (⊥.colon {g x}).radical
n : ℕ
hb : b ^ n • x ∈ g.ker
⊢ b ∈ p

Tactic:
hfg.linearMap_ker_eq

Goal state after:
case neg.refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
b : R
x✝ : b ∈ (⊥.colon {g x}).radical
n : ℕ
hb : b ^ n • x ∈ f.range
⊢ b ∈ p
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)
b : Fin n → M
hb : ∀ (i : Fin n), (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ i.asIdeal) M) 1) (b i) = fun x ↦ (b' x) i
⊢ Nonempty (Basis (Fin n) R M)

Tactic:
refine ⟨⟨.symm <| .ofBijective (Finsupp.linearCombination R b) <| bijective_of_isLocalized_maximal
    _ (fun P _ ↦ Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization P.primeCompl)))
    _ (fun P _ ↦ TensorProduct.mk R (Localization P.primeCompl) M 1) _ fun P _ ↦ ?_⟩⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)
b : Fin n → M
hb : ∀ (i : Fin n), (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ i.asIdeal) M) 1) (b i) = fun x ↦ (b' x) i
P : Ideal R
x✝ : P.IsMaximal
⊢ Function.Bijective
    ⇑((IsLocalizedModule.map P.primeCompl (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization P.primeCompl)))
          ((TensorProduct.mk R (Localization P.primeCompl) M) 1))
        (Finsupp.linearCombination R b))
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)
b : Fin n → M
hb : ∀ (i : Fin n), (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ i.asIdeal) M) 1) (b i) = fun x ↦ (b' x) i
P : Ideal R
x✝ : P.IsMaximal
⊢ Function.Bijective
    (⇑(AlgebraTensorModule.cancelBaseChange R (Localization P.primeCompl) P.ResidueField
              (IsLocalRing.ResidueField (Localization P.primeCompl)) M).toAddEquiv.toEquiv ∘
      ⇑(Finsupp.linearCombination (IsLocalRing.ResidueField (Localization P.primeCompl))
          (⇑((TensorProduct.mk (Localization P.primeCompl) (IsLocalRing.ResidueField (Localization P.primeCompl))
                  (Localization P.primeCompl ⊗[R] M))
                1) ∘
            ⇑((TensorProduct.mk R (Localization P.primeCompl) M) 1) ∘ b)))

Tactic:
← (AlgebraTensorModule.cancelBaseChange R (R ⧸ P) P.ResidueField ..).symm.comp_bijective

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)
b : Fin n → M
hb : ∀ (i : Fin n), (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ i.asIdeal) M) 1) (b i) = fun x ↦ (b' x) i
P : Ideal R
x✝ : P.IsMaximal
⊢ Function.Bijective
    (⇑(AlgebraTensorModule.cancelBaseChange R (R ⧸ P) P.ResidueField
                (IsLocalRing.ResidueField (Localization P.primeCompl)) M).symm.toAddEquiv.toEquiv ∘
      ⇑(AlgebraTensorModule.cancelBaseChange R (Localization P.primeCompl) P.ResidueField
                (IsLocalRing.ResidueField (Localization P.primeCompl)) M).toAddEquiv.toEquiv ∘
        ⇑(Finsupp.linearCombination (IsLocalRing.ResidueField (Localization P.primeCompl))
            (⇑((TensorProduct.mk (Localization P.primeCompl) (IsLocalRing.ResidueField (Localization P.primeCompl))
                    (Localization P.primeCompl ⊗[R] M))
                  1) ∘
              ⇑((TensorProduct.mk R (Localization P.primeCompl) M) 1) ∘ b)))
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)
b : Fin n → M
hb : ∀ (i : Fin n), (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ i.asIdeal) M) 1) (b i) = fun x ↦ (b' x) i
P : Ideal R
x✝ : P.IsMaximal
⊢ Function.Bijective
    (⇑(AlgebraTensorModule.cancelBaseChange R (R ⧸ P) P.ResidueField
                (IsLocalRing.ResidueField (Localization P.primeCompl)) M).symm.toAddEquiv.toEquiv ∘
      ⇑(AlgebraTensorModule.cancelBaseChange R (Localization P.primeCompl) P.ResidueField
                (IsLocalRing.ResidueField (Localization P.primeCompl)) M).toAddEquiv.toEquiv ∘
        ⇑(Finsupp.linearCombination (IsLocalRing.ResidueField (Localization P.primeCompl))
            (⇑((TensorProduct.mk (Localization P.primeCompl) (IsLocalRing.ResidueField (Localization P.primeCompl))
                    (Localization P.primeCompl ⊗[R] M))
                  1) ∘
              ⇑((TensorProduct.mk R (Localization P.primeCompl) M) 1) ∘ b)))

Tactic:
convert! ((b' ⟨P, ‹_›⟩).repr.lTensor _ ≪≫ₗ finsuppScalarRight _ _ P.ResidueField _).symm.bijective

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)
b : Fin n → M
hb : ∀ (i : Fin n), (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ i.asIdeal) M) 1) (b i) = fun x ↦ (b' x) i
P : Ideal R
x✝ : P.IsMaximal
⊢ ⇑(AlgebraTensorModule.cancelBaseChange R (R ⧸ P) P.ResidueField (IsLocalRing.ResidueField (Localization P.primeCompl))
                M).symm.toAddEquiv.toEquiv ∘
      ⇑(AlgebraTensorModule.cancelBaseChange R (Localization P.primeCompl) P.ResidueField
                (IsLocalRing.ResidueField (Localization P.primeCompl)) M).toAddEquiv.toEquiv ∘
        ⇑(Finsupp.linearCombination (IsLocalRing.ResidueField (Localization P.primeCompl))
            (⇑((TensorProduct.mk (Localization P.primeCompl) (IsLocalRing.ResidueField (Localization P.primeCompl))
                    (Localization P.primeCompl ⊗[R] M))
                  1) ∘
              ⇑((TensorProduct.mk R (Localization P.primeCompl) M) 1) ∘ b)) =
    ⇑(LinearEquiv.lTensor P.ResidueField (b' { asIdeal := P, isMaximal := x✝ }).repr ≪≫ₗ
          finsuppScalarRight (R ⧸ { asIdeal := P, isMaximal := x✝ }.asIdeal)
            (R ⧸ { asIdeal := P, isMaximal := x✝ }.asIdeal) P.ResidueField (Fin n)).symm
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e : J = (⊥.colon {(Ideal.Quotient.mkₐ R I) x}).radical
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
y : R
⊢ (Ideal.Quotient.mk I) y * (Ideal.Quotient.mk I) x ∈ ⊥ ↔ (Ideal.Quotient.mk I) (y * x) = 0

Tactic:
← map_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e : J = (⊥.colon {(Ideal.Quotient.mkₐ R I) x}).radical
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
y : R
⊢ (Ideal.Quotient.mk I) (y * x) ∈ ⊥ ↔ (Ideal.Quotient.mk I) (y * x) = 0