mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ↑((inhomogeneousCochains A).X 1)
y : G × G
⊢ (A.ρ y.1) (x ((Equiv.funUnique (Fin 1) G).symm y.2)) - x ((Equiv.funUnique (Fin 1) G).symm (y.1 * y.2)) +
      x ((Equiv.funUnique (Fin 1) G).symm y.1) =
    (A.ρ ((piFinTwoEquiv fun x ↦ G).symm y 0)) (x fun i ↦ (piFinTwoEquiv fun x ↦ G).symm y i.succ) +
      ∑ j, (-1) ^ (↑j + 1) • x (j.contractNth (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y))

Tactic:
Fin.sum_univ_two

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
⊢ (A.ρ y.1) (x ((Equiv.funUnique (Fin 1) G).symm y.2)) - x ((Equiv.funUnique (Fin 1) G).symm (y.1 * y.2)) +
      x ((Equiv.funUnique (Fin 1) G).symm y.1) =
    (A.ρ ((piFinTwoEquiv fun x ↦ G).symm y 0)) (x fun i ↦ (piFinTwoEquiv fun x ↦ G).symm y i.succ) +
      ((-1) ^ (↑0 + 1) • x (Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y)) +
        (-1) ^ (↑1 + 1) • x (Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y)))
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G → ↑A
⊢ (ModuleCat.Hom.hom (d₁₂ A)) f = 0 ↔ ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0

Tactic:
by
    simp_rw [funext_iff, d₁₂_hom_apply, Prod.forall]
    rfl

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
f : ↥(cocycles₁ A)
this : (A.ρ 1) (f 1) - f (1 * 1) + f 1 = 0
⊢ f 1 = 0

Tactic:
simpa only [map_one, Module.End.one_apply, mul_one, sub_self, zero_add] using this

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

Goal state before:
pp: case h
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 : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ (A.quotientToInvariants S))
hx :
  (ConcreteCategory.hom (H1π (of A.ρ)))
      ((ConcreteCategory.hom (mapCocycles₁ (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)))) x) =
    0
⊢ (ConcreteCategory.hom (H1π (A.quotientToInvariants S))) x = 0

Tactic:
rcases (H1π_eq_zero_iff _).1 hx with ⟨y, hy⟩

Goal state after:
case h
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 : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ (A.quotientToInvariants S))
hx :
  (ConcreteCategory.hom (H1π (of A.ρ)))
      ((ConcreteCategory.hom (mapCocycles₁ (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)))) x) =
    0
y : ↑(ModuleCat.of k ↑(of A.ρ))
hy :
  (ModuleCat.Hom.hom (d₀₁ (of A.ρ))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)))) x)
⊢ (ConcreteCategory.hom (H1π (A.quotientToInvariants S))) x = 0
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
S : ShortComplex (Rep R G)
hS : S.ShortExact
a✝ : ℕ
⊢ (S.map
      (tateComplexFunctor R G ⋙ HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) (Int.negSucc a✝))).ShortExact

Tactic:
exact ShortComplex.shortExact_of_iso (ShortComplex.mapNatIso _ (tateComplex.evalNeg _).symm)
      <| map_chainsFunctor_eval_shortExact hS _

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
⊢ I.FG

Tactic:
refine ⟨image p univ ∪ image (a • i) univ, le_antisymm ?_ (fun y hy ↦ ?_)⟩
    <;> simp only [coe_union, coe_image, coe_univ, image_univ, Pi.smul_apply, span_union]

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
⊢ span (Set.range p) ⊔ span (Set.range fun a_1 ↦ a • i a_1) ≤ I

case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
y : R
hy : y ∈ I
⊢ y ∈ span (Set.range p) ⊔ span (Set.range fun a_1 ↦ a • i a_1)
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
⊢ I.FG

Tactic:
classical
    obtain ⟨_, f, hf⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hsup
    obtain ⟨_, i, hi⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hcolon
    rw [submodule_span_eq] at hf
    have H k : ∃ r : R, ∃ p ∈ I, r * a + p = f k := by
      apply mem_span_singleton_sup.1
      rw [sup_comm, ← hf]
      exact mem_span_range_self
    choose! r p p_mem_I Hf using H
    refine ⟨image p univ ∪ image (a • i) univ, le_antisymm ?_ (fun y hy ↦ ?_)⟩
    <;> simp only [coe_union, coe_image, coe_univ, image_univ, Pi.smul_apply, span_union]
    · simp only [sup_le_iff, span_le, range_subset_iff, smul_eq_mul]
      exact ⟨p_mem_I, fun _ ↦ mul_comm a _ ▸ mem_colon_span_singleton.1 (hi ▸ mem_span_range_self)⟩
    · rw [Submodule.mem_sup]
      obtain ⟨s, H⟩ := mem_span_range_iff_exists_fun.1 (hf ▸ Ideal.mem_sup_left hy)
      simp_rw [← Hf] at H
      ring_nf at H
      rw [sum_add_distrib, ← sum_mul, add_comm] at H
      refine ⟨(∑ k, s k * p k), sum_mem _ (fun _ _ ↦ mul_mem_left _ _ mem_span_range_self),
        (∑ k, s k * r k) * a, ?_, H⟩
      rw [mul_comm, ← smul_eq_mul, range_smul, ← submodule_span_eq, Submodule.span_smul, hi]
      exact smul_mem_smul_set <| mem_colon_span_singleton.2 <|
        (I.add_mem_iff_right <| I.sum_mem (fun _ _ ↦ mul_mem_left _ _ <| p_mem_I _)).1 (H ▸ hy)

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

Goal state before:
pp: case add
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : CommSemiring R
P Q : MvPolynomial σ R
hP : (rename f) ↑P = ↑((MvPolynomial.rename f) P)
hQ : (rename f) ↑Q = ↑((MvPolynomial.rename f) Q)
⊢ (rename f) ↑(P + Q) = ↑((MvPolynomial.rename f) (P + Q))

Tactic:
simp [hP, hQ]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
h : 0 ∈ closure {r | Prime r}
l : Multiset R
hl : ∀ y ∈ l, y ∈ {r | Prime r}
hprod : l.prod = 0
⊢ False

Tactic:
exact not_prime_zero (hl 0 (Multiset.prod_eq_zero_iff.1 hprod))

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
g : G
a : ↑A
⊢ single g ((A.ρ g) a) + single g⁻¹ a ∈ boundaries₁ A

Tactic:
rw [← d₂₁_single_ρ_add_single_inv_mul g 1]
  exact Set.mem_range_self _

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
C : ↑(H0 A) → Prop
x : ↑(H0 A)
h : ∀ (x : ↑A), C ((ConcreteCategory.hom (H0π A)) x)
y : ↑(cycles A 0)
⊢ C ((ConcreteCategory.hom (π A 0)) y)

Tactic:
by simpa using h ((cyclesIso₀ A).hom y)

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 (H1π A)) x = 0 ↔ ↑x ∈ boundaries₁ A

Tactic:
by
  have h := leftHomologyπ_naturality'_assoc (isoShortComplexH1 A).inv
    (shortComplexH1 A).moduleCatLeftHomologyData (leftHomologyData _)
    ((inhomogeneousChains A).sc 1).leftHomologyIso.hom
  simp only [H1π, 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₁, shortComplexH1, 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
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:
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.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ i)

Tactic:
intro n

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ n)
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R⟦X⟧
S : Set R
P : Ideal R⟦X⟧
inst✝² : P.IsPrime
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
⊢ UniqueFactorizationMonoid R⟦X⟧

Tactic:
refine UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime.mpr (fun P h₁ h₂ ↦ ?_)
  by_cases hXP : X ∈ P
  · exact ⟨X, hXP, X_prime⟩
  · obtain ⟨_, h⟩ := (IsPrincipalIdealRing.principal (P.map constantCoeff)).principal
    obtain ⟨_, rfl, _, h⟩ := exist_eq_span_eq_ncard_of_X_notMem hXP h.symm (finite_singleton _)
    simp only [ncard_singleton, ncard_eq_one] at h
    obtain ⟨_, rfl⟩ := h
    exact ⟨_, mem_span_singleton_self _,
      (span_singleton_prime (span_singleton_eq_bot.not.1 h₁)).1 h₂⟩

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
I : Ideal R
hI : IsAdic I
⊢ IsHausdorff I R ↔ T2Space R

Tactic:
rw [I.ringFilterBasis.t2Space_iff_sInter_subset hI.symm, isHausdorff_iff]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
I : Ideal R
hI : IsAdic I
⊢ (∀ (x : R), (∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]) → x = 0) ↔ ⋂₀ I.ringFilterBasis.sets ⊆ {0}
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mp.left
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
this : TopologicalSpace R := ⋯
⊢ ∀ (n : ℕ), IsOpen[J.adicTopology] ↑(J ^ n)

Tactic:
intro n

Goal state after:
case mp.left
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
this : TopologicalSpace R := J.adicTopology
n : ℕ
⊢ IsOpen[J.adicTopology] ↑(J ^ n)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : 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 : ℕ
p q : MvPowerSeries σ R
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) (p * q)) =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) p) *
      (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) q)

Tactic:
rw [← map_mul, Ideal.Quotient.mk_eq_mk_iff_sub_mem]

Goal state after:
σ✝ : 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 : ℕ
p q : MvPowerSeries σ R
⊢ (truncTotal n) (p * q) - (truncTotal n) p * (truncTotal n) q ∈ MvPolynomial.idealOfVars σ R ^ n
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (factorPow I hle).comp (f n) = f m
F : R →+* S
hF : ∀ (n : ℕ), (Ideal.Quotient.mk (I ^ n)).comp F = f n
⊢ ∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ n)) (F r) = (Ideal.Quotient.mk (I ^ n)) ((liftRingHom I f ⋯) r)

Tactic:
intro n

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (factorPow I hle).comp (f n) = f m
F : R →+* S
hF : ∀ (n : ℕ), (Ideal.Quotient.mk (I ^ n)).comp F = f n
n : ℕ
⊢ ∀ (r : R), (Ideal.Quotient.mk (I ^ n)) (F r) = (Ideal.Quotient.mk (I ^ n)) ((liftRingHom I f ⋯) r)
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: case refine_2
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
⊢ ∀ (m : ℕ), (f m) x = (Submodule.factor ⋯) ((f (m + 1)) x)

Tactic:
· intro s
    simp only [RingHom.ext_iff] at hf
    simpa using (hf x).symm

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: 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
inst✝ : IsAdicComplete I S
F : R →+* S
hF : ∀ (n : ℕ), (Ideal.Quotient.mk (I ^ a n)).comp F = f n
⊢ ∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ a n)) (F r) = (Ideal.Quotient.mk (I ^ a n)) ((liftRingHom I ha f ⋯) r)

Tactic:
intro n

Goal state after:
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
inst✝ : IsAdicComplete I S
F : R →+* S
hF : ∀ (n : ℕ), (Ideal.Quotient.mk (I ^ a n)).comp F = f n
n : ℕ
⊢ ∀ (r : R), (Ideal.Quotient.mk (I ^ a n)) (F r) = (Ideal.Quotient.mk (I ^ a n)) ((liftRingHom I ha f ⋯) r)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range

Tactic:
rcases (H1π_eq_zero_iff _).1 hx with ⟨y, hy⟩

Goal state after:
case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range
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
⊢ ∀ (t : Finset A), ↑t ⊆ {a | IsGroupLikeElem R a} → LinearIndepOn R id ↑t

Tactic:
rintro s hs

Goal state after:
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
s : Finset A
hs : ↑s ⊆ {a | IsGroupLikeElem R a}
⊢ LinearIndepOn R id ↑s
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun g ↦ (s ↑g, (s ↑g)⁻¹ * g)
he : Function.Injective e
ve : G × G →₀ ↑A := mapDomain e v
hS : ↑(v + (ConcreteCategory.hom (d₂₁ A)) ve).support ⊆ ↑S
⊢ ↑((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype A))))
          ⟨comapDomain Subtype.val (v + (ConcreteCategory.hom (d₂₁ A)) ve) ⋯, ?w⟩) -
      ↑⟨x, hxc⟩ ∈
    boundaries₁ A

Tactic:
use ve - z

Goal state after:
case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := ⋯
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := ⋯
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := ⋯
he : Function.Injective e
ve : G × G →₀ ↑A := ⋯
hS : ↑(v + (ConcreteCategory.hom (d₂₁ A)) ve).support ⊆ ↑S
⊢ (ModuleCat.Hom.hom (d₂₁ A)) (ve - z) =
    ↑((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype A))))
          ⟨comapDomain Subtype.val (v + (ConcreteCategory.hom (d₂₁ A)) ve) ⋯, ?w✝⟩) -
      ↑⟨x, hxc⟩
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1CoresCoinf A S).f).range

Tactic:
rcases (H1π_eq_zero_iff _).1 hx with ⟨y, hy⟩

Goal state after:
case h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1CoresCoinf A S).f).range
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ contentIdeal 1 = ⊤

Tactic:
← span_singleton_one,

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ contentIdeal 1 = span {1}
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case neg.mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
h : ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1
⊢ ∀ i ∈ p.support, (v.intAdicAbv hb) (p.coeff i) < 1

Tactic:
intro n

Goal state after:
case neg.mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
h : ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1
n : ℕ
⊢ n ∈ p.support → (v.intAdicAbv hb) (p.coeff n) < 1
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
g : G
r : R
⊢ r • single ((mapDomainOfBialgHom f) g) 1 = f (r • single g 1)

Tactic:
map_smul

Goal state after:
R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
g : G
r : R
⊢ r • single ((mapDomainOfBialgHom f) g) 1 = r • f (single g 1)
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✝ n : ℕ
X✝ Y✝ Z✝ : Rep k G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ map (MonoidHom.id G) (f ≫ g) n = map (MonoidHom.id G) f n ≫ map (MonoidHom.id G) g n

Tactic:
simp only [← HomologicalComplex.homologyMap_comp, ← chainsMap_comp]

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✝ n : ℕ
X✝ Y✝ Z✝ : Rep k G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ map (MonoidHom.id G) (f ≫ g) n =
    HomologicalComplex.homologyMap (chainsMap ((MonoidHom.id G).comp (MonoidHom.id G)) (f ≫ resMap (MonoidHom.id G) g))
      n