mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case succ.refine_2
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ Finset.range n.succ ∧ p.coeff x = 0
⊢ p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) = 0

Tactic:
hx.2,

Goal state after:
case succ.refine_2
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ Finset.range n.succ ∧ p.coeff x = 0
⊢ 0 * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) = 0
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
⊢ b = c

Tactic:
nontriviality R

Goal state after:
R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
a✝ : Nontrivial R
⊢ b = c
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: case inr.inr
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z ^ 2
⊢ False

Tactic:
exact z_ne_zero (eq_zero_of_pow_eq_zero (by rwa [key, add_self_eq_zero] at h2))

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
f : R[X]
hf : (map (algebraMap R S) f).Splits
inst✝ : MulAction.IsPretransitive G ↑(f.rootSet S)
h : ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ m.asIdeal)).ncard + 1
hG : ⨆ m, Ideal.inertia G m.asIdeal = ⊤
⊢ Function.Surjective ⇑(MulAction.toPermHom G ↑(f.rootSet S))

Tactic:
apply surjective_of_isSwap_of_isPretransitive'
      (⋃ m : MaximalSpectrum S, m.asIdeal.inertia G)

Goal state after:
case hS1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
f : R[X]
hf : (map (algebraMap R S) f).Splits
inst✝ : MulAction.IsPretransitive G ↑(f.rootSet S)
h : ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ m.asIdeal)).ncard + 1
hG : ⨆ m, Ideal.inertia G m.asIdeal = ⊤
⊢ ∀ σ ∈ ⋃ m, ↑(Ideal.inertia G m.asIdeal),
    (MulAction.toPermHom G ↑(f.rootSet S)) σ = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) σ).IsSwap

case hS2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
f : R[X]
hf : (map (algebraMap R S) f).Splits
inst✝ : MulAction.IsPretransitive G ↑(f.rootSet S)
h : ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ m.asIdeal)).ncard + 1
hG : ⨆ m, Ideal.inertia G m.asIdeal = ⊤
⊢ Subgroup.closure (⋃ m, ↑(Ideal.inertia G m.asIdeal)) = ⊤
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ ↑n.succ • f = ↑n • f + f

Tactic:
simp_rw [HSMul.hSMul, SMul.smul]
    simp only [Nat.cast_succ, Int.cast_add, Int.cast_natCast, Int.cast_one, add_smul, one_smul]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
B : Subalgebra R S
hB : B.FG
⊢ (φ R (Exists.choose hB)).range = B

Tactic:
by simp only [range_φ, hB.choose_spec]

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
⊢ radical n = ∏ p ∈ n.primeFactors, p

Tactic:
simp [radical, primeFactors_eq_natPrimeFactors]

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 : S ⊗[R] M
s : S
⊢ ∃ n ψ p q, (rTensor M ψ.toLinearMap) p = t ∧ ψ q = s

Tactic:
obtain ⟨A, hA, ht⟩ := TensorProduct.Algebra.exists_of_fg t

Goal state after:
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 : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ (rTensor M A.val.toLinearMap).range
⊢ ∃ n ψ p q, (rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
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
reg : IsWeaklyRegular ↑M []
mem : ∀ r ∈ [], r ∈ maximalIdeal R
len : [].length = n + 1
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList [] • ⊤)) = projectiveDimension M + ↑(n + 1)

Tactic:
simp at len

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
S : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup S
inst✝² : Module R M
inst✝¹ : Module R S
inst✝ : IsSemisimpleModule R M
h : IsIsotypicOfType R M S
s : Set (Submodule R M)
e : M ≃ₗ[R] Π₀ (m : ↑s), ↥↑m
left✝ : sSupIndep s
hs : ∀ (m : ↑s), IsSimpleModule R ↥↑m
⊢ ∃ ι, Nonempty (M ≃ₗ[R] ι →₀ S)

