mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: case e_a
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∏ x ∈ univ.sigma Ioi, f x.fst x.snd = ∏ x ∈ univ.sigma Iio, f x.snd x.fst

Tactic:
refine prod_nbij' (fun i ↦ ⟨i.2, i.1⟩) (fun i ↦ ⟨i.2, i.1⟩) ?_ ?_ ?_ ?_ ?_

Goal state after:
case e_a.refine_1
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∀ a ∈ univ.sigma Ioi, ⟨a.snd, a.fst⟩ ∈ univ.sigma Iio

case e_a.refine_2
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∀ a ∈ univ.sigma Iio, ⟨a.snd, a.fst⟩ ∈ univ.sigma Ioi

case e_a.refine_3
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∀ a ∈ univ.sigma Ioi, ⟨⟨a.snd, a.fst⟩.snd, ⟨a.snd, a.fst⟩.fst⟩ = a

case e_a.refine_4
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∀ a ∈ univ.sigma Iio, ⟨⟨a.snd, a.fst⟩.snd, ⟨a.snd, a.fst⟩.fst⟩ = a

case e_a.refine_5
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∀ a ∈ univ.sigma Ioi, f a.fst a.snd = f ⟨a.snd, a.fst⟩.snd ⟨a.snd, a.fst⟩.fst
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
⊢ univ.sup (disjointed f) = univ.sup f

Tactic:
← hun,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
⊢ (univ.biUnion Iic).sup (disjointed f) = (univ.biUnion Iic).sup f
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝⁵ : CommMonoid M
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c : α
⊢ ∏ x ∈ Ico a b, f (x + c) = ∏ x ∈ Ico (a + c) (b + c), f x

Tactic:
rw [← map_add_right_Ico, prod_map]
  rfl

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

Goal state before:
pp: n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (i, j) ∈ {a ∈ antidiagonal n | k ≤ a.1} ↔
    (i, j) ∈ map ({ toFun := fun x ↦ x + k, inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal (n - k))

Tactic:
suffices i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i by simpa

Goal state after:
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
⊢ {a ∈ antidiagonal n | k ≤ a.2} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + k, inj' := ⋯ }) (antidiagonal (n - k))

Tactic:
have aux₁ : fun a ↦ k ≤ a.snd = (fun a ↦ k ≤ a.fst) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl

Goal state after:
n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ k ≤ a.2) = (fun a ↦ k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
⊢ {a ∈ antidiagonal n | k ≤ a.2} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + k, inj' := ⋯ }) (antidiagonal (n - k))
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: α : Type u
inst✝² : Semiring α
I : Ideal α
inst✝¹ : I.IsTwoSided
inst✝ : I.IsPrime
x y : α
hx : x ∉ I
⊢ x * y ∈ I ↔ y ∈ I

Tactic:
grind [Ideal.IsPrime.mul_mem_iff_mem_or_mem]

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

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i) = x * (x ^ i * y ^ (n - i) * ↑(n.choose i))

Tactic:
rw [pow_succ' x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]

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

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ span {x} < span {y} ↔ DvdNotUnit y x

Tactic:
lt_iff_le_not_ge,

Goal state after:
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ span {x} ≤ span {y} ∧ ¬span {y} ≤ span {x} ↔ DvdNotUnit y x
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
r : (i : ι) → R i
⊢ (pi fun x ↦ span {r x}) = span {r}

Tactic:
by
  ext; simp_rw [mem_pi, mem_span_singleton', funext_iff, Classical.skolem, Pi.mul_def]

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

Goal state before:
pp: case refine_2
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
x y : R
h : (mk I) x * (mk I) y = 0
⊢ (mk I) x = 0 ∨ (mk I) y = 0

Tactic:
have := @IsDomain.to_noZeroDivisors (R ⧸ I) _ H

Goal state after:
case refine_2
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
x y : R
h : (mk I) x * (mk I) y = 0
this : NoZeroDivisors (R ⧸ I)
⊢ (mk I) x = 0 ∨ (mk I) y = 0
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
not_field : ¬IsField R
max : ⊥.IsMaximal
I : Ideal R
hIbot : ⊥ < I
hItop : I < ⊤
⊢ False

Tactic:
exact hIbot.ne (max.eq_of_le hItop.ne bot_le)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ (f.prodOfFinsuppNat x).2 = f (f.prodOfFinsuppNat ((comapDomain.addMonoidHom ⋯) x))

Tactic:
by
  simp_rw [prodOfFinsuppNat, coe_lsum, sum, Prod.snd_sum]
  rw [← Finset.sum_preimage (· + 1) _ (add_left_injective 1).injOn _ (by simp_all)]
  simp [pow_succ']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
h : Surjective m
⊢ comap m g₁ ⊓ comap m g₂ = ⊥ ↔ g₁ ⊓ g₂ = ⊥

Tactic:
← comap_inf,

Goal state after:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
h : Surjective m
⊢ comap m (g₁ ⊓ g₂) = ⊥ ↔ g₁ ⊓ g₂ = ⊥
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
s' t : Set α
⊢ t ∈ l ⊓ 𝓟 s' ↔ ∃ i, p i ∧ s i ∩ s' ⊆ t

Tactic:
by
    simp only [mem_inf_principal, hl.mem_iff, subset_def, mem_ofPred_eq, mem_inter_iff, and_imp]

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

Goal state before:
pp: case inl
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

Tactic:
rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]
    simp [← Classical.nonempty_pi]

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 ∩ Z = f '' (V ∩ f ⁻¹' Z)

Tactic:
rw [image_inter_preimage]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
a : α
ha : a ∈ t
⊢ g a ∈ s.seq t

Tactic:
exact ⟨g, hs, a, ha, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
⊢ SurjOn (map m) (Iic F) (Iic G) ↔ G ≤ map m F

Tactic:
refine ⟨fun hm ↦ ?_, fun hm ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : SurjOn (map m) (Iic F) (Iic G)
⊢ G ≤ map m F

case refine_2
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
⊢ SurjOn (map m) (Iic F) (Iic G)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosReflectLT α β
h : 0 < a • b
hb : 0 ≤ b
⊢ 0 • b < a • b

Tactic:
by rwa [zero_smul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosReflectLT α β
h : a • b < 0
hb : 0 ≤ b
⊢ a • b < 0 • b

Tactic:
by rwa [zero_smul]

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 : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
⊢ a ∈ s ∪ t

Tactic:
have hdst : d ∩ s ∪ d ∩ t = d := by grind

Goal state after:
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
⊢ a ∈ s ∪ t
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
⊢ f a ≤ b

Tactic:
· by_cases ha : a ∈ s
    · simp_all [mem_upperBounds]
    · have ha' := hs.isSuccLimit_of_notMem hs' ha
      rw [le_iff_forall_le hf ha']
      intro c hc
      obtain ⟨d, hd, hcd, hda⟩ := hs.exists_between hc
      simp_rw [mem_upperBounds, forall_mem_image] at hb
      exact (hf.strictMono hcd).le.trans (hb hd)

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
a : α
⊢ IsNormal fun x ↦ ⟨f ↑x, ⋯⟩

Tactic:
rw [isNormal_iff]
  refine ⟨fun x y h ↦ hf.strictMono h, fun b hb c hc ↦ hf.2 (hb.subtypeVal (isLowerSet_Iio _)) ?_⟩
  simpa [upperBounds] using! fun d hd ↦ hc ⟨d, hd.trans b.2⟩ hd

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : ι
⊢ (typein r).toRelEmbedding i < o

Tactic:
← ho

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : ι
⊢ (typein r).toRelEmbedding i < type r
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
⊢ ∀ (α_1 : Type u) (r_1 : α_1 → α_1 → Prop) [inst : IsWellOrder α_1 r_1] (hr : type r_1 < type r)
    (hs : type r_1 < type s), f ((enum r) ⟨type r_1, hr⟩) = (enum s) ⟨type r_1, hs⟩

Tactic:
rintro γ t wo ⟨g⟩ ⟨h⟩

Goal state after:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ f ((enum r) ⟨type t, ⋯⟩) = (enum s) ⟨type t, ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a b : Ordinal.{v}
⊢ lift.{u, v} a < lift.{u, v} b ↔ a < b

Tactic:
lt_iff_le_not_ge,

Goal state after:
a b : Ordinal.{v}
⊢ lift.{u, v} a ≤ lift.{u, v} b ∧ ¬lift.{u, v} b ≤ lift.{u, v} a ↔ a ≤ b ∧ ¬b ≤ a
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case neg
s : Set Cardinal.{u_3}
hn : s.Nonempty
hs : ¬BddAbove s
⊢ (sSup s).ord = sSup (ord '' s)

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

Goal state before:
pp: o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
a : Ordinal.{max (max u v) w}
x✝ : a ∈ o.brange fun a ha ↦ succ (f a ha)
b : Ordinal.{u}
hb : b < o
c : Ordinal.{v}
hc : c < o'
hc' : g c hc = f b hb
hb' : succ (g c hc) = a
⊢ a ∈ o'.brange fun a ha ↦ succ (g a ha)

Tactic:
exact ⟨c, hc, hb'⟩

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

Goal state before:
pp: case inl
⊢ 0 ^ 0 = 1

Tactic:
rw [zero_opow', Ordinal.sub_zero]

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

Goal state before:
pp: a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : IsSuccLimit b
⊢ a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c

Tactic:
opow_limit a0 h,

Goal state after:
a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : IsSuccLimit b
⊢ ⨆ x, a ^ ↑x ≤ c ↔ ∀ b' < b, a ^ b' ≤ c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ (log b n + 1) ≤ n * b

Tactic:
pow_succ',

Goal state after:
case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b * b ^ log b n ≤ n * b
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case h₂
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b ^ (log b n + 1 + 1)

Tactic:
pow_succ',

Goal state after:
case h₂
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b * b ^ (log b n + 1)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
h : a < ω
⊢ a + ω = ω

Tactic:
by
  obtain ⟨n, rfl⟩ := lt_omega0.1 h
  exact natCast_add_omega0 n

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

Goal state before:
pp: b k n : ℕ
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
rcases k.eq_zero_or_pos with rfl | hk
  · simp
  · rcases Nat.lt_or_ge 1 b with hb | hb
    · 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']
    · suffices (k - 1) / k = 0 by grind [clog_of_left_le_one, Nat.pow_le_one_iff]
      apply Nat.div_eq_of_lt
      grind

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

Goal state before:
pp: b o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o % b ^ log b o < o

Tactic:
by
  rcases eq_or_ne b 0 with (rfl | hb)
  · simpa using pos_iff_ne_zero.2 ho
  · exact (mod_lt _ <| opow_ne_zero _ hb).trans_le (opow_log_le_self _ ho)

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

Goal state before:
pp: case inr
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b (o % b ^ log b o) < log b o

Tactic:
· rw [← lt_opow_iff_log_lt hb h]
    exact mod_lt _ (opow_pos _ hb.pos).ne'

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

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

Tactic:
obtain rfl | ha' := eq_or_ne o 0
  · rw [opow_zero, isPrincipal_one_iff, add_zero]
  · rw [isPrincipal_add_iff_add_self_lt]
    intro a ha
    obtain ⟨c, hc, m, hm⟩ := (lt_omega0_opow ha').1 ha
    apply (add_lt_add_of_le_of_lt hm.le hm).trans_le
    rw [← mul_add, ← Nat.cast_add]
    exact (opow_mul_lt_opow (natCast_lt_omega0 _) hc).le

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

Goal state before:
pp: a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ a * b ≤ max a b

Tactic:
convert! mul_le_mul' (le_max_left a b) (le_max_right a b) using 1

Goal state after:
case e'_4
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ max a b = max a b * max a b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : ℵ₀ ≤ b
⊢ a * b = max a b

pp: case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
⊢ a * b = max a b

Tactic:
· exact mul_eq_max h hb

Goal state after:
case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
⊢ a * b = max a b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: α : Type u_1
⊢ ℵ_ 1 ≤ #α ↔ Uncountable α

Tactic:
rw [aleph_one_le_iff, aleph0_lt_mk_iff]

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

Goal state before:
pp: a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a ≤ b
ha' : a ≠ 0
⊢ b * a = b

Tactic:
mul_eq_left hb ha ha'

Goal state after:
a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a ≤ b
ha' : a ≠ 0
⊢ b = b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
| ω ^ ω ^ b

Tactic:
← one_mul (ω ^ _)

Goal state after:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
| 1 * ω ^ ω ^ b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ lift.{v, u_1} (ℶ_ o) = ℶ_ (Ordinal.lift.{v, u_1} o)

Tactic:
by
  rw [beth_eq_preBeth, beth_eq_preBeth, lift_preBeth, Ordinal.lift_add, lift_omega0]

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

Goal state before:
pp: case refine_1.inr.inr
a : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) ((fun x ↦ ω ^ x) a)
ho₂ : 2 < (fun x ↦ ω ^ x) a
⊢ (fun x ↦ ω ^ x) a ≤ 2 ∨ (fun x ↦ ω ^ x) a ∈ Set.range fun x ↦ ω ^ ω ^ x

Tactic:
· 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⟩

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

Goal state before:
pp: case refine_2.inr
a : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) ((fun x ↦ ω ^ ω ^ x) a)

Tactic:
· exact isPrincipal_mul_omega0_opow_opow a

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

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

Tactic:
rintro (ho₂ | ⟨a, rfl⟩)
    · exact isPrincipal_mul_of_le_two ho₂
    · exact isPrincipal_mul_omega0_opow_opow a

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ o.cof.ord ≤ a

Tactic:
← hf.iSup_add_one_eq,

Goal state after:
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ (⨆ i, ↑(f i) + 1).cof.ord ≤ a
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
⊢ ∃ f, a.IsFundamentalSequence a.cof.ord f

Tactic:
exact ⟨_, hf.ord_cof⟩

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

Goal state before:
pp: case refine_1
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'
⊢ type r ≤ a.cof.ord

pp: case refine_2
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 j : Ordinal.{u}
x✝¹ : i < type r'
h : j < type r'
x✝ : i < j
⊢ r ↑((enum r') ⟨i, x✝¹⟩) ↑((enum r') ⟨j, h⟩)

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 [← hι, hr]

Goal state after:
case refine_2
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 j : Ordinal.{u}
x✝¹ : i < type r'
h : j < type r'
x✝ : i < j
⊢ r ↑((enum r') ⟨i, x✝¹⟩) ↑((enum r') ⟨j, h⟩)

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⟩)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: 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

Tactic:
rw [lt_ord, card_mul] at *

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ a.card * b.card < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : Infinite α
this : Nonempty ((α → Bool) ↪ Perm (α × Bool))
⊢ Nonempty (α ≃ α × Bool)

Tactic:
by simp [← Cardinal.eq, mul_two]

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

Goal state before:
pp: case a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := ⋯
⊢ #α ≤ #{ s // #↑s < (#α).ord.cof }

Tactic:
· refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
    · rw [mk_singleton, one_lt_cof_iff]
      exact isSuccLimit_ord h'.aleph0_le
    · intro a b hab
      simpa [singleton_eq_singleton_iff] using hab

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsSingular
⊢ IsSuccLimit c

Tactic:
by
  rw [Cardinal.isSuccLimit_iff, isSuccPrelimit_iff_succ_ne]
  refine ⟨hc.pos.ne', ?_⟩
  rintro c rfl
  exact not_isSingular_succ c hc

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

Goal state before:
pp: case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ ⨆ i, ⨆ (_ : p i), S i ≤
    AddMonoidHom.mrange ((sumAddHom fun i ↦ (S i).subtype).comp (filterAddMonoidHom (fun i ↦ ↥(S i)) p))

pp: case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange ((sumAddHom fun i ↦ (S i).subtype).comp (filterAddMonoidHom (fun i ↦ ↥(S i)) p)) ≤
    ⨆ i, ⨆ (_ : p i), S i

Tactic:
· refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩
    rw [AddMonoidHom.comp_apply, filterAddMonoidHom_apply, filter_single_pos _ _ hi]
    exact sumAddHom_single _ _ _

Goal state after:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange ((sumAddHom fun i ↦ (S i).subtype).comp (filterAddMonoidHom (fun i ↦ ↥(S i)) p)) ≤
    ⨆ i, ⨆ (_ : p i), S i
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
⊢ comapDomain' h hh' (r • f) = r • comapDomain' h hh' f

Tactic:
by
  ext
  rw [smul_apply, comapDomain'_apply, smul_apply, comapDomain'_apply]

Goal state after: