mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case inr.h
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
⊢ ∀ (ne : s.Nonempty), n = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y

Tactic:
_

Goal state after:
case inr.h
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
⊢ n = s.max' ne✝ → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ t ∈ ⨅ i ∈ dom, l i ↔ ∃ i, (i.fst ∈ dom ∧ p i.fst i.snd) ∧ s i.fst i.snd ⊆ t

Tactic:
mem_biInf_of_directed h hdom,

Goal state after:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (∃ i ∈ dom, t ∈ l i) ↔ ∃ i, (i.fst ∈ dom ∧ p i.fst i.snd) ∧ s i.fst i.snd ⊆ t
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ t ∈ ⨅ i ∈ dom, l i ↔ ∃ i, (i.1 ∈ dom ∧ p i.1 i.2) ∧ s i.1 i.2 ⊆ t

Tactic:
mem_biInf_of_directed h hdom,

Goal state after:
α : Type u_1
ι : Type u_6
ι' : Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (∃ i ∈ dom, t ∈ l i) ↔ ∃ i, (i.1 ∈ dom ∧ p i.1 i.2) ∧ s i.1 i.2 ⊆ t
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ Ioi a
⊢ x ∈ ⋃ i ∈ s, Ici i

Tactic:
rcases a_glb.exists_between hx with ⟨y, hys, _, hyx⟩
    rw [mem_iUnion₂]
    exact ⟨y, hys, hyx.le⟩

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
⊢ (iInf f).NeBot

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h✝ : IsEmpty ι
⊢ (iInf f).NeBot

case inr
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h✝ : Nonempty ι
⊢ (iInf f).NeBot
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
h : ∀ᶠ (x : α) in f, p x
x✝ : Set α
a✝ : α
pa : p a✝
⊢ a✝ ∈ x✝ → p a✝

Tactic:
_

Goal state after:
α : Type u
f : Filter α
p : α → Prop
h : ∀ᶠ (x : α) in f, p x
x✝ : Set α
a✝¹ : α
pa : p a✝¹
a✝ : a✝¹ ∈ x✝
⊢ p a✝¹
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p q : α → Prop
⊢ (∃ᶠ (x : α) in f, p x → q x) ↔ (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in f, q x

Tactic:
by
  simp [imp_iff_not_or]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ (map (fun x1 x2 ↦ x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x1 x2 ↦ x1 ∘ x2) h
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x1 x2 ↦ x1 ∘ x2) '' w ⊆ u
⊢ (u.seq v).seq t ∈ h.seq (g.seq x)

Tactic:
← hu

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ (map (fun x1 x2 ↦ x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x1 x2 ↦ x1 ∘ x2) h
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x1 x2 ↦ x1 ∘ x2) '' w ⊆ u
⊢ (((fun x1 x2 ↦ x1 ∘ x2) '' w).seq v).seq t ∈ h.seq (g.seq x)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
m : α → β
⊢ InjOn (map m) (Iic (𝓟 s)) ↔ InjOn m s

Tactic:
refine ⟨fun hm x hx y hy hxy ↦ ?_, fun hm F hF G hG ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : m x = m y
⊢ x = y

case refine_2
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn m s
F : Filter α
hF : F ∈ Iic (𝓟 s)
G : Filter α
hG : G ∈ Iic (𝓟 s)
⊢ map m F = map m G → F = G
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
a : α
⊢ True → f '' Ici a ∈ atTop

Tactic:
_

Goal state after:
case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
a : α
a✝ : True
⊢ f '' Ici a ∈ atTop
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : n ≤ m
x : M
hx : (f ^ m) x ∈ ↑(LinearMap.ker (f ^ n))
⊢ (f ^ n) x = 0

Tactic:
replace hx : x ∈ LinearMap.ker (f ^ (n + m)) := by
    simpa [f.pow_apply n, f.pow_apply m, ← f.pow_apply (n + m), ← iterate_add_apply] using hx

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : n ≤ m
x : M
hx : x ∈ LinearMap.ker (f ^ (n + m))
⊢ (f ^ n) x = 0
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
hs : IsCofinal s
hf : Monotone f
hf' : IsCofinal (range f)
⊢ IsCofinal (f '' s)

Tactic:
by
  intro a
  obtain ⟨_, ⟨b, rfl⟩, hb⟩ := hf' a
  obtain ⟨c, hc, hc'⟩ := hs b
  exact ⟨_, mem_image_of_mem f hc, hb.trans (hf hc')⟩

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
c : Cardinal.{max u v}
⊢ c ≤ lift.{v, u} (⨅ s, #↑↑s) ↔ ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #↑s

Tactic:
lift_iInf,

Goal state after:
α : Type u
inst✝ : Preorder α
c : Cardinal.{max u v}
⊢ c ≤ ⨅ i, lift.{v, u} #↑↑i ↔ ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #↑s
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : ↑s → α
hg : ∀ (x : ↑s), ↑x ≤ f (g x)
a b : α
hb : f a ≤ f b
c : β
hc : c ∈ s
hc' : f b ≤ c
⊢ ∃ y ∈ range g, a ≤ y

Tactic:
refine ⟨_, Set.mem_range_self ⟨c, hc⟩, ?_⟩

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : ↑s → α
hg : ∀ (x : ↑s), ↑x ≤ f (g x)
a b : α
hb : f a ≤ f b
c : β
hc : c ∈ s
hc' : f b ≤ c
⊢ a ≤ g ⟨c, hc⟩
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ lift.{v, u} (cof α) = lift.{u, v} (cof β)

Tactic:
apply le_antisymm <;> rw [le_lift_cof_iff] <;> intro s hs
  · have H (x : s) : ∃ y : α, x ≤ f y := by simpa using hf' x
    choose g hg using H
    refine (lift_le.2 <| cof_le (s := range g) fun a ↦ ?_).trans mk_range_le_lift
    obtain ⟨_, ⟨b, rfl⟩, hb⟩ := hf' (f a)
    obtain ⟨c, hc, hc'⟩ := hs (f b)
    refine ⟨_, Set.mem_range_self ⟨c, hc⟩, ?_⟩
    rw [← hf.le_iff_le]
    exact hb.trans (hc'.trans (hg ⟨c, hc⟩))
  · exact (lift_le.2 <| cof_le (hs.image hf.monotone hf')).trans mk_image_le_lift

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

Goal state before:
pp: α γ : Type u
inst✝¹ : Preorder α
inst✝ : Preorder γ
f : γ → α
g : α → γ
h : GaloisConnection f g
⊢ cof γ ≤ cof α

Tactic:
by
  simpa using h.cof_le_lift

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
t : Finset M
⊢ IsCompactElement (span R ↑t)

Tactic:
span_eq_iSup_of_singleton_spans,

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
t : Finset M
⊢ IsCompactElement (⨆ x ∈ ↑t, R ∙ x)
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_7
P : Type u_6
inst✝² : Semiring S
inst✝¹ : AddCommMonoid P
inst✝ : Module S P
σ : R →+* S
hM : ⊤.FG
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
⊢ ⊤.FG

Tactic:
Submodule.fg_def

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_7
P : Type u_6
inst✝² : Semiring S
inst✝¹ : AddCommMonoid P
inst✝ : Module S P
σ : R →+* S
hM : ∃ S, S.Finite ∧ span R S = ⊤
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
⊢ ∃ S_1, S_1.Finite ∧ span S S_1 = ⊤
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
d : Set α
hda : d ⊆ {a}
hdn : d.Nonempty
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a_2 : α⦄, IsLUB d a_2 → a_2 ∈ {a}

Tactic:
_

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : α
d : Set α
hda : d ⊆ {a}
hdn : d.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
⊢ ∀ ⦃a_1 : α⦄, IsLUB d a_1 → a_1 ∈ {a}
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
hb : b ⋖ f a
⊢ False

Tactic:
obtain ⟨c, hc, hc'⟩ := (hf.lt_iff_exists_lt ha).1 hb.lt
    have hc' := hb.ge_of_gt hc'
    rw [hf.strictMono.le_iff_le] at hc'
    exact hc.not_ge hc'

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → ∀ ⦃a : α⦄, IsLUB s a → a ∈ range f

Tactic:
_

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ ∀ ⦃a : α⦄, IsLUB s a → a ∈ range f
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
⊢ ∀ [inst : IsWellOrder β s], type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type s < univ.{u, v}

Tactic:
_

Goal state after:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type s < univ.{u, v}
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
a : Ordinal.{u}
e : liftInitialSeg.toRelEmbedding a = type s
α : Type u
r : α → α → Prop
⊢ ∀ [inst : IsWellOrder α r], liftInitialSeg.toRelEmbedding (type r) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

Tactic:
_

Goal state after:
case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
a : Ordinal.{u}
e : liftInitialSeg.toRelEmbedding a = type s
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ liftInitialSeg.toRelEmbedding (type r) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
a : Ordinal.{u}
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < a
⊢ liftInitialSeg.toRelEmbedding a = lift.{max (u + 1) v, max (u + 1) v} (type s)

Tactic:
induction a using inductionOn with

Goal state after:
case mpr.type
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
⊢ liftInitialSeg.toRelEmbedding (type r) = lift.{max (u + 1) v, max (u + 1) v} (type s)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Subsingleton α
⊢ typeLT α ≤ (cof α).ord

Tactic:
cases isEmpty_or_nonempty α
    · simpa
    · cases nonempty_unique α
      have := BoundedOrder.ofUnique α
      simp

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

Goal state before:
pp: case h
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : s ≺i r
⊢ (RelEmbedding.ofMonotone lift.{u, v} liftInitialSeg._proof_1) ((typein r).toRelEmbedding f.top) = type s

Tactic:
rw [RelEmbedding.ofMonotone_coe, ← lift_umax, lift_typein_top, lift_id']

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

Goal state before:
pp: case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
⊢ typeLT α ∈ range succ

Tactic:
refine ⟨typein (α := α) (· < ·) a, eq_of_forall_lt_iff fun o ↦ ?_⟩
    rw [lt_succ_iff]
    refine ⟨fun h ↦ h.trans_lt (typein_lt_type _ _), fun h ↦ ?_⟩
    rw [← typein_enum _ h, typein_le_typein, not_lt]
    apply ha

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ iSup f = lsub f ↔ ∀ a < lsub f, succ a < lsub f

Tactic:
refine ⟨fun h => ?_, fun hf => le_antisymm (iSup_le_lsub f) (lsub_le fun i => ?_)⟩

Goal state after:
case refine_1
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
⊢ ∀ a < lsub f, succ a < lsub f

case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
⊢ f i < iSup f
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
b1 : 0 < b
⊢ a ≤ a ^ b

Tactic:
← opow_one a

Goal state after:
a b : Ordinal.{u_1}
b1 : 0 < b
⊢ a ^ 1 ≤ a ^ b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl.inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1✝ : a ≤ 1
a1 : a = 1
⊢ 1 ^ 1 ≤ 1 ^ b

Tactic:
one_opow,

Goal state after:
case inl.inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1✝ : a ≤ 1
a1 : a = 1
⊢ 1 ≤ 1 ^ b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
ha : 1 < a
hb : 1 < b
| a

Tactic:
← opow_one a

Goal state after:
a b : Ordinal.{u_1}
ha : 1 < a
hb : 1 < b
| a ^ 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ sSup ((fun x ↦ 1 ^ x) ⁻¹' Iic x) = 0

Tactic:
one_opow,

Goal state after:
case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ sSup ((fun x ↦ 1) ⁻¹' Iic x) = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
⊢ clog b (n + 1) ≤ clog b n → clog b n ≤ clog b (n + 1)

Tactic:
exact fun _ ↦ clog_monotone b (le_add_right n 1)

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

Goal state before:
pp: case inl
b : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (0 ^ b)

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)
    · rw [opow_zero]
      exact isPrincipal_add_one
    · rwa [zero_opow hb]

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

Goal state before:
pp: a : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) a
b : Ordinal.{u_1}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a ^ b)

Tactic:
by
  rcases isPrincipal_add_iff_zero_or_omega0_opow.1 ha with (rfl | ⟨c, rfl⟩)
  · rcases eq_or_ne b 0 with (rfl | hb)
    · rw [opow_zero]
      exact isPrincipal_add_one
    · rwa [zero_opow hb]
  · rw [← opow_mul]
    exact isPrincipal_add_omega0_opow _

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr.inr.inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
· exact le_max_of_le_right (mul_lt_aleph0 ha hb).le

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ preBeth (o + 1) = 2 ^ preBeth o

Tactic:
rw [preBeth, ← succ_eq_add_one, Iio_succ]

Goal state after:
o : Ordinal.{u_1}
⊢ ⨆ a, 2 ^ preBeth ↑a = 2 ^ preBeth o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_2.inl
a b : Cardinal.{u_1}
hb : b ≠ 0
ha : ℵ₀ ≤ a
hab : b ≤ a
⊢ max a b = a

Tactic:
max_eq_left hab

Goal state after:
case refine_2.inl
a b : Cardinal.{u_1}
hb : b ≠ 0
ha : ℵ₀ ≤ a
hab : b ≤ a
⊢ a = a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ preBeth (Ordinal.lift.{v, u_1} ω + Ordinal.lift.{v, u_1} o) = preBeth (ω + Ordinal.lift.{v, u_1} o)

Tactic:
lift_omega0

Goal state after:
o : Ordinal.{u_1}
⊢ preBeth (ω + Ordinal.lift.{v, u_1} o) = preBeth (ω + Ordinal.lift.{v, u_1} o)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
by
  rcases le_or_gt ℵ₀ a with ha | ha
  · rw [add_eq_max ha]
    exact le_max_left _ _
  · rcases le_or_gt ℵ₀ b with hb | hb
    · rw [add_comm, add_eq_max hb, max_comm]
      exact le_max_left _ _
    · exact le_max_of_le_right (add_lt_aleph0 ha hb).le

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ max a b
⊢ max a b < c

Tactic:
exact max_lt h1 h2

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℶ_ ↑n = lift.{v, u} c ↔ ℶ_ ↑n = c

Tactic:
by
  simpa using lift_inj (a := ℶ_ n)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : IsEmpty ι
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

case inr
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
⊢ (⨆ i, f i) * c = ⨆ i, f i * c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case add_one
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ (a ^ b * a).card ≤ max a.card (b + 1).card

Tactic:
card_mul,

Goal state after:
case add_one
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ (a ^ b).card * a.card ≤ max a.card (b + 1).card
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
H : c.IsRegular
⊢ 0 < c.ord

Tactic:
rw [Cardinal.lt_ord, card_zero]
  exact H.pos

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type (max u_1 u_2)
f : ι → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c.ord.cof

Tactic:
by rwa [hc.cof_ord]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c.ord.cof

Tactic:
by rwa [hc.cof_ord]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
ho : lift.{v, u} o.card < c
⊢ lift.{v, u} o.card < c.ord.cof

Tactic:
by rwa [hc.cof_ord]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{max u_1 u_2}
f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
ho : o.card < c
⊢ o.card < c.ord.cof

Tactic:
by rwa [hc.cof_ord]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} o.card < c
⊢ lift.{v, u} o.card < c.ord.cof

Tactic:
by rwa [hc.cof_ord]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{max u_1 u_2}
f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
hι : o.card < c
⊢ o.card < c.ord.cof

Tactic:
by rwa [hc.cof_ord]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u_1
f : ι → Cardinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c.ord.cof

Tactic:
by rwa [hc.cof_ord]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
⊢ lift.{?u.55, u} #ι < c.ord.cof

Tactic:
by rwa [hc.cof_ord]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b < c.ord → derivFamily f b < c.ord
hb' : b + 1 < c.ord
⊢ lift.{?u.60, u} #ι < c.ord.cof

Tactic:
by rwa [hc.cof_ord]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ (ω * ω).card < c

Tactic:
card_mul,

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ω.card * ω.card < c
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ ((sumAddHom fun i ↦ (S i).subtype).comp (filterAddMonoidHom (fun i ↦ ↥(S i)) p)) (single i ⟨y, hy⟩) = y

Tactic:
AddMonoidHom.comp_apply,

Goal state after:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ (sumAddHom fun i ↦ (S i).subtype) ((filterAddMonoidHom (fun i ↦ ↥(S i)) p) (single i ⟨y, hy⟩)) = y