mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ ((freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv ≫
        ((barComplex k G).linearYonedaObj k A).d n (n + 1) ≫ (freeLiftLEquiv k G (Fin (n + 1) → G) A).toModuleIso.hom) ≫
      (freeLiftLEquiv k G (Fin (n + 1) → G) A).toModuleIso.inv ≫
        ((barComplex k G).linearYonedaObj k A).d (n + 1) (n + 1 + 1) ≫
          (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A).toModuleIso.hom =
    0

Tactic:
slice_lhs 3 4 => rw [Iso.hom_inv_id]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ (freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv ≫
      ((barComplex k G).linearYonedaObj k A).d n (n + 1) ≫
        (𝟙 (((barComplex k G).linearYonedaObj k A).X (n + 1)) ≫
            ((barComplex k G).linearYonedaObj k A).d (n + 1) (n + 1 + 1)) ≫
          (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A).toModuleIso.hom =
    0
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
X'✝ X✝ : Rep k G
Y✝ : Rep k H
x✝³ : X'✝ ⟶ X✝
x✝² : X✝ ⟶ (resFunctor φ).obj Y✝
x✝¹ : H
x✝ : ↑X'✝
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom ((indResHomEquiv φ X'✝ Y✝).symm (x✝³ ≫ x✝²))).toLinearMap ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X'✝.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom ((indFunctor k φ).map x✝³ ≫ (indResHomEquiv φ X✝ Y✝).toEquiv.symm x✝²)).toLinearMap ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X'✝.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝

Tactic:
simp [indMap, indResHomEquiv]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev i) i

Tactic:
induction i generalizing h₀ with

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
⊢ MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1

Tactic:
congr

Goal state after:
case e_m
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
⊢ (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) = Fin.partialProd i ∘ Fin.succ
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Goal state before:
pp: k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
⊢ ((A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G)).toModuleIso.inv ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
          (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.hom) ≫
      (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.inv ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
          (A.coinvariantsTensorFreeLEquiv (Fin n → G)).toModuleIso.hom =
    0

Tactic:
slice_lhs 3 4 => rw [Iso.hom_inv_id]

Goal state after:
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
⊢ (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G)).toModuleIso.inv ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
        (𝟙 ((HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X (n + 1)) ≫
            (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n) ≫
          (A.coinvariantsTensorFreeLEquiv (Fin n → G)).toModuleIso.hom =
    0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ (ComplexShape.down ℕ).Rel i ((ComplexShape.down ℕ).next i)

Tactic:
induction i generalizing h₀ with

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ ψ : res f A ⟶ B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ cochainsMap f φ = cochainsMap f ψ

Tactic:
congr

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ ψ : res f A ⟶ B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ φ = ψ
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
ψ : res f A ⟶ B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ map f φ n = map f ψ n

Tactic:
congr

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
ψ : res f A ⟶ B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ φ = ψ
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
y : G × G →₀ ↑X.X₂
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
⊢ (Rep.Hom.hom X.f) ((ModuleCat.Hom.hom (d₁₀ X.X₁)) x) = (Rep.Hom.hom X.f) 0

Tactic:
have := congr($((mapShortComplexH1 (MonoidHom.id G) X.f).comm₂₃.symm) x)
  simp_all [shortComplexH1]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
f g : G → k
nat :
  (forget k G).map mulRepHom ≫ η.hom.hom.app rightFDRep =
    η.hom.hom.app (rightFDRep ⊗ rightFDRep) ≫ (forget k G).map mulRepHom
tensor : ∀ (X Y : FDRep k G), η.hom.hom.app (X ⊗ Y) = η.hom.hom.app X ⊗ₘ η.hom.hom.app Y
⊢ let α := Hom.hom (η.hom.hom.app rightFDRep).hom;
  α (f * g) = α f * α g

Tactic:
rw [tensor] at nat

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
f g : G → k
nat :
  (forget k G).map mulRepHom ≫ η.hom.hom.app rightFDRep =
    (η.hom.hom.app rightFDRep ⊗ₘ η.hom.hom.app rightFDRep) ≫ (forget k G).map mulRepHom
tensor : ∀ (X Y : FDRep k G), η.hom.hom.app (X ⊗ Y) = η.hom.hom.app X ⊗ₘ η.hom.hom.app Y
⊢ let α := Hom.hom (η.hom.hom.app rightFDRep).hom;
  α (f * g) = α f * α g
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g h : G
a : ↑A
⊢ single (1, h) ((A.ρ g⁻¹) a) - single (g, 1) a ∈ boundaries₂ A

Tactic:
use single (g, 1, h) a
  simp [d₃₂]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : span S = Ideal.map constantCoeff I
⊢ span {X} ⊔ Ideal.map (C.comp constantCoeff) I ≤ I

Tactic:
simp [Ideal.span_le, hXI, map_constantCoeff_le_self_of_X_mem]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
S : Finset R
hS : span ↑S = Ideal.map constantCoeff P
hX : X ∈ P
H : P = span (insert X (⇑C '' ↑S))
this : (insert X (⇑C '' ↑S)).Finite
⊢ P.FG

Tactic:
lift insert X <| (C (R := R)) '' S to Finset R⟦X⟧ using this with T hT

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
S : Finset R
hS : span ↑S = Ideal.map constantCoeff P
hX : X ∈ P
T : Finset R⟦X⟧
hT : ↑T = insert X (⇑C '' ↑S)
H : P = span ↑T
⊢ P.FG
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: M : Type u_3
inst✝ : AddCommMonoid M
n : ℕ
i : M
x : Fin n →₀ M
⊢ embDomain (finSuccEquiv n).toEmbedding (Finsupp.cons i x) = optionElim i x

Tactic:
ext a; cases a <;> simp [embDomain_eq_mapDomain]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case pos
σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
h : n = 0
this : Subsingleton (MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n)
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) 1) = 1

Tactic:
exact Subsingleton.allEq ..

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ chainsMap f φ = chainsMap f ψ

Tactic:
congr

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ φ = ψ
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ map f φ n = map f ψ n

Tactic:
congr

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ φ = ψ
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
hf : ∀ {m : ℕ}, (factorPow I ⋯).comp (f (m + 1)) = f m
m n : ℕ
hle : m ≤ n
x : R
⊢ Antitone fun n ↦ I ^ a n

Tactic:
exact fun _ _ le ↦ Ideal.pow_le_pow_right (ha.monotone le)

Goal state after:
Module: Mathlib.RingTheory.Flat.Domain

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁴ : AddCommGroup P
inst✝³ : Module R P
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst✝ : Module.Flat R Q
hf : Injective ⇑f
hg : Injective ⇑g
⊢ Injective ⇑(map f g)

Tactic:
by
  let K := FractionRing R
  refine .of_comp (f := TensorProduct.mk R K _ 1) ?_
  have H₁ := TensorProduct.map_injective_of_flat_flat (f.baseChange K) (g.baseChange K)
    (Module.Flat.lTensor_preserves_injective_linearMap f hf)
    (Module.Flat.lTensor_preserves_injective_linearMap g hg)
  have H₂ := (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm.injective
  have H₃ := (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N).injective
  have H₄ := (AlgebraTensorModule.assoc R R K K P Q).symm.injective
  have H₅ := (AlgebraTensorModule.assoc R R K K M N).injective
  have H₆ := Module.Flat.rTensor_preserves_injective_linearMap (M := P ⊗[R] Q)
    (Algebra.linearMap R K) (FaithfulSMul.algebraMap_injective R K)
  have H₇ := (TensorProduct.lid R (P ⊗[R] Q)).symm.injective
  convert! H₅.comp <| H₃.comp <| H₁.comp <| H₂.comp <| H₄.comp <| H₆.comp <| H₇
  dsimp only [← LinearMap.coe_comp, ← LinearEquiv.coe_toLinearMap,
    ← @LinearMap.coe_restrictScalars R K]
  congr! 1
  ext p q
  -- `simp` solves the goal but it times out
  change (1 : K) ⊗ₜ[R] (f p ⊗ₜ[R] g q) = (AlgebraTensorModule.assoc R R K K M N)
    (((1 : K) • (algebraMap R K) 1 ⊗ₜ[R] f p) ⊗ₜ[R] g q)
  simp only [map_one, one_smul, AlgebraTensorModule.assoc_tmul]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: case rTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map counit I.mkQ ∘ₗ comul = (TensorProduct.mk R R (C ⧸ I)) 1 ∘ₗ I.mkQ

Tactic:
CoassocSimps.map_counit_comp_comul_left

Goal state after:
case rTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map LinearMap.id I.mkQ ∘ₗ ↑(TensorProduct.lid R C).symm = (TensorProduct.mk R R (C ⧸ I)) 1 ∘ₗ I.mkQ
Module: Mathlib.RingTheory.Bialgebra.Quotient

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ map counit ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) ∘ₗ comul =
    (↑(Algebra.TensorProduct.lid R (A ⧸ I)).symm).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap

Tactic:
CoassocSimps.map_counit_comp_comul_left

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ map LinearMap.id ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) ∘ₗ
      ↑(TensorProduct.lid R A).symm =
    (↑(Algebra.TensorProduct.lid R (A ⧸ I)).symm).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I : ↥(Ideal A)⁰
⊢ ↑((Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) ((FractionalIdeal.mk0 (FractionRing A)) I)) =
    ↑((FractionalIdeal.mk0 (FractionRing B)) (extendedIdeal A B I))

Tactic:
congr

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I : ↥(Ideal A)⁰
⊢ (Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) ((FractionalIdeal.mk0 (FractionRing A)) I) =
    (FractionalIdeal.mk0 (FractionRing B)) (extendedIdeal A B I)
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case h.refine_2
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s)
⊢ IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s) ∈ p

Tactic:
apply Ideal.IsTwoSided.mul_mem_of_left

Goal state after:
case h.refine_2
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s)
⊢ IsLocalization.mk' R' (↑t * r) 1 ∈ p
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup M''
inst✝ : Module R M''
r : R
f : M →ₗ[R] M'
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : f.range = g.ker
h1 : IsSMulRegular M r
h2 : IsSMulRegular M'' r
⊢ IsSMulRegular M' r

Tactic:
refine IsSMulRegular.of_right_eq_zero_of_smul ?_
  intro x hx
  obtain ⟨y, ⟨⟩⟩ := (congrArg (x ∈ ·) hfg).mpr <| h2.right_eq_zero_of_smul <|
    (g.map_smul r x).symm.trans <| (congrArg _ hx).trans g.map_zero
  refine (congrArg f (h1.right_eq_zero_of_smul ?_)).trans f.map_zero
  exact hf <| (f.map_smul r y).trans <| hx.trans f.map_zero.symm

Goal state after:
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| ⊤ = Ideal.ofList (r :: rs) • ⊤ ↔ ⊤ = Ideal.ofList rs • ⊤

Tactic:
congr

Goal state after:
case a
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| ⊤ = Ideal.ofList (r :: rs) • ⊤

case b
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| ⊤ = Ideal.ofList rs • ⊤
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
h : ∀ (x : M), f (r • x) = s • f x
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
| AddSubgroup.map f (Ideal.ofList (r :: l₁✝) • ⊤).toAddSubgroup = (Ideal.ofList (s :: l₂✝) • ⊤).toAddSubgroup

Tactic:
congr

Goal state after:
case a
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
h : ∀ (x : M), f (r • x) = s • f x
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
| AddSubgroup.map f (Ideal.ofList (r :: l₁✝) • ⊤).toAddSubgroup

case a
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
h : ∀ (x : M), f (r • x) = s • f x
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
| (Ideal.ofList (s :: l₂✝) • ⊤).toAddSubgroup
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.mem.mem
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
i : ι
n : ι →₀ ℕ
⊢ ((Finsupp.single i k + n).prod fun i k ↦ dp R k (v i)) =
    dp R (k + n i) (v i) * (Finsupp.erase i n).prod fun i k ↦ dp R k (v i)

Tactic:
rw [← (Finsupp.single i k + n).mul_prod_erase' i _ (fun i ↦ dp_zero (m := v i))]

Goal state after:
case dp.mem.mem
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
i : ι
n : ι →₀ ℕ
⊢ (dp R ((Finsupp.single i k + n) i) (v i) * (Finsupp.erase i (Finsupp.single i k + n)).prod fun i k ↦ dp R k (v i)) =
    dp R (k + n i) (v i) * (Finsupp.erase i n).prod fun i k ↦ dp R k (v i)
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case mk.mk
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
toRingHom✝¹ : A →+* B
ideal_comp✝¹ : map toRingHom✝¹ I ≤ J
dpow_comp✝¹ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝¹ a) = toRingHom✝¹ (hI.dpow n a)
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' :
  (fun h ↦ ⇑h.toRingHom) { toRingHom := toRingHom✝¹, ideal_comp := ideal_comp✝¹, dpow_comp := dpow_comp✝¹ } =
    (fun h ↦ ⇑h.toRingHom) { toRingHom := toRingHom✝, ideal_comp := ideal_comp✝, dpow_comp := dpow_comp✝ }
⊢ { toRingHom := toRingHom✝¹, ideal_comp := ideal_comp✝¹, dpow_comp := dpow_comp✝¹ } =
    { toRingHom := toRingHom✝, ideal_comp := ideal_comp✝, dpow_comp := dpow_comp✝ }

Tactic:
congr

Goal state after:
case mk.mk
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
toRingHom✝¹ : A →+* B
ideal_comp✝¹ : map toRingHom✝¹ I ≤ J
dpow_comp✝¹ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝¹ a) = toRingHom✝¹ (hI.dpow n a)
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' :
  (fun h ↦ ⇑h.toRingHom) { toRingHom := toRingHom✝¹, ideal_comp := ideal_comp✝¹, dpow_comp := dpow_comp✝¹ } =
    (fun h ↦ ⇑h.toRingHom) { toRingHom := toRingHom✝, ideal_comp := ideal_comp✝, dpow_comp := dpow_comp✝ }
⊢ toRingHom✝¹ = toRingHom✝
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.mem
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
i : ι
⊢ x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
induction hx using span_induction with

Goal state after: