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

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : α → β
l₁ : Filter α
l₂ : Filter β
hl : f₁ =ᶠ[l₁] f₂
⊢ Tendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂

Tactic:
Tendsto,

Goal state after:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
l₁ : Filter α
l₂ : Filter β
hl : f₁ =ᶠ[l₁] f₂
⊢ map f₁ l₁ ≤ l₂ ↔ Tendsto f₂ l₁ l₂
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : α → β
l₁ : Filter α
l₂ : Filter β
hl : f₁ =ᶠ[l₁] f₂
⊢ map f₁ l₁ ≤ l₂ ↔ Tendsto f₂ l₁ l₂

Tactic:
Tendsto,

Goal state after:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
l₁ : Filter α
l₂ : Filter β
hl : f₁ =ᶠ[l₁] f₂
⊢ map f₁ l₁ ≤ l₂ ↔ map f₂ l₁ ≤ l₂
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
x : Filter α
y : Filter γ
⊢ Tendsto f (map g x) y ↔ Tendsto (f ∘ g) x y

Tactic:
Tendsto,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
x : Filter α
y : Filter γ
⊢ map f (map g x) ≤ y ↔ Tendsto (f ∘ g) x y
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
x : Filter α
y : Filter γ
⊢ map f (map g x) ≤ y ↔ Tendsto (f ∘ g) x y

Tactic:
Tendsto,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
x : Filter α
y : Filter γ
⊢ map f (map g x) ≤ y ↔ map (f ∘ g) x ≤ y
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
⊢ Tendsto (m ∘ i) (comap i f) g ↔ Tendsto m f g

Tactic:
Tendsto,

Goal state after:
α : 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
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : Tendsto (g ∘ f) a c
hg : comap g c ≤ b
⊢ Tendsto f a b

Tactic:
by
  rw [tendsto_iff_comap] at hfg ⊢
  calc
    a ≤ comap (g ∘ f) c := hfg
    _ ≤ comap f b := by simpa [comap_comap] using comap_mono hg

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
H : ∀ᶠ (i : ι) in F, ∃ b, P i b
i : ι
⊢ (∃ b, P i b) → P i (if h : ∃ b, P i b then h.choose else ⋯.some)

Tactic:
hi

Goal state after:
ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
H : ∀ᶠ (i : ι) in F, ∃ b, P i b
i : ι
hi : ∃ b, P i b
⊢ P i (if h : ∃ b, P i b then h.choose else ⋯.some)
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddGroup β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
⊢ f - g =ᶠ[l] 0

Tactic:
simpa using ((EventuallyEq.refl l f).sub h).symm

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

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

Tactic:
Set.seq_seq

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Small.{v, u_2} α
inst✝ : Mul α
x y : Shrink.{v, u_2} α
⊢ (equivShrink α).symm (x * y) = (equivShrink α).symm x * (equivShrink α).symm y

Tactic:
by
  simp [Equiv.mul_def]

Goal state after:
Module: Mathlib.Algebra.Group.Shrink

Goal state before:
pp: α : Type u_2
inst✝¹ : Small.{v, u_2} α
inst✝ : Mul α
x y : α
⊢ (equivShrink α) (x * y) = (equivShrink α) x * (equivShrink α) y

Tactic:
by
  simp [Equiv.mul_def]

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

Goal state before:
pp: k : ℕ
hk : 0 < k
b : ℕ
x✝ : 1 ≤ b
⊢ b ≤ b + (k - 1) / k

Tactic:
Nat.div_eq_of_lt,

Goal state after:
k : ℕ
hk : 0 < k
b : ℕ
x✝ : 1 ≤ b
⊢ b ≤ b + 0

k : ℕ
hk : 0 < k
b : ℕ
x✝ : 1 ≤ b
⊢ k - 1 < k
Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst✝² : Monoid M
inst✝¹ : AddMonoid B
inst✝ : DistribMulAction M B
this : AddMonoid A := e.addMonoid
⊢ DistribMulAction M A

Tactic:
exact { e.distribSMul M, e.mulAction M with }

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : ⋃ i ∈ s, Iio i = univ
⊢ ⋃ i ∈ s, Iic i = univ

Tactic:
← univ_subset_iff,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : ⋃ i ∈ s, Iio i = univ
⊢ univ ⊆ ⋃ i ∈ s, Iic i
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ cof α = 1 ↔ ¬∀ (x : α), ¬IsTop x

Tactic:
cof_eq_one_iff

Goal state after:
α : Type u
inst✝ : Preorder α
⊢ (∃ x, IsTop x) ↔ ¬∀ (x : α), ¬IsTop x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ cof α = 0 ∨ cof α = 1 ↔ ∃ x, IsTop x

Tactic:
cof_eq_one_iff

Goal state after:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ (cof α = 0 ∨ ∃ x, IsTop x) ↔ ∃ x, IsTop x
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ < a₁
hb : b₂ < b₁
⊢ a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂

Tactic:
simp_rw [add_comm (a₁ • _)]; exact smul_add_smul_lt_smul_add_smul ha hb

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

Goal state before:
pp: R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
hM : ∃ S, S.Finite ∧ span R S = ⊤
⊢ ∃ S, S.Finite ∧ span A S = ⊤

Tactic:
obtain ⟨S, hSfin, hSgen⟩ := hM

Goal state after:
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : span R S = ⊤
⊢ ∃ S, S.Finite ∧ span A S = ⊤
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e : Ordinal.liftPrincipalSeg.toRelEmbedding o = c.ord
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
have := card_ord c

Goal state after:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this✝ : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e : Ordinal.liftPrincipalSeg.toRelEmbedding o = c.ord
this : c.ord.card = c
⊢ ∃ c', c = lift.{u + 1, u} c'
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
t : Set α
x : α
h : s ⊆ t
⊢ ↑((enum t ⋯) x) ≤ ↑((enum s hs) x)

Tactic:
induction x using WellFoundedLT.induction with

Goal state after:
case ind
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
t : Set α
h : s ⊆ t
x : α
IH : ∀ y < x, ↑((enum t ⋯) y) ≤ ↑((enum s hs) y)
⊢ ↑((enum t ⋯) x) ≤ ↑((enum s hs) x)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ a - 0 = a

Tactic:
by simpa only [zero_add] using add_sub_cancel 0 a

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

Goal state before:
pp: s : Set Cardinal.{u_3}
⊢ (sSup s).ord = sSup (ord '' s)

Tactic:
by
  obtain rfl | hn := s.eq_empty_or_nonempty
  · simp
  · by_cases hs : BddAbove s
    · exact isNormal_ord.map_sSup hn hs
    · rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (bddAbove_ord_image_iff.not.2 hs)]
      simp

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

Goal state before:
pp: case mp.refine_1
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
⊢ a < typeLT α

Tactic:
← ha,

Goal state after:
case mp.refine_1
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
⊢ a < succ a
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case cons.nil
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
hm : [].SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) [] (a :: as)
i : α
⊢ i ∈ [] → (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

Tactic:
hi

Goal state after:
case cons.nil
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
hm : [].SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) [] (a :: as)
i : α
hi : i ∈ []
⊢ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
β : Type u_2
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
a : Ordinal.{max u v}
ha : a < o'
⊢ g a ha < o

Tactic:
by rw [← hg]; apply lt_blsub

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

Goal state before:
pp: case cons.cons
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) (b :: bs) (a :: as)
i : α
⊢ i ∈ b :: bs → (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

Tactic:
hi

Goal state after:
case cons.cons
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
⊢ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b + a ≤ a * (d * succ (b / d))

Tactic:
← mul_succ

Goal state after:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * succ b ≤ a * (d * succ (b / d))
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ
b n k : ℕ
hk : log b (n / b ^ k) = log b n - k
⊢ log b (n / b ^ (k + 1)) = log b n - (k + 1)

Tactic:
Nat.pow_succ,

Goal state after:
case succ
b n k : ℕ
hk : log b (n / b ^ k) = log b n - k
⊢ log b (n / (b ^ k * b)) = log b n - (k + 1)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ b ^ (clog b x).pred < x

Tactic:
← lt_clog_iff_pow_lt hb

Goal state after:
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ (clog b x).pred < clog b x
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ derivFamily f o < derivFamily f (succ o)

pp: case refine_2
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : IsSuccLimit o
⊢ IsLUB (derivFamily f '' Set.Iio o) (derivFamily f o)

Tactic:
· rw [derivFamily_succ, ← succ_le_iff]
    exact le_nfpFamily _ _

Goal state after:
case refine_2
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : IsSuccLimit o
⊢ IsLUB (derivFamily f '' Set.Iio o) (derivFamily f o)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_1
a : Ordinal.{u}
⊢ deriv (fun x ↦ a + x) 0 = a * ω + 0

Tactic:
deriv_zero_right,

Goal state after:
case refine_1
a : Ordinal.{u}
⊢ nfp (fun x ↦ a + x) 0 = a * ω + 0
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
rw [← opow_one_add, one_add_omega0]

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

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
⊢ ¬b = 0 → a ^ ω ≤ b

Tactic:
intro hb

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

Goal state before:
pp: case refine_1
a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun x ↦ a * x) 0 = a ^ ω * 0

Tactic:
deriv_zero_right,

Goal state after:
case refine_1
a : Ordinal.{u}
ha : 0 < a
⊢ nfp (fun x ↦ a * x) 0 = a ^ ω * 0
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ ≤ ℵ_ o

Tactic:
rw [aleph_eq_preAleph, aleph0_le_preAleph]
  exact le_self_add

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o = 0 ∨ o.cof = 1 ↔ o = 0 ∨ o ∈ range succ

Tactic:
cof_eq_one_iff

Goal state after:
o : Ordinal.{u_1}
⊢ o = 0 ∨ o ∈ range succ ↔ o = 0 ∨ o ∈ range succ
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
t : Set ↑s
ht : IsCofinal t
ht' : typeLT ↑t = (Order.cof α).ord
⊢ typeLT ↑(Subtype.val '' t) = (Order.cof α).ord

Tactic:
← ht'

Goal state after:
case refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
t : Set ↑s
ht : IsCofinal t
ht' : typeLT ↑t = (Order.cof α).ord
⊢ typeLT ↑(Subtype.val '' t) = typeLT ↑t
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_2
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this : StrictMono fun i ↦ ⟨f i, ⋯⟩
⊢ Cardinal.lift.{v, u} (⨆ i, f i + 1).cof = Cardinal.lift.{u, v} (Order.cof β)

Tactic:
have := lift_cof_congr_of_strictMono this ?_

Goal state after:
case refine_2.refine_2
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this✝ : StrictMono fun i ↦ ⟨f i, ⋯⟩
this : Cardinal.lift.{u + 1, v} (Order.cof β) = Cardinal.lift.{v, u + 1} (Order.cof ↑(Iio (⨆ i, f i + 1)))
⊢ Cardinal.lift.{v, u} (⨆ i, f i + 1).cof = Cardinal.lift.{u, v} (Order.cof β)

case refine_2.refine_1
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this : StrictMono fun i ↦ ⟨f i, ⋯⟩
⊢ IsCofinal (range fun i ↦ ⟨f i, ⋯⟩)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
intro hb

Goal state after:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
hb : b < c
⊢ False
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ a < b → a < a + b

Tactic:
intro hb

Goal state after:
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
hb : a < b
⊢ a < a + b
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: β : Type u_1
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o.card ≤ c
hc : ℵ₀ ≤ c
A : Ordinal.{u_1} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ lift.{u_1, u_1} o.card ≤ lift.{u_1, u_1} c

Tactic:
Cardinal.lift_le

Goal state after:
β : Type u_1
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o.card ≤ c
hc : ℵ₀ ≤ c
A : Ordinal.{u_1} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ o.card ≤ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
b c : Cardinal.{u_1}
hb : ∃ n, b = ↑n
hc : ∃ n, c = ↑n
n : ℕ
h : ↑n + b = ↑n + c
⊢ b = c

Tactic:
rcases hb with ⟨m, rfl⟩

Goal state after:
case inr
c : Cardinal.{u_1}
hc : ∃ n, c = ↑n
n m : ℕ
h : ↑n + ↑m = ↑n + c
⊢ ↑m = c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u}
c : Cardinal.{v}
f : ↑(Iio o) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ Cardinal.lift.{u + 1, max v u} (Cardinal.lift.{v, u} o.card) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)

Tactic:
Cardinal.lift_le

Goal state after:
o : Ordinal.{u}
c : Cardinal.{v}
f : ↑(Iio o) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case zero
a : Ordinal.{u_1}
ha : ω ≤ a
⊢ (a ^ 0).card ≤ max a.card (card 0)

Tactic:
simpa using one_lt_omega0.le.trans ha

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

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

Tactic:
rw [← hf, lsub_le_iff]

Goal state after:
case refine_3
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 : ι), f i < (type r').blsub fun i x ↦ f ↑((enum r') ⟨i, x⟩)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_2
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
l : List ι
⊢ List.foldr f a l < c

Tactic:
induction l with

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

Goal state before:
pp: ⊢ (ℵ_ 1).IsRegular

Tactic:
← succ_aleph0

Goal state after:
⊢ (succ ℵ₀).IsRegular
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: case h
β α : Type u
f : β → α
s : Set β
hθ : #↑s ≤ #β
h₁ : ℵ₀ ≤ #↑s
h₂ : #α < (#↑s).ord.cof
a : α
ha : #↑(f ∘ Subtype.val ⁻¹' {a}) = #↑s
⊢ #↑s ≤ #↑(f ⁻¹' {a})

Tactic:
← ha,

Goal state after:
case h
β α : Type u
f : β → α
s : Set β
hθ : #↑s ≤ #β
h₁ : ℵ₀ ≤ #↑s
h₂ : #α < (#↑s).ord.cof
a : α
ha : #↑(f ∘ Subtype.val ⁻¹' {a}) = #↑s
⊢ #↑(f ∘ Subtype.val ⁻¹' {a}) ≤ #↑(f ⁻¹' {a})
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ #(List α) = max ℵ₀ #α

Tactic:
rw [mk_list_eq_aleph0, eq_comm, max_eq_left]
    exact mk_le_aleph0

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

Goal state before:
pp: case h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈ ↑⟨s, ⋯⟩ →
    x ∈
      ↑((fun f ↦ ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y ↦
          if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 })

Tactic:
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.Arithmetic

Goal state before:
pp: case refine_1
α : Type u
c : Cardinal.{u}
⊢ Set α ↪ Set (ULift.{u, 0} ℕ ⊕ α)

pp: case refine_2
α : Type u
c : Cardinal.{u}
⊢ ∀ ⦃x : Set α⦄, #↑x ≤ c → #↑(?refine_1 x) ≤ c

Tactic:
· apply Embedding.image
      use Sum.inr
      apply Sum.inr.inj

Goal state after:
case refine_2
α : Type u
c : Cardinal.{u}
⊢ ∀ ⦃x : Set α⦄, #↑x ≤ c → #↑({ toFun := Sum.inr, inj' := ⋯ }.image x) ≤ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ lift.{v, u} #↑s = lift.{u, v} #↑(range ⇑f)

Tactic:
mk_range_eq_of_injective

Goal state after:
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ lift.{v, u} #↑s = lift.{v, u} #↑s

α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ Injective ⇑f
Module: Mathlib.Data.List.Pi

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
l : List ι
fs : (i : ι) → List (α i)
⊢ ((↑l).pi fun x ↦ ↑(fs x)) = ↑(l.pi fs)

Tactic:
induction l with

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
s : Finset ι
hs : f.support ⊆ s
map_zero : ∀ i ∈ s, g i 0 = 1
i : ι
⊢ i ∈ s → i ∉ f.support → g i (f i) = 1

Tactic:
hi

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
s : Finset ι
hs : f.support ⊆ s
map_zero : ∀ i ∈ s, g i 0 = 1
i : ι
hi : i ∈ s
⊢ i ∉ f.support → g i (f i) = 1
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: case neg
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ ((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) j) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) j) b

Tactic:
suffices Finsupp.single (⟨i, a⟩ : Σ i, η i) n ⟨j, b⟩ = 0 by simp [split_apply, dif_neg h, this]

Goal state after:
case neg
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ (single ⟨i, a⟩ n) ⟨j, b⟩ = 0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
f_eq : ∏ i ∈ f.support ∪ g.support, h i (f i) = f.prod h
g_eq : ∏ i ∈ f.support ∪ g.support, h i (g i) = g.prod h
⊢ ∏ i ∈ f.support ∪ g.support, h i ((f + g) i) =
    (∏ i ∈ f.support ∪ g.support, h i (f i)) * ∏ i ∈ f.support ∪ g.support, h i (g i)

Tactic:
{ simp [h_add, Finset.prod_mul_distrib] }

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
a✝ : i ∈ Finset.univ
⊢ i ∉ v.support → f i (v i) = 1

Tactic:
hi

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
a✝ : i ∈ Finset.univ
hi : i ∉ v.support
⊢ f i (v i) = 1