mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case inr
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
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne : s.Nonempty
n : ℕ
hn : n = s.max' ne
⊢ f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y

Tactic:
revert x y

Goal state after:
case inr
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 : ℕ
⊢ ∀ ⦃x y : ℕ →₀ P⦄,
    let s := x.support ∪ y.support;
    ∀ (ne : s.Nonempty), n = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case inl
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
i : α
x : M
hx : x ∈ p i
⊢ ((lsingle i) x) i ∈ p i

Tactic:
simp_all

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

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
i : α
x : M
hx : x ∈ p i
j : α
h : i ≠ j
⊢ ((lsingle i) x) j ∈ p j

Tactic:
simp_all

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
a✝ : I
⊢ ((mapRange.linearMap f) { support := x.support, toFun := y, mem_support_toFun := ⋯ }) a✝ = x a✝

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
⊢ comap f (comap g F) = F

Tactic:
by
  rw [comap_comap, hfg.comp_eq_id, comap_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
s : Set α
g : Filter β
⊢ comap m g ≤ 𝓟 s ↔ g ≤ 𝓟 (kernImage m s)

Tactic:
le_principal_iff,

Goal state after:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
g : Filter β
⊢ s ∈ comap m g ↔ g ≤ 𝓟 (kernImage m s)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
s : Set α
g : Filter β
⊢ s ∈ comap m g ↔ g ≤ 𝓟 (kernImage m s)

Tactic:
le_principal_iff,

Goal state after:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
g : Filter β
⊢ s ∈ comap m g ↔ kernImage m s ∈ g
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
l : Filter β
⊢ range f ∈ l

Tactic:
by simp only [hf.range_eq, univ_mem]

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

Goal state before:
pp: α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
⊢ Disjoint atBot atTop

Tactic:
by_cases hle : x ≤ y

Goal state after:
case pos
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint atBot atTop

case neg
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint atBot atTop
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : SemilatticeSup β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
⊢ f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂

Tactic:
filter_upwards [hf, hg] with x hfx hgx using sup_le_sup hfx hgx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ {g} ∈ pure g

Tactic:
exact singleton_mem_pure

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 β
⊢ atTop ≤ 𝓟 (f ⁻¹' s) ↔ ∃ N, ∀ (n : α), N ≤ n → f n ∈ s

Tactic:
le_principal_iff,

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
f : α → β
s : Set β
⊢ f ⁻¹' s ∈ atTop ↔ ∃ N, ∀ (n : α), N ≤ n → f n ∈ s
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]

Goal state after:
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')
⊢ ↑s' ⊆ ↑(span R s)
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
hsb : ∀ (i : ι), (p i).FG
⊢ (pi univ p).FG

Tactic:
by
  classical
    simp_rw [fg_def] at hsb ⊢
    choose t htf hts using hsb
    refine
      ⟨⋃ i, (LinearMap.single R _ i) '' t i, Set.finite_iUnion fun i => (htf i).image _, ?_⟩
    -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 changed `span_image` into `span_image _`
    simp_rw [span_iUnion, span_image _, hts, iSup_map_single]

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 α β
hb : b₁ < b₂
ha : a < 0
⊢ -(-a • b₂) < -(-a • b₁)

Tactic:
neg_lt_neg_iff

Goal state after:
α : 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 α β
hb : b₁ < b₂
ha : a < 0
⊢ -a • b₁ < -a • b₂
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✝ : PosSMulReflectLT α β
h : -(-a • b₁) < -(-a • b₂)
ha : a ≤ 0
⊢ b₂ < b₁

Tactic:
neg_lt_neg_iff

Goal state after:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulReflectLT α β
h : -a • b₂ < -a • b₁
ha : a ≤ 0
⊢ b₂ < b₁
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:
neg_lt_neg_iff

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
⊢ b < f a ↔ ∃ a' < a, b < f a'

Tactic:
by
  simpa [mem_upperBounds] using lt_isLUB_iff (hf.isLUB_image_Iio_of_isSuccLimit ha)

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
inst✝⁴ : LinearOrder α
inst✝³ : WellFoundedLT α
inst✝² : SuccOrder α
inst✝¹ : LinearOrder β
inst✝ : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
⊢ f = g → f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)

Tactic:
simp_all

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

Goal state before:
pp: case mpr.type.refine_2
b✝ : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h✝ : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
a b : β
h : s a b
⊢ (typein r).toRelEmbedding ((enum r) ⟨f a, ⋯⟩) < (typein r).toRelEmbedding ((enum r) ⟨f b, ⋯⟩)

