mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: case right
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h✝ : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
this : (rTensor N P₁.subtype) u₁ = (rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (rTensor N (inclusion hP₁_le)) u₁ = (rTensor N (inclusion hP₁_le)) u'₁
s : Finset S
hs : span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
⊢ (rTensor N (Subalgebra.inclusion hBA).toLinearMap) ((rTensor N P.subtype) u) =
    (rTensor N (Subalgebra.inclusion hBA).toLinearMap) t'

Tactic:
← hu'

Goal state after:
case right
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h✝ : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
this : (rTensor N P₁.subtype) u₁ = (rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (rTensor N (inclusion hP₁_le)) u₁ = (rTensor N (inclusion hP₁_le)) u'₁
s : Finset S
hs : span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
⊢ (rTensor N (Subalgebra.inclusion hBA).toLinearMap) ((rTensor N P.subtype) u) =
    (rTensor N (Subalgebra.inclusion hBA).toLinearMap) ((rTensor N P'.subtype) u')
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: case bot
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 ≤ ⊥

Tactic:
simpa [projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton] using sub.symm

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✝ : IsSimpleModule R M
S : Submodule R M
hS : IsSimpleModule R ↥S
⊢ Nonempty (↥S ≃ₗ[R] M)

Tactic:
rw [isSimpleModule_iff_isAtom, isAtom_iff_eq_top] at hS
    exact ⟨.trans (.ofEq _ _ hS) Submodule.topEquiv⟩

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
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ IsIsotypicOfType R (↥N) S ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule R
          ↥↑({ toFun := fun p' ↦ ⟨Submodule.map N.subtype p', ⋯⟩, invFun := fun q ↦ Submodule.comap N.subtype ↑q,
                  left_inv := ⋯, right_inv := ⋯ }
                a)],
      Nonempty
        (↥↑({ toFun := fun p' ↦ ⟨Submodule.map N.subtype p', ⋯⟩, invFun := fun q ↦ Submodule.comap N.subtype ↑q,
                  left_inv := ⋯, right_inv := ⋯ }
                a) ≃ₗ[R]
          S)

Tactic:
Equiv.coe_fn_mk,

Goal state after:
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
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ IsIsotypicOfType R (↥N) S ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule R ↥(Submodule.map N.subtype a)],
      Nonempty (↥(Submodule.map N.subtype a) ≃ₗ[R] S)
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
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ IsIsotypic R ↥N ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule R
          ↥↑({ toFun := fun p' ↦ ⟨Submodule.map N.subtype p', ⋯⟩, invFun := fun q ↦ Submodule.comap N.subtype ↑q,
                  left_inv := ⋯, right_inv := ⋯ }
                a)],
      IsIsotypicOfType R ↥N
        ↥↑({ toFun := fun p' ↦ ⟨Submodule.map N.subtype p', ⋯⟩, invFun := fun q ↦ Submodule.comap N.subtype ↑q,
                left_inv := ⋯, right_inv := ⋯ }
              a)

Tactic:
Equiv.coe_fn_mk,

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ IsIsotypic R ↥N ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule R ↥(Submodule.map N.subtype a)],
      IsIsotypicOfType R ↥N ↥(Submodule.map N.subtype a)
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularRing R
ι : Type u_2
inst✝ : Finite ι
⊢ IsRegularRing (MvPolynomial ι R)

Tactic:
by
  induction ι using Finite.induction_empty_option with
  | of_equiv e H => exact IsRegularRing.of_ringEquiv (renameEquiv _ e).toRingEquiv
  | h_empty => exact IsRegularRing.of_ringEquiv (isEmptyRingEquiv R _).symm
  | h_option IH =>
    exact IsRegularRing.of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv.symm

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

Goal state before:
pp: case inr
R : Type u_2
M : Type u
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
S : Submodule R M
inst✝ : IsSimpleModule R ↥S
f : M →ₗ[R] N
eq : f ∘ₗ S.subtype = 0
⊢ (f ∘ₗ S.subtype).range ≤ isotypicComponent R N ↥S

Tactic:
simp_rw [eq, LinearMap.range_zero, bot_le]

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 : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ I.ringCon (Multiset.map f s).sum (Multiset.map (fun x ↦ 0) ?m.25).sum

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

pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Multiset ?m.22

Tactic:
exact I.ringCon.multisetSum s hs

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
hb : Squarefree b
hab : Squarefree (a * b)
⊢ (-1) ^ (factors (a * b)).card = moebius a * moebius b

Tactic:
Multiset.card_eq_card_of_rel (factors_mul ha.ne_zero hb.ne_zero),

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
hb : Squarefree b
hab : Squarefree (a * b)
⊢ (-1) ^ (factors a + factors b).card = moebius a * moebius b
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

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

Tactic:
rw [← Units.val_one, Units.val_lt_val]

Goal state after:
case inr
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
this : Subsingleton (ValueGroupWithZero R)ˣ
u : (ValueGroupWithZero R)ˣ
⊢ u < 1 → ↑u ≤ 0
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
⊢ Irreducible ↑p

Tactic:
by
  have hp : ¬IsUnit (p : 𝕎 k) := by
    intro hp
    simpa only [constantCoeff_apply, coeff_p_zero, not_isUnit_zero] using
      (constantCoeff : WittVector p k →+* _).isUnit_map hp
  refine ⟨hp, fun a b hab => ?_⟩
  obtain ⟨ha0, hb0⟩ : a ≠ 0 ∧ b ≠ 0 := by
    rw [← mul_ne_zero_iff]; intro h; rw [h] at hab; exact p_nonzero p k hab
  obtain ⟨m, a, ha, rfl⟩ := verschiebung_nonzero ha0
  obtain ⟨n, b, hb, rfl⟩ := verschiebung_nonzero hb0
  cases m; · exact Or.inl (isUnit_of_coeff_zero_ne_zero a ha)
  rcases n with - | n; · exact Or.inr (isUnit_of_coeff_zero_ne_zero b hb)
  rw [iterate_verschiebung_mul] at hab
  apply_fun fun x => coeff x 1 at hab
  simp only [coeff_p_one, Nat.add_succ, add_comm _ n, Function.iterate_succ', Function.comp_apply,
    verschiebung_coeff_add_one, verschiebung_coeff_zero] at hab
  exact (one_ne_zero hab).elim

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

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

Tactic:
rw [← sInter_range]
  exact .sInter_of_orderTop (by simpa)

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

Goal state before:
pp: case h
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)
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y ↦
    f₀ fun a ↦
      Subtype.casesOn a fun a ha ↦
        Function.uncurry ![x, y]
          (let S := {a | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
a : ↥(univ ×ˢ range (n + 1))
⊢ ![truncateFun (n + 1) x, truncateFun (n + 1) y] (↑a).1 ⟨(↑a).2, ⋯⟩ =
    (Function.uncurry ![fun i ↦ x.coeff i, fun i ↦ y.coeff i] ∘ Subtype.val) a

Tactic:
obtain ⟨a, ha⟩ := a

Goal state after:
case h
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)
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y ↦
    f₀ fun a ↦
      Subtype.casesOn a fun a ha ↦
        Function.uncurry ![x, y]
          (let S := {a | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
a : Fin 2 × ℕ
ha : a ∈ univ ×ˢ range (n + 1)
⊢ ![truncateFun (n + 1) x, truncateFun (n + 1) y] (↑⟨a, ha⟩).1 ⟨(↑⟨a, ha⟩).2, ⋯⟩ =
    (Function.uncurry ![fun i ↦ x.coeff i, fun i ↦ y.coeff i] ∘ Subtype.val) ⟨a, ha⟩
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := ⋯
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
n : ℕ
⊢ ¬IsCofinal (range fun x ↦ f x (Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) n))

pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := ⋯
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
n : ℕ
⊢ (fun n ↦ f ⟨t, ht⟩ (g n)) n ∈ range fun x ↦ f x (Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) n)

Tactic:
· exact fun hg' ↦ (cof_le hg').not_gt (mk_range_le.trans_lt hsα)

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := ⋯
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
n : ℕ
⊢ (fun n ↦ f ⟨t, ht⟩ (g n)) n ∈ range fun x ↦ f x (Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) n)
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: case refine_1
x✝ : ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
⊢ univ.{v, u + 1} < univ.{u, v + 1}

Tactic:
rw [univ_umax.{v, u}, ← lift_le.{u + 1}, lift_univ, lift_lift] at le

Goal state after:
case refine_1
x✝ : ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α
⊢ univ.{v, u + 1} < univ.{u, v + 1}
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: C : Ordinal.{u_2} → Sort u_1
b : Ordinal.{u_2}
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ (if h : 0 = 0 then ⋯ ▸ H0 else H 0 h (CNF.rec b H0 H (0 % b ^ log b 0))) = H0

Tactic:
dif_pos rfl

Goal state after:
C : Ordinal.{u_2} → Sort u_1
b : Ordinal.{u_2}
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ ⋯ ▸ H0 = H0
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ x ≤ ⨆ b, lfpApprox f x ↑b

pp: case right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ ∀ (i : Ordinal.{u}), ⨆ (_ : i < a), f (lfpApprox f x i) ≤ ⨆ b, lfpApprox f x ↑b

Tactic:
· refine le_iSup_of_le ⟨0, ha.bot_lt⟩ (by simp [lfpApprox_zero])

Goal state after:
case right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ ∀ (i : Ordinal.{u}), ⨆ (_ : i < a), f (lfpApprox f x i) ≤ ⨆ b, lfpApprox f x ↑b
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case nil
α : Type u_1
⊢ (ofList []).toList = []

Tactic:
simp [*]

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case cons
α : Type u_1
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : (ofList tail✝).toList = tail✝
⊢ (ofList (head✝ :: tail✝)).toList = head✝ :: tail✝

Tactic:
simp [*]

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

Goal state before:
pp: case ind
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ lfpApprox g x y
⊢ x ⊔ ⨆ b, ⨆ (_ : b < i), f (lfpApprox f x b) ≤ x ⊔ ⨆ b, ⨆ (_ : b < i), g (lfpApprox g x b)

Tactic:
exact sup_le_sup_left (iSup₂_mono fun j hj ↦ (f.mono (IH j hj)).trans (h _)) _

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
a : Lists α
x✝ : Lists' α true
h : a ∈ nil.toList
⊢ a ∈ x✝

Tactic:
by cases h

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

Goal state before:
pp: s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1 ⊆ s, t_1.Nonempty ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
⊢ ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = sSup t

Tactic:
bddAbove_iff_small

Goal state after:
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} ↑t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1 ⊆ s, t_1.Nonempty ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
⊢ ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = sSup t
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ a ∈ closure s ↔ ∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a

Tactic:
by
  apply ((mem_closure_tfae a s).out 0 4).trans
  simp_rw [exists_prop]

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

Goal state before:
pp: case pos
b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
a : Ordinal.{u_1}
ha : a ∈ f.support
⊢ f a < b

pp: case neg
b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
a : Ordinal.{u_1}
ha : a ∉ f.support
⊢ f a < b

Tactic:
· apply (hb a).trans_eq'
        rw [add_apply, single_eq_of_ne, zero_add]
        rintro rfl
        contradiction

Goal state after:
case neg
b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
a : Ordinal.{u_1}
ha : a ∉ f.support
⊢ f a < b
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case mpr.inr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb✝ : b < o + 1
hb : b < o
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb✝⟩)

Tactic:
· rw [← ha]
      exact veblenWith_veblenWith_of_lt hf hb _

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

Goal state before:
pp: case a
x : PSet.{u_1}
⊢ x.powerset.rank ≤ succ x.rank

pp: case a
x : PSet.{u_1}
⊢ succ x.rank ≤ x.powerset.rank

Tactic:
· simp_rw [rank_le_iff, mem_powerset, lt_succ_iff]
    intro
    exact rank_mono

Goal state after:
case a
x : PSet.{u_1}
⊢ succ x.rank ≤ x.powerset.rank
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: case inr
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
h : Hereditarily p y
a : ZFSet.{u}
ha : a ∈ ↑y
⊢ p ∅

Tactic:
exact IH a ha (h.mem ha)

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

Goal state before:
pp: x : ZFSet.{u}
hx : ↑x = IsOrdinal
this : x.IsOrdinal
⊢ False

Tactic:
apply Class.mem_irrefl x
    rwa [Class.coe_mem, hx]

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

Goal state before:
pp: case mpr
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ y ∈ V_ o

Tactic:
· rw [mem_vonNeumann']
    have := hx hy
    exact ⟨_, this, subset_vonNeumann.2 le_rfl⟩

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

Goal state before:
pp: 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

pp: 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'

Tactic:
· simp only [opow_one, repr_sub, repr_one, Nat.cast_one] at this ⊢
        refine IH₁.below_of_lt' <| (mul_lt_mul_iff_right₀ omega0_pos).1 <|
          (le_self_add (α := Ordinal) (b := m')).trans_lt ?_
        rw [← this, ← IH₂]
        exact h.snd'.repr_lt

Goal state after:
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
s t : Stream'.Seq α
h : dist s t ≤ 2⁻¹
⊢ s = nil ∧ t = nil ∨ ∃ hd s' t', s = Seq.cons hd s' ∧ t = Seq.cons hd t'

Tactic:
by
    cases s <;> cases t <;> norm_num at h <;> simp
    grind [dist_cons_cons_eq_one]

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

Goal state before:
pp: hd : ℝ → ℝ
tl : Basis
h : WellFormedBasis (hd :: tl)
f : ℝ → ℝ
hf : f ∈ tl
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)

Tactic:
rw [WellFormedBasis, List.pairwise_cons] at h
  exact h.left.left _ hf

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

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

Tactic:
simp only [friendlyOperation_iff_dist_le_dist, dist_cons_cons]

Goal state after:
α : Type u_1
hd : α
⊢ ∀ (s t : Stream'.Seq α), 2⁻¹ * dist s t ≤ dist s t
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
h : F b = none
⊢ gcorec F op b = nil

Tactic:
by
  unfold gcorec
  rw [Seq.gcorec_nil]
  · simp [nil]
  · simpa

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

Goal state before:
pp: 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_basis : WellFormedBasis (basis_hd :: basis_tl_hd :: basis_tl_tl)
h_length : tl.length = basis_tl_tl.length
⊢ Majorized (toFun tl basis_tl_tl) basis_hd 0

Tactic:
exact fun exp h_exp ↦
        (ih h_length h_basis.tail 1 (by simp)).trans <|
        h_basis.tail_pow_majorized_head (by simp) 1 exp h_exp

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

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
this : 0 + 1 = ↑m
⊢ m = 1

Tactic:
exact PNat.coe_inj.1 this.symm

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

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
this : m' + 1 + 1 = ↑m
⊢ m = 1

Tactic:
exact PNat.coe_inj.1 this.symm

Goal state after:
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
this : m' + 1 + 1 = ↑m
⊢ m = 1