mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b + 1
f : ℕ → M
⊢ ∏ k ∈ Icc a (b + 1), f k = (∏ k ∈ Icc a b, f k) * f (b + 1)

Tactic:
← Ico_add_one_right_eq_Icc,

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b + 1
f : ℕ → M
⊢ ∏ k ∈ Ico a (b + 1 + 1), f k = (∏ k ∈ Icc a b, f k) * f (b + 1)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ x ∈ (Ico a b).sigma fun i ↦ Ico i b, f x.fst x.snd = ∑ x ∈ (Ico a b).sigma fun j ↦ Ico a (j + 1), f x.snd x.fst

Tactic:
refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl) <;>
  simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma] <;>
  lia

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

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ i ∈ Ico a b, ∑ j ∈ Ico i b, f i j = ∑ j ∈ Ico a b, ∑ i ∈ Ico a (j + 1), f i j

Tactic:
rw [Finset.sum_sigma', Finset.sum_sigma']
  refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl) <;>
  simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma] <;>
  lia

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

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ x ∈ (Ico a b).sigma fun i ↦ Ico (i + 1) b, f x.fst x.snd = ∑ x ∈ (Ico a b).sigma (Ico a), f x.snd x.fst

Tactic:
refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl) <;>
  simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma] <;>
  lia

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

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ i ∈ Ico a b, ∑ j ∈ Ico (i + 1) b, f i j = ∑ j ∈ Ico a b, ∑ i ∈ Ico a j, f i j

Tactic:
rw [Finset.sum_sigma', Finset.sum_sigma']
  refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl) <;>
  simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma] <;>
  lia

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
hpq : Commute p q
⊢ 2 • (q * p) = 0 + 2 • p

Tactic:
convert congrArg (· + 2 • p) h

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
hpq : Commute p q
⊢ 2 • (q * p) = p * (q - p) + (q - p) * p + 2 • p
Module: Mathlib.RingTheory.Ideal.Span

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

Tactic:
← span_pair_sub_left,

Goal state after:
α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, x - y - x} = span {x, y}
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case cons
α : 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 ∈ Finset.range ((s.card + 1) * n + 1 + 1),
    a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
      span (insert (a ^ (n + 1)) ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset)

Tactic:
intro c _hc

Goal state after:
case cons
α : 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)
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
    span (insert (a ^ (n + 1)) ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset)
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case a
α : Type u_1
B : FilterBasis α
⊢ generate B.sets ≤ B.filter

Tactic:
intro U U_in
    rcases B.mem_filter_iff.mp U_in with ⟨V, V_in, h⟩
    exact GenerateSets.superset (GenerateSets.basic V_in) h

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

Goal state before:
pp: case a
α : Type u_3
inst✝ : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x y : α
ys : y ∈ s
hy : x ≤ y
A : Ici y ∈ generate (Ici '' s)
⊢ Ici x ∈ (generate (Ici '' s)).sets

Tactic:
have B : Ici y ⊆ Ici x := Ici_subset_Ici.2 hy

Goal state after:
case a
α : Type u_3
inst✝ : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x y : α
ys : y ∈ s
hy : x ≤ y
A : Ici y ∈ generate (Ici '' s)
B : Ici y ⊆ Ici x
⊢ Ici x ∈ (generate (Ici '' s)).sets
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
F : Filter α
⊢ map (ψ ∘ φ) F = map ρ (map θ F)

Tactic:
H,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
F : Filter α
⊢ map (ρ ∘ θ) F = map ρ (map θ F)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
G : Filter δ
⊢ comap (ψ ∘ φ) G = comap θ (comap ρ G)

Tactic:
H,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
G : Filter δ
⊢ comap (ρ ∘ θ) G = comap θ (comap ρ G)
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
f : α → β
x : Filter α
y : ι → Filter β
⊢ Tendsto f x (⨅ i, y i) ↔ ∀ (i : ι), Tendsto f x (y i)

