mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i a✝ : ι
⊢ a✝ ∈ Iic (Order.succ i) ↔ a✝ ∈ Iic i ∪ {Order.succ i}

Tactic:
simp only [mem_Iic, mem_union, mem_singleton]

Goal state after:
α : Type u_1
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i a✝ : ι
⊢ a✝ ≤ Order.succ i ↔ a✝ ≤ i ∨ a✝ = Order.succ i
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' Set.Ioc a b = ↑(Ioc (c + a) (c + b))

Tactic:
coe_Ioc

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' Set.Ioc a b = Set.Ioc (c + a) (c + b)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' Set.Ioc a b = ↑(Ioc (a + c) (b + c))

Tactic:
coe_Ioc

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' Set.Ioc a b = Set.Ioc (a + c) (b + c)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)

Tactic:
by
  rw [← map_add_left_Ioo, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
step1 : f i \ (Iio i).sup f = (partialSups f) i \ (Iio i).sup f
⊢ disjointed (⇑(partialSups f)) i = disjointed f i

Tactic:
simp only [disjointed_apply, step1, funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion]

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
step1 : f i \ (Iio i).sup f = (partialSups f) i \ (Iio i).sup f
⊢ (Iic i).sup f \ ((Iio i).biUnion Iic).sup f = (Iic i).sup f \ (Iio i).sup f
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ -↑(Nat.find ⋯) = -max (- -↑(Nat.find ⋯)) 0

Tactic:
max_eq_left,

Goal state after:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ -↑(Nat.find ⋯) = - - -↑(Nat.find ⋯)

case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ 0 ≤ - -↑(Nat.find ⋯)
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
a✝ : ι
⊢ a✝ ∈ Iio (succ i) ↔ a✝ ∈ Iic i

Tactic:
simp only [mem_Iio, lt_succ_iff_eq_or_lt_of_not_isMax h, mem_Iic, le_iff_lt_or_eq, Or.comm]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_3
ι : Type u_4
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → Set α
hf : Monotone f
m n : ι
hm : n ≤ m
⊢ ⋃ i ∈ Ioc n m, disjointed f i = f m \ f n

Tactic:
by
  simp [← sup_Ioc_disjointed_of_monotone hf hm]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ a - x ∈ I

Tactic:
rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]

Goal state after:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ -↑⟨i, hi⟩ ∈ I
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
⊢ ⇑(mk I) ⁻¹' ⇑(mk I) '' s = ⋃ x, (fun y ↦ ↑x + y) '' s

Tactic:
ext x
  simp only [mem_preimage, mem_image, mem_iUnion, Ideal.Quotient.eq]
  exact
    ⟨fun ⟨a, a_in, h⟩ => ⟨⟨_, I.neg_mem h⟩, a, a_in, by simp⟩, fun ⟨⟨i, hi⟩, a, ha, Eq⟩ =>
      ⟨a, ha, by rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]; exact I.neg_mem hi⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
x : R
⊢ ∃ a, (lift I f H) a = f x

Tactic:
use Ideal.Quotient.mk I x

Goal state after:
case h
R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
x : R
⊢ (lift I f H) ((mk I) x) = f x
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
x : Finset α
h0 : x.Nonempty
⊢ ∑ m ∈ x.powerset, (-1) ^ #m = 0

Tactic:
classical
  rw [sum_powerset_neg_one_pow_card]
  exact if_neg (nonempty_iff_ne_empty.mp h0)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case right
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
⊢ ∀ (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
x

Goal state after:
case right
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
⊢ I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
⊢ ⊤ ≤ span (range fun i ↦ Pi.single i 1)

Tactic:
rintro x -

Goal state after:
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
x : (j : ι) → R j
⊢ x ∈ span (range fun i ↦ Pi.single i 1)
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
⊢ ∀ {x y : Set ℕ}, x ∈ range Ici → y ∈ range Ici → ∃ z ∈ range Ici, z ⊆ x ∩ y

Tactic:
rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
n m : ℕ
⊢ ∃ z ∈ range Ici, z ⊆ Ici n ∩ Ici m
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s : Set (Set α)
f : Filter α
h : s ⊆ f.sets
x✝¹ : Set α
hu : x✝¹ ∈ generate s
s✝ t✝ : Set α
x✝ : GenerateSets s s✝
hxy : s✝ ⊆ t✝
⊢ s✝ ∈ f → t✝ ∈ f

Tactic:
by gcongr

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_5
M : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
X : Type u_7
Y : Type u_8
inst✝³ : Finite X
inst✝² : Finite Y
inst✝¹ : DecidableEq X
inst✝ : DecidableEq Y
f : X → Y
x : X
m : M
⊢ (linearMap R M f) (Pi.single x m) = Pi.single (f x) m

Tactic:
by
  apply map_piSingle

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
⊢ comap inl (map inr g) = ⊥

Tactic:
ext
  rw [mem_comap_iff_compl]
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
⊢ comap inr (map inl f) = ⊥

Tactic:
ext
  rw [mem_comap_iff_compl]
  simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ ¬Disjoint l l' ↔ ¬∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')

Tactic:
by simp only [_root_.disjoint_iff, ← Ne.eq_def, ← neBot_iff, inf_eq_inter,
    hl.inf_basis_neBot_iff hl', not_exists, not_and, bot_eq_empty, ← nonempty_iff_ne_empty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' (V ∩ f ⁻¹' Z) ⊆ f '' (V ∩ W)

Tactic:
by gcongr

Goal state after:
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 : M →ₗ[R] M
⊢ ∀ᶠ (n : ℕ) in atTop, ⨆ m, (f ^ m).ker = (f ^ n).ker

Tactic:
by
  obtain ⟨n, hn : ∀ m, n ≤ m → ker (f ^ n) = ker (f ^ m)⟩ :=
    monotone_stabilizes_iff_noetherian.mpr inferInstance f.iterateKer
  refine eventually_atTop.mpr ⟨n, fun m hm ↦ ?_⟩
  refine le_antisymm (iSup_le fun l ↦ ?_) (le_iSup (fun i ↦ LinearMap.ker (f ^ i)) m)
  rcases le_or_gt m l with h | h
  · rw [← hn _ (hm.trans h), hn _ hm]
  · exact f.iterateKer.monotone h.le

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ ¬IsCofinal s ↔ BddAbove s

Tactic:
use .of_not_isCofinal

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ BddAbove s → ¬IsCofinal s
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst✝⁶ : CommSemiring A₁
inst✝⁵ : CommSemiring B₁
inst✝⁴ : CommSemiring A₂
inst✝³ : Semiring B₂
inst✝² : Algebra A₁ B₁
inst✝¹ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
inst✝ : Module.Finite A₁ B₁
this✝ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
⊢ Module.Finite A₂ B₂

Tactic:
have : IsScalarTower A₁ A₂ B₁ := IsScalarTower.of_algebraMap_eq
    (fun x ↦ by simp [RingHom.algebraMap_toAlgebra])

Goal state after:
A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst✝⁶ : CommSemiring A₁
inst✝⁵ : CommSemiring B₁
inst✝⁴ : CommSemiring A₂
inst✝³ : Semiring B₂
inst✝² : Algebra A₁ B₁
inst✝¹ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
inst✝ : Module.Finite A₁ B₁
this✝¹ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this✝ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
this : IsScalarTower A₁ A₂ B₁
⊢ Module.Finite A₂ B₂
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
⊢ IsLUB d a → a ∈ s → (d ∩ s).Nonempty

Tactic:
hda

Goal state after:
α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ a ∈ s → (d ∩ s).Nonempty
Module: Mathlib.Order.DirSupClosed

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

Tactic:
hda

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : α
d : Set α
hda : d ⊆ {a}
⊢ d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a_3 : α⦄, IsLUB d a_3 → a_3 ∈ {a}
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 : type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding

Tactic:
· rw [← lift_id (type s)] at h ⊢
      obtain ⟨f⟩ := lift_type_lt.{_,_,v}.1 h
      obtain ⟨f, a, hf⟩ := f
      exists a
      induction a using inductionOn with | type α r
      refine lift_type_eq.{u, max (u + 1) v, max (u + 1) v}.2
        ⟨(RelIso.ofSurjective (RelEmbedding.ofMonotone ?_ ?_) ?_).symm⟩
      · exact fun b => enum r ⟨f b, (hf _).1 ⟨_, rfl⟩⟩
      · refine fun a b h => (typein_lt_typein r).1 ?_
        rw [typein_enum, typein_enum]
        exact f.map_rel_iff.2 h
      · intro a'
        obtain ⟨b, e⟩ := (hf _).2 (typein_lt_type _ a')
        exists b
        simp only [RelEmbedding.ofMonotone_coe]
        simp [e]

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

Goal state before:
pp: c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
have := ord_lt_ord.2 h
    rw [ord_univ] at this
    obtain ⟨o, e⟩ := Ordinal.liftPrincipalSeg.mem_range_of_rel_top (by simpa)
    have := card_ord c
    rw [← e, Ordinal.liftPrincipalSeg_coe, ← Ordinal.lift_card] at this
    exact ⟨_, this.symm⟩

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

Goal state before:
pp: case mpr
α : Type u
⊢ (∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c') → Small.{v, u} α

Tactic:
· rintro ⟨c, hc⟩
    exact ⟨⟨c.out, lift_mk_eq.{u, _, v + 1}.1 (hc.trans (congr rfl c.mk_out.symm))⟩⟩

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x : α
⊢ ∀ b ∈ {x}, r b ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Tactic:
intro b hb

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : b ∈ {x}
⊢ r b ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_3
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
b : α
⊢ (RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯) b < type r

Tactic:
exact (PrincipalSeg.ofElement _ _).ordinal_type_lt

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

Goal state before:
pp: case refine_3
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯) → a < type r

Tactic:
rintro ⟨b, rfl⟩
    exact (PrincipalSeg.ofElement _ _).ordinal_type_lt

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

Goal state before:
pp: a b c : Ordinal.{u_4}
h : a - b ≤ c
⊢ b + (a - b) ≤ b + c

Tactic:
by gcongr

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

Goal state before:
pp: a b c : Ordinal.{u_4}
hc : c ≠ 0
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ b + d < b + c

Tactic:
by gcongr

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

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a * b = 0 ↔ a = 0 ∨ b = 0

Tactic:
induction a, b using inductionOn₂ with

Goal state after:
case type
α : Type u_4
r✝ : α → α → Prop
inst✝¹ : IsWellOrder α r✝
β : Type u_4
s✝ : β → β → Prop
inst✝ : IsWellOrder β s✝
⊢ type r✝ * type s✝ = 0 ↔ type r✝ = 0 ∨ type s✝ = 0
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) := ⋯
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b : α
hb : ∀ b_1 < a, (Subtype.val ∘ ⇑(enum s hs)) b_1 ≤ b
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := ⋯
this : ConditionallyCompleteLinearOrderBot α := ⋯
⊢ (Subtype.val ∘ ⇑(enum s hs)) a ≤ sSup (Subtype.val ∘ ⇑(enum s hs) '' Iio a)

pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) := ⋯
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b : α
hb : ∀ b_1 < a, (Subtype.val ∘ ⇑(enum s hs)) b_1 ≤ b
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := ⋯
this : ConditionallyCompleteLinearOrderBot α := ⋯
⊢ sSup (Subtype.val ∘ ⇑(enum s hs) '' Iio a) ≤ b

Tactic:
· refine enum_le_of_forall_lt (hs' ?_ ?_ (isLUB_csSup' bdd)) fun b hb ↦ ?_
    · grind
    · simpa using ha.ne_bot
    · obtain ⟨c, hca, hbc⟩ := ha.lt_iff_exists_lt.1 hb
      refine (H hbc).trans_le <| le_csSup bdd ⟨c, ?_⟩
      simpa

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) := ⋯
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b : α
hb : ∀ b_1 < a, (Subtype.val ∘ ⇑(enum s hs)) b_1 ≤ b
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := ⋯
this : ConditionallyCompleteLinearOrderBot α := ⋯
⊢ sSup (Subtype.val ∘ ⇑(enum s hs) '' Iio a) ≤ b
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: case mpr.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
⊢ ∀ b < sInf t, enumOrd s b < a

Tactic:
intro b hb

Goal state after:
case mpr.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
b : Ordinal.{u}
hb : b < sInf t
⊢ enumOrd s b < a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : IsSuccLimit b
H : ∀ b' < b, a * b' ≤ c
⊢ ¬c < a * b

Tactic:
induction a, b using inductionOn₂ with

Goal state after:
case type
c : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
inst✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
inst✝ : IsWellOrder β s
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
⊢ ¬c < type r * type s
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : (#α).ord ≤ type s
⊢ #α ≤ (type s).card

Tactic:
e

Goal state after:
case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : type r ≤ type s
⊢ #α ≤ (type s).card
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case add_one
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
IH : (a + b) * (c + 1) = a * (c + 1) + b
⊢ a * (c + 1) + b + a + b = a * (c + 1 + 1) + b

Tactic:
add_assoc _ b,

Goal state after:
case add_one
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
IH : (a + b) * (c + 1) = a * (c + 1) + b
⊢ a * (c + 1) + (b + a) + b = a * (c + 1 + 1) + b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
H : a % b = 0
⊢ a = b * (a / b)

Tactic:
simpa [H] using (div_add_mod a b).symm

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b c m n : ℕ
hc : 1 < c
hb : c ≤ b
hmn : m ≤ n
⊢ log c m ≤ log c n

Tactic:
by gcongr

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

Goal state before:
pp: case succ
a : Ordinal.{u_1}
n : ℕ
IH : a ^ ↑n = a ^ n
⊢ a ^ succ ↑n = a ^ (n + 1)

Tactic:
opow_succ,

Goal state after:
case succ
a : Ordinal.{u_1}
n : ℕ
IH : a ^ ↑n = a ^ n
⊢ a ^ ↑n * a = a ^ (n + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ succ c < b ^ succ c

Tactic:
opow_succ,

Goal state after:
a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ c * a < b ^ succ c
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
by gcongr

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

Goal state before:
pp: case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
⊢ ∀ d < ω, ω * (x / ω) + d ≤ a

Tactic:
intro b hb

Goal state after:
case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
b : Ordinal.{u_4}
hb : b < ω
⊢ ω * (x / ω) + b ≤ a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ b ^ c ≤ x ↔ c ≤ log b x

Tactic:
by
  obtain rfl | hx := eq_or_ne x 0
  · simpa [hc] using hb.ne_bot
  · exact opow_le_iff_le_log hb hx

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b c m n : ℕ
hc : 1 < c
hb : c ≤ b
hmn : m ≤ n
⊢ clog c m ≤ clog c n

Tactic:
by gcongr

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

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsSuccPrelimit c.ord

Tactic:
· simp_rw [isSuccPrelimit_iff_succ_lt, succ_eq_add_one, lt_ord, card_add_one]
    refine fun a ha ↦ ?_
    contrapose! ha
    rwa [add_one_of_aleph0_le] at ha
    rw [← ord_le, ← IsSuccLimit.le_succ_iff, succ_eq_add_one, ord_le, card_add_one]
    · exact hc.trans ha
    · simp

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl
b k n : ℕ
hk : k > 0
hb : 1 < b
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
refine eq_of_forall_lt_iff fun c ↦ ?_
      rw [lt_clog_iff_pow_lt (Nat.one_lt_pow (Nat.ne_of_gt hk) hb), Nat.lt_div_iff_mul_lt hk,
        Nat.add_sub_cancel, lt_clog_iff_pow_lt hb, Nat.pow_mul']

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

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ nfp f a

Tactic:
rw [← iSup_iterate_eq_nfp]

Goal state after:
f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ ⨆ n, f^[n] a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ a < nfp f b ↔ ∃ n, a < f^[n] b

Tactic:
rw [← iSup_iterate_eq_nfp]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ a < ⨆ n, f^[n] b ↔ ∃ n, a < f^[n] b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ nfp f a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b

Tactic:
rw [← iSup_iterate_eq_nfp]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ ⨆ n, f^[n] a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : StrictMono f
a : Ordinal.{u}
h : a < f a
n : ℕ
⊢ f^[n] a < nfp f a

Tactic:
by
  apply (hf.iterate n h).trans_le
  rw [← iterate_succ_apply]
  exact iterate_le_nfp ..

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

Goal state before:
pp: a : Ordinal.{u_1}
⊢ nfp 0 a = a

Tactic:
rw [← iSup_iterate_eq_nfp]

Goal state after:
a : Ordinal.{u_1}
⊢ ⨆ n, 0^[n] a = a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1.inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
⊢ a + o = o

Tactic:
cases le_one_iff.1 ho₁

Goal state after:
case refine_1.inr.inl
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
h✝ : o = 0
⊢ a + o = o

case refine_1.inr.inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
h✝ : o = 1
⊢ a + o = o