mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ IsIdempotentElem (q - p) ↔ p * q = p ∧ q * p = p

Tactic:
refine ⟨fun hqp ↦ ?_, fun ⟨h1, h2⟩ => hp.sub hq h1 h2⟩

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)
⊢ p * q = p ∧ q * p = p
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ ∑ i ∈ range (n + 1), x * t n i + ∑ i ∈ range (n + 1), y * t n i =
    ∑ x_1 ∈ range n.succ, x * t n x_1 + (∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1))

Tactic:
congr 1

Goal state after:
case succ.e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ ∑ i ∈ range (n + 1), y * t n i = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ 4 ^ n = (1 + 1) ^ (2 * n)

Tactic:
simp [pow_mul]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m ∈ x.powerset, f #m = ∑ m ∈ range (#x + 1), (#x).choose m • f m

Tactic:
trans ∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j
  · refine (sum_fiberwise_of_maps_to ?_ _).symm
    intro y hy
    rw [mem_range, Nat.lt_succ_iff]
    rw [mem_powerset] at hy
    exact card_le_card hy
  · refine sum_congr rfl fun y _ ↦ ?_
    rw [← card_powersetCard, ← sum_const]
    refine sum_congr powersetCard_eq_filter.symm fun z hz ↦ ?_
    rw [(mem_powersetCard.1 hz).2]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i =
    (∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x) * ∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x)

Tactic:
congr 1

Goal state after:
case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i = ∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x

case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i = ∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
ι : Type u_5
f : ι → α
s : Finset ι
I : Ideal α
i : ι
hi : i ∈ s
hfi : f i ∈ I
⊢ ∏ i ∈ s, f i ∈ I

Tactic:
rw [Finset.prod_eq_prod_sdiff_singleton_mul hi]
  exact Ideal.mul_mem_left _ _ hfi

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

Goal state before:
pp: case inr.h
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
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
⊢ ∀ ⦃x y : ℕ →₀ P⦄,
    let s := x.support ∪ y.support;
    ∀ (ne : s.Nonempty), n = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y

Tactic:
intro x y s _ hn eq

Goal state after:
case inr.h
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
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
⊢ x = y
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 ↦ x1 ≥ x2) l
t : Set α
⊢ t ∈ ⨅ i, l i ↔ ∃ i, p i.fst i.snd ∧ s i.fst i.snd ⊆ t

Tactic:
rw [mem_iInf_of_directed h, Sigma.exists]

Goal state after:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 ↦ x1 ≥ x2) l
t : Set α
⊢ (∃ i, t ∈ l i) ↔ ∃ a b, p ⟨a, b⟩.fst ⟨a, b⟩.snd ∧ s ⟨a, b⟩.fst ⟨a, b⟩.snd ⊆ t
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ (∃ i, p i ∧ s i ⊆ t) ∧ t ∈ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∪ s' i.snd ⊆ t

Tactic:
hl'.mem_iff,

Goal state after:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ ((∃ i, p i ∧ s i ⊆ t) ∧ ∃ i, p' i ∧ s' i ⊆ t) ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∪ s' i.snd ⊆ t
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:
rw [Tendsto, ← map_compose]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) {x | p x}
ne : ∃ i, p i
⊢ map m (⨅ i, ⨅ (_ : p i), f i) = ⨅ i, ⨅ (_ : p i), map m (f i)

Tactic:
have := nonempty_subtype.2 ne

Goal state after:
α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) {x | p x}
ne : ∃ i, p i
this : Nonempty (Subtype p)
⊢ map m (⨅ i, ⨅ (_ : p i), f i) = ⨅ i, ⨅ (_ : p i), map m (f i)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
⊢ (fun g ↦ g a) '' s ∈ f.seq (pure a)

Tactic:
rw [← seq_singleton]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
⊢ s.seq {a} ∈ f.seq (pure a)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
⊢ h.seq (g.seq x) = ((map (fun x1 x2 ↦ x1 ∘ x2) h).seq g).seq x

Tactic:
by
  refine le_antisymm (le_seq fun s hs t ht => ?_) (le_seq fun s hs t ht => ?_)
  · rcases mem_seq_iff.1 hs with ⟨u, hu, v, hv, hs⟩
    rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hu⟩
    grw [← hs, ← hu]
    rw [← Set.seq_seq]
    exact seq_mem_seq hw (seq_mem_seq hv ht)
  · rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩
    grw [← ht]
    rw [Set.seq_seq]
    exact seq_mem_seq (seq_mem_seq (image_mem_map hs) hu) hv

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e✝ e : α ≃ β
inst✝ : Mul β
x✝ : Mul α := e.mul
x y : α
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
by
        simp [mul_def]

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
⊢ Group α

Tactic:
let npow := e.pow ℕ

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ Group α
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
⊢ CommGroup α

Tactic:
let npow := e.pow ℕ

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ CommGroup α
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
⊢ atTop ≤ map f atTop

Tactic:
(atTop_basis.map f).ge_iff

Goal state after:
case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
⊢ ∀ (i' : α), True → f '' Ici i' ∈ atTop
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:
obtain ⟨s, rfl⟩ := hN

Goal state after:
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₂) ⋯
s : Finset M
⊢ motive (span R ↑s) ⋯
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
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
N : Submodule R M
hN : N.FG
⊢ motive N hN

Tactic:
obtain ⟨s, rfl⟩ := hN

Goal state after:
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
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
s : Finset M
⊢ motive (span R ↑s) ⋯
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
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
N : Submodule R M
hN : N.FG
⊢ motive N hN

Tactic:
by classical
  obtain ⟨s, rfl⟩ := hN
  induction s using Finset.induction with
  | empty => simp [bot]
  | insert x s hxs ih => simpa [span_insert, sup_comm] using sup (span R s) x (by use s) ih

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
t : Finset M
huspan : ↑(Finset.image sp t) ⊆ sp '' ↑s
husup : s ≤ (Finset.image sp t).sup id
ssup : s = (Finset.image sp t).sup id
⊢ s.FG

Tactic:
rw [Finset.sup_image, Function.id_comp, Finset.sup_eq_iSup, supr_rw,
      ← span_eq_iSup_of_singleton_spans, eq_comm] at ssup

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
t : Finset M
huspan : ↑(Finset.image sp t) ⊆ sp '' ↑s
husup : s ≤ (Finset.image sp t).sup id
ssup : span R ↑t = s
⊢ s.FG
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ a₁ • _b ≤ a₂ • _b

Tactic:
← sub_nonneg,

Goal state after:
α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ 0 ≤ a₂ • _b - a₁ • _b
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
hs : DirSupInacc s
ht : DirSupInacc t
⊢ DirSupInacc (s ∩ t)

Tactic:
simpa using hs.dirSupInaccOn.inter isLowerSet_univ ht.dirSupInaccOn

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

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

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

Tactic:
· rwa [← add_le_add_iff_left b, Ordinal.add_sub_cancel_of_le h']

Goal state after:
case inr
a b c : Ordinal.{u_4}
h : a ≤ b + c
h' : a < b
⊢ a - b ≤ c
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u}
⊢ (typein LT.lt).toRelEmbedding o = lift.{u + 1, u} (typeLT o.ToType)

Tactic:
rw [← ToType.mk.toRelIsoLT.ordinal_lift_type_eq, lift_id'.{u, u + 1}, type_Iio_lt]

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

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
b : Ordinal.{u}
hb : b ∈ s
⊢ ∃ a, enumOrd s a = b

Tactic:
← range_enumOrd hs

Goal state after:
s : Set Ordinal.{u}
hs : ¬BddAbove s
b : Ordinal.{u}
hb : b ∈ range (enumOrd s)
⊢ ∃ a, enumOrd s a = b
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case e'_2
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
a✝ : Ordinal.{u}
⊢ (∀ (h : a✝ < o), f a✝ h < a) ↔ ∀ (h : a✝ < o), succ (f a✝ h) ≤ a

Tactic:
succ_le_iff

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

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

Tactic:
succ_le_iff

Goal state after:
case h₂
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ b < d * succ (b / d)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
add_zero

Goal state after:
a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
⊢ a * b / (a * c) = a * b / (a * c)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case e'_2
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = (x * y + 0) % (x * z)

Tactic:
add_zero

Goal state after:
case e'_2
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = x * y % (x * z)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case e'_3
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * (y % z) = x * (y % z) + 0

Tactic:
add_zero

Goal state after:
case e'_3
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * (y % z) = x * (y % z)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: n b fuel : ℕ
hn : 1 < n
hb : 1 < b
hfuel : 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)

Tactic:
induction fuel generalizing b with
  | zero => simp_all
  | succ fuel ih =>
    cases Nat.lt_or_ge b n with
    | inr hbn => simp_all [go]
    | inl hbn =>
      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₃⟩
      simp_all only [go, if_neg (Nat.not_le_of_gt hbn), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul (Nat.zero_lt_of_lt hbn), Nat.div_div_eq_div_mul,
        Nat.mul_comm n b, Nat.mul_add_one, @Nat.pow_add_one' _ (2 * _ + 1),
        Nat.mul_lt_mul_left, Nat.mul_div_mul_left, Nat.zero_lt_of_lt hb]
      split <;> simp_all [Nat.mul_add_one, Nat.pow_add_one']

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

Goal state before:
pp: case inr.inr.inr.limit
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ (b * o') = (a ^ b) ^ o'
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_mul_right hb)).le_iff_forall_le l).trans ?_
    simpa +contextual [IH] using (opow_le_of_isSuccLimit (opow_ne_zero _ ha) l).symm

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

Goal state before:
pp: b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ clog b ((n + b - 1) / b) + 1 = 1

Tactic:
clog_of_right_le_one

Goal state after:
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ 0 + 1 = 1

case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ (n + b - 1) / b ≤ 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case e'_3
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ x = x + 0

Tactic:
add_zero

Goal state after:
case e'_3
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ x = x
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
add_zero

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

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

Tactic:
add_zero

Goal state after:
case inl
⊢ 0 = 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this : IsWellOrder (α × α) s
⊢ #α * #α ≤ #α

Tactic:
refine @card_le_card (type s) (typeLT α) <| le_of_forall_lt fun o h ↦ ?_

Goal state after:
case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this : IsWellOrder (α × α) s
o : Ordinal.{u_1}
h : o < type s
⊢ o < typeLT α
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hd : ∃ c' < b, d < a * c'
x : Ordinal.{u}
hx : x < b
hx' : c < a * x
⊢ ∃ c' < b, (fun x1 x2 ↦ x1 + x2) c d < a * c'

Tactic:
rcases hd with ⟨y, hy, hy'⟩

Goal state after:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
⊢ ∃ c' < b, (fun x1 x2 ↦ x1 + x2) c d < a * c'
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : b < d
⊢ succ b ≤ d

Tactic:
succ_le_iff

Goal state after:
case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : b < d
⊢ b < d
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ succ ℵ₀ ≤ c ↔ ℵ₀ < c

Tactic:
succ_le_iff

Goal state after:
c : Cardinal.{u_1}
⊢ ℵ₀ < c ↔ ℵ₀ < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
h2b✝ : 1 < m
| n

Tactic:
← mul_one n

Goal state after:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
h2b✝ : 1 < m
| n * 1
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → n < n * m

Tactic:
conv_rhs => left; rw [← mul_one n]

Goal state after:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → n * 1 < n * m
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1.inr
n m : ℕ
h : n + m = n
⊢ n = n + 0

Tactic:
add_zero

Goal state after:
case refine_1.inr
n m : ℕ
h : n + m = n
⊢ n = n
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_2.inr
a b : Cardinal.{u_1}
h3 : b = 0
⊢ a + 0 = a

Tactic:
add_zero

Goal state after:
case refine_2.inr
a b : Cardinal.{u_1}
h3 : b = 0
⊢ a = a
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
this : Cardinal.lift.{u, max u v} (⨆ i, f i).card ≤ sum fun i ↦ (f i).card
⊢ (⨆ i, f i).card ≤ sum fun i ↦ (f i).card

Tactic:
Cardinal.lift_id'

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
this : (⨆ i, f i).card ≤ sum fun i ↦ (f i).card
⊢ (⨆ i, f i).card ≤ sum fun i ↦ (f i).card
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:
← hf,

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'
⊢ lsub f ≤ (type r').blsub fun i x ↦ f ↑((enum r') ⟨i, x⟩)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀
⊢ κ₂ + μ₁ < κ₂ + μ₂

Tactic:
· simpa [add_comm] using (add_lt_add_iff_of_right_lt_aleph0 hfin_.left).mpr hμ

Goal state after: