mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
n : ℕ
⊢ (eval₂Hom (algebraMap ℤ S) fun i ↦ g (x.coeff i)) (φ n) = (aeval fun i ↦ g (x.coeff i)) (φ n)

Tactic:
aeval_eq_eval₂Hom

Goal state after:
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
⊢ ↑p ≠ 0

Tactic:
by
  simpa using (IsFractionRing.injective (𝕎 R) (FractionRing (𝕎 R))).ne (WittVector.p_nonzero _ _)

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
h : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
hp : ↑p ∣ r
⊢ r ∈ Ideal.span {↑p}

Tactic:
Ideal.mem_span_singleton

Goal state after:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
h : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
hp : ↑p ∣ r
⊢ ↑p ∣ r
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : O
⊢ ↑p ∣ x ↔ x ∈ Ideal.span {↑p}

Tactic:
Ideal.mem_span_singleton

Goal state after:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : O
⊢ ↑p ∣ x ↔ ↑p ∣ x
Module: Mathlib.RingTheory.WittVector.Domain

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
x y : 𝕎 R
⊢ x ≠ 0 ∧ y ≠ 0 → x * y ≠ 0

Tactic:
rintro ⟨ha, hb⟩

Goal state after:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
x y : 𝕎 R
ha : x ≠ 0
hb : y ≠ 0
⊢ x * y ≠ 0
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
h : ∀ i < n, x.coeff i = y.coeff i
i : Fin n
⊢ TruncatedWittVector.coeff i ((truncate n) x) = TruncatedWittVector.coeff i ((truncate n) y)

Tactic:
simp [h i]

Goal state after:
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x * ↑p = 0
⊢ x = 0

Tactic:
by
  rwa [← frobenius_verschiebung, _root_.map_eq_zero_iff _ (frobenius_bijective p k).injective,
      _root_.map_eq_zero_iff _ (verschiebung_injective p k)] at h

Goal state after:
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
g : ℕ → R := fun x ↦ 0
⊢ ∀ x_1 ∈ Finset.Iic n \ {i},
    ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ x_1) (x.coeff x_1)) * ↑p ^ x_1).coeff i = g x_1

Tactic:
· intro b hb
      simp only [Finset.mem_sdiff, Finset.mem_Iic, Finset.mem_singleton] at hb
      exact teichmuller_mul_pow_coeff_of_ne _ (Ne.intro hb.2).symm

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

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
hx : x = 0
⊢ ∃ i, (∃ y, i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)

pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
hx : ¬x = 0
⊢ ∃ i, (∃ y, i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)

Tactic:
· simp only [hx, and_true, inv_zero, or_true]
      exact ⟨_, 1, rfl, one_ne_zero⟩

Goal state after:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
hx : ¬x = 0
⊢ ∃ i, (∃ y, i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ (match d - rootMultiplicity 1 p - 1 + 1 with
      | 0 => 0
      | d.succ =>
        ∑ i ∈ (q * (-1) ^ rootMultiplicity 1 p).support,
          (q * (-1) ^ rootMultiplicity 1 p).coeff i • preHilbertPoly F d i).natDegree =
    d - rootMultiplicity 1 p - 1

Tactic:
apply natDegree_eq_of_le_of_coeff_ne_zero

Goal state after:
case pn
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ (match d - rootMultiplicity 1 p - 1 + 1 with
      | 0 => 0
      | d.succ =>
        ∑ i ∈ (q * (-1) ^ rootMultiplicity 1 p).support,
          (q * (-1) ^ rootMultiplicity 1 p).coeff i • preHilbertPoly F d i).natDegree ≤
    d - rootMultiplicity 1 p - 1

case p1
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ (match d - rootMultiplicity 1 p - 1 + 1 with
        | 0 => 0
        | d.succ =>
          ∑ i ∈ (q * (-1) ^ rootMultiplicity 1 p).support,
            (q * (-1) ^ rootMultiplicity 1 p).coeff i • preHilbertPoly F d i).coeff
      (d - rootMultiplicity 1 p - 1) ≠
    0
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: case a.e_a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ ↑((x + n)! / x !) = C ↑((x + n)! / (x ! * n !)) * ↑n !

Tactic:
simp only [Int.natCast_ediv, cast_mul, eq_intCast]

Goal state after:
case a.e_a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ ↑((x + n)! / x !) = ↑(↑(x + n)! / (↑x ! * ↑n !)) * ↑n !
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ Function.support ((expand p hp) φ) ⊆ (fun x ↦ p • x) '' Function.support φ

Tactic:
rw [expand, MvPowerSeries.support_expand]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ Function.support ((expand p hp) φ) = (fun x ↦ p • x) '' Function.support φ

Tactic:
rw [expand, MvPowerSeries.support_expand]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
h : (rTensor N P.subtype) t = (rTensor N P.subtype) 0
⊢ ∃ Q, ∃ (hPQ : P ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = 0

Tactic:
simpa only [map_zero] using TensorProduct.eq_of_fg_of_subtype_eq hP h

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
ht : t ∈ (rTensor M A.val.toLinearMap).range
⊢ ∃ s, (rTensor M φ.toLinearMap) s = t

Tactic:
obtain ⟨u, hu⟩ := ht
  suffices h_surj : Function.Surjective ((φ.rangeRestrict.toLinearMap).rTensor M) by
    obtain ⟨p, hp⟩ := h_surj ((Subalgebra.inclusion hφ).toLinearMap.rTensor M u)
    use p
    rw [← hu, ← Subalgebra.val_comp_inclusion hφ, comp_toLinearMap, rTensor_comp,
      LinearMap.comp_apply, ← hp, ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]
    simp
  exact rTensor_surjective M (rangeRestrict_surjective φ)

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
eqbot : ¬p = ⊥
⊢ IsRegularLocalRing (Localization.AtPrime p)

Tactic:
have := IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain
      R eqbot (Localization.AtPrime p)

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
eqbot : ¬p = ⊥
this : IsDiscreteValuationRing (Localization.AtPrime p)
⊢ IsRegularLocalRing (Localization.AtPrime p)
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
M : Type u_1
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
x : S
hx✝ : x ∈ (φ R s).range
hx : x ∈ Algebra.adjoin R ↑s
⊢ h x ∈ Subalgebra.map h (Algebra.adjoin R ↑s)

Tactic:
exact ⟨x, hx, rfl⟩

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n✝ n : ℕ
S : ShortComplex (ModuleCat R) := M.smulShortComplex x
hS : S.ShortExact
h : HasProjectiveDimensionLE (of R (QuotSMulTop x ↑M)) (n + 1)
L : ModuleCat R
a✝ : Module.Finite R ↑L
zero : Subsingleton (Ext (of R (QuotSMulTop x ↑M)) L (n + 2))
exac :
  { X₁ := AddCommGrpCat.of (Ext S.X₂ L (n + 1)), X₂ := AddCommGrpCat.of (Ext S.X₁ L (n + 1)),
      X₃ := AddCommGrpCat.of (Ext S.X₃ L (n + 2)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp L ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp L ⋯), zero := ⋯ }.Exact
this✝ : S.f = x • 𝟙 M
epi : Function.Surjective ⇑((Ext.mk₀ (x • 𝟙 M)).precomp L ⋯)
ntr : Nontrivial (Ext M L (n + 1))
this : x ∈ (annihilator R (Ext M L (n + 1))).jacobson
y : Ext M L (n + 1)
hy : y ∈ ⊤
z : Ext (M.smulShortComplex x).X₂ L (n + 1)
hz : ((Ext.mk₀ (x • 𝟙 M)).precomp L ⋯) z = y
⊢ y ∈ x • ⊤

Tactic:
simp only [ModuleCat.smulShortComplex, Ext.mk₀_smul,
        Ext.bilinearComp_apply_apply, Ext.smul_comp, Ext.mk₀_id_comp] at hz

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n✝ n : ℕ
S : ShortComplex (ModuleCat R) := M.smulShortComplex x
hS : S.ShortExact
h : HasProjectiveDimensionLE (of R (QuotSMulTop x ↑M)) (n + 1)
L : ModuleCat R
a✝ : Module.Finite R ↑L
zero : Subsingleton (Ext (of R (QuotSMulTop x ↑M)) L (n + 2))
exac :
  { X₁ := AddCommGrpCat.of (Ext S.X₂ L (n + 1)), X₂ := AddCommGrpCat.of (Ext S.X₁ L (n + 1)),
      X₃ := AddCommGrpCat.of (Ext S.X₃ L (n + 2)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp L ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp L ⋯), zero := ⋯ }.Exact
this✝ : S.f = x • 𝟙 M
epi : Function.Surjective ⇑((Ext.mk₀ (x • 𝟙 M)).precomp L ⋯)
ntr : Nontrivial (Ext M L (n + 1))
this : x ∈ (annihilator R (Ext M L (n + 1))).jacobson
y : Ext M L (n + 1)
hy : y ∈ ⊤
z : Ext (M.smulShortComplex x).X₂ L (n + 1)
hz : x • z = y
⊢ y ∈ x • ⊤
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
a : A
ha : IsUnit a
⊢ IsUnit (a • h)

Tactic:
Algebra.smul_def

Goal state after:
case refine_1
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
a : A
ha : IsUnit a
⊢ IsUnit ((algebraMap A A⟦X⟧) a * h)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case degree_lt
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ⋯
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ (Polynomial.X ^ n - f).degree < ↑((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) g).order.toNat

pp: case eq_mul_add
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ⋯
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ X ^ n = g * ↑⋯.unit⁻¹ + ↑(Polynomial.X ^ n - f)

Tactic:
· refine (Polynomial.degree_sub_lt_left ?_ (Polynomial.monic_X_pow n).ne_zero ?_).trans_eq
      (by simpa)
    · simp_rw [H.degree_eq_coe_lift_order_map, Polynomial.degree_X_pow, n,
        ENat.lift_eq_toNat_of_lt_top]
    · rw [(Polynomial.monic_X_pow n).leadingCoeff, H.isDistinguishedAt.monic.leadingCoeff]

Goal state after:
case eq_mul_add
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ⋯
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ X ^ n = g * ↑⋯.unit⁻¹ + ↑(Polynomial.X ^ n - f)
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst✝⁹ : CommSemiring R₀
inst✝⁸ : Ring R
inst✝⁷ : Algebra R₀ R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R S
inst✝ : IsSimpleModule R S
s : Set ↑(isotypicComponents R M)
c : ↑(isotypicComponents R M)
hc : c ∈ {c | ↑c ≤ ↑(⨆ c ∈ s, ⟨↑c, ⋯⟩)}
hcs : c ∉ s
⊢ ↑(⨆ c ∈ s, ⟨↑c, ⋯⟩) ≤ sSup (isotypicComponents R M \ {↑c})

Tactic:
simp_rw [CompleteSublattice.coe_iSup, iSup₂_le_iff]
      exact fun c hc ↦ le_sSup ⟨c.2, Subtype.coe_ne_coe.mpr (ne_of_mem_of_not_mem hc hcs)⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R S
L : Type u_5
inst✝⁴ : Field L
inst✝³ : Algebra R L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R K L
inst✝ : IsPurelyInseparable K L
⊢ IsHomeomorph (comap (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S)).toRingHom)

Tactic:
by
  let e : (L ⊗[R] S) ≃ₐ[K] L ⊗[K] (K ⊗[R] S) :=
    (Algebra.TensorProduct.cancelBaseChange R K K L S).symm
  let e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] (K ⊗[R] S) ⊗[K] L := Algebra.TensorProduct.comm ..
  have heq : Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) =
      (e.symm.toAlgHom.comp e2.symm.toAlgHom).comp
        (IsScalarTower.toAlgHom K (K ⊗[R] S) ((K ⊗[R] S) ⊗[K] L)) := by
    ext; simp [e, e2]
  rw [heq]
  simp only [AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom,
    AlgEquiv.toAlgHom_toRingHom, IsScalarTower.coe_toAlgHom, comap_comp]
  exact (isHomeomorph_comap_of_isPurelyInseparable K L (K ⊗[R] S)).comp <|
    (isHomeomorph_comap_of_bijective e2.symm.bijective).comp <|
    isHomeomorph_comap_of_bijective e.symm.bijective

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : Associated a b
⊢ (if Squarefree a then (-1) ^ (factors a).card else 0) = if Squarefree b then (-1) ^ (factors b).card else 0

Tactic:
h.squarefree_iff,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : Associated a b
⊢ (if Squarefree b then (-1) ^ (factors a).card else 0) = if Squarefree b then (-1) ^ (factors b).card else 0
Module: Mathlib.RingTheory.Valuation.Quotient

Goal state before:
pp: case a.mk
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x✝ : R ⧸ J
x : R
hx : Quot.mk (⇑(Submodule.quotientRel J)) x ∈ (v.onQuot hJ).supp
⊢ Quot.mk (⇑(Submodule.quotientRel J)) x ∈ ⇑(Ideal.Quotient.mk J) '' ↑v.supp

Tactic:
exact ⟨x, hx, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (0, n + 1)) *
      ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) *
            ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (1, n + 1) *
          ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      remainder p n

Tactic:
conv_lhs =>
    arg 2
    rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (0, n + 1)) *
      (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (1, n + 1)) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) *
            ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (1, n + 1) *
          ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      remainder p n
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: case succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
⊢ succNthVal p n a₁ a₂ (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂))))
        (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (mk p (frobeniusRotationCoeff p ha₁ ha₂))) (truncateFun (n + 1) a₂)

Tactic:
have :=
      succNthVal_spec' p n a₁ a₂ (fun i : Fin (n + 1) => frobeniusRotationCoeff p ha₁ ha₂ i.val)
        ha₁ ha₂

Goal state after:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
this :
  succNthVal p n a₁ a₂ (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (frobeniusRotationCoeff p ha₁ ha₂ ↑0 ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun v ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * frobeniusRotationCoeff p ha₁ ha₂ ↑0 ^ p ^ (n + 1) +
      nthRemainder p n (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) (truncateFun (n + 1) a₂)
⊢ succNthVal p n a₁ a₂ (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂))))
        (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (mk p (frobeniusRotationCoeff p ha₁ ha₂))) (truncateFun (n + 1) a₂)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (remainder p n).vars ⊆ univ ×ˢ range (n + 1)

pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (wittPolyProdRemainder p (n + 1)).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
· apply remainder_vars

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (wittPolyProdRemainder p (n + 1)).vars ⊆ univ ×ˢ range (n + 1)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (polyOfInterest p n).vars =
    (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars

Tactic:
rw [polyOfInterest, this, vars_C_mul]

Goal state after:
case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ ↑p ^ (n + 1) ≠ 0
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
⊢ IsClub (⋂₀ s)

Tactic:
cases isEmpty_or_nonempty α; · simp
  cases topOrderOrNoTopOrder α
  · exact .sInter_of_orderTop hs
  · cases one_lt_cof.not_ge hα

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := ⋯
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
n : ℕ
⊢ ¬IsCofinal (range fun x ↦ f x (Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) n))

Tactic:
exact fun hg' ↦ (cof_le hg').not_gt (mk_range_le.trans_lt hsα)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hs : ∀ x ∈ s, IsClub x
hα : cof α < ℵ₀
⊢ IsClub (⋂₀ s)

Tactic:
apply IsClub.sInter_of_cof_le_one _ hs

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hs : ∀ x ∈ s, IsClub x
hα : cof α < ℵ₀
⊢ cof α ≤ 1
Module: Mathlib.SetTheory.Cardinal.EventuallyConst

Goal state before:
pp: α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
f : α → β
inst✝ : Nonempty α
hf : Monotone f
hf' : ¬IsCofinal (range (rangeSplitting f))
i : α
hi : ∀ y ∈ range (rangeSplitting f), y < i
⊢ ∃ i, ∀ (j : α), i ≤ j → f j = f i

Tactic:
refine ⟨i, fun j hij ↦ (hf hij).antisymm' <| (hf (hi _ ⟨⟨f j, j, rfl⟩, rfl⟩).le).trans' ?_⟩

Goal state after:
α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
f : α → β
inst✝ : Nonempty α
hf : Monotone f
hf' : ¬IsCofinal (range (rangeSplitting f))
i : α
hi : ∀ y ∈ range (rangeSplitting f), y < i
j : α
hij : i ≤ j
⊢ f j ≤ f (rangeSplitting f ⟨f j, ⋯⟩)
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: case refine_1
x✝ : ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
⊢ univ.{v, u + 1} < univ.{u, v + 1}

Tactic:
univ_umax.{v, u},

Goal state after:
case refine_1
x✝ : ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, u} ≤ lift.{v + 1, u} #α
⊢ univ.{v, u + 1} < univ.{u, v + 1}