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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
⊢ Countable ι

Tactic:
rcases isEmpty_or_nonempty ι with _ | hι
  · infer_instance
  · exact Countable.of_equiv _ orderIsoRangeToZOfLinearSuccPredArch.symm.toEquiv

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

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
⊢ toZ hι.some ((fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) n) = n

Tactic:
by
    rcases le_or_gt 0 n with hn | hn
    · simp_rw [if_pos hn]
      rw [toZ_iterate_succ]
      exact Int.toNat_of_nonneg hn
    · simp_rw [if_neg (not_le.mpr hn)]
      rw [toZ_iterate_pred]
      simp only [hn.le, Int.toNat_of_nonneg, Int.neg_nonneg_of_nonpos, Int.neg_neg]

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal n = map { toFun := fun i ↦ (n - i, i), inj' := ⋯ } (range (n + 1))

Tactic:
rw [← map_swap_antidiagonal, antidiagonal_eq_map, map_map]

Goal state after:
n : ℕ
⊢ map ({ toFun := fun i ↦ (i, n - i), inj' := ⋯ }.trans { toFun := Prod.swap, inj' := ⋯ }) (range (n + 1)) =
    map { toFun := fun i ↦ (n - i, i), inj' := ⋯ } (range (n + 1))
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: case mp
α : Type u
inst✝ : Semiring α
y : α
I : Ideal α
ya : α
hya : ya ∈ span {y}
b : α
hb : b ∈ I
⊢ ∃ a, ∃ b_1 ∈ I, a * y + b_1 = ya + b

Tactic:
obtain ⟨a, rfl⟩ := mem_span_singleton'.mp hya

Goal state after:
case mp
α : Type u
inst✝ : Semiring α
y : α
I : Ideal α
b : α
hb : b ∈ I
a : α
hya : a * y ∈ span {y}
⊢ ∃ a_1, ∃ b_1 ∈ I, a_1 * y + b_1 = a * y + b
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
ι : Type u_1
x : ι → α
⊢ range x \ {0} = range fun i ↦ x ↑i

Tactic:
ext1 a

Goal state after:
α : Type u
inst✝ : Semiring α
ι : Type u_1
x : ι → α
a : α
⊢ a ∈ range x \ {0} ↔ a ∈ range fun i ↦ x ↑i
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y : α
⊢ span {y - x, y} = span {x, y}

Tactic:
by
  rw [← span_pair_sub_right, sub_sub_cancel_left, span_insert_neg]

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

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
⊢ ↑x ^ (n + 1) ∈ ↑(span ((fun x ↦ x ^ (n + 1)) '' s))

Tactic:
exact subset_span ⟨x, x.prop, rfl⟩

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

Goal state before:
pp: case a
α : 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'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ l' ≤ l

Tactic:
hl'.le_basis_iff hl

Goal state after:
case a
α : 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'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ ∀ (i' : ι), p i' → ∃ i, p' i ∧ s' i ⊆ s i'
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
B : ∀ (s t : Set α), q s → q t → q (s ∩ t)
C : ∀ (i : ι), ∀ s ∈ f i, q s
𝓖 : Filter α := { sets := {t | q t}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
this : 𝓖 ≤ iInf f
⊢ p s

Tactic:
exact (this hs).2 s subset_rfl

Goal state after:
Module: Mathlib.Order.Interval.Set.Disjoint

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

Tactic:
rcases h.exists_between hx with ⟨y, hys, _, hyx⟩

Goal state after:
case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ x ∈ ⋃ i ∈ s, Ioi i
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : α → β
f : Filter α
g : Filter β
i : γ → α
h : range i ∈ f
⊢ map (m ∘ i) (comap i f) ≤ g ↔ Tendsto m f g

Tactic:
← map_compose

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α → β
f : Filter α
g : Filter β
i : γ → α
h : range i ∈ f
⊢ (map m ∘ map i) (comap i f) ≤ g ↔ Tendsto m f g
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ B ∈ F, f x ∈ B
V : Set α
U : Set β
U_in : U ∈ F
f_U_V : f ⁻¹' U ⊆ V
⊢ x ∈ V

Tactic:
exact f_U_V (h U U_in)

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
F : Filter β
u : α → β
inst✝ : Nonempty α
⊢ (F ⊓ map u atTop).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n, N ≤ n ∧ u n ∈ U

Tactic:
simp_rw [inf_neBot_iff_frequently_left, frequently_map, frequently_atTop]

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
F : Filter β
u : α → β
inst✝ : Nonempty α
⊢ (∀ {p : β → Prop}, (∀ᶠ (x : β) in F, p x) → ∀ (a : α), ∃ b, a ≤ b ∧ p (u b)) ↔
    ∀ U ∈ F, ∀ (N : α), ∃ n, N ≤ n ∧ u n ∈ U
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 : α
a✝ : True
⊢ f '' Ici a ∈ atTop

Tactic:
filter_upwards [eventually_ge_atTop (f a), eventually_ge_atTop b] with c hac hbc

Goal state after:
α : 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
c : β
hac : f a ≤ c
hbc : b ≤ c
⊢ c ∈ f '' Ici a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #↑s = cof α
⊢ #↑s < ℵ₀

Tactic:
exact hs'.trans_lt h

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

Goal state before:
pp: case h.a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
⊢ M' ≤ N (S.attach.sup f)

Tactic:
rw [← hS, span_le]

Goal state after:
case h.a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
⊢ ↑S ⊆ ↑(N (S.attach.sup f))
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulStrictMono α γ
_a : α
ha : 0 < _a
_b₁ _b₂ : β × γ
h₁ : _b₁.1 ≤ _b₂.1
h₂ : _b₁.2 < _b₂.2
⊢ (_a • _b₁).1 < (_a • _b₂).1 ∧ (_a • _b₁).2 ≤ (_a • _b₂).2 ∨ (_a • _b₁).1 ≤ (_a • _b₂).1 ∧ (_a • _b₁).2 < (_a • _b₂).2

Tactic:
exact .inr ⟨smul_le_smul_of_nonneg_left h₁ ha.le, smul_lt_smul_of_pos_left h₂ ha⟩

Goal state after:
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
⊢ DirSupInaccOn D s

Tactic:
intro d hd₀ hd₁ hd₂ a hda hd₃
  obtain ⟨b, hbd, hb⟩ := h hd₀ hd₁ hd₂ hda hd₃
  exact ⟨b, hbd, hb ⟨le_rfl, hbd⟩⟩

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : (i : ι) → Preorder (β i)
inst✝² : (i : ι) → SMul α (β i)
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : ∀ (i : ι), SMulPosReflectLE α (β i)
_b : (i : ι) → β i
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
⊢ _a₁ ≤ _a₂

Tactic:
obtain ⟨-, i, hi⟩ := lt_def.1 hb

Goal state after:
α : Type u_1
β✝ : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : (i : ι) → Preorder (β i)
inst✝² : (i : ι) → SMul α (β i)
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : ∀ (i : ι), SMulPosReflectLE α (β i)
_b : (i : ι) → β i
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
i : ι
hi : 0 i < _b i
⊢ _a₁ ≤ _a₂
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
n : ℕ
⊢ f^[n.succ] a ≤ ⨆ n, f^[n] a

Tactic:
exact le_ciSup hf' _

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

Goal state before:
pp: case refine_1
c : Cardinal.{v}
a : Ordinal.{max v u}
ha : a < Ordinal.lift.{u, v} c.ord
⊢ a < (lift.{u, v} c).ord

Tactic:
rcases Ordinal.lt_lift_iff.1 ha with ⟨a, _, rfl⟩
    rwa [lt_ord, ← lift_card, lift_lt, ← lt_ord, ← Ordinal.lift_lt]

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

Goal state before:
pp: case refine_2
c : Cardinal.{v}
⊢ (lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord

Tactic:
rw [ord_le, ← lift_card, card_ord]

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
x✝ : (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧ ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
h₁ : ∀ (a : Ordinal.{u}), f a < f (succ a)
h₂ : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
a✝ : Ordinal.{u}
ho : IsSuccLimit a✝
⊢ IsLUB (f '' Iio a✝) (f a✝)

Tactic:
rw [← h₂ _ ho]
      simpa [IsLUB, upperBounds, lowerBounds, IsLeast, bsup_le_iff] using le_bsup _

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

Goal state before:
pp: case inr.inr.inl
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
c : ℕ
⊢ c ≤ log (b ^ k) n ↔ c ≤ log b n / k

Tactic:
le_log_iff_pow_le (Nat.one_lt_pow (Nat.ne_of_gt hk) hb) hn,

Goal state after:
case inr.inr.inl
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
c : ℕ
⊢ (b ^ k) ^ c ≤ n ↔ c ≤ log b n / k
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
⊢ f i (⨆ i, List.foldr f a i) = ⨆ i, List.foldr f a i

Tactic:
H.map_iSup bddAbove_of_small

Goal state after:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
⊢ ⨆ i_1, f i (List.foldr f a i_1) = ⨆ i, List.foldr f a i
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
⊢ f i (⨆ b, derivFamily f ↑b) = ⨆ b, derivFamily f ↑b

Tactic:
H.map_iSup bddAbove_of_small

Goal state after:
case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
⊢ ⨆ i_1, f i (derivFamily f ↑i_1) = ⨆ b, derivFamily f ↑b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case zero
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ ∃ o, derivFamily f o = a

Tactic:
refine ⟨0, le_antisymm ?_ h₁⟩

Goal state after:
case zero
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ derivFamily f 0 ≤ a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case limit.inl
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : a = derivFamily f o
⊢ ∃ o, derivFamily f o = a

pp: case limit.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : a < derivFamily f o
⊢ ∃ o, derivFamily f o = a

Tactic:
· exact ⟨_, h.symm⟩

Goal state after:
case limit.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : a < derivFamily f o
⊢ ∃ o, derivFamily f o = a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ IsPrincipal op (nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o)

Tactic:
intro a b ha hb

Goal state after:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
ha : a < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o
hb : b < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o
⊢ op a b < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
⊢ nfp (fun x ↦ a + x) 0 = a * ω

Tactic:
simp [← iSup_iterate_eq_nfp]

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

Goal state before:
pp: case inl
b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ 0 ^ ω
⊢ nfp (fun x ↦ 0 * x) b = 0 ^ ω

Tactic:
rw [zero_opow omega0_ne_zero] at hba

Goal state after:
case inl
b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ 0
⊢ nfp (fun x ↦ 0 * x) b = 0 ^ ω
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inl
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ a ^ ω ≤ b

Tactic:
ha,

Goal state after:
case inl
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ 0 ^ ω ≤ b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inl
a b : Ordinal.{u_1}
ha : a = 0
⊢ a * b = b ↔ a ^ ω ∣ b

Tactic:
ha,

Goal state after:
case inl
a b : Ordinal.{u_1}
ha : a = 0
⊢ 0 * b = b ↔ 0 ^ ω ∣ b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: ⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) 2

Tactic:
intro a b ha hb

Goal state after:
a b : Ordinal.{u_1}
ha : a < 2
hb : b < 2
⊢ (fun x1 x2 ↦ x1 * x2) a b < 2
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inl
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂ : o ≠ 2
ho₁ : o < 2
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o

Tactic:
exact isPrincipal_add_of_le_one <| lt_two_iff.mp ho₁

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

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : o ≠ 0
⊢ preAleph o = ⨆ a, preAleph ↑a

Tactic:
exact isNormal_preAleph.apply_of_isSuccLimit ⟨by simpa, ho⟩

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

Goal state before:
pp: ⊢ preBeth 0 = 0

Tactic:
by
  rw [preBeth]
  simp

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

Goal state before:
pp: o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) o ↔ o ≤ 2 ∨ o ∈ Set.range fun x ↦ ω ^ ω ^ x

Tactic:
refine ⟨fun ho => ?_, ?_⟩
  · rcases le_or_gt o 2 with ho₂ | ho₂
    · exact Or.inl ho₂
    · rcases isPrincipal_add_iff_zero_or_omega0_opow.1
        (isPrincipal_add_of_isPrincipal_mul ho ho₂.ne') with (rfl | ⟨a, rfl⟩)
      · exact (not_lt_zero ho₂).elim
      · rcases isPrincipal_add_iff_zero_or_omega0_opow.1
          (isPrincipal_add_of_isPrincipal_mul_opow one_lt_omega0 ho) with (rfl | ⟨b, rfl⟩)
        · simp
        · exact Or.inr ⟨b, rfl⟩
  · rintro (ho₂ | ⟨a, rfl⟩)
    · exact isPrincipal_mul_of_le_two ho₂
    · exact isPrincipal_mul_omega0_opow_opow a

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

Goal state before:
pp: case inr
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
⊢ b = c

Tactic:
· have hc : c < ℵ₀ := by
      rw [← not_le]
      intro hc
      apply lt_irrefl ℵ₀
      apply (hc.trans (self_le_add_left _ a)).trans_lt
      rw [← h]
      apply add_lt_aleph0 ha hb
    rw [lt_aleph0] at *
    rcases ha with ⟨n, rfl⟩
    rcases hb with ⟨m, rfl⟩
    rcases hc with ⟨k, rfl⟩
    norm_cast at h ⊢
    apply add_left_cancel h

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

Goal state before:
pp: o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
x✝ : b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
⊢ a ≤ #ι

Tactic:
exact H _ hf

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

Goal state before:
pp: case neg
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∃ j, r j i ∧ f i ≤ f j
⊢ ∃ i', ∃ (hi' : i' < type r'), f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) i' hi'

Tactic:
obtain ⟨hji, hij⟩ := wo.wf.min_mem _ h

Goal state after:
case neg
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∃ j, r j i ∧ f i ≤ f j
hji : r (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h)
⊢ ∃ i', ∃ (hi' : i' < type r'), f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) i' hi'
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ho : 0 < o
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) (ω_ o)

Tactic:
intro a b ha hb

Goal state after:
case inr
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a < ω_ o
hb : b < ω_ o
⊢ (fun x1 x2 ↦ x1 ^ x2) a b < ω_ o
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) c.ord

Tactic:
intro a b ha hb

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a < c.ord
hb : b < c.ord
⊢ (fun x1 x2 ↦ x1 + x2) a b < c.ord
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) c.ord

Tactic:
intro a b ha hb

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a < c.ord
hb : b < c.ord
⊢ (fun x1 x2 ↦ x1 * x2) a b < c.ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccPrelimit b
⊢ (a * b).cof = b.cof

Tactic:
by
  by_cases hb' : IsMin b
  · simp [hb'.eq_bot]
  · exact cof_map_of_isNormal (isNormal_mul_right ha.pos) ⟨hb', hb⟩

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ #α ^ c

Tactic:
by
  rw [← add_one_eq (aleph0_le_mk α)]
  induction c using Cardinal.inductionOn with | _ β
  fapply mk_le_of_surjective
  · intro f
    use Sum.inl ⁻¹' range f
    refine le_trans (mk_preimage_of_injective _ _ fun x y => Sum.inl.inj) ?_
    apply mk_range_le
  rintro ⟨s, ⟨g⟩⟩
  classical
  use fun y => if h : ∃ x : s, g x = y then Sum.inl (Classical.choose h).val
               else Sum.inr (ULift.up 0)
  apply Subtype.ext; ext x
  constructor
  · rintro ⟨y, h⟩
    dsimp only at h
    by_cases h' : ∃ z : s, g z = y
    · rw [dif_pos h'] at h
      cases Sum.inl.inj h
      exact (Classical.choose h').2
    · rw [dif_neg h'] at h
      cases h
  · intro h
    have : ∃ z : s, g z = g ⟨x, h⟩ := ⟨⟨x, h⟩, rfl⟩
    use g ⟨x, h⟩
    dsimp only
    rw [dif_pos this]
    congr
    suffices Classical.choose this = ⟨x, h⟩ from congr_arg Subtype.val this
    apply g.2
    exact Classical.choose_spec this

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

Goal state before:
pp: case inr
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ¬(succ c).IsSingular

Tactic:
exact (isRegular_succ hc).not_isSingular

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ {i ∈ (↑s).toFinset | { toFun := f, support' := Trunc.mk s } i ≠ 0} ↔ { toFun := f, support' := Trunc.mk s } i ≠ 0

Tactic:
rw [Finset.mem_filter, Multiset.mem_toFinset, coe_mk']

Goal state after:
case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ ↑s ∧ f i ≠ 0 ↔ f i ≠ 0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
⊢ (fun c ↦ Trunc.lift (fun s ↦ ∑ i ∈ (↑s).toFinset, (φ i) (0 i)) c (support' 0)) ⋯ = 0

Tactic:
simp only [toFun_eq_coe, coe_zero, Pi.zero_apply, map_zero, Finset.sum_const_zero]; rfl

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι₁ : Type u_4
ι₂ : Type u_5
β₁ : ι₁ → Type u_1
β₂ : ι₂ → Type u_2
γ : Type u_3
inst✝⁴ : DecidableEq ι₁
inst✝³ : DecidableEq ι₂
inst✝² : (i : ι₁) → AddZeroClass (β₁ i)
inst✝¹ : (i : ι₂) → AddZeroClass (β₂ i)
inst✝ : AddCommMonoid γ
f₁ : Π₀ (i : ι₁), β₁ i
f₂ : Π₀ (i : ι₂), β₂ i
h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ
⊢ (sumAddHom fun i₂ ↦ (sumAddHom fun i₁ ↦ h i₁ i₂) f₁) f₂ =
    (sumAddHom fun i₁ ↦ (sumAddHom fun i₂ ↦ (h i₁ i₂).flip) f₂) f₁

Tactic:
obtain ⟨⟨f₁, s₁, h₁⟩, ⟨f₂, s₂, h₂⟩⟩ := f₁, f₂

Goal state after:
case mk.mk
ι₁ : Type u_4
ι₂ : Type u_5
β₁ : ι₁ → Type u_1
β₂ : ι₂ → Type u_2
γ : Type u_3
inst✝⁴ : DecidableEq ι₁
inst✝³ : DecidableEq ι₂
inst✝² : (i : ι₁) → AddZeroClass (β₁ i)
inst✝¹ : (i : ι₂) → AddZeroClass (β₂ i)
inst✝ : AddCommMonoid γ
h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ
f₁ : (i : ι₁) → β₁ i
support'✝¹ : Trunc { s // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 }
s₁ : Multiset ι₁
h₁ : ∀ (i : ι₁), i ∈ s₁ ∨ f₁ i = 0
f₂ : (i : ι₂) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 }
s₂ : Multiset ι₂
h₂ : ∀ (i : ι₂), i ∈ s₂ ∨ f₂ i = 0
⊢ (sumAddHom fun i₂ ↦ (sumAddHom fun i₁ ↦ h i₁ i₂) { toFun := f₁, support' := Quot.mk ⇑trueSetoid ⟨s₁, h₁⟩ })
      { toFun := f₂, support' := Quot.mk ⇑trueSetoid ⟨s₂, h₂⟩ } =
    (sumAddHom fun i₁ ↦ (sumAddHom fun i₂ ↦ (h i₁ i₂).flip) { toFun := f₂, support' := Quot.mk ⇑trueSetoid ⟨s₂, h₂⟩ })
      { toFun := f₁, support' := Quot.mk ⇑trueSetoid ⟨s₁, h₁⟩ }