Tactic:
typein_enum,

Goal state after:
case mpr.type.refine_2
b✝ : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h✝ : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
a b : β
h : s a b
⊢ f a < (typein r).toRelEmbedding ((enum r) ⟨f b, ⋯⟩)
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
⊢ ∃ c', c = lift.{max (u + 1) v, u} c'

Tactic:
let ⟨a, h', e⟩ := lt_lift_iff.1 h
    rw [mk_ordinal] at h'
    rcases lt_univ.{u}.1 h' with ⟨c', rfl⟩
    exact ⟨c', by simp only [e.symm, lift_lift]⟩

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

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

Tactic:
le_antisymm_iff,

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.Basic

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

Tactic:
simp_rw [le_antisymm_iff, lift_le]

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
⊢ Cardinal.lift.{(max u v) + 1, max u v} (sInf (range f)ᶜ).card ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι

Tactic:
apply (lift_card_sInf_compl_le _).trans

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ #↑(range f) ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ f ((type r).bsup g) = (type r).bsup fun a h ↦ f (g a h)

Tactic:
rw [← iSup'_eq_bsup r, Order.IsNormal.map_iSup H bddAbove_of_small, ← iSup'_eq_bsup r] <;>
      rfl

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

Goal state before:
pp: case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
w✝ : ι
hf : f w✝ = iSup f
⊢ iSup f < lsub f

Tactic:
← hf

Goal state after:
case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
w✝ : ι
hf : f w✝ = iSup f
⊢ f w✝ < lsub f
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case zero
n : ℕ
hn : n ≠ 0
b : ℕ
hb : 1 < b
hfuel : n < b ^ 0
⊢ (go n b 0).fst = n / b ^ (go n b 0).snd ∧ b ^ (go n b 0).snd ≤ n ∧ n < b ^ ((go n b 0).snd + 1)

Tactic:
simp_all

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

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

Tactic:
simp_all

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

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

Tactic:
simp_all

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

Goal state before:
pp: case refine_2
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w✝¹ : Ordinal.{u}
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = o.bsup f
⊢ o.bsup f < o.blsub f

Tactic:
← hf

Goal state after:
case refine_2
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w✝¹ : Ordinal.{u}
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = o.bsup f
⊢ f w✝¹ w✝ < o.blsub f
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ (typein r).toRelEmbedding (⋯.min sᶜ h) ≤ (typein r).toRelEmbedding ((enum r) ⟨(#↑s).ord, ⋯⟩)

Tactic:
typein_enum,

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ (typein r).toRelEmbedding (⋯.min sᶜ h) ≤ (#↑s).ord
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
le_antisymm_iff,

Goal state after:
case inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ log b n ≤ m ∧ m ≤ log b n ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
a b c : Ordinal.{u_1}
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : a = 1
⊢ a ^ b ≤ a ^ c

Tactic:
simp_all

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

Goal state before:
pp: case pos
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
h✝ : c = 0
⊢ a ^ c ≤ b ^ c

Tactic:
simp_all

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

Goal state before:
pp: case neg
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
h✝ : ¬c = 0
⊢ a ^ c ≤ b ^ c

Tactic:
simp_all

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

Goal state before:
pp: case zero
n : ℕ
hn : 1 < n
b : ℕ
hb : 1 < b
hfuel : n < b ^ 0
⊢ (go n b 0).fst = b ^ ((go n b 0).snd + 1) / n ∧ b ^ (go n b 0).snd < n ∧ n ≤ b ^ ((go n b 0).snd + 1)

Tactic:
simp_all

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

Goal state before:
pp: case pos
b c : Ordinal.{u_1}
hb : 0 < b
this : b ≠ 0
h✝ : c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

Tactic:
simp_all

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

Goal state before:
pp: case neg
b c : Ordinal.{u_1}
hb : 0 < b
this : b ≠ 0
h✝ : ¬c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

Tactic:
simp_all

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

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

Tactic:
opow_add_one

Goal state after:
case inr.inr.inr.add_one
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b * c) = (a ^ b) ^ c
⊢ (a ^ b) ^ c * a ^ b = (a ^ b) ^ c * a ^ b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a * ω ≤ nfp (fun x ↦ a + x) b

pp: a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a + a * ω ≤ a * ω

Tactic:
· rw [← nfp_add_zero]
    exact nfp_monotone (isNormal_add_right a).monotone zero_le

Goal state after:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a + a * ω ≤ a * ω
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1.inr.inl
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
h✝ : o = 0
⊢ a + o = o

Tactic:
simp_all

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

Goal state before:
pp: case refine_1.inr.inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
h✝ : o = 1
⊢ a + o = o

Tactic:
simp_all

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

Goal state before:
pp: x : Ordinal.{u_1}
⊢ ω < preOmega x ↔ ω < x

Tactic:
by
  conv_lhs => rw [← preOmega_omega0, preOmega_lt_preOmega]

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

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
⊢ max a b * max a b < c

Tactic:
obtain h | h := lt_or_ge (max a b) ℵ₀

Goal state after:
case inl
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : max a b < ℵ₀
⊢ max a b * max a b < c

case inr
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : ℵ₀ ≤ max a b
⊢ max a b * max a b < c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof < ℵ₀ ↔ o.cof ≤ 1

Tactic:
by
  simpa using Order.cof_lt_aleph0_iff (α := o.ToType)

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

Goal state before:
pp: ⊢ succ ℵ₀ = ℵ_ 1

Tactic:
by
  rw [← aleph_zero, succ_aleph, zero_add]

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

Goal state before:
pp: case inr.inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
rw [mul_comm, mul_eq_max_of_aleph0_le_left hb ha0, max_comm]

Goal state after:
case inr.inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ max a b ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a + b = b ↔ max ℵ₀ a ≤ b ∨ a = 0

Tactic:
by
  rw [add_comm, add_eq_left_iff]

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ ⨆ i, f i * c = ⨆ i, c * f i

Tactic:
simp_rw [mul_comm]

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

Goal state before:
pp: case add_one
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ (a ^ (b + 1)).card ≤ max a.card (b + 1).card

Tactic:
rw [opow_add_one, card_mul, card_add_one, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]

Goal state after:
case add_one
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ max a.card (a ^ b).card ≤ max a.card (b.card + 1)

case add_one.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ (a ^ b).card ≠ 0

case add_one.h
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ ℵ₀ ≤ a.card
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, lift.{u, v} (f i)
⊢ sum f = lift.{u, v} (⨆ i, f i)

Tactic:
apply (lift_iSup_le_sum f).antisymm'

Goal state after:
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, lift.{u, v} (f i)
⊢ sum f ≤ lift.{u, v} (⨆ i, f i)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_1
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
⊢ o.cof ≤ #ι

Tactic:
← hf

Goal state after:
case refine_1
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
⊢ (lsub f).cof ≤ #ι
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
have hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀ := add_lt_aleph0_iff.1 hfin

Goal state after:
case inr
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀
⊢ κ₁ + μ₁ < κ₂ + μ₂
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
⊢ ∃ a, ℵ₀ < #↑(f ⁻¹' {a})

Tactic:
← aleph_one_le_iff

Goal state after:
β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
⊢ ∃ a, ℵ_ 1 ≤ #↑(f ⁻¹' {a})
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
x : Π₀ (i : ι), β₁ i
s : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
i : ι
h : x i = 0
⊢ f i (x i) = 0

Tactic:
← hf i,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
x : Π₀ (i : ι), β₁ i
s : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
i : ι
h : x i = 0
⊢ f i (x i) = f i 0
Module: Mathlib.Data.DFinsupp.BigOperators

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

Tactic:
intro i hi hi'

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
⊢ ((Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
          ⟨Finset.univ.val, ⋯⟩).liftOn
      (fun l ↦ Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ ⟦a i⟧)) ⋯ =
    ⟦a⟧

Tactic:
obtain ⟨l, hl⟩ := (Finset.univ.val : Multiset ι).exists_rep

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
l : List ι
hl : ⟦l⟧ = Finset.univ.val
⊢ ((Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
          ⟨Finset.univ.val, ⋯⟩).liftOn
      (fun l ↦ Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ ⟦a i⟧)) ⋯ =
    ⟦a⟧
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β₁ i)
inst✝¹ : (i : ι) → Zero (β₂ i)
inst✝ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ (mapRange f hf g) i✝ = (mk g.support fun i ↦ f (↑i) (g ↑i)) i✝

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
P : (Fin 0 → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin 0 → α), P x

Tactic:
simp only [Forall, Fin.forall_fin_zero_pi]
    rfl

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
m : M
hm : (Finsupp.lsingle i) m ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), (fun i ↦ (Finsupp.lsingle i).range) j)
this✝ : ⨆ j, ⨆ (_ : j ≠ i), (Finsupp.lsingle j).range ≤ Finsupp.supported M R {i}ᶜ
this : ↑((Finsupp.lsingle i) m).support ⊆ {i}ᶜ
⊢ (Finsupp.lsingle i) m ∈ ⊥

Tactic:
simp_all

Goal state after: