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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ ∑ x ∈ range n,
      (C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x) * C (⅟↑p ^ n) -
        C (↑p ^ x) * X x ^ p ^ (n + 1 - x) * C (⅟↑p ^ n)) =
    ∑ x ∈ range n,
      ∑ i ∈ range (p ^ (n - x)),
        C ↑p *
          (MvPolynomial.map (Int.castRingHom ℚ))
            ((X x ^ p) ^ (p ^ (n - x) - (i + 1)) * frobeniusPolyAux p x ^ (i + 1) *
              C ↑((p ^ (n - x)).choose (i + 1) / p ^ (n - x - v p (i + 1)) * p ^ (i - v p (i + 1))))

Tactic:
apply sum_congr rfl

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ ∀ x ∈ range n,
    C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x) * C (⅟↑p ^ n) -
        C (↑p ^ x) * X x ^ p ^ (n + 1 - x) * C (⅟↑p ^ n) =
      ∑ i ∈ range (p ^ (n - x)),
        C ↑p *
          (MvPolynomial.map (Int.castRingHom ℚ))
            ((X x ^ p) ^ (p ^ (n - x) - (i + 1)) * frobeniusPolyAux p x ^ (i + 1) *
              C ↑((p ^ (n - x)).choose (i + 1) / p ^ (n - x - v p (i + 1)) * p ^ (i - v p (i + 1))))
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ (-x✝).coeff n = (aeval x✝.coeff) ((fun n ↦ (rename Prod.snd) (wittNeg p n)) n)

Tactic:
neg_coeff,

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ peval (wittNeg p n) ![x✝.coeff] = (aeval x✝.coeff) ((fun n ↦ (rename Prod.snd) (wittNeg p n)) n)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case neg
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
hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
s : O
hy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) (r + s) = 0
⊢ v ((algebraMap O K) r + (algebraMap O K) s) ≤ max (v ((algebraMap O K) r)) (v ((algebraMap O K) s))

Tactic:
exact v.map_add _ _

Goal state after:
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
⊢ ∑ i_1 ∈ range (p ^ (n - i)),
      C (↑p ^ i) *
          ((C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (i_1 + 1) *
              (X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) *
            ↑((p ^ (n - i)).choose (i_1 + 1))) *
        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:
apply sum_congr rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPoly p n) = frobeniusPolyRat p n

Tactic:
by
  rw [frobeniusPoly, map_add, map_mul, map_pow, map_C, map_X, eq_intCast, Int.cast_natCast,
    frobeniusPolyRat]
  refine Nat.strong_induction_on n ?_; clear n
  intro n IH
  rw [xInTermsOfW_eq]
  simp only [map_sum, map_sub, map_mul, map_pow (bind₁ _), bind₁_C_right]
  have h1 : (p : ℚ) ^ n * ⅟(p : ℚ) ^ n = 1 := by rw [← mul_pow, mul_invOf_self, one_pow]
  rw [bind₁_X_right, Function.comp_apply, wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ,
    sum_range_succ, tsub_self, add_tsub_cancel_left, pow_zero, pow_one, pow_one, sub_mul, add_mul,
    add_mul, mul_right_comm, mul_right_comm (C ((p : ℚ) ^ (n + 1))), ← C_mul, ← C_mul, pow_succ',
    mul_assoc (p : ℚ) ((p : ℚ) ^ n), h1, mul_one, C_1, one_mul, add_comm _ (X n ^ p), add_assoc,
    ← add_sub, add_right_inj, frobeniusPolyAux_eq, map_sub, map_X, mul_sub, sub_eq_add_neg,
    add_comm _ (C (p : ℚ) * X (n + 1)), ← add_sub,
    add_right_inj, neg_eq_iff_eq_neg, neg_sub, eq_comm]
  simp only [map_sum, mul_sum, sum_mul, ← sum_sub_distrib]
  apply sum_congr rfl
  intro i hi
  rw [mem_range] at hi
  rw [← IH i hi]
  clear IH
  rw [add_comm (X i ^ p), add_pow, sum_range_succ', pow_zero, tsub_zero, Nat.choose_zero_right,
    one_mul, Nat.cast_one, mul_one, mul_add, add_mul, Nat.succ_sub (le_of_lt hi),
    Nat.succ_eq_add_one (n - i), pow_succ', pow_mul, add_sub_cancel_right, mul_sum, sum_mul]
  apply sum_congr rfl
  intro j hj
  rw [mem_range] at hj
  rw [map_mul, map_mul, map_pow, map_pow, map_pow, map_pow, map_pow, map_C, map_X, mul_pow]
  rw [mul_comm (C (p : ℚ) ^ i), mul_comm _ ((X i ^ p) ^ _), mul_comm (C (p : ℚ) ^ (j + 1)),
    mul_comm (C (p : ℚ))]
  simp only [mul_assoc]
  apply congr_arg
  apply congr_arg
  rw [← C_eq_coe_nat]
  simp only [← map_pow, ← C_mul]
  rw [C_inj]
  simp only [invOf_eq_inv, eq_intCast, inv_pow, Int.cast_natCast, Nat.cast_mul, Int.cast_mul]
  rw [Rat.natCast_div _ _ (map_frobeniusPoly.key₁ p (n - i) j hj)]
  push_cast
  linear_combination (norm := skip) -p / p ^ n / p ^ (n - i - v p (j + 1))
    * (p ^ (n - i)).choose (j + 1) * congr((p : ℚ) ^ $(map_frobeniusPoly.key₂ p hi.le hj))
  field [hp.1.ne_zero]

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
hp : Nat.Prime p
this : Nontrivial (PreTilt O p)
a✝ b✝ : PreTilt O p
hfg : a✝ * b✝ = 0
⊢ a✝ = 0 ∨ b✝ = 0

Tactic:
by
      simp_rw [← map_eq_zero hv] at hfg ⊢; contrapose! hfg; rw [Valuation.map_mul]
      exact mul_ne_zero hfg.1 hfg.2

Goal state after:
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : 𝕎 (R ⧸ 𝔭)
h : 𝔭 ^ (0 + 1) = 𝔭
⊢ (quotEquivOfEq h) ((ghostComponentModPPow 0) x) = (ghostComponent 0) x

Tactic:
by
  obtain ⟨y, hy⟩ := map_surjective _ Ideal.Quotient.mk_surjective x
  simp [← hy, ghostComponent_apply]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
r : R
| (MvPowerSeries.expand p hp) (r • 1)

Tactic:
AlgHom.map_smul_of_tower,

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
r : R
| r • (MvPowerSeries.expand p hp) 1
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n q : ℕ
hq : n = p * q
⊢ (coeff q) φ = (coeff (p * q / p)) φ

Tactic:
Nat.mul_div_cancel_left _ (p.pos_of_ne_zero hp)

Goal state after:
case pos
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n q : ℕ
hq : n = p * q
⊢ (coeff q) φ = (coeff q) φ
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0

Tactic:
apply sum_congr rfl

Goal state after:
n : ℕ
hn : 0 < n
⊢ ∀ x ∈ range n,
    (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
      if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
this :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
⊢ (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) =
    ∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder

Tactic:
apply sum_congr rfl

Goal state after:
n : ℕ
hn : 0 < n
this :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
⊢ ∀ x ∈ Ico 1 n,
    (if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) = (x - 1).largeSchroder * (n - x).largeSchroder
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
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = ↑r
this : ∀ (k i : ℕ), (coeff i) q ∈ I ^ k
⊢ q = 0 ∧ r = 0

Tactic:
have hq : q = 0 := by
      ext i
      refine IsHausdorff.haus' (I := I) _ fun k ↦ ?_
      rw [SModEq.zero, smul_eq_mul, Ideal.mul_top]
      exact this _ _

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = ↑r
this : ∀ (k i : ℕ), (coeff i) q ∈ I ^ k
hq : q = 0
⊢ q = 0 ∧ r = 0
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n✝ : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
w✝⁴ : Type v
w✝³ : AddCommGroup w✝⁴
w✝² : Module R w✝⁴
w✝¹ : Free R w✝⁴
w✝ : Module.Finite R w✝⁴
f : w✝⁴ →ₗ[R] ↑M
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))) → HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1 + 1))
⊢ HasProjectiveDimensionLT S.X₁ (n + 1)

Tactic:
have (L : ModuleCat.{v} R) : Subsingleton (Ext S.X₁ L (n + 1)) ↔
        Subsingleton (Ext M L (n + 2)) := by
        have (m : ℕ) : Subsingleton (Ext S.X₂ L (m + 1)) := Ext.subsingleton_of_projective S.X₂ L m
        have isi : IsIso (AddCommGrpCat.ofHom (hS.extClass.precomp L (add_comm 1 _))) :=
          (Ext.contravariantSequence_exact hS L (n + 1) (n + 2)
            (add_comm 1 _)).isIso_map' 1 (by decide)
              ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_src _)
                ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_tgt _)
        exact (asIso (AddCommGrpCat.ofHom (hS.extClass.precomp L
          (add_comm 1 _)))).addCommGroupIsoToAddEquiv.subsingleton_congr

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n✝ : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
w✝⁴ : Type v
w✝³ : AddCommGroup w✝⁴
w✝² : Module R w✝⁴
w✝¹ : Free R w✝⁴
w✝ : Module.Finite R w✝⁴
f : w✝⁴ →ₗ[R] ↑M
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))) → HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1 + 1))
this : ∀ (L : ModuleCat R), Subsingleton (Ext S.X₁ L (n + 1)) ↔ Subsingleton (Ext M L (n + 2))
⊢ HasProjectiveDimensionLT S.X₁ (n + 1)
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
peq : p = span (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})
⊢ ↑(Submodule.spanFinrank
        (span
          (⇑(algebraMap R[X] (Localization.AtPrime p)) ''
            (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})))) ≤
    ringKrullDim (Localization.AtPrime p)

Tactic:
← maximalIdeal_height_eq_ringKrullDim,

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
peq : p = span (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})
⊢ ↑(Submodule.spanFinrank
        (span
          (⇑(algebraMap R[X] (Localization.AtPrime p)) ''
            (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})))) ≤
    ↑(maximalIdeal (Localization.AtPrime p)).height
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
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R),
    IsWeaklyRegular (↑M) rs →
      (∀ r ∈ rs, r ∈ maximalIdeal R) →
        rs.length = n → projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑n
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
x : R
rs' : List R
mem : x ∈ maximalIdeal R ∧ ∀ a ∈ rs', a ∈ maximalIdeal R
reg : IsSMulRegular (↑M) x ∧ IsWeaklyRegular (QuotSMulTop x ↑M) rs'
this : Nontrivial (QuotSMulTop x ↑M)
len : rs'.length = n
⊢ projectiveDimension (of R (QuotSMulTop x ↑M ⧸ Ideal.ofList rs' • ⊤)) = projectiveDimension M + (↑n + 1)

Tactic:
add_comm _ 1,

Goal state after:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Small.{v, u} R
inst✝³ : IsLocalRing R
inst✝² : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R),
    IsWeaklyRegular (↑M) rs →
      (∀ r ∈ rs, r ∈ maximalIdeal R) →
        rs.length = n → projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑n
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
x : R
rs' : List R
mem : x ∈ maximalIdeal R ∧ ∀ a ∈ rs', a ∈ maximalIdeal R
reg : IsSMulRegular (↑M) x ∧ IsWeaklyRegular (QuotSMulTop x ↑M) rs'
this : Nontrivial (QuotSMulTop x ↑M)
len : rs'.length = n
⊢ projectiveDimension (of R (QuotSMulTop x ↑M ⧸ Ideal.ofList rs' • ⊤)) = projectiveDimension M + (1 + ↑n)
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:
rw [Algebra.smul_def]
    exact (ha.map _).mul H.isUnit

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ I.ringCon (s.sum f) 0

Tactic:
← Finset.sum_const_zero

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ I.ringCon (s.sum f) (∑ _x ∈ ?m.23, 0)

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Type ?u.28

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Finset ?m.21
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree = ↑p

Tactic:
degree_sub_eq_left_of_degree_lt,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p

p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ (X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree < (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree
Module: Mathlib.SetTheory.Cardinal.NatCount

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ↑(count p n) ≤ Cardinal.mk ↑{k | p k}

Tactic:
count_eq_card_fintype,

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ↑(Fintype.card { k // k < n ∧ p k }) ≤ Cardinal.mk ↑{k | p k}
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : α
l₂ : Lists α
⊢ ∀ ⦃l₃ : Lists α⦄, atom a ~ l₂ → l₂ ~ l₃ → atom a ~ l₃

Tactic:
l₃

Goal state after:
case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : α
l₂ l₃ : Lists α
⊢ atom a ~ l₂ → l₂ ~ l₃ → atom a ~ l₃
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂ : Lists α
⊢ ∀ ⦃l₃ : Lists α⦄, of' l₁ ~ l₂ → l₂ ~ l₃ → of' l₁ ~ l₃

Tactic:
l₃

Goal state after:
case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂ l₃ : Lists α
⊢ of' l₁ ~ l₂ → l₂ ~ l₃ → of' l₁ ~ l₃
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
⊢ lfpApprox f x o = x ↔ f x = x ∨ o = 0

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Goal state after:
case refine_1
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : lfpApprox f x o = x
⊢ f x = x ∨ o = 0

case refine_2
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : f x = x ∨ o = 0
⊢ lfpApprox f x o = x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ e.repr < b

Tactic:
exact h₃

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

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ eval b (coeff b o) = o

Tactic:
conv_rhs => rw [← CNF.foldr b o]

Goal state after:
b o : Ordinal.{u_1}
⊢ eval b (coeff b o) = foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o)
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: x y z : PSet.{?u.3}
hxy : x ⊆ y
hyz : y ⊆ z
a : x.Type
b : y.Type
hb : (x.Func a).Equiv (y.Func b)
c : z.Type
hc : (y.Func b).Equiv (z.Func c)
⊢ ∃ b, (x.Func a).Equiv (z.Func b)

Tactic:
exact ⟨c, hb.trans hc⟩

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

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
⊢ Decidable (e.oadd n a).NF

Tactic:
by
    have := decidableNF e
    have := decidableNF a
    apply decidable_of_iff (NF e ∧ NF a ∧ TopBelow e a)
    rw [← and_congr_right fun h => @nfBelow_iff_topBelow _ h _]
    exact ⟨fun ⟨h₁, h₂⟩ => NF.oadd h₁ n h₂, fun h => ⟨h.fst, h.snd'⟩⟩

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : o ≠ 0
⊢ a ∈ range (veblenWith f o) ↔ ∀ b < o, veblenWith f b a = a

Tactic:
veblenWith_of_ne_zero f h,

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : o ≠ 0
⊢ a ∈ range (derivFamily fun x ↦ veblenWith f ↑x) ↔ ∀ b < o, veblenWith f b a = a
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c✝ : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, (Γ a).Equiv (Δ b)
δγ : ∀ (b : δ), ∃ a, (Γ a).Equiv (Δ b)
c : (A a).Type := c✝
⊢ γ

Tactic:
rwa [ea] at c

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

Goal state before:
pp: x y : ZFSet.{u_1}
H : {x} = {y}
this : ⋃₀ {x} = ⋃₀ {y} := congr_arg sUnion H
⊢ x = y

Tactic:
rwa [sUnion_singleton, sUnion_singleton] at this

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ω ^ ε_ o = ε_ o

Tactic:
rw [epsilon_eq_deriv, deriv_fp (isNormal_opow one_lt_omega0)]

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

Goal state before:
pp: case a
x y : ZFSet.{u_1}
⊢ (x ∪ y).rank ≤ max x.rank y.rank

Tactic:
simp_rw [rank_le_iff, mem_union, lt_max_iff]

Goal state after:
case a
x y : ZFSet.{u_1}
⊢ ∀ ⦃y_1 : ZFSet.{u_1}⦄, y_1 ∈ x ∨ y_1 ∈ y → y_1.rank < x.rank ∨ y_1.rank < y.rank
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u}
⊢ (V_ o).card = preBeth o

Tactic:
by
  induction o using Ordinal.limitRecOn with
  | zero => simp
  | add_one o ih => simp [ih]
  | limit o ho ih =>
    simp_rw [preBeth_limit ho.isSuccPrelimit, ← fun i : Set.Iio o => ih i i.2,
      vonNeumann_of_isSuccPrelimit ho.isSuccPrelimit]
    apply iSup_card_le_card_iUnion.antisymm'
    rw [← lift_le.{u + 1}]
    apply lift_card_iUnion_le_sum_card.trans
    refine (sum_eq_lift_iSup_of_lift_mk_le_lift_iSup ?_ ?_).le
    · rw [mk_Iio_ordinal, ← lift_aleph0.{u + 1, u}, lift_le, Ordinal.aleph0_le_card]
      exact Ordinal.omega0_le_of_isSuccLimit ho
    · rw [mk_Iio_ordinal, lift_lift, lift_le]
      by_contra! h
      refine (⨆ i : Set.Iio o, (V_ ↑i).card).card_ord.not_lt <|
        (Ordinal.card_le_card_vonNeumann _).trans_lt <| (cantor _).trans_le ?_
      rw [← card_powerset, ← vonNeumann_add_one]
      refine le_ciSup bddAbove_of_small (⟨_, ho.succ_lt ?_⟩ : Set.Iio o)
      exact (ord_card_le _).trans_lt' (ord_strictMono h)

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
exp f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
hf_exp : f_exp ≤ exp
hg_exp : g_exp ≤ exp
exp' : ℝ
h_exp' : exp' > exp
⊢ exp' > f_exp

Tactic:
by order

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
exp f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
hf_exp : f_exp ≤ exp
hg_exp : g_exp ≤ exp
exp' : ℝ
h_exp' : exp' > exp
⊢ exp' > g_exp

Tactic:
by order

Goal state after: