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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ C (↑p ^ i) *
          (∑ k ∈ range (p ^ (n - i)),
              (C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (k + 1) *
                  (X i ^ p) ^ (p ^ (n - i) - (k + 1)) *
                ↑((p ^ (n - i)).choose (k + 1)) +
            1 * (X i ^ p) ^ p ^ (n - i) * ↑((p ^ (n - i)).choose 0)) *
        C (⅟↑p ^ n) -
      C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * C (⅟↑p ^ n) =
    ∑ i_1 ∈ range (p ^ (n - i)),
      C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
            C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))))

Tactic:
Nat.choose_zero_right,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ C (↑p ^ i) *
          (∑ k ∈ range (p ^ (n - i)),
              (C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (k + 1) *
                  (X i ^ p) ^ (p ^ (n - i) - (k + 1)) *
                ↑((p ^ (n - i)).choose (k + 1)) +
            1 * (X i ^ p) ^ p ^ (n - i) * ↑1) *
        C (⅟↑p ^ n) -
      C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * C (⅟↑p ^ n) =
    ∑ i_1 ∈ range (p ^ (n - i)),
      C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
            C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))))
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ verschiebung (frobenius x) = x * ↑p

Tactic:
by
  ext ⟨i⟩
  · rw [mul_charP_coeff_zero, verschiebung_coeff_zero]
  · rw [mul_charP_coeff_succ, verschiebung_coeff_succ, coeff_frobenius_charP]

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ frobeniusFun 0 = 0

Tactic:
by
    refine IsPoly.ext (IsPoly.comp (hg := frobeniusFun_isPoly p) (hf := WittVector.zeroIsPoly))
      (IsPoly.comp (hg := WittVector.zeroIsPoly) (hf := frobeniusFun_isPoly p))
      ?_ _ 0
    simp only [Function.comp_apply, map_zero, forall_const]
    ghost_simp

Goal state after:
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
⊢ (truncate n) x = (truncate n) y

pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
h : (truncate n) x = (truncate n) y
i : ℕ
hi : i < n
⊢ x.coeff i = y.coeff i

Tactic:
· ext i
      simp [h i]

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
h : (truncate n) x = (truncate n) y
i : ℕ
hi : i < n
⊢ x.coeff i = y.coeff i
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f h : R⟦X⟧
g : R[X]
distinguish : g.IsDistinguishedAt I
notMem : PowerSeries.constantCoeff h ∉ I
eq : f = ↑g * h
⊢ g.degree = ↑(((PowerSeries.map (Ideal.Quotient.mk I)) f).order.lift ⋯)

Tactic:
by
  have : Nontrivial R := _root_.nontrivial_iff.mpr
    ⟨0, PowerSeries.constantCoeff h, ne_of_mem_of_not_mem I.zero_mem notMem⟩
  rw [Polynomial.degree_eq_natDegree distinguish.monic.ne_zero, Nat.cast_inj, ← ENat.natCast_inj,
    ENat.natCast_lift, Eq.comm, PowerSeries.order_eq_nat]
  have mapf : f.map (Ideal.Quotient.mk I) = (Polynomial.X ^ g.natDegree : (R ⧸ I)[X]) *
      h.map (Ideal.Quotient.mk I) := by
    simp [← map_eq_X_pow distinguish, eq]
  constructor
  · simp [mapf, PowerSeries.coeff_X_pow_mul', eq_zero_iff_mem, notMem]
  · intro i hi
    simp [mapf, PowerSeries.coeff_X_pow_mul', hi]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case succ.zero
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
hnk : Odd (n + Nat.succ 0)
⊢ (hermite (n + 1)).coeff 0 = 0

Tactic:
coeff_hermite_succ_zero,

Goal state after:
case succ.zero
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
hnk : Odd (n + Nat.succ 0)
⊢ -(hermite n).coeff 1 = 0
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case e'_3
n : ℕ
⊢ (-1) ^ (n + 1) * ↑((2 * n + 1) * (2 * n - 1)‼) * ↑((2 * (n + 1) + 0).choose 0) =
    -((-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + 1).choose 1))

Tactic:
Nat.choose_zero_right,

Goal state after:
case e'_3
n : ℕ
⊢ (-1) ^ (n + 1) * ↑((2 * n + 1) * (2 * n - 1)‼) * ↑1 = -((-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + 1).choose 1))
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case e_a.e_a
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ (hermite (2 * (n + 1) + k)).coeff (k + 2) = hermite_explicit n (k + 2)

Tactic:
· rw [(by ring : 2 * (n + 1) + k = 2 * n + (k + 2)), coeff_hermite_explicit n (k + 2)]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ (p * (1 - X)).hilbertPoly (d + 1) = p.hilbertPoly d

Tactic:
by
  apply eq_hilbertPoly_of_forall_coeff_eq_eval (p * (1 - X)).natDegree
  intro n hn
  have heq : 1 - PowerSeries.X = ((1 - X : F[X]) : F⟦X⟧) := by simp only [coe_sub, coe_one, coe_X]
  rw [← one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val F d 1, pow_one, ← mul_assoc, heq,
    ← coe_mul, coeff_mul_invOneSubPow_eq_hilbertPoly_eval (d + 1) hn]

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

Goal state before:
pp: case e'_3
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
hroots : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
p : R[X] := C a * X ^ 2 + C b * X + C c
⊢ 2 = {x1, x2}.card

Tactic:
Multiset.card_pair

Goal state after:
case e'_3
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
hroots : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
p : R[X] := C a * X ^ 2 + C b * X + C c
⊢ 2 = 2
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
hroots : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
p : R[X] := C a * X ^ 2 + C b * X + C c
hp_natDegree : p.natDegree = 2
⊢ {x1, x2}.card = 2

Tactic:
Multiset.card_pair

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
hroots : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
p : R[X] := C a * X ^ 2 + C b * X + C c
hp_natDegree : p.natDegree = 2
⊢ 2 = 2
Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
I J : Ideal A
f g : A⟦X⟧
n : ℕ
hf : ∀ i ≤ n, (coeff i) f ∈ I
hg : ∀ i ≤ n, (coeff i) g ∈ J
i : ℕ
hi : i ≤ n
⊢ (coeff i) (f * g) ∈ I * J

Tactic:
rw [coeff_mul]
  exact Ideal.sum_mem _ fun p hp ↦ Ideal.mul_mem_mul
    (hf _ ((Finset.HasAntidiagonal.antidiagonal.fst_le hp).trans hi))
    (hg _ ((Finset.HasAntidiagonal.antidiagonal.snd_le hp).trans hi))

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
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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
u'FG : (φ R s').range.FG
huu' : (rTensor M (φ R s).range.val.toLinearMap) u = (rTensor M (φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (φ R s).range ≤ B
hA'B : (φ R s').range ≤ B
h : (rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = (rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (φ R t).range
hAB' : (φ R s).range ≤ (φ R t).range
hA'B' : (φ R s').range ≤ (φ R t).range
q : MvPolynomial (Fin t.card) R ⊗[R] M
hq :
  (rTensor M (φ R t).rangeRestrict.toLinearMap) q =
    (rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
⊢ (rTensor M ((Subalgebra.inclusion hAB').comp (φ R s).rangeRestrict).toLinearMap) p =
    (rTensor M (φ R t).rangeRestrict.toLinearMap) q

Tactic:
· simp only [hq, hu, ← LinearMap.comp_apply, comp_toLinearMap, rTensor_comp]
    congr; ext; rfl

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
⊢ (coeff i) (H.seq f (k + 1) - H.seq f k) ∈ I ^ k

Tactic:
seq,

Goal state after:
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
⊢ (coeff i)
      (H.seq f k +
          (mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) (f - g * H.seq f k)) * ↑⋯.unit⁻¹ -
        H.seq f k) ∈
    I ^ k
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
⊢ H.seq f 1 = (mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) f) * ↑⋯.unit⁻¹

Tactic:
seq,

Goal state after:
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
⊢ 0 + (mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) (f - g * 0)) * ↑⋯.unit⁻¹ =
    (mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) f) * ↑⋯.unit⁻¹
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
⊢ IsRegularRing R

Tactic:
rw [isRegularRing_iff]
  intro p hp
  by_cases eqbot : p = ⊥
  · let : Field (Localization.AtPrime p) := IsField.toField <| by
      simp [isField_iff_maximalIdeal_eq, ← Localization.AtPrime.map_eq_maximalIdeal, eqbot]
    infer_instance
  · have := IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain
      R eqbot (Localization.AtPrime p)
    infer_instance

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

Goal state before:
pp: case zero
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L 0)
this : Subsingleton (M ⟶ M)
⊢ HasProjectiveDimensionLT M 0

Tactic:
have : Limits.IsZero M := (Limits.IsZero.iff_id_eq_zero M).mpr (Subsingleton.eq_zero (𝟙 M))

Goal state after:
case zero
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L 0)
this✝ : Subsingleton (M ⟶ M)
this : Limits.IsZero M
⊢ HasProjectiveDimensionLT M 0
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
f g : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ toFun S (f + g) t = toFun S f t + toFun S g t

Tactic:
obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
  simp only [Pi.add_apply, toFun_eq_rTensor_φ_toFun' _ ha, add_def, map_add]

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f f' g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ (f + f') /ʷ g = f /ʷ g + f' /ʷ g

Tactic:
simp_rw [weierstrassDiv]

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f f' g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ (if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.div ⋯ (f + f') else 0) =
    (if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.div ⋯ f else 0) +
      if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.div ⋯ f' else 0
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
a : A
f g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ a • f /ʷ g = a • (f /ʷ g)

Tactic:
simp_rw [weierstrassDiv]

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
a : A
f g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ (if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.div ⋯ (a • f) else 0) =
    a • if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.div ⋯ f else 0
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ 0 /ʷ g = 0

Tactic:
simp_rw [weierstrassDiv]

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ (if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.div ⋯ 0 else 0) = 0
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (⋃ i, {x | f.coeff i ∉ x.asIdeal})

Tactic:
exact isOpen_iUnion fun i => isOpen_basicOpen

Goal state after:
Module: Mathlib.RingTheory.Valuation.Minpoly

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : K
⊢ v ((minpoly K ((algebraMap K L) x)).coeff 0) = v x

Tactic:
by
  rw [minpoly.eq_X_sub_C, coeff_sub, coeff_X_zero, coeff_C_zero, zero_sub, Valuation.map_neg]

Goal state after:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ f.ker ⊓ I • ⊤
⊢ x ∈ I • f.ker

pp: case refine_2
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ I • f.ker
⊢ x ∈ f.ker ⊓ I • ⊤

Tactic:
· rcases (Submodule.ext_iff.mp (I.subtype_rTensor_range M) x).mpr hx.2 with ⟨y, hy⟩
    have inj : Function.Injective ((TensorProduct.lid R N).comp (I.subtype.rTensor N)) := by
      simpa using Module.Flat.iff_rTensor_injective'.mp ‹_› I
    have comm1 : ((TensorProduct.lid R N).comp (I.subtype.rTensor N)).comp (f.lTensor I) =
      f.comp ((TensorProduct.lid R M).comp (I.subtype.rTensor M)) := by
      ext
      simp
    have eq0 : f.lTensor I y = 0 := by
      apply inj
      rw [map_zero, ← LinearMap.comp_apply, comm1, LinearMap.comp_apply, hy, f.mem_ker.mp hx.1]
    rcases ((lTensor_exact I (f.exact_subtype_ker_map) surj) y).mp eq0 with ⟨z, hz⟩
    have comm2 : ((TensorProduct.lid R M).comp (I.subtype.rTensor M)).comp
      (f.ker.subtype.lTensor I) = f.ker.subtype.comp
      ((TensorProduct.lid R f.ker).comp (I.subtype.rTensor f.ker)) := by
      ext
      simp
    apply (Submodule.mem_smul_top_iff I f.ker ⟨x, hx.1⟩).mp
    rw [← Ideal.subtype_rTensor_range]
    use z
    apply f.ker.subtype_injective
    rw [← LinearMap.comp_apply, ← comm2, LinearMap.comp_apply, hz, hy, Submodule.subtype_apply]

Goal state after:
case refine_2
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ I • f.ker
⊢ x ∈ f.ker ⊓ I • ⊤
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: case inr
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
this : Subsingleton (ValueGroupWithZero R)ˣ
u : (ValueGroupWithZero R)ˣ
hx : ↑u ≠ 0
hx' : ↑u ≠ 1
⊢ False

Tactic:
· simp_all [Subsingleton.elim u 1]

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

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

Tactic:
rw [← add_sub_assoc, eq_sub_iff_add_eq, mul_polyOfInterest_aux2]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ wittPolyProd p (n + 1) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
      remainder p n
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case refine_1
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ IsClub (⋂ x, f ↑x ⋯)

Tactic:
apply IsClub.iInter hα

Goal state after:
case refine_1.hι
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ lift.{v, v} #↑s < lift.{v, v} (cof α)

case refine_1.hf
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ ∀ (i : ↑s), IsClub (f ↑i ⋯)
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
hx : x ≤ f x
hab : a < b
hac : a ≤ c
hf : lfpApprox f x a = lfpApprox f x b
⊢ lfpApprox f x a ∈ fixedPoints ⇑f

Tactic:
rw [mem_fixedPoints_iff, ← lfpApprox_add_one f hx]

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
hx : x ≤ f x
hab : a < b
hac : a ≤ c
hf : lfpApprox f x a = lfpApprox f x b
⊢ lfpApprox f x (a + 1) = lfpApprox f x a
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2.inr.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hob : o < b
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
rw [CNF.of_lt ho hob]

Goal state after:
case refine_2.inr.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hob : o < b
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst [(0, o)])
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
b : Ordinal.{0}
h : o.NFBelow b
⊢ o.repr < ω ^ b

Tactic:
by
  induction h with
  | zero => exact opow_pos _ omega0_pos
  | oadd' _ _ h₃ _ IH =>
    rw [repr]
    apply (add_lt_add_right IH _).trans_le
    grw [← mul_succ, succ_le_of_lt (natCast_lt_omega0 _), ← opow_succ, succ_le_of_lt h₃]
    exact omega0_pos

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.inr.inr
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
⊢ (a₁.cmp a₂).Compares a₁ a₂ →
    (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)

Tactic:
cases cmp a₁ a₂ <;> intro IHa <;> dsimp at IHa

Goal state after:
case eq.inr.inr.lt
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : a₁ < a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.lt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)

case eq.inr.inr.eq
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : a₁ = a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.eq)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)

case eq.inr.inr.gt
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : a₁ > a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.gt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst✝ : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ out f xs ≈ out f ys

Tactic:
rw [← Quotient.eq_iff_equiv, mk_eq, mk_eq, mk_out, mk_out]
  exact congrArg _ (funext fun i ↦ Quotient.sound (h i))

Goal state after:
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x y : ZFSet.{u}
⊢ lift.{u + 1, u} (insert x y).card ≤ lift.{u + 1, u} (y.card + 1)

Tactic:
simpa [← cardinalMk_coe_sort] using! mk_insert_le

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u_1}
h : x.Nonempty
⊢ y ∈ ZFSet.sep (fun y ↦ ∀ z ∈ x, y ∈ z) (⋃₀ x) ↔ ∀ z ∈ x, y ∈ z

Tactic:
simp only [and_iff_right_iff_imp, mem_sep]

Goal state after:
x y : ZFSet.{u_1}
h : x.Nonempty
⊢ (∀ z ∈ x, y ∈ z) → y ∈ ⋃₀ x
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List ↑(Iio o)
⊢ ∃ b < o, List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ veblenWith f b 0

Tactic:
induction l with
  | nil => use 0; simpa using ho.bot_lt
  | cons a l IH =>
    obtain ⟨b, hb, hb'⟩ := IH
    refine ⟨_, ho.succ_lt (max_lt a.2 hb), ((veblenWith_right_strictMono hf _).monotone <|
      hb'.trans <| veblenWith_left_monotone hf _ <|
        (le_max_right a.1 b).trans (le_succ _)).trans ?_⟩
    rw [veblenWith_veblenWith_of_lt hf]
    rw [lt_succ_iff]
    exact le_max_left _ b

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
z : α
hz : f z = ⟦y⟧
⊢ y.Equiv ((PSet.mk (Shrink.{u, u_1} α) (Quotient.out ∘ f ∘ ⇑(equivShrink α).symm)).Func ((equivShrink α) z))

Tactic:
simpa [hz] using PSet.Equiv.symm (Quotient.mk_out y)

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun w ↦ z.pair w ∈ map f x) y
⊢ y = f z

Tactic:
by
    let ⟨w, _, we⟩ := mem_image.1 yx
    let ⟨wz, fy⟩ := pair_injective we
    rw [← fy, wz]

Goal state after: