mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ projectiveDimension (of R (QuotSMulTop x ↑M)) = projectiveDimension M + 1

Tactic:
have aux (n : ℕ) : projectiveDimension (ModuleCat.of R (QuotSMulTop x M)) ≤ n ↔
    projectiveDimension M + 1 ≤ n := by
    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:
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)
aux : ∀ (n : ℕ), projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ ↑n ↔ projectiveDimension M + 1 ≤ ↑n
⊢ projectiveDimension (of R (QuotSMulTop x ↑M)) = projectiveDimension M + 1
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
S c : Submodule R M
hc : c ∈ isotypicComponents R M
inst✝ : IsSimpleModule R ↥S
le : S ≤ c
⊢ c = isotypicComponent R M ↥S

Tactic:
obtain ⟨S', _, rfl⟩ := hc

Goal state after:
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
S : Submodule R M
inst✝ : IsSimpleModule R ↥S
S' : Submodule R M
left✝ : IsSimpleModule R ↥S'
le : S ≤ isotypicComponent R M ↥S'
⊢ isotypicComponent R M ↥S' = isotypicComponent R M ↥S
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Nontrivial M ∧
    ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module R N] (f : M →ₗ[R] N), f = 0 ∨ Function.Injective ⇑f
hM1 : Nontrivial M
hM2 : ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module R N] (f : M →ₗ[R] N), f = 0 ∨ Function.Injective ⇑f
p : Submodule R M
h : p.mkQ = 0
⊢ p = ⊤

Tactic:
simpa [Submodule.ext_iff, LinearMap.ext_iff] using h

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

Goal state before:
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:
induction hx using Submodule.smul_induction_on' with

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

Goal state before:
pp: case hx
R : Type u_1
inst✝⁶ : CommRing R
ΓR : Type u_6
inst✝⁵ : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst✝⁴ : CommRing S
inst✝³ : LinearOrderedCommGroupWithZero ΓS
inst✝² : Algebra R S
inst✝¹ : IsLocalHom (algebraMap R S)
vS : Valuation S ΓS
inst✝ : vR.HasExtension vS
r : ↥vR.integer
hr : IsUnit ((algebraMap ↥vR.integer ↥vS.integer) r)
⊢ IsUnit ((algebraMap (↥vR.integer) R) r)

pp: case hvx
R : Type u_1
inst✝⁶ : CommRing R
ΓR : Type u_6
inst✝⁵ : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst✝⁴ : CommRing S
inst✝³ : LinearOrderedCommGroupWithZero ΓS
inst✝² : Algebra R S
inst✝¹ : IsLocalHom (algebraMap R S)
vS : Valuation S ΓS
inst✝ : vR.HasExtension vS
r : ↥vR.integer
hr : IsUnit ((algebraMap ↥vR.integer ↥vS.integer) r)
⊢ vR ((algebraMap (↥vR.integer) R) r) = 1

Tactic:
· exact (isUnit_map_iff (algebraMap R S) _).mp (hr.map (algebraMap _ S))

