mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : s.Finite
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1

Tactic:
by_cases h : a ∈ s

Goal state after:
case pos
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : s.Finite
h : a ∈ s
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1

case neg
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : s.Finite
h : a ∉ s
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

Tactic:
by_cases h : a ∈ s

Goal state after:
case pos
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

case neg
α : Type u_1
s : Set α
a : α
h : a ∉ s
⊢ s.ncard - 1 ≤ (s \ {a}).ncard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s

Tactic:
exact s.mul_mem_cancel_right h

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
⊢ (fun a ↦ Quotient.map' (fun b ↦ f a.1 * ↑b) ⋯ a.2)
      ((fun a ↦ (Quotient.map' id ⋯ a, Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a))
        (Quotient.mk'' a)) =
    Quotient.mk'' a

Tactic:
simp_rw [Quotient.map'_mk'', id, mul_inv_cancel_left]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ hs.toFinset.card ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
Finset.card_le_one,

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ (∀ a ∈ hs.toFinset, ∀ b ∈ hs.toFinset, a = b) ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
⊢ sSup S = ringConGen fun x y ↦ ∃ c ∈ S, c x y

Tactic:
by
  rw [sSup_def]
  congr! with x y
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
b : (i : ι) → φ i
hb : ∀ i ∈ J, b i = 0
i : ι
hiI : i ∉ I
⊢ Pi.single i (b i) i = 0

Tactic:
rw [Pi.single_eq_same]

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
b : (i : ι) → φ i
hb : ∀ i ∈ J, b i = 0
i : ι
hiI : i ∉ I
⊢ b i = 0
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a < b
⊢ insert a (Ico (succ a) b) = Ico a b

Tactic:
Ico_succ_left_of_not_isMax h.not_isMax,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a < b
⊢ insert a (Ioo a b) = Ico a b
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
a : α
⊢ ↑(Icc a (pred b)) = ↑(Ico a b)

Tactic:
simpa using Set.Icc_pred_right_eq_Ico_of_not_isMin hb _

Goal state after:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
⊢ ↑(Ioi (pred a)) = ↑(Ici a)

Tactic:
by simpa using Set.Ioi_pred_eq_Ici_of_not_isMin ha

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: n : ℕ
⊢ (∑ i ∈ range n, i) * 2 = ∑ i ∈ range n, i + ∑ i ∈ range n, (n - 1 - i)

Tactic:
by
      rw [sum_range_reflect (fun i => i) n, mul_two]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ IsIdempotentElem (a + b) ↔ a * b + b * a = 0

Tactic:
refine ⟨fun h ↦ ?_, ha.add hb⟩
  rw [← add_right_cancel_iff (a := b), add_assoc, ← add_left_cancel_iff (a := a),
    ← add_assoc, add_add_add_comm]
  simpa [add_mul, mul_add, ha.eq, hb.eq] using h.eq

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x ∈ (LinearMap.toSpanSingleton R R e).ker ↔ x ∈ Ideal.span {1 - e}

Tactic:
rw [Ideal.mem_span_singleton']

Goal state after:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x ∈ (LinearMap.toSpanSingleton R R e).ker ↔ ∃ a, a * (1 - e) = x
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
⊢ (a + b) ^ k ∈ I

Tactic:
simp_rw [hab.add_pow, ← Nat.cast_comm]
  apply I.sum_mem
  intro c _
  apply mul_mem_left
  by_cases h : m ≤ c
  · rw [hab.pow_pow]
    exact I.mul_mem_left _ (I.pow_mem_of_pow_mem ha h)
  · refine I.mul_mem_left _ (I.pow_mem_of_pow_mem hb ?_)
    lia

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

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c < n + 1
⊢ ∃ a_1,
    ∃ z ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset,
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = a_1 * a ^ (n + 1) + z

Tactic:
· use 0
    simp_rw [zero_mul, zero_add]
    refine ⟨_, ?_, rfl⟩
    replace h : c ≤ n := Nat.lt_succ_iff.mp h
    have : (Multiset.card s + 1) * n + 1 - c = Multiset.card s * n + 1 + (n - c) := by
      rw [add_mul, one_mul, add_assoc, add_comm n 1, ← add_assoc, add_tsub_assoc_of_le h]
    rw [this, pow_add]
    simp_rw [mul_assoc, mul_comm (s.sum ^ (Multiset.card s * n + 1)), ← mul_assoc]
    exact mul_mem_left _ _ hs

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n i : ℕ
hi : i ∈ range (n + 1)
⊢ i ≤ n

Tactic:
simpa [Nat.lt_succ_iff] using hi

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
⊢ f.iterateMapComap i (n + 1) K = f.iterateMapComap i (n + 1 + 1) K

Tactic:
rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
      Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t✝ : Set α
f g : Filter α
x✝ y✝ : Set α
hx : x✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
hy : y✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
t : Set α
htg : t ∈ g
ht : x✝ ∩ y✝ ⊆ t
⊢ x✝ ∩ y✝ ∪ t ∈ f

Tactic:
inter_union_distrib_right

Goal state after:
α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t✝ : Set α
f g : Filter α
x✝ y✝ : Set α
hx : x✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
hy : y✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
t : Set α
htg : t ∈ g
ht : x✝ ∩ y✝ ⊆ t
⊢ (x✝ ∪ t) ∩ (y✝ ∪ t) ∈ f
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst✝² : Fintype X
inst✝¹ : Finite Y
inst✝ : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ equivFunOnFinite (mapDomain f s) y = ∑ x with f x = y, equivFunOnFinite s x

Tactic:
← Finsupp.univ_sum_single s

Goal state after:
M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst✝² : Fintype X
inst✝¹ : Finite Y
inst✝ : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ equivFunOnFinite (mapDomain f (∑ a, Finsupp.single a (s a))) y = ∑ x with f x = y, equivFunOnFinite s x
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ atTop = generate (Ici '' s)

Tactic:
rw [atTop_eq_generate_Ici]
  apply le_antisymm
  · rw [le_generate_iff]
    rintro - ⟨y, -, rfl⟩
    exact mem_generate_of_mem ⟨y, rfl⟩
  · rw [le_generate_iff]
    rintro - ⟨x, -, -, rfl⟩
    rcases hs x with ⟨y, ys, hy⟩
    have A : Ici y ∈ generate (Ici '' s) := mem_generate_of_mem (mem_image_of_mem _ ys)
    have B : Ici y ⊆ Ici x := Ici_subset_Ici.2 hy
    exact sets_of_superset (generate (Ici '' s)) A B

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
la : Filter α
lb : Filter β
h : la.NeBot → Tendsto f la lb
⊢ Tendsto f la lb

Tactic:
by
  rcases eq_or_neBot la with rfl | hla
  · exact tendsto_bot
  · exact h hla

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter γ
m₁ : α → γ
m₂ : β → γ
s : Set (α ⊕ β)
⊢ s ∈ comap (Sum.elim m₁ m₂) l ↔ s ∈ map inl (comap m₁ l) ⊔ map inr (comap m₂ l)

Tactic:
simp_rw [mem_sup, mem_map, mem_comap_iff_compl]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter γ
m₁ : α → γ
m₂ : β → γ
s : Set (α ⊕ β)
⊢ (Sum.elim m₁ m₂ '' sᶜ)ᶜ ∈ l ↔ (m₁ '' (inl ⁻¹' s)ᶜ)ᶜ ∈ l ∧ (m₂ '' (inr ⁻¹' s)ᶜ)ᶜ ∈ l
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Semigroup β
⊢ Semigroup α

Tactic:
let mul := e.mul
  apply e.injective.semigroup _; intros; exact e.apply_symm_apply _

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit (f a)
b : α
hb : b ⋖ a
⊢ False

Tactic:
rw [← f.apply_covBy_apply_iff] at hb

Goal state after:
case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit (f a)
b : α
hb : f b ⋖ f a
⊢ False
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
⊢ b₁ < b₂

Tactic:
obtain ha | ha := ha.eq_or_lt
    · simp [← ha] at h
    · exact h₀ _ ha _ _ h

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupClosedOn D (s ∩ t)ᶜ

Tactic:
compl_inter

Goal state after:
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupClosedOn D (sᶜ ∪ tᶜ)
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_2
V : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
S₁ : Submodule R V
⊢ Module.Finite R ↥S₁ → ∀ (a₂ : Submodule R V), Module.Finite R ↥a₂ → Module.Finite R ↥(S₁ ⊔ a₂)

Tactic:
hS₁

Goal state after:
R : Type u_2
V : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
S₁ : Submodule R V
hS₁ : Module.Finite R ↥S₁
⊢ ∀ (a₂ : Submodule R V), Module.Finite R ↥a₂ → Module.Finite R ↥(S₁ ⊔ a₂)
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_2
V : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
⊢ Module.Finite R ↥(s.sup S)

Tactic:
by
  refine s.sup_induction (f := S) (p := fun i => Module.Finite R ↑i) (Module.Finite.bot R V) ?_
    inferInstance
  intro S₁ hS₁ S₂ hS₂
  exact finite_sup S₁ S₂

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

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

pp: case inr
a b : Ordinal.{u_4}
h : a < b
⊢ a ≤ b + (a - b)

Tactic:
· exact (Ordinal.add_sub_cancel_of_le h).ge

Goal state after:
case inr
a b : Ordinal.{u_4}
h : a < b
⊢ a ≤ b + (a - b)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
rw [sub_le, sub_le, sub_le, add_assoc]

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

Goal state before:
pp: a b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ a + b ≤ c ↔ ∀ d < b, a + d < c

Tactic:
simpa using (lt_add_iff hb).not

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ IsNormal (Subtype.val ∘ ⇑(enum s hs)) ↔ DirSupClosed s

Tactic:
let H := (Subtype.strictMono_coe _).comp (enum s hs).strictMono

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (enum s hs))
⊢ IsNormal (Subtype.val ∘ ⇑(enum s hs)) ↔ DirSupClosed s
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case succ
n : ℕ
IH : ↑n ≤ (↑n).ord
⊢ ↑(n + 1) ≤ (↑(n + 1)).ord

Tactic:
exact (IH.trans_lt <| by simp).succ_le

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

Goal state before:
pp: case refine_1
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : succ (o.bsup f) ≤ o.blsub f
⊢ ∃ i, ∃ (hi : i < o), f i hi = o.bsup f

pp: case refine_2
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (∃ i, ∃ (hi : i < o), f i hi = o.bsup f) → succ (o.bsup f) ≤ o.blsub f

Tactic:
· by_contra! hf
    exact
      ne_of_lt (succ_le_iff.1 h)
        (le_antisymm (bsup_le_blsub f) (blsub_le (lt_bsup_of_ne_bsup.1 hf)))

Goal state after:
case refine_2
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (∃ i, ∃ (hi : i < o), f i hi = o.bsup f) → succ (o.bsup f) ≤ o.blsub f
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case pos
a b : Ordinal.{u_1}
h✝¹ : a = 0
h✝ : b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
simp_all [opow_ne_zero]

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

Goal state before:
pp: case neg
a b : Ordinal.{u_1}
h✝¹ : a = 0
h✝ : ¬b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
simp_all [opow_ne_zero]

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

Goal state before:
pp: case pos
a b : Ordinal.{u_1}
h✝¹ : ¬a = 0
h✝ : b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
simp_all [opow_ne_zero]

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

Goal state before:
pp: case neg
a b : Ordinal.{u_1}
h✝¹ : ¬a = 0
h✝ : ¬b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
simp_all [opow_ne_zero]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ⨆ n, o * ↑n = o * iSup Nat.cast

Tactic:
Ordinal.mul_iSup

Goal state after:
o : Ordinal.{u_1}
⊢ ⨆ n, o * ↑n = ⨆ i, o * ↑i
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
conv_lhs => rw [← opow_one a]

Goal state after:
a b : Ordinal.{u_1}
ha : 1 < a
hb : 1 < b
⊢ a ^ 1 < a ^ b
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ.inl
n : ℕ
hn : 1 < n
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      n < b ^ fuel →
        (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧
          b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b < n
⊢ (go n b (fuel + 1)).fst = b ^ ((go n b (fuel + 1)).snd + 1) / n ∧
    b ^ (go n b (fuel + 1)).snd < n ∧ n ≤ b ^ ((go n b (fuel + 1)).snd + 1)

Tactic:
rcases ih (Nat.one_mul 1 ▸ Nat.mul_lt_mul_of_lt_of_lt hb hb)
        (log.go_aux hb hfuel (Nat.le_of_lt hbn)) with ⟨ih₁, ih₂, ih₃⟩

Goal state after:
case succ.inl
n : ℕ
hn : 1 < n
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      n < b ^ fuel →
        (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧
          b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b < n
ih₁ : (go n (b * b) fuel).fst = (b * b) ^ ((go n (b * b) fuel).snd + 1) / n
ih₂ : (b * b) ^ (go n (b * b) fuel).snd < n
ih₃ : n ≤ (b * b) ^ ((go n (b * b) fuel).snd + 1)
⊢ (go n b (fuel + 1)).fst = b ^ ((go n b (fuel + 1)).snd + 1) / n ∧
    b ^ (go n b (fuel + 1)).snd < n ∧ n ≤ b ^ ((go n b (fuel + 1)).snd + 1)
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
⊢ x < ω * (a / ω)

Tactic:
rw [lt_mul_iff_div_lt omega0_ne_zero, ← succ_le_iff, ← mul_le_iff_le_div omega0_ne_zero,
      mul_succ, add_le_iff_of_isSuccLimit isSuccLimit_omega0]

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

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

Tactic:
by_contra! hb

Goal state after:
x : Ordinal.{u_1}
h : 0 ≤ 1
hb : BddAbove ((fun x ↦ 0 ^ x) ⁻¹' Iic x)
⊢ False
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
⊢ log 0 0 = 0

pp: case inr
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ log b 0 = 0

Tactic:
· exact log_zero_left 0

Goal state after:
case inr
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ log b 0 = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case refine_1
b n : ℕ
hb : 1 < b
H : clog b n < clog b (n + 1)
⊢ b ^ clog b n = n

Tactic:
apply le_antisymm _ (le_pow_clog hb n)
    apply le_of_lt_succ
    exact (lt_clog_iff_pow_lt hb).mp H

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

Goal state before:
pp: case inl
b : Ordinal.{u_1}
⊢ log b 0 ≤ 0

pp: case inr
b x : Ordinal.{u_1}
hx : x ≠ 0
⊢ log b x ≤ x

Tactic:
· rw [log_zero_right]

Goal state after:
case inr
b x : Ordinal.{u_1}
hx : x ≠ 0
⊢ log b x ≤ x
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b x : Ordinal.{u_1}
⊢ log b x ≤ x

Tactic:
by
  obtain rfl | hx := eq_or_ne x 0
  · rw [log_zero_right]
  · obtain hb | hb := lt_or_ge 1 b
    · exact (right_le_opow _ hb).trans (opow_log_le_self b hx)
    · simp_rw [log_of_left_le_one hb, zero_le]

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

Goal state before:
pp: case hc
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < b + 1
n : ℕ
hn : a < ω ^ c * ↑n
⊢ 0 < ω

Tactic:
exact omega0_pos

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

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ a * ω ≤ b

Tactic:
← nfp_add_zero a,

Goal state after:
case refine_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ nfp (fun x ↦ a + x) 0 ≤ b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : 1 ≤ b
⊢ nfp (fun x ↦ a * x) 1 ≤ b

Tactic:
exact nfp_le_fp (isNormal_mul_right ha).monotone hb (le_of_eq hab)

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

Goal state before:
pp: case inr
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : ℵ₀ ≤ max a b
⊢ max a b * max a b < c

Tactic:
· rw [mul_eq_self h]
    exact max_lt ha hb

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

Goal state before:
pp: case isSuccPrelimit.mp
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi : i ∈ Iio o
⊢ (fun i ↦ lift.{v, u_1} (preBeth ↑i)) ⟨i, hi⟩ ∈ range fun a ↦ preBeth ↑a

pp: case isSuccPrelimit.mpr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{max u_1 v}
hi : i ∈ Iio (Ordinal.lift.{v, u_1} o)
⊢ (fun a ↦ preBeth ↑a) ⟨i, hi⟩ ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)

Tactic:
· refine ⟨⟨i.lift, ?_⟩, (IH _ hi).symm⟩
      simpa

Goal state after:
case isSuccPrelimit.mpr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{max u_1 v}
hi : i ∈ Iio (Ordinal.lift.{v, u_1} o)
⊢ (fun a ↦ preBeth ↑a) ⟨i, hi⟩ ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
rw [eq_of_add_eq_of_aleph0_le h this hb]

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

Goal state before:
pp: case inl
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c
bdd : BddAbove (range fun x ↦ f x + c)
hs : ⨆ i, f i < ℵ₀
⊢ (⨆ i, f i) + c ≤ ⨆ i, f i + c

pp: case inr
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c
bdd : BddAbove (range fun x ↦ f x + c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ (⨆ i, f i) + c ≤ ⨆ i, f i + c

Tactic:
· obtain ⟨i, hi⟩ := exists_eq_ciSup_of_not_isSuccLimit hf (not_isSuccLimit_of_lt_aleph0 hs)
    exact hi ▸ le_ciSup bdd i

Goal state after:
case inr
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c
bdd : BddAbove (range fun x ↦ f x + c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ (⨆ i, f i) + c ≤ ⨆ i, f i + c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case pos.inl
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c
bdd : BddAbove (range fun x ↦ f x * c)
hs : ⨆ i, f i < ℵ₀
⊢ (⨆ i, f i) * c ≤ ⨆ i, f i * c

pp: case pos.inr
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c
bdd : BddAbove (range fun x ↦ f x * c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ (⨆ i, f i) * c ≤ ⨆ i, f i * c

Tactic:
· obtain ⟨i, hi⟩ := exists_eq_ciSup_of_not_isSuccLimit hf (not_isSuccLimit_of_lt_aleph0 hs)
    exact hi ▸ le_ciSup bdd i

Goal state after:
case pos.inr
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c
bdd : BddAbove (range fun x ↦ f x * c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ (⨆ i, f i) * c ≤ ⨆ i, f i * c
Module: Mathlib.SetTheory.Cardinal.Ordinal

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

pp: a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ b ≤ a ^ b

Tactic:
· exact left_le_opow a hb

Goal state after:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ b ≤ a ^ b
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: 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 : ∃ i', ∃ (hi' : i' < type r'), f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) i' hi'
⊢ f i < (type r').blsub fun i x ↦ f ↑((enum r') ⟨i, x⟩)

Tactic:
by
      rcases h with ⟨i', hi', hfg⟩
      exact hfg.trans_lt (lt_blsub _ _ _)

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

Goal state before:
pp: a : Ordinal.{u_1}
h : 1 < a
⊢ (a ^ ω).card = max ℵ₀ a.card

Tactic:
rw [card_opow_eq_of_omega0_le_right h le_rfl, card_omega0, max_comm]

Goal state after: