mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : Module R' M
inst✝³ : SMulWithZero R R'
inst✝² : IsScalarTower R R' M
inst✝¹ : FaithfulSMul R R'
inst✝ : IsScalarTower R R' R'
⊢ ⨆ ι, #↑↑ι ≤ ⨆ ι, #↑↑ι

Tactic:
exact ciSup_le' fun ⟨s, hs⟩ ↦ le_ciSup_of_le Cardinal.bddAbove_of_small
    ⟨s, hs.restrict_scalars (by simpa [← faithfulSMul_iff_injective_smul_one])⟩ le_rfl

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
⊢ (f '' s).encard = s.encard

Tactic:
rw [encard, ENat.card_image_of_injOn h, encard]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
h : ↑(𝒫 s).ncard = 2 ^ ↑s.ncard
⊢ (𝒫 s).ncard = 2 ^ s.ncard

Tactic:
norm_cast at h

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
⊢ Nontrivial c.Quotient ↔ c ≠ ⊤

Tactic:
simp [← not_subsingleton_iff_nontrivial]

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
⊢ insert a (Icc (succ a) b) = Icc a b

Tactic:
ext x; simp [or_and_left, eq_comm, ← le_iff_eq_or_succ_le]; aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ (inl R M M₂).range = (snd R M M₂).ker

Tactic:
ext x
  simp only [mem_ker, mem_range]
  constructor
  · rintro ⟨y, rfl⟩
    rfl
  · intro h
    exact ⟨x.fst, Prod.ext rfl h.symm⟩

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : IsMin b
⊢ Ioc a (pred b) = Ioo a b

Tactic:
Ioc_eq_empty (hb.mono <| pred_le _).not_lt,

Goal state after:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : IsMin b
⊢ ∅ = Ioo a b
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
s : Set M
t : Set M₂
⊢ span R (⇑(inl R M M₂) '' s) ⊔ span R (⇑(inr R M M₂) '' t) = span R (⇑(inl R M M₂) '' s) ⊔ map (inr R M M₂) (span R t)

Tactic:
← span_image

Goal state after:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
s : Set M
t : Set M₂
⊢ span R (⇑(inl R M M₂) '' s) ⊔ span R (⇑(inr R M M₂) '' t) = span R (⇑(inl R M M₂) '' s) ⊔ span R (⇑(inr R M M₂) '' t)
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
a b : α
inst✝ : NoMaxOrder α
h : a ≤ b
⊢ insert b (Ico a b) = Ico a (b + 1)

Tactic:
simpa [succ_eq_add_one] using insert_Ico_right_eq_Ico_succ h

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b c : M
⊢ (fun x ↦ a + x) '' Ioc b c = Ioc (a + b) (a + c)

Tactic:
by
  simp only [add_comm a, image_add_const_Ioc]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: ι : Type u_2
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
α : Type u_3
f : ι → Set α
n : ι
⊢ ⋃ i ∈ Iic n, disjointed f i = (partialSups f) n

Tactic:
by
  rw [← partialSups_disjointed, partialSups_eq_biSup]
  simp

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

Goal state before:
pp: case inl
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : k < m
i : ℕ
left✝¹ : k ≤ i
im : i < m
j : ℕ
left✝ : k ≤ j
jm : j < m
Hij : n - i = n - j
⊢ n - (n - i) = j

Tactic:
Hij,

Goal state after:
case inl
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : k < m
i : ℕ
left✝¹ : k ≤ i
im : i < m
j : ℕ
left✝ : k ≤ j
jm : j < m
Hij : n - i = n - j
⊢ n - (n - j) = j
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
p : α
hp : p ≠ 0
⊢ (span {p}).IsPrime ↔ Prime p

Tactic:
simp [isPrime_iff, Prime, span_singleton_eq_top, hp, mem_span_singleton]

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

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y + x * z} = span {x, y}

Tactic:
span_pair_add_left_mul

Goal state after:
α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y} = span {x, y}
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ (1 + 1) ^ (2 * n) = ∑ m ∈ range (2 * n + 1), (2 * n).choose m

Tactic:
simp [-Nat.reduceAdd, add_pow]

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

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

Tactic:
← span_pair_add_left_mul,

Goal state after:
α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y - x * z + x * ?z} = span {x, y}

case z
α : Type u
inst✝ : CommRing α
x y z : α
⊢ α
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) ↔ IsSimpleOrder (Ideal R)

Tactic:
exact ⟨fun h => ⟨h⟩, fun h => h.2⟩

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

Goal state before:
pp: M : Type u_5
inst✝¹ : AddCommMonoid M
X : Type u_6
inst✝ : Finite X
⊢ map _root_.id = _root_.id

Tactic:
ext s

Goal state after:
M : Type u_5
inst✝¹ : AddCommMonoid M
X : Type u_6
inst✝ : Finite X
s : X → M
x✝ : X
⊢ map _root_.id s x✝ = _root_.id s x✝
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
Z : Type u_8
inst✝² : Finite X
inst✝¹ : Finite Y
inst✝ : Finite Z
g : Y → Z
f : X → Y
⊢ map (g ∘ f) = map g ∘ map f

Tactic:
ext s

Goal state after:
M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
Z : Type u_8
inst✝² : Finite X
inst✝¹ : Finite Y
inst✝ : Finite Z
g : Y → Z
f : X → Y
s : X → M
x✝ : Z
⊢ map (g ∘ f) s x✝ = (map g ∘ map f) s x✝
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
inst✝ : f.NeBot
c : β
⊢ map (fun x ↦ c) f = pure c

Tactic:
ext s

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : f.NeBot
c : β
s : Set β
⊢ s ∈ map (fun x ↦ c) f ↔ s ∈ pure c
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
inst✝ : f.NeBot
c : β
⊢ map (fun x ↦ c) f = pure c

Tactic:
ext s
  by_cases h : c ∈ s <;> simp [h]

Goal state after:
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : Preorder α
a b : α
⊢ Disjoint (Ici a) (Iic b) ↔ ¬a ≤ b

Tactic:
rw [Set.disjoint_iff_inter_eq_empty, Ici_inter_Iic, Icc_eq_empty_iff]

Goal state after:
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : Preorder α
a : α
⊢ ⋃ b, Ioc a b = Ioi a

Tactic:
by
  simp only [← Ioi_inter_Iic, ← inter_iUnion, iUnion_Iic, inter_univ]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f✝ g : Filter α
s t : Set α
f : Filter α
⊢ ⊤ \ f = ￢f

Tactic:
ext s

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f✝ g : Filter α
s✝ t : Set α
f : Filter α
s : Set α
⊢ s ∈ ⊤ \ f ↔ s ∈ ￢f
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter γ
m₁ : α → γ
m₂ : β → γ
⊢ comap (Sum.elim m₁ m₂) l = map inl (comap m₁ l) ⊔ map inr (comap m₂ l)

Tactic:
ext s

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter γ
m₁ : α → γ
m₂ : β → γ
s : Set (α ⊕ β)
⊢ s ∈ comap (Sum.elim m₁ m₂) l ↔ s ∈ map inl (comap m₁ l) ⊔ map inr (comap m₂ l)
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst✝ : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ y, r x y
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)

Tactic:
have : Nonempty β := let ⟨_, hx⟩ := h.exists; hx.nonempty
  choose! f hf using fun x (hx : ∃ y, r x y) => hx
  exact ⟨f, h.mono hf⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → Filter β
p : β → Prop
⊢ (¬∃ᶠ (y : β) in f.bind m, p y) ↔ ¬∃ᶠ (x : α) in f, ∃ᶠ (y : β) in m x, p y

Tactic:
simp only [not_frequently, eventually_bind]

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

Goal state before:
pp: ι : Type u_6
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : Tendsto x atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto (fun n ↦ x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))

Tactic:
choose ns hge hns using frequently_atTop.1 h

Goal state after:
ι : Type u_6
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : Tendsto x atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
ns : ℕ → ℕ
hge : ∀ (a : ℕ), a ≤ ns a
hns : ∀ (a : ℕ), p (x (ns a))
⊢ ∃ ns, Tendsto (fun n ↦ x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))
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
c : α
hb : f c ⋖ f a
⊢ False

Tactic:
f.apply_covBy_apply_iff

Goal state after:
case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit a
c : α
hb : c ⋖ a
⊢ False
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ IsNormal f ↔ StrictMono f ∧ ∀ (o : α), IsSuccLimit o → ∀ (a : β), (∀ b < o, f b ≤ a) → f o ≤ a