Tactic:
by
  simp only [Tendsto, le_iInf_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
⊢ x ∈ (fun x ↦ if p x then f x else g x) ⁻¹' s

Tactic:
mem_preimage

Goal state after:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
⊢ (if p x then f x else g x) ∈ s
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
⊢ (if p x then f x else g x) ∈ s

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
h : p x
⊢ f x ∈ s

case neg
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
h : ¬p x
⊢ g x ∈ s
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsCancelMul β
⊢ IsCancelMul α

Tactic:
let := e.mul; exact e.injective.isCancelMul _ fun _ _ ↦ e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
f : α → β
s : Set β
⊢ (∃ a, ∀ (b : α), a ≤ b → b ∈ f ⁻¹' s) ↔ ∃ N, ∀ (n : α), N ≤ n → f n ∈ s

Tactic:
mem_preimage

Goal state after:
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
s : Set α
h : s.Finite
⊢ range ⇑(Fintype.equivFin ↑↑h.toFinset).symm.asEmbedding = s

Tactic:
simp only [Finset.coe_sort_coe, Equiv.asEmbedding_range, Finite.coe_toFinset, ofPred_mem_eq]

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

Goal state before:
pp: G : Type u_3
inst✝ : AddCommGroup G
P : Submodule ℤ G
x✝ : P.FG
S : Finset G
hS : span ℤ ↑S = P
⊢ AddSubgroup.closure ↑S = P.toAddSubgroup

Tactic:
simpa [← span_int_eq_addSubgroupClosure]

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s'' : Finset M
hs'' : span R ↑s'' = span R s
s' : Finset M
hs's : ↑s' ⊆ s
hss' : ↑s'' ⊆ ↑(span R ↑s')
⊢ span R ↑s' ≤ span R s

Tactic:
rw [span_le]
      exact le_trans hs's subset_span

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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
singleton : ∀ (x : M), motive (R ∙ x) ⋯
sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯
N : Submodule R M
hN : N.FG
⊢ motive N hN

Tactic:
classical
  obtain ⟨s, rfl⟩ := hN
  induction s using Finset.induction with
  | empty => simpa using singleton 0
  | insert x s hxs ih =>
    simpa [span_insert, sup_comm] using
      sup (span R s) (R ∙ x) _ (fg_span_singleton _) ih (singleton x)

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

Goal state before:
pp: case refine_2
A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
R : Type u_7
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ restrictScalars R S ≤ restrictScalars R (span A ↑s)

Tactic:
rw [← e]

Goal state after:
case refine_2
A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
R : Type u_7
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ span R ↑s ≤ restrictScalars R (span A ↑s)
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)

pp: case 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)
⊢ N (S.attach.sup f) ≤ M'

Tactic:
· rw [← hS, span_le]
    intro s hs
    exact N.monotone' (Finset.le_sup <| S.mem_attach ⟨s, hs⟩) (hf _)

Goal state after:
case 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)
⊢ N (S.attach.sup f) ≤ M'
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff, neg_nonneg, neg_nonpos]

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
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulStrictMono α γ
⊢ ∀ ⦃a : α⦄, 0 < a → ∀ ⦃b₁ b₂ : β × γ⦄, b₁ < b₂ → a • b₁ < a • b₂

Tactic:
by
    simp_rw [lt_iff]
    rintro _a ha _b₁ _b₂ (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
    · exact .inl ⟨smul_lt_smul_of_pos_left h₁ ha, smul_le_smul_of_nonneg_left h₂ ha.le⟩
    · 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.IsNormal

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
f : α → β
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : SuccOrder α
inst✝ : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
hb : ¬IsMax b
IH : a < b → f a < f b
⊢ a < succ b → f a < f (succ b)

Tactic:
intro hab
    obtain rfl | h := (lt_succ_iff_eq_or_lt_of_not_isMax hb).1 hab
    · exact hs a
    · exact (IH h).trans (hs b)

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

Goal state before:
pp: case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
a : Ordinal.{u}
e : liftInitialSeg.toRelEmbedding a = type s
⊢ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

Tactic:
rw [← e]

Goal state after:
case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
a : Ordinal.{u}
e : liftInitialSeg.toRelEmbedding a = type s
⊢ liftInitialSeg.toRelEmbedding a < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
s : Set Ordinal.{u_2}
hs : #↑s < Cardinal.univ.{u_2, u_2 + 1}
⊢ ¬IsCofinal s

Tactic:
rw [← Cardinal.lift_id (#s), ← small_iff_lift_mk_lt_univ] at hs

Goal state after:
α : Type u_1
s : Set Ordinal.{u_2}
hs : Small.{u_2, u_2 + 1} ↑s
⊢ ¬IsCofinal s
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{v}
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred

Tactic:
obtain ⟨a, rfl⟩ | ho := mem_range_succ_or_isSuccPrelimit o
  · simp
  · rwa [ho.ordinalPred_eq, eq_comm, pred_eq_iff_isSuccPrelimit, isSuccPrelimit_lift]

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
x : α
⊢ StrictMono fun x ↦ ↑((StrictMono.orderIso f hf) x)

pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
x : α
⊢ (range fun x ↦ ↑((StrictMono.orderIso f hf) x)) = range f

Tactic:
· exact (Subtype.strictMono_coe _).comp (OrderIso.strictMono _)

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
x : α
⊢ (range fun x ↦ ↑((StrictMono.orderIso f hf) x)) = range f
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case left
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a b : Ordinal.{u}
x✝³ x✝² x✝¹ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
x✝ : ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤ ⟦{ α := β, r := s, wo := wo✝¹ }⟧
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
f : InitialSeg r s
a₁✝ : γ
b₁✝ : α
a₂✝ : γ
b₂✝ : α
h' : t a₁✝ a₂✝
⊢ Prod.Lex t s ((a₁✝, b₁✝).1, f (a₁✝, b₁✝).2) ((a₂✝, b₂✝).1, f (a₂✝, b₂✝).2)

Tactic:
exact Prod.Lex.left _ _ h'

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

Goal state before:
pp: α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this : type r * (typein s).toRelEmbedding b + type r ≤ c
⊢ (typein (Prod.Lex s r)).toRelEmbedding (b, a) < c

Tactic:
have := ((add_lt_add_iff_left _).2 (typein_lt_type _ a)).trans_le this

Goal state after:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
⊢ (typein (Prod.Lex s r)).toRelEmbedding (b, a) < c
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
⊢ ⨆ i, f i + 1 ≤ ⨆ i, f i

Tactic:
by_cases hf' : BddAbove (range f)

Goal state after:
case pos
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
⊢ ⨆ i, f i + 1 ≤ ⨆ i, f i

case neg
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : ¬BddAbove (range f)
⊢ ⨆ i, f i + 1 ≤ ⨆ i, f i
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a + 1 ≤ b ↔ a < b

Tactic:
by
  refine inductionOn₂ a b fun α r _ β s _ ↦ ⟨?_, ?_⟩ <;> rintro ⟨f⟩
  · refine ⟨((InitialSeg.leAdd _ _).trans f).toPrincipalSeg fun h ↦ ?_⟩
    simpa using h (f (Sum.inr PUnit.unit))
  · apply (RelEmbedding.ofMonotone (Sum.recOn · f fun _ ↦ f.top) ?_).ordinal_type_le
    simpa [f.map_rel_iff] using f.lt_top

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

Goal state before:
pp: x : ToType 1
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding x = 0

Tactic:
rw [one_toType_eq x, typein_enum]

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

Goal state before:
pp: case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ a + c / b ≤ (b * a + c) / b

Tactic:
rw [← mul_le_iff_le_div b0, mul_add, add_le_add_iff_left]
    apply mul_div_le

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

Goal state before:
pp: case inr
a : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ 0 = 1

Tactic:
opow_of_ne_zero h,

Goal state after:
case inr
a : Ordinal.{u_1}
h : a ≠ 0
⊢ (limitRecOn 0 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯) = 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ (b + 1) = a ^ b * a

Tactic:
opow_of_ne_zero h,

Goal state after:
case inr
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ (limitRecOn (b + 1) 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯) = a ^ b * a
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
← succ_eq_add_one,

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ n + b ≤ n * b

Tactic:
exact Nat.add_le_mul hn hb

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

Goal state before:
pp: case inr.zero
b : ℕ
hb : 1 < b
⊢ log b 0 ≤ clog b 0

Tactic:
rw [log_zero_right]

Goal state after:
case inr.zero
b : ℕ
hb : 1 < b
⊢ 0 ≤ clog b 0
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
rw [log_zero_right]

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

Goal state before:
pp: case pos
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
⊢ IsPrincipal op (sSup s)

Tactic:
obtain rfl | hs' := s.eq_empty_or_nonempty

Goal state after:
case pos.inl
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
this : IsPrincipal op (sSup ∅)
H : ∀ x ∈ ∅, IsPrincipal op x
hs : BddAbove ∅
⊢ IsPrincipal op (sSup ∅)

case pos.inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
⊢ IsPrincipal op (sSup s)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a ^ ω * (b / a ^ ω) + a * (b % a ^ ω) = a ^ ω * (b / a ^ ω) + b % a ^ ω
⊢ b % a ^ ω = 0

Tactic:
add_left_cancel_iff

Goal state after:
case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * (b % a ^ ω) = b % a ^ ω
⊢ b % a ^ ω = 0
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a.ab
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * succ b

Tactic:
rw [mul_succ]
      gcongr

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ⨆ a, 2 ^ preBeth ↑a = 2 ^ preBeth o

Tactic:
← succ_eq_add_one,

Goal state after:
o : Ordinal.{u_1}
⊢ ⨆ a, 2 ^ preBeth ↑a = 2 ^ preBeth o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
intro hc

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} c).cof

Tactic:
Cardinal.lift_umax,

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{v, u} #ι < (lift.{u, max u v} c).cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < iSup f
hf : Cardinal.lift.{v, u} #ι < (iSup f).cof
⊢ Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} (iSup f)).cof

Tactic:
Cardinal.lift_umax,

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < iSup f
hf : Cardinal.lift.{v, u} #ι < (iSup f).cof
⊢ Cardinal.lift.{v, u} #ι < (lift.{u, max u v} (iSup f)).cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.ord.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{max u v, u} #ι < (Cardinal.lift.{u, max u v} c).ord.cof

Tactic:
Cardinal.lift_umax,

Goal state after:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.ord.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{v, u} #ι < (Cardinal.lift.{u, max u v} c).ord.cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_1
ι : 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
⊢ Cardinal.lift.{max u v, u} #(List ι) < (lift.{u, max u v} c).cof

Tactic:
Cardinal.lift_umax,

Goal state after:
case refine_1
ι : 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
⊢ Cardinal.lift.{v, u} #(List ι) < (lift.{u, max u v} c).cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a.refine_1
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
x : α
⊢ IsSuccLimit (#α).ord

Tactic:
apply isSuccLimit_ord ha

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

Goal state before:
pp: α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #↑(⋃ x, t ↑x ⋯) < c
a : α
ha : a ∈ s
this : ∀ (i : ↑s), #↑(t ↑i ⋯) < c
⊢ #↑(t a ha) < c

Tactic:
simp_all only [iUnion_coe_set, Subtype.forall]

Goal state after: