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

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
g : G
v : W
⊢ (sumOfConjugates G π) (MonoidAlgebra.single g 1 • v) = MonoidAlgebra.single g 1 • (sumOfConjugates G π) v

Tactic:
simp only [sumOfConjugates_apply, Finset.smul_sum, conjugate_apply]

Goal state after:
k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
g : G
v : W
⊢ ∑ g_1, MonoidAlgebra.single g_1⁻¹ 1 • π (MonoidAlgebra.single g_1 1 • MonoidAlgebra.single g 1 • v) =
    ∑ x, MonoidAlgebra.single g 1 • MonoidAlgebra.single x⁻¹ 1 • π (MonoidAlgebra.single x 1 • v)
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: 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
s s₁ : ↥S
⊢ (fun m ↦ m • (↑s * g₁)) (s₁ * s⁻¹) = s₁ • g₁

Tactic:
by simp [S.1.smul_def, smul_eq_mul, mul_assoc]

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case inr
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₂ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₂ g₁
⊢ (A.indToCoindAux (↑s * g₁)) ((A.ρ s) a) g₂ = (A.indToCoindAux g₁) a g₂

Tactic:
· rw [indToCoindAux_of_not_rel (h := h), indToCoindAux_of_not_rel]
    exact mt (fun ⟨s₁, hs₁⟩ => ⟨s₁ * s, by simp_all [S.1.smul_def, mul_assoc]⟩) h

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 : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupCohomologyπEven A g hg i hi)) x -
        (ConcreteCategory.hom (groupCohomologyπEven A g hg i hi)) y =
      0 ↔
    ↑x - ↑y ∈ (Hom.hom A.norm).range

Tactic:
← map_sub,

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
i : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupCohomologyπEven A g hg i hi)) (x - y) = 0 ↔ ↑x - ↑y ∈ (Hom.hom A.norm).range
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 : ℕ
hi : Odd i
x y : ↥(Hom.hom A.norm).ker
⊢ (ConcreteCategory.hom (groupCohomologyπOdd A g hg i hi)) x -
        (ConcreteCategory.hom (groupCohomologyπOdd A g hg i hi)) y =
      0 ↔
    ↑x - ↑y ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range

Tactic:
← map_sub,

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
i : ℕ
hi : Odd i
x y : ↥(Hom.hom A.norm).ker
⊢ (ConcreteCategory.hom (groupCohomologyπOdd A g hg i hi)) (x - y) = 0 ↔
    ↑x - ↑y ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: case refine_2
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
hε : ↑ε / g ↑ε = (algebraMap B L) η
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
⊢ η * ((galRestrict A K L B) g) a = a

Tactic:
replace hε := hε.symm

Goal state after:
case refine_2
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η = ↑ε / g ↑ε
⊢ η * ((galRestrict A K L B) g) a = a
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (cocyclesIso₀ A).inv ≫ iCocycles A 0 = (shortComplexH0 A).f ≫ (cochainsIso₀ A).inv

Tactic:
Iso.inv_comp_eq,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ iCocycles A 0 = (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f ≫ (cochainsIso₀ A).inv
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (isoCocycles₂ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.i = iCocycles A 2 ≫ (cochainsIso₂ A).hom

Tactic:
simp [isoCocycles₂, iCocycles, HomologicalComplex.iCycles, iCycles]

Goal state after:
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 y : ↥(cocycles₁ A)
⊢ (ConcreteCategory.hom (H1π A)) x - (ConcreteCategory.hom (H1π A)) y = 0 ↔ ⇑x - ⇑y ∈ coboundaries₁ A

Tactic:
← map_sub,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cocycles₁ A)
⊢ (ConcreteCategory.hom (H1π A)) (x - y) = 0 ↔ ⇑x - ⇑y ∈ coboundaries₁ A
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 y : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (H2π A)) x - (ConcreteCategory.hom (H2π A)) y = 0 ↔ ⇑x - ⇑y ∈ coboundaries₂ A

Tactic:
← map_sub,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (H2π A)) (x - y) = 0 ↔ ⇑x - ⇑y ∈ coboundaries₂ A
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 : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(LinearMap.ker A.ρ.norm)
⊢ (ConcreteCategory.hom (groupHomologyπEven A g hg i hi)) x -
        (ConcreteCategory.hom (groupHomologyπEven A g hg i hi)) y =
      0 ↔
    ↑x - ↑y ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range

Tactic:
← map_sub,

Goal state after:
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 : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(LinearMap.ker A.ρ.norm)
⊢ (ConcreteCategory.hom (groupHomologyπEven A g hg i hi)) (x - y) = 0 ↔ ↑x - ↑y ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
A : Rep k G
i : ℕ
hi : Odd i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupHomologyπOdd A g hg i hi)) x - (ConcreteCategory.hom (groupHomologyπOdd A g hg i hi)) y =
      0 ↔
    ↑x - ↑y ∈ LinearMap.range A.ρ.norm

Tactic:
← map_sub,

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
A : Rep k G
i : ℕ
hi : Odd i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupHomologyπOdd A g hg i hi)) (x - y) = 0 ↔ ↑x - ↑y ∈ LinearMap.range A.ρ.norm
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case h₂
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A
y : ↑(ModuleCat.of k (G →₀ ↑A))
hy : (ModuleCat.Hom.hom (d₁₀ A)) y = x
⊢ x ∈ Submodule.span k (Set.range fun gv ↦ (A.ρ gv.1) gv.2 - gv.2)

Tactic:
induction y using Finsupp.induction generalizing x with
    | zero => simp [← hy]
    | single_add _ _ _ _ _ h =>
      simpa [← hy, add_sub_add_comm, sum_add_index, d₁₀_single (G := G)]
        using! Submodule.add_mem _ (Coinvariants.mem_ker_of_eq _ _ _ rfl) (h rfl)

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
i : σ
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((killCompl e) (X (e i))) = (coeff n✝) (X i)

Tactic:
simp [coeff_X, coeff_killCompl, ← embDomain_single]

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

Goal state before:
pp: case mem.inr
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}
z : R
h : Prime z
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z

Tactic:
· exact ⟨{z}, by simpa⟩

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cycles₁ A)
⊢ (ConcreteCategory.hom (H1π A)) x - (ConcreteCategory.hom (H1π A)) y = 0 ↔ ↑x - ↑y ∈ boundaries₁ A

Tactic:
← map_sub,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cycles₁ A)
⊢ (ConcreteCategory.hom (H1π A)) (x - y) = 0 ↔ ↑x - ↑y ∈ boundaries₁ A
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g h : G
a : ↑A
⊢ (Multiplicative.toAdd
        (Multiplicative.ofAdd
          (↑(ModuleCat.Hom.hom (H1π A) ∘ₗ
                ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).inv ∘ₗ lsingle (g * h))).toIntLinearMap))
      a =
    (Multiplicative.toAdd
        (Multiplicative.ofAdd
            (↑(ModuleCat.Hom.hom (H1π A) ∘ₗ
                  ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).inv ∘ₗ lsingle g)).toIntLinearMap *
          Multiplicative.ofAdd
            (↑(ModuleCat.Hom.hom (H1π A) ∘ₗ
                  ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).inv ∘ₗ lsingle h)).toIntLinearMap))
      a

Tactic:
by
      simpa [← map_add] using ((H1π_eq_iff _ _).2 ⟨single (g, h) a, by
        simp [cycles₁IsoOfIsTrivial, sub_add_eq_add_sub, add_comm (single h a),
          d₂₁_single (A := A)]⟩).symm

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₂ A)
⊢ (ConcreteCategory.hom (H2π A)) x = 0 ↔ ↑x ∈ boundaries₂ A

Tactic:
have h := leftHomologyπ_naturality'_assoc (isoShortComplexH2 A).inv
    (shortComplexH2 A).moduleCatLeftHomologyData (leftHomologyData _)
    ((inhomogeneousChains A).sc 2).leftHomologyIso.hom
  simp only [H2π, isoCycles₂, π, HomologicalComplex.homologyπ, homologyπ,
    cyclesMapIso'_inv, leftHomologyπ, ← h, ← leftHomologyMapIso'_inv, ModuleCat.hom_comp,
    LinearMap.coe_comp, Function.comp_apply, map_eq_zero_iff _
    ((ModuleCat.mono_iff_injective <| _).1 inferInstance)]
  simp [LinearMap.range_codRestrict, boundaries₂, shortComplexH2, cycles₂]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cycles₂ A)
⊢ (ConcreteCategory.hom (H2π A)) x - (ConcreteCategory.hom (H2π A)) y = 0 ↔ ↑x - ↑y ∈ boundaries₂ A

Tactic:
← map_sub,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cycles₂ A)
⊢ (ConcreteCategory.hom (H2π A)) (x - y) = 0 ↔ ↑x - ↑y ∈ boundaries₂ A
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mpr.h
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen[top] ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n ↦ J ^ n • ⊤ := Ideal.adic_basis J
⊢ s ∈ 𝓝 0 ↔ s ∈ 𝓝 0

Tactic:
rw [J.hasBasis_nhds_zero_adic.mem_iff]

Goal state after:
case mpr.h
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen[top] ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n ↦ J ^ n • ⊤ := Ideal.adic_basis J
⊢ s ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(J ^ i) ⊆ s
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : optionElim n y = x
h2 : ¬n = x none
⊢ r = (coeff y) 0

Tactic:
absurd h2
    rw [← optionElim_apply_none n, h1]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Denominator

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Algebra.denominator ℤ Polynomial.X = 0

Tactic:
by
  by_contra h
  exact Polynomial.transcendental_X ℤ
    ((Algebra.isIntegral_denominator_smul _).isAlgebraic.of_smul
      (mem_nonZeroDivisors_of_ne_zero h))

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
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
⊢ Injective (⇑((mk R K (M ⊗[R] N)) 1) ∘ ⇑(map f g))

Tactic:
convert! H₅.comp <| H₃.comp <| H₁.comp <| H₂.comp <| H₄.comp <| H₆.comp <| H₇

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) =
    ⇑(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
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: 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
⊢ Coalgebra R (C ⧸ I)

Tactic:
by
  constructor <;> ext : 1 <;>
    simp only [coassoc_simps, comul_comp_mkQ, counit_comp_mkQ]
  · rw [CoassocSimps.map_counit_comp_comul_left]; rfl
  · rw [CoassocSimps.map_counit_comp_comul_right]; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_8
N : Type u_9
O : Type u_10
inst✝³ : CommSemiring R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : N →* O
g : M →* N
⊢ mapDomainBialgHom R (f.comp g) = (mapDomainBialgHom R f).comp (mapDomainBialgHom R g)

Tactic:
by
  ext; simp [Finsupp.mapDomain_comp]

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    exp
      (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {(IsLocalization.sec R⁰ ↑x).1})).factors) +
        - -↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑(IsLocalization.sec R⁰ ↑x).2})).factors))

Tactic:
valuationOfNeZeroToFun,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(Multiplicative.ofAdd
        (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {(IsLocalization.sec R⁰ ↑x).1})).factors) -
          -↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑(IsLocalization.sec R⁰ ↑x).2})).factors))) =
    exp
      (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {(IsLocalization.sec R⁰ ↑x).1})).factors) +
        - -↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑(IsLocalization.sec R⁰ ↑x).2})).factors))
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : a ∈ ⊥
⊢ (if (if 0 = 0 ∧ n = 0 then 1 else 0) = 0 ∧ m = 0 then 1 else 0) = if m = 0 ∨ n = 0 then ↑(m.uniformBell n) else 0

Tactic:
by_cases hm : m = 0

Goal state after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : a ∈ ⊥
hm : m = 0
⊢ (if (if 0 = 0 ∧ n = 0 then 1 else 0) = 0 ∧ m = 0 then 1 else 0) = if m = 0 ∨ n = 0 then ↑(m.uniformBell n) else 0

case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : a ∈ ⊥
hm : ¬m = 0
⊢ (if (if 0 = 0 ∧ n = 0 then 1 else 0) = 0 ∧ m = 0 then 1 else 0) = if m = 0 ∨ n = 0 then ↑(m.uniformBell n) else 0
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ (if hx : x ∈ Ideal.span {↑p} then ⋯.choose else 0) = if hx : x ∈ Ideal.span {↑p} then ⟨dpow' p n ↑x, ⋯⟩ else 0

Tactic:
split_ifs with hx

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
⊢ ⋯.choose = ⟨dpow' p n ↑x, ⋯⟩

case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∉ Ideal.span {↑p}
⊢ 0 = 0
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R✝ : Type u
S✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
inst✝³ : Algebra R✝ S✝
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (IsScalarTower.toAlgHom R P.extendScalars.Ring S).comp (IsScalarTower.toAlgHom R P.Ring P.extendScalars.Ring) =
    (IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R P.Ring S)

Tactic:
by dsimp; ext; simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (↑P.h1CotangentEquivCotangent ∘ₗ Algebra.H1Cotangent.map R P.Ring S S).range = Submodule.map h1Cotangentι ⊤

Tactic:
LinearMap.range_comp,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Submodule.map (↑P.h1CotangentEquivCotangent) (Algebra.H1Cotangent.map R P.Ring S S).range =
    Submodule.map h1Cotangentι ⊤
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
a : A
ha : a ∈ ↑I
n : ℕ
⊢ hK.dpow n (f a) = hK'.dpow n (f a)

Tactic:
hIK.2 a ha,

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
a : A
ha : a ∈ ↑I
n : ℕ
⊢ f (hI.dpow n a) = hK'.dpow n (f a)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ f (hI.dpow n ↑(Classical.choose h)) - f (hI.dpow n a) = 0

Tactic:
← map_sub,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ f (hI.dpow n ↑(Classical.choose h) - hI.dpow n a) = 0
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d
⊢ Units.mkOfMulEqOne (1 - X) (mk 1) ⋯ ^ (d + 1) * invOneSubPow S (d + 1) = 1

Tactic:
← Units.val_eq_one,

Goal state after:
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d
⊢ ↑(Units.mkOfMulEqOne (1 - X) (mk 1) ⋯ ^ (d + 1) * invOneSubPow S (d + 1)) = 1