Tactic:
by
  simp [isNormal_iff', mem_lowerBounds, mem_upperBounds]

Goal state after:
Module: Mathlib.Order.IsNormal

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

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

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ sSup (f ⁻¹' Iic x) ∈ f ⁻¹' Iic x

Tactic:
· rw [mem_preimage, hf.map_sSup h₁ h₂]
    apply (csSup_le_csSup bddAbove_Iic _ (image_preimage_subset ..)).trans
    · rw [csSup_Iic]
    · simpa

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case e'_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ a = ⨆ i, ↑i

Tactic:
exact ha.iSup_Iio.symm

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

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

Tactic:
mk_ordinal

Goal state after:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
a : Cardinal.{u + 1}
h' : a < univ.{u, u + 1}
e : lift.{v, u + 1} a = c
⊢ ∃ c', c = lift.{max (u + 1) v, u} c'
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_3
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯) → a < type r

pp: case refine_4
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a < type r → a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯)

Tactic:
· rintro ⟨b, rfl⟩
    exact (PrincipalSeg.ofElement _ _).ordinal_type_lt

Goal state after:
case refine_4
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a < type r → a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯)
Module: Mathlib.SetTheory.Ordinal.Basic

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

Tactic:
← o.type_toType

Goal state after:
o : Ordinal.{u}
⊢ (typein LT.lt).toRelEmbedding o = lift.{u + 1, u} (typeLT o.ToType)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
⊢ a ≤ b → ∃ c, b = a + c

Tactic:
refine inductionOn₂ a b fun α r _ β s _ ⟨f⟩ ↦ ?_

Goal state after:
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝² : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝¹ : IsWellOrder β s
x✝ : type r ≤ type s
f : r ≼i s
⊢ ∃ c, type s = type r + c
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: β : Type u_2
f : β → Ordinal.{u_3}
⊢ ⨆ i, f i ≤ ⨆ i, f i + 1

Tactic:
rw [iSup, iSup, range_comp' (· + 1)]

Goal state after:
β : Type u_2
f : β → Ordinal.{u_3}
⊢ sSup (range fun i ↦ f i) ≤ sSup ((fun x ↦ x + 1) '' range f)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case neg
α β : 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
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : ¬b = b'
⊢ { x // s x b } × α ⊕ { x // r x a }

Tactic:
· exact .inl (⟨b', by grind⟩, a')

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

Goal state before:
pp: a b c : Ordinal.{u_4}
ba : b + a = a
l : IsSuccLimit c
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
⊢ a * c ≤ (a + b) * c

Tactic:
by grw [← le_self_add]

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

Goal state before:
pp: ⊢ ℵ₀.ord = ω

Tactic:
by
  refine le_antisymm (ord_le.2 le_rfl) <| le_of_forall_lt fun o h ↦ ?_
  rcases Ordinal.lt_lift_iff.1 h with ⟨o, ho, rfl⟩
  rw [lt_ord, ← lift_card, lift_lt_aleph0, ← typein_enum _ ho]
  exact lt_aleph0_iff_fintype.2 ⟨Set.fintypeLTNat _⟩

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

Goal state before:
pp: case inl
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
h : (log.go y b y).snd < x
⊢ (log.go y b y).snd < x ↔ y < b ^ x

Tactic:
| inl h =>

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

Goal state before:
pp: a : Cardinal.{u_1}
⊢ 0 < a.ord ↔ 0 < a

Tactic:
by
  rw [← ord_zero, ord_lt_ord]

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

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

Tactic:
← hc'

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

Goal state before:
pp: case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ log b n < c + 1 ↔ log b (n / b) + 1 < c + 1

Tactic:
rw [log_lt_iff_lt_pow, Nat.add_lt_add_iff_right, log_lt_iff_lt_pow,
      Nat.pow_add_one, Nat.div_lt_iff_lt_mul] <;> grind

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

Goal state before:
pp: b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
⊢ b ^ 0 ≤ y

Tactic:
Nat.pow_zero,

Goal state after:
b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
⊢ 1 ≤ y
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b c : ℕ
hc : 1 < c
hb : c ≤ b
⊢ 0 ≤ log c 0

Tactic:
log_zero_right

Goal state after:
case inl
b c : ℕ
hc : 1 < c
hb : c ≤ b
⊢ 0 ≤ 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b 0 = 0 - 1

Tactic:
log_zero_right

Goal state after:
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ 0 = 0 - 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
h : a ≠ 1 ∧ b ≠ 0
ha : 1 < a
⊢ a ^ b ≠ 1

Tactic:
simpa using ((opow_lt_opow_iff_right ha).2 h.2.pos).ne'

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

Goal state before:
pp: case inl
⊢ 0 = log 2 0

Tactic:
log_zero_right

Goal state after:
case inl
⊢ 0 = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
⊢ log b n ≤ clog b n

Tactic:
obtain hb | hb := le_or_gt b 1

Goal state after:
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ clog b n

case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ clog b n
Module: Mathlib.Data.Nat.Log

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

Tactic:
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: b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
⊢ b ^ c ≤ x

Tactic:
obtain hb | hb := le_or_gt b 1

Goal state after:
case inl
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : b ≤ 1
⊢ b ^ c ≤ x

case inr
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : 1 < b
⊢ b ^ c ≤ x
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b x : Ordinal.{u_1}
hx : x ≠ 0
⊢ b ^ log b x ≤ x

Tactic:
obtain hb | hb := le_or_gt b 1

Goal state after:
case inl
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : b ≤ 1
⊢ b ^ log b x ≤ x

case inr
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : 1 < b
⊢ b ^ log b x ≤ x
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
log_zero_right

Goal state after:
case inl
b : Ordinal.{u_1}
⊢ 0 ≤ 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b : Ordinal.{u_1}
hb : b ≤ 1
⊢ log b 1 = 0

Tactic:
· exact log_of_left_le_one hb 1

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

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

Tactic:
log_zero_right

Goal state after:
case inl
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ 0 < log b o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ List.foldr (fun x ↦ f) a (List.replicate n ()) ≤ nfp f a

Tactic:
exact Ordinal.le_iSup _ _

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

Goal state before:
pp: case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ f^[l.length] a ≤ ⨆ n, f^[n] a

Tactic:
exact Ordinal.le_iSup _ _

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

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

Tactic:
· rw [← mul_assoc, ← opow_one_add, one_add_omega0]

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℶ_ ↑n < lift.{v, u} c ↔ ℶ_ ↑n < c

Tactic:
by
  simpa using lift_lt (a := ℶ_ n)

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

Goal state before:
pp: α : Type u
β' : Type v
⊢ IsEmpty (α ≃ β') ↔ lift.{v, u} #α ≠ lift.{u, v} #β'

Tactic:
← not_nonempty_iff,

Goal state after:
α : Type u
β' : Type v
⊢ ¬Nonempty (α ≃ β') ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
⊢ IsEmpty (α ↪ β') ↔ lift.{u, v} #β' < lift.{v, u} #α

Tactic:
← not_nonempty_iff,

Goal state after:
α : Type u
β' : Type v
⊢ ¬Nonempty (α ↪ β') ↔ lift.{u, v} #β' < lift.{v, u} #α
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 : α
⊢ Bounded r {x}

pp: case a.refine_2
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
⊢ Injective fun x ↦ ⟨{x}, ⋯⟩

Tactic:
· apply bounded_singleton
      rw [← hr]
      apply isSuccLimit_ord ha

Goal state after:
case a.refine_2
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
⊢ Injective fun x ↦ ⟨{x}, ⋯⟩
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → SMulZeroClass γ (β i)
p : ι → Prop
inst✝ : DecidablePred p
r : γ
f : Π₀ (i : ι), β i
⊢ filter p (r • f) = r • filter p f

Tactic:
ext
  simp [smul_apply, smul_ite]

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: case a
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C✝ : ((i : ι) → Quotient (S i)) → Prop
f : ∀ (a : (i : ι) → α i), C✝ fun x ↦ ⟦a x⟧
q : (i : ι) → Quotient (S i)
a✝ : List ι
C : ((i : ι) → i ∈ ⟦a✝⟧ → Quotient (S i)) → Prop
⊢ (∀ (a : (i : ι) → i ∈ ⟦a✝⟧ → α i), C fun x1 x2 ↦ ⟦a x1 x2⟧) → ∀ (q : (i : ι) → i ∈ ⟦a✝⟧ → Quotient (S i)), C q

Tactic:
exact list_ind

Goal state after:
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
⊢ mapRange f hf g = mk g.support fun i ↦ f (↑i) (g ↑i)

Tactic:
by
  ext
  simp_all

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

Goal state before:
pp: case some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
j : ι
⊢ (extendWith x 0) (some j) = (single none x) (some j)

Tactic:
extendWith_some,

Goal state after:
case some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
j : ι
⊢ 0 j = (single none x) (some j)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case some
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
i : ι
⊢ ((fun f ↦ extendWith f.1 f.2) ((fun f ↦ (f none, comapDomain some ⋯ f)) f)) (some i) = f (some i)

Tactic:
extendWith_some,

Goal state after:
case some
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
i : ι
⊢ ((fun f ↦ (f none, comapDomain some ⋯ f)) f).2 i = f (some i)