Tactic:
classical exact ⟨s, ⟨e.trans (DFinsupp.mapRange.linearEquiv fun m : s ↦ (h m.1).some)
    |>.trans (finsuppLequivDFinsupp R).symm⟩⟩

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
⊢ (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g (↑⋯.unit⁻¹)
    (Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f)

Tactic:
set n := (g.map (IsLocalRing.residue A)).order.toNat with hn
  constructor
  · 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]
  · simp_rw [H.eq_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, Polynomial.coe_sub,
      Polynomial.coe_pow, Polynomial.coe_X, add_sub_cancel]

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_5
inst✝ : Semiring R
I : Ideal R
⊢ Submodule.IsFullyInvariant I ↔ I.IsTwoSided

Tactic:
by
  simpa only [Submodule.IsFullyInvariant, ← MulOpposite.opEquiv.trans (RingEquiv.moduleEndSelf R
    |>.toEquiv) |>.forall_congr_right, SetLike.le_def, I.isTwoSided_iff] using! forall_comm

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

Goal state before:
pp: R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : IsBaseChange S h₁
isb₂ : IsBaseChange S h₂
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
⊢ IsBaseChange S h₃

Tactic:
simp only [IsBaseChange, IsTensorProduct] at isb₁ isb₂ ⊢

Goal state after:
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)))
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
⊢ Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₃ →ₗ[R] N₃))).flip h₃)))
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: case zero
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung)^[n] b ≠ 0
ha0 : (⇑verschiebung)^[0] a ≠ 0
hab : ↑p = (⇑verschiebung)^[0] a * (⇑verschiebung)^[n] b
⊢ IsUnit ((⇑verschiebung)^[0] a) ∨ IsUnit ((⇑verschiebung)^[n] b)

pp: case succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung)^[n] b ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
hab : ↑p = (⇑verschiebung)^[n✝ + 1] a * (⇑verschiebung)^[n] b
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n] b)

Tactic:
· exact Or.inl (isUnit_of_coeff_zero_ne_zero a ha)

Goal state after:
case succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung)^[n] b ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
hab : ↑p = (⇑verschiebung)^[n✝ + 1] a * (⇑verschiebung)^[n] b
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n] b)
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun v ↦ bs v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
      nthRemainder p n bs (truncateFun (n + 1) a₂)

Tactic:
rw [← sub_eq_zero]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
        nthRemainder p n (fun v ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
      (succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
⊢ TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k

Tactic:
by
    intro x y
    apply f₀
    rintro ⟨a, ha⟩
    apply Function.uncurry ![x, y]
    let S : Set (Fin 2 × ℕ) := { a | a.2 = n ∨ a.2 < n }
    have ha' : a ∈ S := by grind
    refine ⟨a.fst, ⟨a.snd, ?_⟩⟩
    obtain ⟨ha, ha⟩ := ha' <;> lia

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

Goal state before:
pp: case h
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
⊢ Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)

Tactic:
let F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := by
    refine LinearEquiv.ofBijective F₀ ⟨?_, ?_⟩
    · rw [← LinearMap.ker_eq_bot]
      exact LinearMap.ker_toSpanSingleton K(p, k) hx
    · rw [← LinearMap.range_eq_top]
      rw [← (finrank_eq_one_iff_of_nonzero x hx).mp h_dim]
      rw [LinearMap.span_singleton_eq_range]

Goal state after:
case h
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
⊢ Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
ι : Type u_1
f : ι → Set α
hα : cof α ≤ 1
hs : ∀ (i : ι), IsClub (f i)
⊢ IsClub (⋂ i, f i)

Tactic:
rw [← sInter_range]
  exact .sInter_of_cof_le_one hα (by simpa)

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

Goal state before:
pp: case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hα : ℵ₀ < cof α
⊢ IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x

Tactic:
apply isStationary_sUnion_iff hα.ne' (hα.trans_le' _)
    rwa [le_aleph0_iff_set_countable]

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
h : IsOpen[inst✝³] {a}
ha : IsSuccLimit a
l u : α
h₁ : a ∈ Ioo l u
h₂ : Ioo l u ⊆ {a}
⊢ l ⋖ a

Tactic:
rw [← succ_eq_iff_covBy]

Goal state after:
case refine_1
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
h : IsOpen[inst✝³] {a}
ha : IsSuccLimit a
l u : α
h₁ : a ∈ Ioo l u
h₂ : Ioo l u ⊆ {a}
⊢ Order.succ l = a
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
h : AccPt a (𝓟 s)
⊢ IsSuccLimit a

Tactic:
by
  rw [isSuccLimit_iff, IsSuccPrelimit]
  simp_rw [accPt_principal, Set.Nonempty] at h
  grind [covBy_iff_Ioo_eq]

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

Goal state before:
pp: x✝ y z x : ZFSet.{u}
a : PSet.{u}
f : a.Type → ↥(mk a) := fun i ↦ ⟨mk (a.Func i), ⋯⟩
⊢ Function.Surjective f

Tactic:
rintro ⟨y, hb⟩

Goal state after:
x✝ y✝ z x : ZFSet.{u}
a : PSet.{u}
f : a.Type → ↥(mk a) := fun i ↦ ⟨mk (a.Func i), ⋯⟩
y : ZFSet.{u}
hb : y ∈ mk a
⊢ ∃ a_1, f a_1 = ⟨y, hb⟩
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a.inr
x y y✝ : PSet.{u_1}
h : y✝ ∈ y
⊢ y✝.rank < max (succ x.rank) y.rank

Tactic:
simp [rank_lt_of_mem h]

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

Goal state before:
pp: case neg
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ω ^ e.repr = ω ^ 1 * ω ^ (e.repr - 1)
⊢ ((e - 1).oadd n a').NF ∧ ω ^ e.repr * ↑↑n + (ω * a'.repr + ↑m') = ω * ((e - 1).oadd n a').repr + ↑m'

Tactic:
refine ⟨NF.oadd (by infer_instance) _ ?_, ?_⟩

Goal state after:
case neg.refine_1
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ω ^ e.repr = ω ^ 1 * ω ^ (e.repr - 1)
⊢ a'.NFBelow (e - 1).repr

case neg.refine_2
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ω ^ e.repr = ω ^ 1 * ω ^ (e.repr - 1)
⊢ ω ^ e.repr * ↑↑n + (ω * a'.repr + ↑m') = ω * ((e - 1).oadd n a').repr + ↑m'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
hd : α
⊢ FriendlyOperation (Seq.cons hd)

Tactic:
by
  simp only [friendlyOperation_iff_dist_le_dist, dist_cons_cons]
  intro x y
  linarith [dist_nonneg (x := x) (y := y)]

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

Goal state before:
pp: o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
rcases e₁ : split o₁ with ⟨a, m⟩
  obtain ⟨N₁, r₁⟩ := nf_repr_split e₁
  obtain - | ⟨a0, n, a'⟩ := a
  #adaptation_note /-- Proof repaired after leanprover/lean4#13363.
  The next block was previously
  ```
  · rcases m with - | m
    · by_cases h : o₂ = 0
      · simp [opow_def, opowAux2, e₁, h, r₁]
      · simpa [opow_def, opowAux2, e₁, h, r₁, eqComm] using mt repr_inj.1 h
    · rcases e₂ : split' o₂ with ⟨b', k⟩
      obtain ⟨_, r₂⟩ := nf_repr_split' e₂
      by_cases h : m = 0
      · simp [opowAux2, opow_def, e₁, h, r₁, r₂]
      simp only [opow_def, opowAux2, e₁, r₁, e₂, r₂, repr,
          Nat.cast_succ, _root_.zero_add,
          add_zero]
  ```
  The replacement proof is a short-term fix, and we request that the authors/maintainers of
  this file review the proof, and either approve it by removing this note, revise
  the proof or the prerequisites appropriately, or minimize a problem in lean4 that still
  needs addressing. -/
  · rcases m with - | m
    · have hzero : (0 : ONote) = zero := rfl
      by_cases h : o₂ = 0
      · subst h; simp [-zero_def, opow_def, opowAux2, e₁, r₁, hzero]
      · have h' := mt repr_inj.1 h
        have hne : o₂ ≠ zero := fun he => h (he ▸ rfl)
        simp [-zero_def, opow_def, opowAux2, e₁, r₁, hne, hzero]
        exact (zero_opow h').symm
    · rcases e₂ : split' o₂ with ⟨b', k⟩
      obtain ⟨_, r₂⟩ := nf_repr_split' e₂
      by_cases h : m = 0
      · simp only [opowAux2, opow_def, e₁, h, r₁, r₂, OfNat.ofNat, Zero.zero, One.one,
          repr]
        simp [opow_add, opow_mul]
      simp only [opow_def, opowAux2, e₁, r₁, e₂, r₂, repr,
          Nat.cast_succ, _root_.zero_add, add_zero]
      rw [opow_add, opow_mul, opow_omega0]
      · simp
      · simpa [Nat.one_le_iff_ne_zero]
      · rw [← Nat.cast_succ, lt_omega0]
        exact ⟨_, rfl⟩
  · have := N₁.fst
    have := N₁.snd
    obtain ⟨a00, ad⟩ := N₁.of_dvd_omega0 (split_dvd e₁)
    have al := split_add_lt e₁
    have aa : repr (a' + ofNat m) = repr a' + m := by
      simp only [ONote.repr_ofNat, ONote.repr_add]
    rcases e₂ : split' o₂ with ⟨b', k⟩
    obtain ⟨_, r₂⟩ := nf_repr_split' e₂
    simp only [opow_def, e₁, r₁, split_eq_scale_split' e₂, opowAux2, repr]
    rcases k with - | k
    · simp [r₂, opow_mul, repr_opow_aux₁ a00 al aa, add_assoc]
    · simp [r₂, opow_add, opow_mul, mul_assoc, add_assoc, repr_one]
      rw [repr_opow_aux₁ a00 al aa, scale_opowAux]
      simp only [repr_mul, repr_scale, repr_one,
        Nat.cast_one, opow_one, opow_mul]
      rw [← mul_add, ← add_assoc ((ω : Ordinal.{0}) ^ repr a0 * (n : ℕ))]
      congr 1
      rw [← pow_succ, ← opow_natCast, ← opow_natCast]
      exact (repr_opow_aux₂ _ ad a00 al _ _).2

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons
exps_hd : ℝ
basis_hd : ℝ → ℝ
h_nonzero : exps_hd ≠ 0
e : ℝ
es : List ℝ
ih :
  ∀ {basis_tl : Basis},
    (∀ b ∈ basis_tl, (log ∘ b) =o[atTop] (log ∘ basis_hd)) → toLogFun es basis_tl =o[atTop] (log ∘ basis_hd)
b : ℝ → ℝ
bs : List (ℝ → ℝ)
hlo : ∀ b_1 ∈ b :: bs, (log ∘ b_1) =o[atTop] (log ∘ basis_hd)
⊢ toLogFun (e :: es) (b :: bs) =o[atTop] (log ∘ basis_hd)

Tactic:
exact (IsLittleO.const_mul_left (hlo b (by simp)) e).add (ih (by grind))

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

Goal state before:
pp: case seq
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < ↑exp
h_tl_coef : ∀ x ∈ (mk tl 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk tl 0).seq
⊢ (Multiseries.cons exp coef tl).Sorted

Tactic:
| seq _ h_tl_coef h_tl_tl =>

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_exps : exps.FirstNonzeroIsNeg
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (fun a ↦ t.coef * t.unit.toFun basis a) atTop (𝓝 0)

Tactic:
convert Filter.Tendsto.const_mul _
    (UnitMonomial.toFun_tendsto_zero_of_firstNonzeroIsNeg h_basis h_length h_exps)

Goal state after:
case e'_5
coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_exps : exps.FirstNonzeroIsNeg
t : Monomial := { coef := coef, unit := exps }
⊢ 0 = t.coef * 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case a
α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
this : ∀ (n : ℕ), dist s t ≤ 2⁻¹ ^ n
⊢ dist s t ≤ 0

pp: case a
α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
this : ∀ (n : ℕ), dist s t ≤ 2⁻¹ ^ n
⊢ 0 ≤ dist s t

Tactic:
· apply ge_of_tendsto' (x := Filter.atTop) _ this
      rw [tendsto_pow_atTop_nhds_zero_iff]
      norm_num

Goal state after:
case a
α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
this : ∀ (n : ℕ), dist s t ≤ 2⁻¹ ^ n
⊢ 0 ≤ dist s t