mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case hc
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g : G
a : ↑A
⊢ (QuotientGroup.rightRel S) g g

Tactic:
· rfl

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

Goal state before:
pp: case neg
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
X✝ Y✝ : Rep k G
f : X✝ ⟶ Y✝
j : ℕ
hj : ¬Even (j + 1)
⊢ f ≫ (HomologicalComplex.alternatingConst Y✝ ⋯ ⋯ ⋯).d (j + 1) j =
    (HomologicalComplex.alternatingConst X✝ ⋯ ⋯ ⋯).d (j + 1) j ≫ f

Tactic:
· simp [if_neg hj, applyAsHom_comm]

Goal state after:
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
i j : ℕ
h : i + 1 = j
⊢ (freeLiftLEquiv k G (Fin i → G) A).toModuleIso.symm.hom ≫ ((barComplex k G).linearYonedaObj k A).d i j =
    (inhomogeneousCochains A).d i j ≫ (freeLiftLEquiv k G (Fin j → G) A).toModuleIso.symm.hom

Tactic:
subst h

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
i : ℕ
⊢ (freeLiftLEquiv k G (Fin i → G) A).toModuleIso.symm.hom ≫ ((barComplex k G).linearYonedaObj k A).d i (i + 1) =
    (inhomogeneousCochains A).d i (i + 1) ≫ (freeLiftLEquiv k G (Fin (i + 1) → G) A).toModuleIso.symm.hom
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
⊢ (Hom.hom ((standardComplex k G).d (n + 1) n)).toLinearMap = d k G (n + 1)

Tactic:
by
  refine MonoidAlgebra.lhom_ext' fun (x : Fin (n + 2) → G) => LinearMap.ext_ring ?_
  simp [standardComplex, Action.ofMulAction_V, SimplicialObject.δ, SimplexCategory.δ,
    Fin.succAboveOrderEmb, ← Int.cast_smul_eq_zsmul k ((-1) ^ _ : ℤ), ← ofHom_smul, ← ofHom_sum,
    Representation.IntertwiningMap.coe_toLinearMap, Representation.IntertwiningMap.sum_apply,
    Representation.IntertwiningMap.smul_apply, (Representation.linearizeMap_single),
    smul_eq_mul, mul_one]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝ : ↑((standardComplex k G).X 1)
⊢ (forget₂ToModuleCat k G).d 1 0 ≫ (forget₂ (Rep k G) (ModuleCat k)).map (ε k G) = 0

Tactic:
rw [← forget₂ToModuleCatHomotopyEquiv_f_0_eq,
      ← (forget₂ToModuleCatHomotopyEquiv k G).1.2 1 0 rfl]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝ : ↑((standardComplex k G).X 1)
⊢ (forget₂ToModuleCatHomotopyEquiv k G).hom.f 1 ≫
      ((ChainComplex.single₀ (ModuleCat k)).obj ((forget₂ (Rep k G) (ModuleCat k)).obj (trivial k G k))).d 1 0 =
    0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ cocyclesMk ((ConcreteCategory.hom (cochainsIso₂ A).inv) ⇑x) ⋯ = (ConcreteCategory.hom (isoCocycles₂ A).inv) x

Tactic:
apply_fun (forget₂ _ Ab).map ((inhomogeneousCochains A).iCycles 2) using
    (AddCommGrpCat.mono_iff_injective _).1 <| (forget₂ _ _).map_mono _
  rw [HomologicalComplex.i_cyclesMk]
  simp; rfl

Goal state after:
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
hg : ∀ (x : G), x ∈ Subgroup.zpowers g✝
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
a : ↑A
g : G
⊢ (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X i)).compr₂
            (ModuleCat.Hom.hom
              (A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom ≫ (moduleCatChainComplex A g✝).d i j)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1 =
    (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X i)).compr₂
            (ModuleCat.Hom.hom
              ((HomologicalComplex.coinvariantsTensorObj A (resolution k g✝⁻¹ ⋯).complex).d i j ≫
                A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1

Tactic:
subst h

Goal state after:
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✝
j : ℕ
a : ↑A
g : G
⊢ (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              (A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom ≫ (moduleCatChainComplex A g✝).d (j + 1) j)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1 =
    (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              ((HomologicalComplex.coinvariantsTensorObj A (resolution k g✝⁻¹ ⋯).complex).d (j + 1) j ≫
                A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1
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₁ f₂ : G →* H
h : f₁ = f₂
φ : res f₁ A ⟶ B
T : Type u_1
F : (f : G →* H) → (res f A ⟶ B) → T
⊢ F f₁ φ = F f₂ (h ▸ φ)

Tactic:
subst h

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
T : Type u_1
F : (f : G →* H) → (res f A ⟶ B) → T
⊢ F f₁ φ = F f₁ (⋯ ▸ φ)
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
hf : Function.Surjective ⇑f
inst✝ : Mono φ
i : ℕ
⊢ Mono ((cochainsMap f φ).f i)

Tactic:
by
  simpa [ModuleCat.mono_iff_injective] using!
    ((Rep.mono_iff_injective φ).1 inferInstance).comp_left.comp <|
    LinearMap.funLeft_injective_of_surjective k A _ hf.comp_left

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: case ofNat
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
⊢ (map (f + g)).f (Int.ofNat i) = (map f + map g).f (Int.ofNat i)

pp: case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
⊢ (map (f + g)).f (Int.negSucc i) = (map f + map g).f (Int.negSucc i)

Tactic:
· rfl

Goal state after:
case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
⊢ (map (f + g)).f (Int.negSucc i) = (map f + map g).f (Int.negSucc i)
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq τ
x : τ →₀ ℕ
⊢ {p | p.1 ∈ Finset.antidiagonal x ∧ p.2 ∈ ⋯.toFinset ×ˢ ⋯.toFinset}.Finite

Tactic:
classical
  apply Set.Finite.subset (s := ↑((Finset.antidiagonal x).sup (fun q ↦ Finset.product {q}
    ((TendstoCofinite.finite_preimage_singleton (Finsupp.mapDomain f) q.1).toFinset ×ˢ
      (TendstoCofinite.finite_preimage_singleton (Finsupp.mapDomain f) q.2).toFinset))))
  · exact Finset.finite_toSet ..
  · intro; simp
    grind

Goal state after:
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I | ¬I.FG}
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
h : (sSup C).FG
⊢ sSup C ∈ C

Tactic:
obtain ⟨G, hG⟩ := h

Goal state after:
R : Type u_1
inst✝ : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I | ¬I.FG}
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
G : Finset R
hG : span ↑G = sSup C
⊢ sSup C ∈ C
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: case one
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod 1

Tactic:
exact ⟨∅, by simp⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = Ideal.map constantCoeff (Submodule.span R⟦X⟧ (Set.range F))
⊢ I ≤ Submodule.span R⟦X⟧ (Set.range F)

Tactic:
rw [submodule_span_eq, map_span, ← Set.range_comp] at h'

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
⊢ I ≤ Submodule.span R⟦X⟧ (Set.range F)
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : f ∈ I
⊢ f ∈ comap constantCoeff (Ideal.map constantCoeff (span T))

Tactic:
mem_comap,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : f ∈ I
⊢ constantCoeff f ∈ Ideal.map constantCoeff (span T)
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case h.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
hn : 0 < 0
⊢ False

Tactic:
exact Nat.not_succ_le_zero 0 hn

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

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = 0 ∧ k = 1)
h3 : k = 1
⊢ 0 = (coeff x) 1

pp: case neg
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = 0 ∧ k = 1)
h3 : ¬k = 1
⊢ 0 = (coeff x) 0

Tactic:
· rw [coeff_one, if_neg (by tauto)]

Goal state after:
case neg
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = 0 ∧ k = 1)
h3 : ¬k = 1
⊢ 0 = (coeff x) 0
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₁ f₂ : G →* H
h : f₁ = f₂
φ : A ⟶ res f₁ B
T : Type u_1
F : (f : G →* H) → (A ⟶ res f B) → T
⊢ F f₁ φ = F f₂ (h ▸ φ)

Tactic:
subst h

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
T : Type u_1
F : (f : G →* H) → (A ⟶ res f B) → T
⊢ F f₁ φ = F f₁ (⋯ ▸ φ)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ ↑f (degree x + 1) = (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ (degree x + 1) • ⊤)) (Quotient.out (↑f n))

Tactic:
← AdicCompletion.transitionMap_ideal_mk _ (Nat.lt_iff_add_one_le.mp h),

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ ↑f (degree x + 1) =
    (AdicCompletion.transitionMap (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) ⋯)
      ((Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) (Quotient.out (↑f n)))
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
I : Ideal S
inst✝² : IsAdicComplete I S
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (factorₐ R ⋯).comp (f n) = f m
n : ℕ
x : A
⊢ (Ideal.Quotient.mk (I ^ n)) ((liftAlgHom I f ⋯) x) = (f n) x

Tactic:
by
  simp [liftAlgHom]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
inst✝³ : Module R B
inst✝² : Coalgebra R B
a : A
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
⊢ counit (f a) = 1

Tactic:
CoalgHomClass.counit_comp_apply,

Goal state after:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
inst✝³ : Module R B
inst✝² : Coalgebra R B
a : A
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
⊢ counit a = 1
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
K : Type u_1 := FractionRing R
H₁ : Injective ⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g))
H₂ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm
H₃ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N)
H₄ : Injective ⇑(AlgebraTensorModule.assoc R R K K P Q).symm
H₅ : Injective ⇑(AlgebraTensorModule.assoc R R K K M N)
H₆ : Injective ⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K))
H₇ : Injective ⇑(TensorProduct.lid R (P ⊗[R] Q)).symm
⊢ ⇑((mk R K (M ⊗[R] N)) 1) ∘ ⇑(map f g) =
    ⇑(AlgebraTensorModule.assoc R R K K M N) ∘
      ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N) ∘
        ⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) ∘
          ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm ∘
            ⇑(AlgebraTensorModule.assoc R R K K P Q).symm ∘
              ⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K)) ∘ ⇑(TensorProduct.lid R (P ⊗[R] Q)).symm

Tactic:
dsimp only [← LinearMap.coe_comp, ← LinearEquiv.coe_toLinearMap,
    ← @LinearMap.coe_restrictScalars R K]

Goal state after:
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
K : Type u_1 := FractionRing R
H₁ : Injective ⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g))
H₂ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm
H₃ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N)
H₄ : Injective ⇑(AlgebraTensorModule.assoc R R K K P Q).symm
H₅ : Injective ⇑(AlgebraTensorModule.assoc R R K K M N)
H₆ : Injective ⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K))
H₇ : Injective ⇑(TensorProduct.lid R (P ⊗[R] Q)).symm
⊢ ⇑((mk R K (M ⊗[R] N)) 1 ∘ₗ map f g) =
    ⇑(↑R ↑(AlgebraTensorModule.assoc R R K K M N) ∘ₗ
        ↑R ↑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N) ∘ₗ
          ↑R (map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) ∘ₗ
            ↑R ↑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm ∘ₗ
              ↑R ↑(AlgebraTensorModule.assoc R R K K P Q).symm ∘ₗ
                LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K) ∘ₗ ↑(TensorProduct.lid R (P ⊗[R] Q)).symm)
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = d • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ y ∈ s, y ≠ x → c y = 0
⊢ (fun a ↦ a * c x) d = (fun a ↦ a * c x) (c x)

Tactic:
by simpa using (key (x, x) (by simp [*]))

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x✝ : Aᵐᵒᵖ
⊢ (↑(TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ) ∘ₗ rTensor Aᵐᵒᵖ comul ∘ₗ comul) x✝ = (lTensor Aᵐᵒᵖ comul ∘ₗ comul) x✝

Tactic:
comul_def,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x✝ : Aᵐᵒᵖ
⊢ (↑(TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ) ∘ₗ
        rTensor Aᵐᵒᵖ (map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm) ∘ₗ
          map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm)
      x✝ =
    (lTensor Aᵐᵒᵖ (map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm) ∘ₗ
        map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm)
      x✝
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
this : span (↑(map f p).coeffs ∪ {0}) = span (⇑f '' ↑p.coeffs ∪ {0})
⊢ (map f p).contentIdeal = Ideal.map f p.contentIdeal

Tactic:
simpa [contentIdeal_def, map_span]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.contentIdeal ≤ span {p.content}

Tactic:
by
  rw [contentIdeal_def, span_le]
  intro _ h1
  rw [Finset.mem_coe, mem_coeffs_iff] at h1
  obtain ⟨n, _, h2⟩ := h1
  rw [SetLike.mem_coe, h2, mem_span_singleton]
  exact content_dvd_coeff n

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
M : Type u_8
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
f g : WithConv (R[M] →ₐ[R] A)
x : M
⊢ (f * g).ofConv (single x 1) = f.ofConv (single x 1) * g.ofConv (single x 1)

Tactic:
by simp [AlgHom.convMul_apply]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
v' i' : R
vi✝ : (algebraMap R K) v' * (algebraMap R K) i' = 1
vi : v' * i' = 1
iv✝ : (algebraMap R K) i' * (algebraMap R K) v' = 1
iv : i' * v' = 1
hx :
  (powMonoidHom n) { val := (algebraMap R K) v', inv := (algebraMap R K) i', val_inv := vi✝, inv_val := iv✝ } =
    (Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  (algebraMap R K) (v' ^ n) = (algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := (algebraMap R K) i', inv := (algebraMap R K) v', val_inv := iv✝, inv_val := vi✝ } ^ n =
    (algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range

Tactic:
exact ⟨⟨v', i', vi, iv⟩, by
      simpa only [Units.ext_iff, powMonoidHom_apply, Units.val_pow_eq_pow_val] using
         FaithfulSMul.algebraMap_injective R K hv⟩

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

Goal state before:
pp: case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n✝ : ℕ
x✝ y✝ : A
ha : x✝ ∈ ⊥
hb : y✝ ∈ ⊥
h : ¬n✝ = 0
⊢ 0 = ∑ x ∈ antidiagonal n✝, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0

Tactic:
symm
      apply sum_eq_zero
      grind [mem_antidiagonal]

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
n : ℕ
M : ModuleCat R
inst✝¹ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
N : ModuleCat R
inst✝ : Module.Finite R ↑N
h_supp : Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I
h_ext : ∀ i < n, Subsingleton (Ext N M i)
⊢ ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs

Tactic:
induction n generalizing M with
  | zero =>
    have : Nontrivial M := (Submodule.nontrivial_iff R).mp (nontrivial_of_lt _ _ smul_lt)
    use []
    simp [isRegular_iff]
  | succ n ih =>
    rw [Module.support_eq_zeroLocus, PrimeSpectrum.zeroLocus_eq_iff] at h_supp
    -- use `Ext N M 0` vanish to obtain an `M`-regular element `x` in `Ann(N)`
    have : Subsingleton (N ⟶ M) := Ext.addEquiv₀.subsingleton_congr.mp (h_ext 0 n.zero_lt_succ)
    have : Subsingleton (N →ₗ[R] M) := ModuleCat.homAddEquiv.symm.subsingleton
    obtain ⟨x, mem_ann, hx⟩ := subsingleton_linearMap_iff.mp this
    -- take a power of it to make `xᵏ` fall into `I`
    obtain ⟨k, hk⟩ := le_of_le_of_eq Ideal.le_radical h_supp mem_ann
    -- verify that `N` indeed make `M ⧸ xᵏM` satisfy the induction hypothesis
    have h_ext' : ∀ i < n, Subsingleton (Ext N (ModuleCat.of R (QuotSMulTop (x ^ k) M)) i) := by
      intro i hi
      -- the vanishing of `Ext` is obtained from the (covariant) long exact sequence given by
      -- `M.smulShortComplex (x ^ k)`
      have zero1 := AddCommGrpCat.isZero_of_iff_subsingleton.mpr (h_ext i (by omega))
      have zero2 := AddCommGrpCat.isZero_of_iff_subsingleton.mpr (h_ext (i + 1) (by omega))
      exact AddCommGrpCat.subsingleton_of_isZero <| ShortComplex.Exact.isZero_of_both_zeros
        ((Ext.covariant_sequence_exact₃' N (hx.pow k).smulShortComplex_shortExact) i (i + 1) rfl)
        (zero1.eq_zero_of_src _) (zero2.eq_zero_of_tgt _)
    obtain ⟨rs, len, mem, reg⟩ := ih (ModuleCat.of R (QuotSMulTop (x ^ k) M))
      (smul_top_quotSMulTop_ne_top_of_smul_top_ne_top hk smul_lt.ne).lt_top h_ext'
    use x ^ k :: rs
    simpa [len, hk] using ⟨mem, hx.pow k, reg⟩

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

Goal state before:
pp: 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 (r • ⊤ ⊔ (Ideal.ofList l₁✝ • ⊤).toAddSubgroup)

Tactic:
AddSubgroup.pointwise_smul_def

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 (AddSubgroup.map ((toAddMonoidEnd R M) r) ⊤ ⊔ (Ideal.ofList l₁✝ • ⊤).toAddSubgroup)