Goal state after:
case hvx
R : Type u_1
inst✝⁶ : CommRing R
ΓR : Type u_6
inst✝⁵ : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst✝⁴ : CommRing S
inst✝³ : LinearOrderedCommGroupWithZero ΓS
inst✝² : Algebra R S
inst✝¹ : IsLocalHom (algebraMap R S)
vS : Valuation S ΓS
inst✝ : vR.HasExtension vS
r : ↥vR.integer
hr : IsUnit ((algebraMap ↥vR.integer ↥vS.integer) r)
⊢ vR ((algebraMap (↥vR.integer) R) r) = 1
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
S : Type u_2
inst✝¹⁰ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁹ : CommRing R'
inst✝⁸ : CommRing S'
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : Module.Flat R S
surj : Function.Surjective ⇑(algebraMap R R')
surjS : Function.Surjective ⇑(algebraMap S S')
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
sq0 : RingHom.ker (algebraMap R R') ^ 2 = ⊥
smoothq : FormallySmooth R' S'
P : Extension R S := (Generators.self R S).toExtension
this✝² : FormallySmooth R P.Ring := instFormallySmoothMvPolynomial S
IP : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) (RingHom.ker (algebraMap R R'))
Gen : Generators R' S' S :=
  { val := ⇑(algebraMap S S'), σ' := fun s' ↦ MvPolynomial.X (Classical.choose ⋯), aeval_val_σ' := ⋯,
    algebraMap_eq := ⋯ }
P' : Extension R' S' := Gen.toExtension
this✝¹ : FormallySmooth R' P'.Ring := instFormallySmoothMvPolynomial S
this✝ : Algebra P.Ring P'.Ring := MvPolynomial.algebraMvPolynomial
this : IsScalarTower R P.Ring P'.Ring :=
  IsScalarTower.of_algebraMap_eq fun x ↦ Eq.symm (MvPolynomial.map_C (algebraMap R R') x)
⊢ FormallySmooth R S

Tactic:
algebraize [(algebraMap S S').comp (algebraMap P.Ring S)]

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
S : Type u_2
inst✝¹⁰ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁹ : CommRing R'
inst✝⁸ : CommRing S'
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : Module.Flat R S
surj : Function.Surjective ⇑(algebraMap R R')
surjS : Function.Surjective ⇑(algebraMap S S')
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
sq0 : RingHom.ker (algebraMap R R') ^ 2 = ⊥
smoothq : FormallySmooth R' S'
P : Extension R S := (Generators.self R S).toExtension
this✝² : FormallySmooth R P.Ring := instFormallySmoothMvPolynomial S
IP : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) (RingHom.ker (algebraMap R R'))
Gen : Generators R' S' S :=
  { val := ⇑(algebraMap S S'), σ' := fun s' ↦ MvPolynomial.X (Classical.choose ⋯), aeval_val_σ' := ⋯,
    algebraMap_eq := ⋯ }
P' : Extension R' S' := Gen.toExtension
this✝¹ : FormallySmooth R' P'.Ring := instFormallySmoothMvPolynomial S
this✝ : Algebra P.Ring P'.Ring := MvPolynomial.algebraMvPolynomial
this : IsScalarTower R P.Ring P'.Ring :=
  IsScalarTower.of_algebraMap_eq fun x ↦ Eq.symm (MvPolynomial.map_C (algebraMap R R') x)
algInst✝ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
scalarTowerInst✝ : IsScalarTower P.Ring S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P.Ring S'))
⊢ FormallySmooth R S
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
c : 𝕎 k
hc : c.coeff 0 ≠ 0
hcm : a = (⇑verschiebung)^[m] c
⊢ ∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b

Tactic:
obtain ⟨b, rfl⟩ := (frobenius_bijective p k).surjective.iterate m c

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : ((⇑frobenius)^[m] b).coeff 0 ≠ 0
hcm : a = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
⊢ ∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 = a₂.coeff 0 / a₁.coeff 0
⊢ False

Tactic:
simpa [ha₁, ha₂] using _root_.div_eq_zero_iff.mp this.symm

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

Goal state before:
pp: α : Type v
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
ι : Sort u_1
f : ι → Set α
inst✝ : Countable ι
hα : cof α ≠ ℵ₀
hf : ∀ (i : ι), IsClub (f i)
⊢ IsClub (⋂ i, f i)

Tactic:
by
  rw [← sInter_range]
  apply IsClub.sInter_of_countable hα (countable_range f)
  simpa

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

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
ι : Sort u_1
f : ι → Set α
hα : cof α ≤ 1
⊢ IsStationary (⋃₀ range f) ↔ ∃ i, IsStationary (f i)

Tactic:
isStationary_sUnion_iff_of_cof_le_one hα

Goal state after:
α : Type v
inst✝ : LinearOrder α
ι : Sort u_1
f : ι → Set α
hα : cof α ≤ 1
⊢ (∃ x ∈ range f, IsStationary x) ↔ ∃ i, IsStationary (f i)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ CNF b (b ^ e * x + y) = (e, x) :: CNF b y

Tactic:
have hb' := hb.ne_bot
  rw [CNF.ne_zero]
  · rw [log_opow_mul_add hb hx hy, log_eq_zero hxb, add_zero,
      mul_add_div _ (opow_ne_zero _ hb'), Ordinal.div_eq_zero_of_lt hy, add_zero,
      mul_add_mod_self, mod_eq_of_lt hy]
  · simp_all

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

Goal state before:
pp: case refine_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
⊢ x ∈ CNF b o → x.2 < b

Tactic:
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.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
hf : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ ⨆ i, lfpApprox f x i = lfpApprox f x a

Tactic:
apply (le_iSup (lfpApprox f x) a).antisymm'
  refine ciSup_le fun i => ?_
  by_cases h : i ≤ a
  · exact lfpApprox_mono_right f h
  · exact (lfpApprox_eq_of_mem_fixedPoints f (le_of_not_ge h) hf).le

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

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : ¬IsMin a
⊢ (∃ᶠ (y : α) in 𝓝 a, y ≠ a ∧ y ∈ s) ↔ ¬IsMin a ∧ ∀ b < a, (s ∩ Ioo b a).Nonempty

Tactic:
rw [not_isMin_iff] at ha ⊢

Goal state after:
case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : ∃ b, b < a
⊢ (∃ᶠ (y : α) in 𝓝 a, y ≠ a ∧ y ∈ s) ↔ (∃ b, b < a) ∧ ∀ b < a, (s ∩ Ioo b a).Nonempty
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case inr
a : Ordinal.{u_1}
h : 0 < a
⊢ a < veblen a a

Tactic:
· apply (left_le_veblen a 0).trans_lt
    simpa

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

Goal state before:
pp: o : Ordinal.{u}
h : veblen o 0 ≤ o
⊢ Γ_ 0 ≤ o

Tactic:
rw [gamma_zero_eq_nfp]
  exact nfp_le_fp (veblen_left_monotone 0) zero_le h

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

Goal state before:
pp: case inr.inr
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
y z w : ↥x
hyz : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y z
hzw : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) z w
hwy : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) w y
⊢ Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y w

Tactic:
cases mem_wf.asymmetric₃ _ _ _ hyz hzw hwy

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

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ dist (Seq.cons hd x) (Seq.cons hd y)
⊢ dist (op (Seq.cons hd x)).tail (op (Seq.cons hd y)).tail ≤ dist x y

Tactic:
by
  rwa [dist_cons_cons, dist_eq_half_of_head, mul_le_mul_iff_right₀ (by norm_num)] at h
  grw [dist_le_one x y, mul_one] at h
  obtain (⟨hx, hy⟩ | ⟨_, _, _, hx, hy⟩) := dist_le_half_iff.mp h <;> simp [hx, hy]

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

Goal state before:
pp: case insert
basis basis✝ : Basis
f✝ : ℝ → ℝ
ex : BasisExtension basis✝
ih : List.Sublist basis✝ ex.getBasis
⊢ List.Sublist basis✝ (insert f✝ ex).getBasis

Tactic:
| insert _ ex ih =>

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
h : (mk (Multiseries.cons exp coef tl) f).Sorted
⊢ coef.Sorted ∧ tl.leadingExp < ↑exp ∧ tl.Sorted

Tactic:
by
  apply Multiseries.Sorted.elim_cons (by simpa using h)

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.seq.Trimmed
⊢ ms.Trimmed

Tactic:
generalize hs : ms.seq = s at h
    cases h with
    | nil =>
      convert Trimmed.nil (f := ms.toFun)
      simp [hs]
    | @cons _ _ exp coef tl _ h_trimmed h_ne_zero =>
      convert Trimmed.cons h_trimmed h_ne_zero (exp := exp) (tl := tl) (f := ms.toFun)
      simp only [ms_eq_mk_iff, hs, and_true]

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

Goal state before:
pp: case hyp.inr.inr
basis_hd : ℝ → ℝ
basis_tl : Basis
ms✝ : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms✝
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : motive ms
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_seq : ms.seq = Multiseries.cons exp coef tl
h_coef : coef.Approximates
h_maj : Majorized ms.toFun basis_hd exp
h_tl : motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ms.toFun =ᶠ[atTop] 0 ∧ ms.seq = Multiseries.nil ∨
    ∃ basis_hd_1 f basis_tl_1 exp coef,
      (coef.Approximates ∨ ∃ (h_basis : basis_tl_1 = basis_hd :: basis_tl), motive (h_basis ▸ coef)) ∧
        Majorized f basis_hd_1 exp ∧
          ∃ x,
            ((mk x (f - basis_hd_1 ^ exp * coef.toFun)).Approximates ∨
                ∃ (h : basis_hd_1 = basis_hd ∧ basis_tl_1 = basis_tl),
                  motive (⋯ ▸ mk x (f - basis_hd_1 ^ exp * coef.toFun))) ∧
              (basis_hd = basis_hd_1 ∧ basis_tl = basis_tl_1) ∧ ms ≍ mk (Multiseries.cons exp coef x) f

Tactic:
refine .inr ⟨basis_hd, ms.toFun, basis_tl, exp, coef, by simpa, ‹_›, tl, ?_⟩

Goal state after:
case hyp.inr.inr
basis_hd : ℝ → ℝ
basis_tl : Basis
ms✝ : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms✝
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : motive ms
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_seq : ms.seq = Multiseries.cons exp coef tl
h_coef : coef.Approximates
h_maj : Majorized ms.toFun basis_hd exp
h_tl : motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ((mk tl (ms.toFun - basis_hd ^ exp * coef.toFun)).Approximates ∨
      ∃ (h : basis_hd = basis_hd ∧ basis_tl = basis_tl), motive (⋯ ▸ mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))) ∧
    (basis_hd = basis_hd ∧ basis_tl = basis_tl) ∧ ms ≍ mk (Multiseries.cons exp coef tl) ms.toFun
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inl.some.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
e' : m.natPred = 0
this : 0 < ω ^ a'.repr
i : ℕ
⊢ ω ^ a'.repr * ↑i + ω ^ a'.repr < ω ^ a'.repr * ω

Tactic:
← mul_add_one,

Goal state after:
case oadd.inl.none.inl.some.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
e' : m.natPred = 0
this : 0 < ω ^ a'.repr
i : ℕ
⊢ ω ^ a'.repr * (↑i + 1) < ω ^ a'.repr * ω
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inl.some.succ.refine_1
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
⊢ ω ^ a'.repr * ↑i + ω ^ a'.repr < ω ^ a'.repr * ω

Tactic:
← mul_add_one,

Goal state after:
case oadd.inl.none.inl.some.succ.refine_1
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
⊢ ω ^ a'.repr * (↑i + 1) < ω ^ a'.repr * ω
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
hS4 : S4 = DFunLike.coe '' S1
h : Equicontinuous fun x ↦ ⇑↑x
⊢ ∀ (x : X → Y), (∃ x_1 ∈ S1, ⇑x_1 = x) ↔ x ∈ (U.pi fun x ↦ W) ∩ Set.range DFunLike.coe

Tactic:
S1,

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
hS4 : S4 = DFunLike.coe '' S1
h : Equicontinuous fun x ↦ ⇑↑x
⊢ ∀ (x : X → Y), (∃ x_1 ∈ {f | Set.MapsTo (⇑f) U W}, ⇑x_1 = x) ↔ x ∈ (U.pi fun x ↦ W) ∩ Set.range DFunLike.coe
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
hS4 : S4 = DFunLike.coe '' S1
h : Equicontinuous fun x ↦ ⇑↑x
⊢ ∀ (x : X → Y), (∃ x_1 ∈ {f | Set.MapsTo (⇑f) U W}, ⇑x_1 = x) ↔ x ∈ (U.pi fun x ↦ W) ∩ Set.range DFunLike.coe

Tactic:
Set.mem_ofPred_eq

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
hS4 : S4 = DFunLike.coe '' S1
h : Equicontinuous fun x ↦ ⇑↑x
⊢ ∀ (x : X → Y), (∃ x_1, Set.MapsTo (⇑x_1) U W ∧ ⇑x_1 = x) ↔ x ∈ (U.pi fun x ↦ W) ∩ Set.range DFunLike.coe
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔
    Tendsto F ℱ (comap (⋃₀ 𝔖).domRestrict (𝓝 ((⋃₀ 𝔖).domRestrict f)))

Tactic:
← nhds_induced

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)