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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i ↦
        ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (φ i)))
      (wittPolynomial p ℤ k) =
    (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i ↦
        ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (ψ i)))
      (wittPolynomial p ℤ k)

Tactic:
convert! h using 1

Goal state after:
case e'_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i ↦
        ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (φ i)))
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k)

case e'_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i ↦
        ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (ψ i)))
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k)
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n k : ℕ
⊢ (∑ x ∈ range (n + 1), if k = x then (-1) ^ x * ↑(n.choose x) * ↑((n + x).choose n) else 0) =
    (-1) ^ k * ↑(n.choose k) * ↑((n + k).choose n)

Tactic:
simp +contextual [choose_eq_zero_of_lt]

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
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (rTensor N P.subtype) t = (rTensor N P'.subtype) t'
⊢ ∃ Q, ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = (rTensor N (inclusion hP'Q)) t'

Tactic:
by
  simp only [← subtype_comp_inclusion _ _ (le_sup_left : _ ≤ P ⊔ P'),
    ← subtype_comp_inclusion _ _ (le_sup_right : _ ≤ P ⊔ P'),
    rTensor_comp, coe_comp, Function.comp_apply] at h
  let ⟨Q, hQ_le, hQ, h⟩ := TensorProduct.eq_of_fg_of_subtype_eq (hP.sup hP') h
  use Q, le_trans le_sup_left hQ_le, le_trans le_sup_right hQ_le, hQ
  simpa [← comp_apply, ← rTensor_comp] using! h

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 : ℕ
⊢ projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ ↑n ↔ projectiveDimension M + 1 ≤ ↑n

Tactic:
match n with
    | 0 =>
      rw [projectiveDimension_le_iff]
      simp only [HasProjectiveDimensionLE, zero_add, ← projective_iff_hasProjectiveDimensionLT_one,
        CharP.cast_eq_zero, ENat.WithBot.add_one_le_zero_iff, projectiveDimension_eq_bot_iff,
        ModuleCat.isZero_iff_subsingleton, sub, ← IsProjective.iff_projective]
      refine ⟨fun h ↦ ?_, fun h ↦ Projective.of_free⟩
      have : Module.Free R (QuotSMulTop x M) := Module.free_of_flat_of_isLocalRing
      by_contra! ntr
      have := QuotSMulTop.mem_annihilator M x
      simp only [annihilator_eq_bot.mpr inferInstance, Submodule.mem_bot] at this
      simp only [this, IsSMulRegular.zero_iff_subsingleton] at reg
      absurd not_subsingleton_iff_nontrivial.mpr ntr
      infer_instance
    | n + 1 =>
      nth_rw 2 [← Nat.cast_one, Nat.cast_add]
      simp only [ENat.WithBot.add_le_add_natCast_right_iff, projectiveDimension_le_iff]
      let S := M.smulShortComplex x
      have hS : S.ShortExact := reg.smulShortComplex_shortExact
      refine ⟨fun h ↦ ?_, fun h ↦ hS.hasProjectiveDimensionLT_X₃ (n + 1) h
        (hasProjectiveDimensionLT_of_ge M (n + 1) (n + 2) (Nat.le_add_right _ 1))⟩
      apply hasProjectiveDimensionLT_of_forall_finite
      intro L _
      have zero := HasProjectiveDimensionLT.subsingleton (ModuleCat.of R (QuotSMulTop x M))
        (n + 2) _ (le_refl _) L
      have exac := Ext.contravariant_sequence_exact₁' hS L (n + 1) (n + 2) (add_comm 1 (n + 1))
      have epi := exac.epi_f ((@AddCommGrpCat.isZero_of_subsingleton _ zero).eq_zero_of_tgt _)
      have : S.f = x • 𝟙 M := rfl
      simp only [S, this, AddCommGrpCat.epi_iff_surjective, AddCommGrpCat.hom_ofHom] at epi
      by_contra! ntr
      have : x ∈ (Module.annihilator R (Ext M L (n + 1))).jacobson :=
        (IsLocalRing.maximalIdeal_le_jacobson _) mem
      absurd Submodule.top_ne_pointwise_smul_of_mem_jacobson_annihilator this
      rw [eq_comm, eq_top_iff]
      intro y hy
      rcases epi y with ⟨z, hz⟩
      simp only [ModuleCat.smulShortComplex, Ext.mk₀_smul,
        Ext.bilinearComp_apply_apply, Ext.smul_comp, Ext.mk₀_id_comp] at hz
      simpa [← hz] using Submodule.smul_mem_pointwise_smul _ _ ⊤ trivial

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsHausdorff (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
f f' : A[X]
h h' : A⟦X⟧
H : g.IsWeierstrassFactorization f h
H2 : g.IsWeierstrassFactorization f' h'
⊢ f = f' ∧ h = h'

Tactic:
by
  obtain ⟨h1, h2⟩ := H.isWeierstrassDivision.elim H.map_ne_zero H2.isWeierstrassDivision
  rw [← Units.ext_iff, inv_inj, Units.ext_iff] at h1
  exact ⟨by simpa using h2, h1⟩

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

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
⊢ m.IsFullyInvariant ↔ ∃ s ⊆ isotypicComponents R M, m = sSup s

Tactic:
refine ⟨fun h ↦ ⟨OrderIso.setIsotypicComponents.symm ⟨m, h⟩, ⟨?_, ?_⟩⟩, ?_⟩
  · rintro _ ⟨c, _, rfl⟩; exact c.2
  · convert! Subtype.ext_iff.mp (OrderIso.setIsotypicComponents.right_inv ⟨m, h⟩).symm
    simp [sSup_image, OrderIso.setIsotypicComponents, OrderIso.symm]
  · rintro ⟨_, hs, rfl⟩
    exact (fullyInvariantSubmodule R M).sSupClosed fun _ h ↦ .of_mem_isotypicComponents (hs h)

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

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSemisimpleRing R
inst✝ : Module.Finite R₀ R
⊢ ∃ n D d x x_1,
    ∃ (_ : ∀ (i : Fin n), Module.Finite R₀ (D i)),
      (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))

Tactic:
have ⟨n, D, d, _, _, hd, ⟨e⟩⟩ := exists_algEquiv_pi_matrix_divisionRing R₀ R

Goal state after:
R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSemisimpleRing R
inst✝ : Module.Finite R₀ R
n : ℕ
D : Fin n → Type u
d : Fin n → ℕ
w✝¹ : (i : Fin n) → DivisionRing (D i)
w✝ : (i : Fin n) → Algebra R₀ (D i)
hd : ∀ (i : Fin n), NeZero (d i)
e : R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)
⊢ ∃ n D d x x_1,
    ∃ (_ : ∀ (i : Fin n), Module.Finite R₀ (D i)),
      (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
⊢ IsDiscrete R

Tactic:
refine ⟨⟨0, zero_lt_one, fun x ↦ ?_⟩⟩
  have := subsingleton_units_valueGroupWithZero_of_trivialRel R Γ
  rcases GroupWithZero.eq_zero_or_unit x with rfl | ⟨u, rfl⟩
  · simp
  · rw [← Units.val_one, Units.val_lt_val]
    simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
x : 𝕎 k
hx : x.coeff 0 ≠ 0
⊢ IsUnit x

Tactic:
let y : kˣ := Units.mk0 (x.coeff 0) hx
  have hy : x.coeff 0 = y := rfl
  exact (mkUnit hy).isUnit

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (wittPolyProdRemainder p n).vars ⊆ univ ×ˢ range n

Tactic:
rw [wittPolyProdRemainder]
  refine Subset.trans (vars_sum_subset _ _) ?_
  rw [biUnion_subset]
  intro x hx
  apply Subset.trans (vars_mul _ _)
  refine union_subset ?_ ?_
  · apply Subset.trans (vars_pow _ _)
    have : (p : 𝕄) = C (p : ℤ) := by simp only [Int.cast_natCast, eq_intCast]
    rw [this, vars_C]
    apply empty_subset
  · apply Subset.trans (vars_pow _ _)
    apply Subset.trans (wittMul_vars _ _)
    apply product_subset_product (Subset.refl _)
    simpa using hx

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

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ((rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
rename_monomial,

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ((monomial (Finsupp.mapDomain (Prod.mk 0) (Finsupp.single x (p ^ (n + 1 - x))))) (↑p ^ x)).vars ⊆
    univ ×ˢ range (n + 1)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ((rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
rename_monomial,

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ((monomial (Finsupp.mapDomain (Prod.mk 1) (Finsupp.single x (p ^ (n + 1 - x))))) (↑p ^ x)).vars ⊆
    univ ×ˢ range (n + 1)
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
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : frobeniusRotation p ha₁ ha₂ = 0
⊢ solution p a₁ a₂ = 0

Tactic:
simpa [← h, frobeniusRotation, frobeniusRotationCoeff] using WittVector.zero_coeff p k 0

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

Goal state before:
pp: case e_a.e_a.e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
this : ↑p = 0
sum_zero_pow_mul_pow_p :
  ∀ (y : 𝕎 k), ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)
⊢ ∑ x_1 ∈ range (n + 1 + 1), 0 ^ x_1 * x.coeff x_1 ^ p ^ (n + 1 - x_1) = x.coeff 0 ^ p ^ (n + 1)

Tactic:
apply sum_zero_pow_mul_pow_p

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

Goal state before:
pp: case e_a.e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
this : ↑p = 0
sum_zero_pow_mul_pow_p :
  ∀ (y : 𝕎 k), ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)
⊢ ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)

Tactic:
apply sum_zero_pow_mul_pow_p

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

Goal state before:
pp: case refine_1
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
⊢ Function.Injective ⇑F₀

pp: case refine_2
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
⊢ Function.Surjective ⇑F₀

Tactic:
· rw [← LinearMap.ker_eq_bot]
      exact LinearMap.ker_toSpanSingleton K(p, k) hx

Goal state after:
case refine_2
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
⊢ Function.Surjective ⇑F₀
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
⊢ T = ⊥ → [] ∉ T

Tactic:
by rintro rfl; simp

Goal state after:
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x : List A
⊢ pullSub (subAt T x) x ≤ T

Tactic:
intro y (h : y ∈ pullSub _ x)

Goal state after:
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
⊢ y ∈ ↑T
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
S T : ↥(tree A)
x : List A
x✝ : pullSub S x ≤ T
⊢ S ≤ subAt T x

Tactic:
rw [← subAt_pullSub S x]

Goal state after:
A : Type u_1
S T : ↥(tree A)
x : List A
x✝ : pullSub S x ≤ T
⊢ subAt (pullSub S x) x ≤ subAt T x
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case cons'
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b b✝ : Bool
a : Lists' α b✝
l : Lists' α true
IH₁ :
  C ⟨b✝, a⟩ ×'
    match b✝, a with
    | true, l => D l
    | false, x => PUnit
IH :
  C ⟨true, l⟩ ×'
    match true, l with
    | true, l => D l
    | false, x => PUnit
⊢ C ⟨true, a.cons' l⟩ ×'
    match true, a.cons' l with
    | true, l => D l
    | false, x => PUnit

Tactic:
| cons' a l IH₁ IH =>

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

Goal state before:
pp: b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → x.2 < b

Tactic:
refine CNF.rec b ?_ (fun o ho IH ↦ ?_) o
  · simp
  · rw [CNF.ne_zero ho]
    intro h
    obtain rfl | h := mem_cons.mp h
    · exact div_opow_log_lt o hb
    · exact IH h

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
haveI : Decidable (l₁ ⊆ l₂) :=
        have : SizeOf.sizeOf l₁ + SizeOf.sizeOf l₂ <
            SizeOf.sizeOf (⟨true, l₁⟩ : Lists α) + SizeOf.sizeOf (⟨true, l₂⟩ : Lists α) := by
          decreasing_tactic
        Subset.decidable l₁ l₂

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
this : Decidable (l₁ ⊆ l₂)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ o.IsAcc S ↔ o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Tactic:
apply SuccOrder.accPt_principal.trans
  simp

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

Goal state before:
pp: o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
⊢ ∀ p < o, p.IsAcc (⋂₀ S) → p ∈ ⋂₀ S

Tactic:
exact fun p plto pAcc C CmemS ↦ (h C CmemS).forall_lt p plto <|
    AccPt.mono pAcc (monotone_principal (sInter_subset_of_mem CmemS))

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

Goal state before:
pp: case inr
x y z : ZFSet.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
hx : x.Nonempty
⊢ y ∈ z

Tactic:
· exact (mem_sInter hx).1 hy z hz

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

Goal state before:
pp: p : ZFSet.{u} → ZFSet.{u} → Prop
x y z : ZFSet.{u}
⊢ z ∈ pairSep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b

Tactic:
by
  refine mem_sep.trans ⟨And.right, fun e => ⟨?_, e⟩⟩
  grind [mem_pair, mem_powerset, mem_singleton, mem_union, pair, subset_def]

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

Goal state before:
pp: case eq.zero
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
⊢ (match Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match 0 with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).NFBelow
    b

pp: case eq.succ
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n✝ : ℕ
⊢ (match Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match n✝ + 1 with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).NFBelow
    b

Tactic:
· by_cases en : n₁ = n₂ <;> simp only [en, ↓reduceIte]
        · exact h'.mono (le_of_lt h₁.lt)
        · exact NFBelow.zero

Goal state after:
case eq.succ
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n✝ : ℕ
⊢ (match Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match n✝ + 1 with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).NFBelow
    b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o' : ONote
m : ℕ
x✝ : NF 0
p : split' 0 = (o', m)
⊢ split 0 = (scale 1 o', m)

Tactic:
injection p

Goal state after:
o' : ONote
m : ℕ
x✝ : NF 0
fst_eq✝ : 0 = o'
snd_eq✝ : 0 = m
⊢ split 0 = (scale 1 o', m)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o' : ONote
m : ℕ
x✝ : NF 0
p : split' 0 = (o', m)
⊢ o'.NF ∧ repr 0 = ω * o'.repr + ↑m

Tactic:
injection p

Goal state after:
o' : ONote
m : ℕ
x✝ : NF 0
fst_eq✝ : 0 = o'
snd_eq✝ : 0 = m
⊢ o'.NF ∧ repr 0 = ω * o'.repr + ↑m
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
na : a.NF
⊢ (o₁ ^ o₂).NF

Tactic:
rcases e₂ : split' o₂ with ⟨b', k⟩

Goal state after:
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
na : a.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
⊢ (o₁ ^ o₂).NF
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case hbc
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
⊢ succ b < ω

Tactic:
exact isSuccLimit_omega0.succ_lt l

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

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
⊢ ∀ᶠ (x : ℝ) in atTop, (f ^ exp') x = 0 → (f ^ exp) x = 0

Tactic:
apply (Tendsto.eventually_gt_atTop h 0).mono
    intro t h1 h2
    absurd h2
    exact (Real.rpow_pos_of_pos h1 _).ne.symm

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

Goal state before:
pp: case zero.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
rcases e₂ : split' o₂ with ⟨b', k⟩

Goal state after:
case zero.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
rcases e₂ : split' o₂ with ⟨b', k⟩

Goal state after:
case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: case cons
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
n : Fin (basis_hd :: basis_tl).length
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ (monomialRpow (basis_hd :: basis_tl) (↑n) r).Approximates

Tactic:
simp only [List.length_cons, monomialRpow, Fin.is_lt, getElem!_pos]

Goal state after:
case cons
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
n : Fin (basis_hd :: basis_tl).length
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ (mk (Multiseries.monomialRpow basis_hd basis_tl (↑n) r) ((basis_hd :: basis_tl)[↑n] ^ r)).Approximates
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
h_length : [].length = List.length basis_tl
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ Majorized 1 basis_hd 0

Tactic:
exact Majorized.const (h_basis.tendsto_atTop (by simp))

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

Goal state before:
pp: case cons.cons
hd : ℝ
tl : List ℝ
ih :
  ∀ {basis_hd : ℝ → ℝ} {basis_tl : Basis},
    tl.length = List.length basis_tl → WellFormedBasis (basis_hd :: basis_tl) → Majorized (toFun tl basis_tl) basis_hd 0
basis_hd basis_tl_hd : ℝ → ℝ
basis_tl_tl : List (ℝ → ℝ)
h_length : (hd :: tl).length = (basis_tl_hd :: basis_tl_tl).length
h_basis : WellFormedBasis (basis_hd :: basis_tl_hd :: basis_tl_tl)
⊢ Majorized (toFun (hd :: tl) (basis_tl_hd :: basis_tl_tl)) basis_hd 0

Tactic:
| cons basis_tl_hd basis_tl_tl =>

Goal state after: