mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: case inl
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : x✝ ∉ I
J : Ideal α
hJ : J ∈ s
h : I ≤ J
⊢ y✝ ∈ J

Tactic:
exact h (((H I hI).mem_or_mem (e hI)).resolve_left hI')

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
x : α
s : Set α
⊢ span {x} ⊔ span s = span (insert x s)

Tactic:
span_insert

Goal state after:
α : Type u
inst✝ : Ring α
x : α
s : Set α
⊢ span {x} ⊔ span s = span {x} ⊔ span s
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
x : α
s : Set α
inst✝ : LinearOrder α
⊢ span {x} ⊔ span s = span (insert x s)

Tactic:
span_insert

Goal state after:
α : Type u
inst✝¹ : Ring α
x : α
s : Set α
inst✝ : LinearOrder α
⊢ span {x} ⊔ span s = span {x} ⊔ span s
Module: Mathlib.RingTheory.Ideal.Basic

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

Tactic:
zero_add

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

Goal state before:
pp: case right
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
intro J x hIJ hxnI hxJ
    rcases hqf.mul_inv_cancel (mt Ideal.Quotient.eq_zero_iff_mem.1 hxnI) with ⟨⟨y⟩, hy⟩
    rw [← zero_add (1 : R), ← sub_self (x * y), sub_add]
    exact J.sub_mem (J.mul_mem_right _ hxJ) (hIJ (Ideal.Quotient.eq.1 hy))

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

Goal state before:
pp: case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : 1 ∈ Submodule.span α s
n : ℕ
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)

Tactic:
Finsupp.mem_span_iff_linearCombination

Goal state after:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : ∃ l, (Finsupp.linearCombination α Subtype.val) l = 1
n : ℕ
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬IsUnit x

Tactic:
have : ¬_ := fun h => hf ⟨exists_pair_ne R, mul_comm, h⟩

Goal state after:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : ¬∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬IsUnit x
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p s
t : Set α
⊢ t ∈ l ↔ t ∈ l'

Tactic:
hl.mem_iff,

Goal state after:
α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p s
t : Set α
⊢ (∃ i, p i ∧ s i ⊆ t) ↔ t ∈ l'
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: ι : Sort u
R : Type u_1
inst✝ : CompleteLinearOrder R
f : ι → R
no_least_elem : ⨅ i, f i ∉ range f
⊢ ⋃ i, Ici (f i) = Ioi (⨅ i, f i)

Tactic:
by
  simp only [← IsGLB.biUnion_Ici_eq_Ioi (@isGLB_iInf _ _ _ f) no_least_elem, mem_range,
    iUnion_exists, iUnion_iUnion_eq']

Goal state after:
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 α
⊢ t ∈ l ∧ 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) ∧ t ∈ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∪ s' i.snd ⊆ t
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
x y : α
⊢ Disjoint (pure x) (pure y) ↔ x ≠ y

Tactic:
simp only [← principal_singleton, disjoint_principal_principal, disjoint_singleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
⊢ f.seq (pure a) = map (fun g ↦ g a) f

Tactic:
refine le_antisymm (le_map fun s hs => ?_) (le_seq fun s hs t ht => ?_)
  · rw [← seq_singleton]
    exact seq_mem_seq hs singleton_mem_pure
  · refine sets_of_superset (map (fun g : α → β => g a) f) (image_mem_map hs) ?_
    rintro b ⟨g, hg, rfl⟩
    exact ⟨g, hg, a, ht, rfl⟩

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

Goal state before:
pp: P : ℕ → ℕ → Prop
h : ∀ (n : ℕ), ∃ N, ∀ k ≥ N, P n k
⊢ ∀ (n : ℕ), ∀ᶠ (k : ℕ) in atTop, P n k

Tactic:
simp [eventually_atTop, h]

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e✝ : G ≃ Fin n
f : Fin n ≃ ULift.{?u.25, 0} (Fin n) := Equiv.ulift.symm
e : G ≃ ULift.{?u.25, 0} (Fin n) := e✝.trans f
groupH : Group (ULift.{?u.25, 0} (Fin n)) := e.symm.group
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Tactic:
exact ⟨ULift (Fin n), groupH, inferInstance, ⟨MulEquiv.symm <| e.symm.mulEquiv⟩⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : AddMonoid M
inst✝ : IsAddTorsionFree M
n : ℕ
x : M
hx : n • x = 0
⊢ n = 0 ∨ x = 0

Tactic:
by
    contrapose! hx; simpa using (nsmul_right_injective hx.1).ne hx.2

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

Goal state before:
pp: case mp
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
⊢ N.FG → ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N

Tactic:
intro hN

Goal state after:
case mp
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
hN : N.FG
⊢ ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ (algebraMap A B).Finite ↔ Module.Finite A B

Tactic:
Finite,

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ Module.Finite A B ↔ Module.Finite A B
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
⊢ ∀ᶠ (n : ℕ) in atTop, Disjoint (f ^ n).ker (f ^ n).range

Tactic:
obtain ⟨n, hn : ∀ m, n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)⟩ :=
    monotone_stabilizes_iff_noetherian.mpr inferInstance f.iterateKer
  refine eventually_atTop.mpr ⟨n, fun m hm ↦ disjoint_iff.mpr ?_⟩
  rw [← hn _ hm, Submodule.eq_bot_iff]
  rintro - ⟨hx, ⟨x, rfl⟩⟩
  apply pow_map_zero_of_le hm
  replace hx : x ∈ LinearMap.ker (f ^ (n + m)) := by
    simpa [f.pow_apply n, f.pow_apply m, ← f.pow_apply (n + m), ← iterate_add_apply] using hx
  rwa [← hn _ (n.le_add_right m)] at hx

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ ¬IsCofinal s ↔ BddAbove s

Tactic:
by
  use .of_not_isCofinal
  rw [not_isCofinal_iff]
  rintro ⟨x, h⟩
  obtain ⟨z, hz⟩ := exists_gt x
  exact ⟨z, fun y hy ↦ (h hy).trans_lt hz⟩

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

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

Tactic:
obtain ⟨c, rfl⟩ := f.mem_range_of_rel hb.lt
    rw [f.apply_covBy_apply_iff] at hb
    exact h _ hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Monoid α
inst✝⁴ : Zero β
inst✝³ : MulAction α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosMono α β
hb : 0 ≤ b
h : a ≤ 1
⊢ a • b ≤ b

Tactic:
simpa only [one_smul] using smul_le_smul_of_nonneg_right h hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Monoid α
inst✝⁴ : Zero β
inst✝³ : MulAction α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosMono α β
hb : 0 ≤ b
h : 1 ≤ a
⊢ b ≤ a • b

Tactic:
simpa only [one_smul] using smul_le_smul_of_nonneg_right h hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁸ : Ring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsOrderedRing α
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ a • b₁ < a • b₂ ↔ b₂ < b₁

Tactic:
rw [← neg_neg a, neg_smul, neg_smul (-a), neg_lt_neg_iff]
  exact smul_lt_smul_iff_of_pos_left (neg_pos_of_neg ha)

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case neg
α : 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)
ha : a ∉ s
⊢ f a ≤ b

Tactic:
· 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: case h
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ a ∈ upperBounds (range Subtype.val)

Tactic:
rintro _ ⟨⟨x, hx⟩, rfl⟩

Goal state after:
case h
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
x : α
hx : x ∈ Iio a
⊢ ↑⟨x, hx⟩ ≤ a
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
h : type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding
⊢ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

pp: case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding

Tactic:
· obtain ⟨a, e⟩ := h
      rw [← e]
      refine inductionOn a ?_
      intro α r _
      exact lift_type_lt.{u, u + 1, max (u + 1) v}.2 ⟨typein r⟩

Goal state after:
case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding
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

Tactic:
← add_le_add_iff_left b,

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

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

Tactic:
← add_le_add_iff_left b,

Goal state after:
a b c : Ordinal.{u_4}
h : b ≤ a
⊢ b + c ≤ b + (a - b) ↔ b + c ≤ a
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}
⊢ ∀ (hr : o < type r) (hs : o < type s), f ((enum r) ⟨o, hr⟩) = (enum s) ⟨o, hs⟩

Tactic:
refine inductionOn o ?_

Goal state after:
α β : 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⟩
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
simp [← nonpos_iff_eq_zero, sub_le]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{?u.38}
ho : 0 < o
⊢ o ≠ 0

Tactic:
by rintro rfl; simp at ho

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

Goal state before:
pp: a b : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < b
⊢ IsSuccLimit (a * b)

Tactic:
by
  rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨b, rfl⟩ | lb)
  · exact b0.false.elim
  · rw [mul_succ]
    exact isSuccLimit_add _ l
  · exact isSuccLimit_mul_right l.bot_lt lb

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

Goal state before:
pp: a : Ordinal.{u_4}
⊢ 0 • a = a * ↑0

Tactic:
rw [zero_nsmul, Nat.cast_zero, mul_zero]

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

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

Tactic:
apply le_antisymm
  · apply (div_le b0).2
    rw [mul_succ, mul_add, add_assoc, add_lt_add_iff_left]
    apply lt_mul_div_add _ b0
  · 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.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 + c < a * (d * succ (b / d))

Tactic:
grw [hc, ← 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.SetTheory.Ordinal.Exponential

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

Tactic:
by
  simpa using (opow_le_of_isSuccLimit b0 h).not

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

Goal state before:
pp: case inr.inr
a b c : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
induction c using limitRecOn with
  | zero => simp
  | add_one c IH => rw [← add_assoc, opow_add_one, IH, opow_add_one, mul_assoc]
  | limit c l IH =>
    refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_add_right b)).le_iff_forall_le l).trans ?_
    simpa +contextual [IH] using
      (((isNormal_mul_right <| opow_pos b (pos_iff_ne_zero.2 ha.ne')).comp
        (isNormal_opow ha')).le_iff_forall_le l).symm

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

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

Tactic:
simp_all [Nat.mul_add_one, Nat.pow_add_one']

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

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

Tactic:
simp_all [Nat.mul_add_one, Nat.pow_add_one']

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

Goal state before:
pp: n : ℕ
⊢ Nat.cast '' Iio n = Iio ↑n

Tactic:
ext o

Goal state after:
n : ℕ
o : Ordinal.{u_4}
⊢ o ∈ Nat.cast '' Iio n ↔ o ∈ Iio ↑n
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
⊢ o % b ^ log b o < b ^ log b o

Tactic:
exact mod_lt _ (opow_pos _ hb.pos).ne'

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

Goal state before:
pp: x : Ordinal.{u_1}
| preOmega ω ≤ preOmega x

Tactic:
preOmega_le_preOmega

Goal state after:
x : Ordinal.{u_1}
| ω ≤ x
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ ℵ_ (0 + 1) = ℵ_ 1

Tactic:
zero_add

Goal state after:
⊢ ℵ_ 1 = ℵ_ 1
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case ha
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ 0 < ω ^ c

pp: case hbc
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ n * b < ω

Tactic:
exacts [opow_pos _ omega0_pos, isPrincipal_mul_omega0 hn hb]

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

Goal state before:
pp: case refine_1.inr
a b : Cardinal.{u_1}
h : a + b = a
ha : (∃ n, a = ↑n) ∧ ∃ n, b = ↑n
⊢ b = 0

Tactic:
rcases ha with ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩

Goal state after:
case refine_1.inr
n m : ℕ
h : ↑n + ↑m = ↑n
⊢ ↑m = 0
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case e'_3
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
⊢ s = range fun i ↦ ↑(f i)

Tactic:
rw [range_comp', f.range_eq]

Goal state after:
case e'_3
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
⊢ s = Subtype.val '' Set.univ
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

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

Tactic:
apply (isSuccLimit_ord _).isSuccPrelimit

Goal state after:
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
ha : 1 < a
⊢ ℵ₀ ≤ o.cof
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ω ≤ c.ord

Tactic:
omega0_le_ord

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ℵ₀ ≤ c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ (ω_ 1).cof = ℵ_ 1

Tactic:
by
  simpa using isRegular_aleph_one.cof_omega_eq

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

Goal state before:
pp: case refine_2
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ θ ≤ #↑{x | ∃ (h : x ∈ s), f ⟨x, h⟩ = a}

Tactic:
refine
      ha.trans
        (ge_of_eq <|
          Quotient.sound ⟨Equiv.trans ?_ (Equiv.subtypeSubtypeEquivSubtypeExists _ _).symm⟩)

Goal state after:
case refine_2
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ ↑{x | ∃ (h : x ∈ s), f ⟨x, h⟩ = a} ≃ { a_1 // ∃ (h : a_1 ∈ s), ⟨a_1, h⟩ ∈ f ⁻¹' {a} }
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : Infinite α
⊢ #(α → α) ≤ #(α ≃ α)

Tactic:
suffices Nonempty ((α → Bool) ↪ Equiv.Perm (α × Bool)) by
      obtain ⟨e⟩ : Nonempty (α ≃ α × Bool) := by simp [← Cardinal.eq, mul_two]
      simp only [← le_def, mk_pi, mk_fintype, Fintype.card_bool, Nat.cast_ofNat,
        prod_const, lift_ofNat, lift_uzero] at this
      rwa [← power_def, power_self_eq (aleph0_le_mk α), e.permCongr.cardinal_eq]

Goal state after:
α : Type u
inst✝ : Infinite α
⊢ Nonempty ((α → Bool) ↪ Perm (α × Bool))
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
apply extend_function f

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, (sumAddHom fun i ↦ (S i).subtype) f = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x

Tactic:
sumAddHom_apply

Goal state after:
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, (f.sum fun x ↦ ⇑(S x).subtype) = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x
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:
ext
  rw [smul_apply, comapDomain'_apply, smul_apply, comapDomain'_apply]

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

Goal state before:
pp: case h.cons.inl
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
h : f i = 0
⊢ p (0 + erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })

Tactic:
zero_add

Goal state after:
case h.cons.inl
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
h : f i = 0
⊢ p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })