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 : ↥A.ρ.invariants
⊢ (ConcreteCategory.hom (iCocycles A 0)) (cocyclesMk ((ConcreteCategory.hom (cochainsIso₀ A).inv) ↑x) ⋯) =
    (ConcreteCategory.hom (iCocycles A 0)) ((ConcreteCategory.hom (cocyclesIso₀ A).inv) x)

Tactic:
rw [iCocycles_mk]
    exact (cocyclesIso₀_inv_comp_iCocycles_apply A x).symm

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
inst✝ : A.IsTrivial
⊢ (inhomogeneousCochains A).d 0 1 = 0

Tactic:
by
    ext; simp [inhomogeneousCochains.d, Unique.eq_default (α := Fin 0 → G),
      CochainComplex.of.d]

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
⊢ cochainsMap f 0 = 0

Tactic:
by rfl

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

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ p ∈ (fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) ⁻¹' ↑(span (m.leadingTerm '' B))

Tactic:
rw [Set.mem_preimage, SetLike.mem_coe]
    convert!
      (span <| m.leadingTerm '' B).mul_mem_left (MvPolynomial.C (hB p hp).unit⁻¹.val) <|
        subset_span ⟨p, hp, rfl⟩
    rw [← C_mul_leadingCoeff_monomial_degree, ← mul_assoc, ← map_mul,
      IsUnit.val_inv_mul, MvPolynomial.C_1, one_mul]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : CommSemiring R
p : MvPowerSeries σ R
x : τ →₀ ℕ
⊢ (coeff x) ((rename f) p) = ∑ x ∈ ⋯.toFinset, (coeff x) p

Tactic:
by 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 : σ ↪ τ
p : MvPowerSeries σ R
x x✝ : σ →₀ ℕ
h : mapDomain (⇑e) x✝ = embDomain e x
h' : ¬x✝ = x
⊢ (coeff x✝) p = 0

Tactic:
by simp [← embDomain_eq_mapDomain, embDomain_inj, h'] at h

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
⊢ Function.Surjective ⇑(ConcreteCategory.hom (chains₁ToCoinvariantsKer A))

Tactic:
by
  rintro ⟨x, hx⟩
  rcases range_d₁₀_eq_coinvariantsKer A ▸ hx with ⟨y, hy⟩
  use y, Subtype.ext hy

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
⊢ IsNoetherianRing R

Tactic:
by
  refine ⟨isOka_fg.forall_of_forall_prime' (fun C hC₁ hC₂ I hI h ↦ ⟨sSup C, ?_, h⟩) H⟩
  obtain ⟨G, hG⟩ := h
  obtain ⟨J, J_mem_C, G_subset_J⟩ : ∃ J ∈ C, (G : Set R) ⊆ J := by
    refine hC₂.directedOn.exists_mem_subset_of_finset_subset_biUnion ⟨I, hI⟩ (fun _ hx ↦ ?_)
    simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop]
    exact (Submodule.mem_sSup_of_directed ⟨I, hI⟩ hC₂.directedOn).1 <| hG ▸ subset_span hx
  suffices J_eq_sSup : J = sSup C from J_eq_sSup ▸ J_mem_C
  exact le_antisymm (le_sSup J_mem_C) (hG ▸ Ideal.span_le.2 G_subset_J)

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
w✝ : Ideal R
hI : w✝ ∈ C
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P

Tactic:
refine ⟨sSup C, ?_, fun _ hz ↦ le_sSup hz⟩

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
w✝ : Ideal R
hI : w✝ ∈ C
⊢ sSup C ∈ kaplanskySet S
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
p : MvPowerSeries τ R
x : σ →₀ ℕ
⊢ (coeff x) ((killCompl e) p) = (coeff (embDomain e x)) p

Tactic:
by rfl

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
this : RingHomSurjective constantCoeff
S : Set R⟦X⟧
inst✝ : (Ideal.span S).IsPrime
hI : X ∉ Ideal.span S
hfg : (Ideal.span S).FG
hS : S.Finite
hScard : S.ncard = (generators (Ideal.map constantCoeff (Ideal.span S))).ncard
⊢ (generators (Ideal.map constantCoeff (Ideal.span S))).ncard ≤ spanFinrank (Ideal.map constantCoeff (Ideal.span S))

Tactic:
FG.generators_ncard

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
this : RingHomSurjective constantCoeff
S : Set R⟦X⟧
inst✝ : (Ideal.span S).IsPrime
hI : X ∉ Ideal.span S
hfg : (Ideal.span S).FG
hS : S.Finite
hScard : S.ncard = (generators (Ideal.map constantCoeff (Ideal.span S))).ncard
⊢ spanFinrank (Ideal.map constantCoeff (Ideal.span S)) ≤ spanFinrank (Ideal.map constantCoeff (Ideal.span S))

case refine_1
R : Type u_1
inst✝¹ : CommRing R
this : RingHomSurjective constantCoeff
S : Set R⟦X⟧
inst✝ : (Ideal.span S).IsPrime
hI : X ∉ Ideal.span S
hfg : (Ideal.span S).FG
hS : S.Finite
hScard : S.ncard = (generators (Ideal.map constantCoeff (Ideal.span S))).ncard
⊢ Submodule.FG (Ideal.map constantCoeff (Ideal.span S))
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this✝ : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ IsAdic I

Tactic:
by rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this✝ : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ IsAdic (Ideal.map e I)

Tactic:
by rfl

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
p : MvPowerSeries σ R
⊢ ↑((toAdicCompletion σ R) p) n = (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) ((truncTotal n) p)

Tactic:
by rfl

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
n : ℕ
⊢ cyclesMap (MonoidHom.id G) (φ ≫ ψ) n = cyclesMap (MonoidHom.id G) φ n ≫ cyclesMap (MonoidHom.id G) ψ n

Tactic:
by
  simp [cyclesMap, chainsMap_id_comp, HomologicalComplex.cyclesMap_comp]

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

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ degree x < n

Tactic:
exact hx

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
x : σ →₀ ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
⊢ (coeff x) (toAdicCompletionInv σ R f) = MvPolynomial.coeff x (Quotient.out (↑f (degree x + 1)))

Tactic:
by rfl

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✝
n : ℕ
A B : Rep k G
f : A ⟶ B
inst✝ : Epi f
Z✝ : ModuleCat k
g h : groupHomology B 0 ⟶ Z✝
hgh : map (MonoidHom.id G) f 0 ≫ g = map (MonoidHom.id G) f 0 ≫ h
⊢ g = h

Tactic:
by
    simp only [← cancel_epi (H0π A)] at hgh
    simp_all [cancel_epi]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
p : MvPowerSeries σ R
⊢ (toAdicCompletionAlgEquiv σ R) p = (toAdicCompletion σ R) p

Tactic:
by rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
y : AdicCompletion I ↥(I ^ n • ⊤)
⊢ n ≤ n

Tactic:
by rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
h : I.FG
⊢ I ^ n • ⊤ = (eval I M n).ker

Tactic:
refine le_antisymm (pow_smul_top_le_ker_eval ..) ?_
  replace h := Ideal.FG.pow (n := n) h
  rcases h with ⟨s, hs⟩
  simp only [← hs, span_smul_eq]
  rw [← restrictScalars_top R (AdicCompletion I R) (AdicCompletion I M),
    ← restrictScalars_image_smul_eq (R := AdicCompletion I R),
    ← restrictScalars_range_ofPowSMul_eq_ker_eval, restrictScalars_le,
    image_smul_top_eq_range_lsum]
  simp only [SetLike.coe_sort_coe]
  rw [← LinearMap.range_comp_of_range_eq_top (f := (finsuppLEquivDirectSum ..).symm.toLinearMap)
    _ (by simp), lsum_smul_comp_finsuppLEquivDirectSum_symm,
    LinearMap.range_comp_of_range_eq_top _ (LinearEquiv.range _),
    LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_eq_top_of_surjective _ <|
      Function.RightInverse.surjective (g := map I (finsuppLEquivDirectSum R M s)) (fun _ ↦ by
      simp [← LinearMap.comp_apply, map_comp]))]
  rintro _ ⟨x, rfl⟩
  have : Function.Surjective ((lsum R fun i : s ↦ i.val • (LinearMap.id : M →ₗ[R] M)).codRestrict
    (I ^ n • ⊤) (fun _ ↦ by simp [← hs, span_smul_eq, smul_top_eq_range_lsum])) := by
    rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict, ← hs, span_smul_eq,
      smul_top_eq_range_lsum]
    simp
  rcases map_surjective I this x with ⟨x, rfl⟩
  exact ⟨x, by rw [← LinearMap.comp_apply, map_comp, LinearMap.subtype_comp_codRestrict]⟩

Goal state after:
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
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)
z : ↥(cycles₁ (res S.subtype (A.toCoinvariants S)))
hz :
  (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
w : ↑(ModuleCat.of k (G × G →₀ ↑(A.toCoinvariants S)))
hzw :
  (ModuleCat.Hom.hom (d₂₁ (A.toCoinvariants S))) w =
    ↑((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) -
      ↑((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
Z : ↥S →₀ ↑A
hZ : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Z = ↑z
W : G × G →₀ ↑A
hW : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ W = w
b : G →₀ ↑A := ⋯
hb : ∀ (g : G), b g ∈ Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)
β : G →₀ ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)) := ⋯
hβb : mapRange Subtype.val ⋯ β = b
α : ↥S →₀ ↑A
hα :
  (ModuleCat.Hom.hom (shortComplexH1 A).pOpcycles ∘ₗ
        ModuleCat.Hom.hom (mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂)
      α =
    (ModuleCat.Hom.hom (shortComplexH1 A).pOpcycles ∘ₗ
        ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂)
      β
δ : G × G →₀ ↑A
hβ :
  (ModuleCat.Hom.hom (shortComplexH1 A).f) δ =
    (ModuleCat.Hom.hom (mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂) α -
      (ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂) β
hαZ : (ConcreteCategory.hom (d₂₁ A)) (W + δ) = mapDomain Subtype.val (α + Z) - ↑x
⊢ (ModuleCat.Hom.hom (H1CoresCoinf A S).f) ((ConcreteCategory.hom (H1π (res S.subtype A))) ⟨α + Z, ?w⟩) =
    (ConcreteCategory.hom (H1π A)) x

Tactic:
simp only [H1CoresCoinf_X₂, H1CoresCoinf_X₁, H1CoresCoinf_f, H1π_comp_map_apply]
    refine (H1π_eq_iff _ _).2 ⟨W + δ, ?_⟩
    simp [hαZ, mapCycles₁_hom]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
⊢ (LinearMap.mul R A[M]).compr₂ comul = (LinearMap.mul R (A[M] ⊗[R] A[M])).compl₁₂ comul comul

Tactic:
ext a b c d
    simp only [Function.comp_apply, LinearMap.coe_comp, LinearMap.compr₂_apply,
      LinearMap.mul_apply', single_mul_single, comul_single, Bialgebra.comul_mul,
      ← (Coalgebra.Repr.arbitrary R b).eq, ← (Coalgebra.Repr.arbitrary R d).eq, Finset.sum_mul_sum,
      Algebra.TensorProduct.tmul_mul_tmul, map_sum, TensorProduct.map_tmul, lsingle_apply,
      LinearMap.compl₁₂_apply, LinearMap.coe_sum, Finset.sum_apply,
      Finset.sum_comm (s := (Coalgebra.Repr.arbitrary R b).index)]

Goal state after:
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 = r • f (single g 1)

Tactic:
exact congr(r • $(single_mapDomainOfBialgHomFun_one f g))

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
S : Set (HeightOneSpectrum R)
n : ℕ
⊢ valuation.ker = selmerGroup.subgroupOf selmerGroup

Tactic:
by
  ext ⟨_, hx⟩
  constructor
  · intro hx' v _
    by_cases hv : v ∈ S
    · exact congr_fun hx' ⟨v, hv⟩
    · exact hx v hv
  · exact fun hx' => funext fun v => hx' v <| Set.notMem_empty v

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : x ∈ ⊥
⊢ ((if x = 0 ∧ m = 0 then 1 else 0) * if x = 0 ∧ n = 0 then 1 else 0) =
    ↑((m + n).choose m) * if x = 0 ∧ m + n = 0 then 1 else 0

Tactic:
by
    rw [mem_bot.mp hx]
    simp only [true_and, mul_ite, mul_one, mul_zero, add_eq_zero]
    by_cases hn : n = 0
    · simp only [hn, ite_true, and_true, add_zero, choose_self, cast_one]
    · rw [if_neg hn, if_neg]
      exact not_and_of_not_right (m = 0) hn

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

Goal state before:
pp: case succ
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : ↑n ! * hI.dpow n a = a ^ n
⊢ ↑(n + 1)! * hI.dpow (n + 1) a = a ^ (n + 1)

Tactic:
factorial_succ,

Goal state after:
case succ
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : ↑n ! * hI.dpow n a = a ^ n
⊢ ↑((n + 1) * n !) * hI.dpow (n + 1) a = a ^ (n + 1)
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
ha : a ∈ I • J
⊢ hI.dpow n a = hJ.dpow n a

Tactic:
induction ha using Submodule.smul_induction_on' generalizing n with

Goal state after:
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
M₃ : Type u_5
M₄ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
r : R
rs : List R
⊢ map (Ideal.ofList rs • ⊤).mkQ (r • ⊤) = r • ⊤

Tactic:
rw [map_pointwise_smul, map_top, range_mkQ]

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

Goal state before:
pp: case pos.x
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec : s.Nonempty → (∀ i ∈ s, r i ∈ I) → hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
h : s.Nonempty
⊢ ∏ x ∈ s, r x ∈ I

Tactic:
obtain ⟨j, hj⟩ := h

Goal state after:
case pos.x
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec : s.Nonempty → (∀ i ∈ s, r i ∈ I) → hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
j : ι
hj : j ∈ s
⊢ ∏ x ∈ s, r x ∈ I
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ span S
hSI : span S ≤ I
z x y : A
hxI : x ∈ Submodule.span A S
hyI : y ∈ Submodule.span A S
hx : ∀ (m : ℕ), m ≠ 0 → hI.dpow m x ∈ span S
hy : ∀ (m : ℕ), m ≠ 0 → hI.dpow m y ∈ span S
m : ℕ
hm : m ≠ 0
⊢ ∀ c ∈ range (m + 1), hI.dpow c x * hI.dpow (m - c) y ∈ span S

Tactic:
intro m _

Goal state after:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ span S
hSI : span S ≤ I
z x y : A
hxI : x ∈ Submodule.span A S
hyI : y ∈ Submodule.span A S
hx : ∀ (m : ℕ), m ≠ 0 → hI.dpow m x ∈ span S
hy : ∀ (m : ℕ), m ≠ 0 → hI.dpow m y ∈ span S
m✝ : ℕ
hm : m✝ ≠ 0
m : ℕ
a✝ : m ∈ range (m✝ + 1)
⊢ hI.dpow m x * hI.dpow (m✝ - m) y ∈ span S
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
⊢ ⟨(J ⊔ J').carrier, ⋯⟩ = ⟨J.carrier, ⋯⟩ ⊔ ⟨J'.carrier, ⋯⟩

Tactic:
by rfl

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
⊢ ⟨(J ⊓ J').carrier, ⋯⟩ = ⟨J.carrier, ⋯⟩ ⊓ ⟨J'.carrier, ⋯⟩

Tactic:
by rfl

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Field k
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra k R
inst✝³ : Algebra R S
inst✝² : IsSepClosed k
inst✝¹ : EssFiniteType k R
inst✝ : FormallyEtale k R
⊢ IsFiniteSplit k R

Tactic:
by
  have := FormallyUnramified.finite_of_free k R
  have : IsArtinianRing R := isArtinian_of_tower k inferInstance
  exact .of_algEquiv (Algebra.FormallyEtale.equivPiOfIsSepClosed k R).symm

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

Goal state before:
pp: case refine_3
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := ⋯
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
x y : A
hx : x ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy : y ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hx_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
n : ℕ
hn : n ≠ 0
⊢ ∀ c ∈ Finset.range (n + 1),
    hI.dpow c x * hI.dpow (n - c) y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
intro m _

Goal state after:
case refine_3
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
x y : A
hx : x ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy : y ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hx_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
n : ℕ
hn : n ≠ 0
m : ℕ
a✝ : m ∈ Finset.range (n + 1)
⊢ hI.dpow m x * hI.dpow (n - m) y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
Module: Mathlib.RingTheory.Etale.Finite

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
k : Type u
inst✝⁸ : Field k
Ω✝ : Type w
inst✝⁷ : Field Ω✝
inst✝⁶ : Algebra R Ω✝
S : Type w
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Ω✝
inst✝² : IsScalarTower R S Ω✝
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
X : FintypeCat
x : ↑(Opposite.unop (Opposite.op (of Ω (X.obj → Ω)))).obj
i : X.obj
⊢ (Algebra.FormallyEtale.equivPiOfIsSepClosed Ω (X.obj → Ω)) x
      (PrimeSpectrum.comap (Pi.evalRingHom (fun a ↦ Ω) i) default) =
    x i

Tactic:
← Pi.coe_evalAlgHom Ω

Goal state after:
R : Type u
inst✝⁹ : CommRing R
k : Type u
inst✝⁸ : Field k
Ω✝ : Type w
inst✝⁷ : Field Ω✝
inst✝⁶ : Algebra R Ω✝
S : Type w
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Ω✝
inst✝² : IsScalarTower R S Ω✝
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
X : FintypeCat
x : ↑(Opposite.unop (Opposite.op (of Ω (X.obj → Ω)))).obj
i : X.obj
⊢ (Algebra.FormallyEtale.equivPiOfIsSepClosed Ω (X.obj → Ω)) x
      (PrimeSpectrum.comap (↑(Pi.evalAlgHom Ω (fun a ↦ Ω) i)) default) =
    x i
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
k : ℕ
A : Type w
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
N : G(k, A ⊗[R] M; A)
⊢ (map f N).toSubmodule = (baseChangeMkQ B N.toSubmodule).ker

Tactic:
by rfl

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case pos.refine_1
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
⊢ Set.MapsTo (fun x ↦ ⟨x.1 + x.2, x⟩) ↑⋯.toFinset
    ↑((image (fun i ↦ i.1 + i.2) ⋯.toFinset).sigma HasAntidiagonal.antidiagonal)

Tactic:
intro ij

Goal state after:
case pos.refine_1
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
ij : ℕ × ℕ
⊢ ij ∈ ↑⋯.toFinset →
    (fun x ↦ ⟨x.1 + x.2, x⟩) ij ∈ ↑((image (fun i ↦ i.1 + i.2) ⋯.toFinset).sigma HasAntidiagonal.antidiagonal)
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f g : R⟦σ →₀ ℕ⟧
n : σ →₀ ℕ
m : (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ m ∈ {x ∈ Finset.antidiagonal ⋯ ⋯ n | f.coeff x.1 * g.coeff x.2 ≠ 0} ↔
    m ∈ {x ∈ HasAntidiagonal.antidiagonal n | f.coeff x.1 * g.coeff x.2 ≠ 0}

Tactic:
simp only [and_congr_left_iff, Finset.mem_antidiagonal, mem_filter, mem_support,
        HasAntidiagonal.mem_antidiagonal]

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f g : R⟦σ →₀ ℕ⟧
n : σ →₀ ℕ
m : (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ f.coeff m.1 * g.coeff m.2 ≠ 0 → (f.coeff m.1 ≠ 0 ∧ g.coeff m.2 ≠ 0 ∧ m.1 + m.2 = n ↔ m.1 + m.2 = n)