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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
H : r ^ n ∈ I
⊢ r ∈ I

Tactic:
induction n with
  | zero =>
    rw [pow_zero] at H
    exact hI.one_notMem.elim H
  | succ n ih =>
    rw [pow_succ] at H
    exact Or.casesOn (hI.mem_or_mem H) ih id

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

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ Commute a b

Tactic:
have := mul_eq_zero_of_anticommute ha hab

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
this : a * b = 0
⊢ Commute a b
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ Commute a b

Tactic:
by
  have := mul_eq_zero_of_anticommute ha hab
  rw [this, zero_add] at hab
  rw [Commute, SemiconjBy, hab, this]

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

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

Tactic:
by
  rw [span_insert, span_singleton_neg, span_insert]

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

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z x✝¹ : α
x✝ : ∃ a b, a * (x + y * z) + b * y = x✝¹
a b : α
h : a * (x + y * z) + b * y = x✝¹
⊢ a * x + (b + a * z) * y = x✝¹

Tactic:
← h

Goal state after:
α : Type u
inst✝ : CommRing α
x y z x✝¹ : α
x✝ : ∃ a b, a * (x + y * z) + b * y = x✝¹
a b : α
h : a * (x + y * z) + b * y = x✝¹
⊢ a * x + (b + a * z) * y = a * (x + y * z) + b * y
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z x✝¹ : α
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : α
h : a * x + b * y = x✝¹
⊢ a * (x + y * z) + (b - a * z) * y = x✝¹

Tactic:
← h

Goal state after:
α : Type u
inst✝ : CommRing α
x y z x✝¹ : α
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : α
h : a * x + b * y = x✝¹
⊢ a * (x + y * z) + (b - a * z) * y = a * x + b * y
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
⊢ x ∈ ⇑(mk I) ⁻¹' ⇑(mk I) '' s ↔ x ∈ ⋃ x, (fun y ↦ ↑x + y) '' s

Tactic:
simp only [mem_preimage, mem_image, mem_iUnion, Ideal.Quotient.eq]

Goal state after:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
⊢ (∃ x_1 ∈ s, x_1 - x ∈ I) ↔ ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
h : ⊥ = ⊤
⊢ 1 ∉ ⊤

Tactic:
← h

Goal state after:
K : Type u
inst✝ : DivisionSemiring K
h : ⊥ = ⊤
⊢ 1 ∉ ⊥
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case zero
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
⊢ 1 ∈ span ((fun x ↦ x ^ 0) '' s)

pp: case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)

Tactic:
· obtain rfl | ⟨x, hx⟩ := eq_empty_or_nonempty s
    · rw [Set.image_empty, hs]
      trivial
    · exact subset_span ⟨_, hx, pow_zero _⟩

Goal state after:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case refine_1
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
⊢ submodule p ≤ ⨆ i, map (lsingle i) (p i)

Tactic:
intro x hx
    rw [← Finsupp.sum_single x]
    refine Submodule.sum_mem _ (fun i _ ↦ ?_)
    exact Submodule.mem_iSup_of_mem i (Submodule.mem_map_of_mem (hx i))

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

Goal state before:
pp: α : Type u
f : Filter α
β : Sort v
s : β → Set α
inst✝ : Subsingleton β
⊢ (∀ i ∈ range s, i ∈ f) ↔ ∀ (i : β), s i ∈ f

Tactic:
forall_mem_range

Goal state after:
α : Type u
f : Filter α
β : Sort v
s : β → Set α
inst✝ : Subsingleton β
⊢ (∀ (i : β), s i ∈ f) ↔ ∀ (i : β), s i ∈ f
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case mpr
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
⊢ x ∈ (mapRange.linearMap f).range

Tactic:
refine ⟨⟨x.support, y, fun i => ?_⟩, by ext; simp_all⟩

Goal state after:
case mpr
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
i : I
⊢ i ∈ x.support ↔ y i ≠ 0
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case mpr
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
i : I
⊢ i ∈ x.support ↔ y i ≠ 0

Tactic:
constructor
    <;> contrapose

Goal state after:
case mpr.mp
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
i : I
⊢ y i = 0 → i ∉ x.support

case mpr.mpr
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
i : I
⊢ i ∉ x.support → y i = 0
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t : Set β
m : α → β
f : Filter α
⊢ ∀ {x y : Set β}, x ∈ kernImage m '' f.sets → y ∈ kernImage m '' f.sets → x ∩ y ∈ kernImage m '' f.sets

Tactic:
rintro _ _ ⟨s₁, h₁, rfl⟩ ⟨s₂, h₂, rfl⟩
    exact ⟨s₁ ∩ s₂, f.inter_sets h₁ h₂, Set.preimage_kernImage.u_inf⟩

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

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

Tactic:
Prod.exists

Goal state after:
α : Type u_1
ι : Type u_6
ι' : Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → 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).1 (a, b).2 ∧ s (a, b).1 (a, b).2 ⊆ t
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (∃ i ∈ dom, t ∈ l i) ↔ ∃ i, (i.1 ∈ dom ∧ p i.1 i.2) ∧ s i.1 i.2 ⊆ t

Tactic:
Prod.exists

Goal state after:
α : Type u_1
ι : Type u_6
ι' : Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (∃ i ∈ dom, t ∈ l i) ↔ ∃ a b, ((a, b).1 ∈ dom ∧ p (a, b).1 (a, b).2) ∧ s (a, b).1 (a, b).2 ⊆ t
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
inj : Injective m
large : range m ∈ f
S : Set α
⊢ S ∈ comap m f ↔ m '' S ∈ f

Tactic:
← image_mem_map_iff inj,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
inj : Injective m
large : range m ∈ f
S : Set α
⊢ m '' S ∈ map m (comap m f) ↔ m '' S ∈ f
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : 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) ∧ s ∈ map inr (comap m₂ l)

Tactic:
mem_map,

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 ↔ inl ⁻¹' s ∈ comap m₁ l ∧ inr ⁻¹' s ∈ comap m₂ l
Module: Mathlib.Algebra.Group.Action.TransferInstance

Goal state before:
pp: M : Type u_1
N : Type u_2
O : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid M
e : α ≃ β
inst✝ : MulAction M β
⊢ ∀ (x y : M) (b : α), (x * y) • b = x • y • b

Tactic:
by simp [smul_def, mul_smul]

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).FG → ∃ s', ↑s' ⊆ s ∧ span R s = span R ↑s'

Tactic:
intro ⟨s'', hs''⟩

Goal state after:
case mp
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', ↑s' ⊆ s ∧ span R s = span R ↑s'
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
hb : 0 = b
⊢ a₁ < a₂

Tactic:
simp [← hb] at h

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
ha✝ : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
h : a₁ • b₁ = a₂ • b₂
ha : a₁ < a₂
⊢ a₁ • b₁ < a₂ • b₂

Tactic:
exact (smul_le_smul_of_nonneg_left hb h₁.le).trans_lt (smul_lt_smul_of_pos_right ha h₂)

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
hb : b₁ < b₂
⊢ a₁ • b₁ < a₂ • b₂

Tactic:
· exact (smul_le_smul_of_nonneg_right ha h₁.le).trans_lt (smul_lt_smul_of_pos_left hb h₂)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosStrictMono α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₁ • _b < a₂ • _b

Tactic:
by
    rw [← neg_lt_neg_iff, ← smul_neg, ← smul_neg]
    exact smul_lt_smul_of_pos_right (β := β) ha <| neg_pos.2 hb

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : CompleteLattice α
⊢ DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → sSup d ∈ s → (d ∩ s).Nonempty

Tactic:
by
  simp [DirSupInacc, isLUB_iff_sSup_eq]

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst✝ : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
unfold iSup

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst✝ : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
⊢ f (sSup (range fun i ↦ g i)) = sSup (range fun i ↦ f (g i))
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
c : α
hb : f c ∈ s
⊢ (f ⁻¹' s).Nonempty

Tactic:
exact ⟨c, hb⟩

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

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

Tactic:
refine ⟨fun h ↦ (le_add_sub a b).trans (by gcongr), fun h ↦ ?_⟩
  obtain h' | h' := le_or_gt b a
  · rwa [← add_le_add_iff_left b, Ordinal.add_sub_cancel_of_le h']
  · simp [sub_eq_zero_of_lt h']

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

Goal state before:
pp: a b c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a < b + c ↔ ∃ d < c, a ≤ b + d

Tactic:
use fun h ↦ ⟨_, sub_lt_of_lt_add h hc.bot_lt, le_add_sub a b⟩

Goal state after:
case mpr
a b c : Ordinal.{u_4}
hc : c ≠ 0
⊢ (∃ d < c, a ≤ b + d) → a < b + c
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
g : Ordinal.{v} → Ordinal.{max v w}
⊢ BddAbove (g '' range f)

Tactic:
exact bddAbove_image hf g

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
h : iSup f = 0
i : ι
⊢ f i ≤ 0

Tactic:
← h

Goal state after:
ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
h : iSup f = 0
i : ι
⊢ f i ≤ iSup f
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
h : o.bsup f = 0
i : Ordinal.{u_3}
hi : i < o
⊢ f i hi ≤ 0

Tactic:
← h

Goal state after:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
h : o.bsup f = 0
i : Ordinal.{u_3}
hi : i < o
⊢ f i hi ≤ o.bsup f
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_1
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
⊢ ∀ a < lsub f, succ a < lsub f

Tactic:
← h

Goal state after:
case refine_1
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
⊢ ∀ a < iSup f, succ a < iSup f
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ o.blsub f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < a

Tactic:
convert! bsup_le_iff.{_, v} (f := fun a ha => succ (f a ha)) (a := a) using 2

Goal state after:
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
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case a
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
⊢ (o'.bsup fun a ha ↦ f (g a ha) ⋯) ≤ o.bsup f

Tactic:
refine bsup_le fun i hi => ?_

Goal state after:
case a
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
i : Ordinal.{max u v}
hi : i < o'
⊢ f (g i hi) ⋯ ≤ o.bsup f
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case a
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
⊢ o.bsup f ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯

Tactic:
refine bsup_le fun i hi => ?_

Goal state after:
case a
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
i : Ordinal.{max u v}
hi : i < o
⊢ f i hi ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
⊢ b ^ log b 0 ≤ 0 + 1

Tactic:
log_zero_right,

Goal state after:
b : ℕ
⊢ b ^ 0 ≤ 0 + 1
Module: Mathlib.Data.Nat.Log

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

Tactic:
log_zero_right,

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

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

Tactic:
log_zero_right,

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

Goal state before:
pp: case inl
b c : Ordinal.{u_1}
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c

Tactic:
obtain rfl | hc := eq_zero_or_pos c; · simp
    have : b + c ≠ 0 := (hc.trans_le le_add_self).ne'
    rw [zero_opow hc.ne', zero_opow, mul_zero]
    exact (hc.trans_le le_add_self).ne'

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

Goal state before:
pp: case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ sSup ((fun x ↦ 1) ⁻¹' Iic x) = 0

Tactic:
preimage_const

Goal state after:
case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ sSup (if 1 ∈ Iic x then univ else ∅) = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ clog b n = clog b ((n + b - 1) / b) + 1

Tactic:
by
  apply eq_of_forall_ge_iff
  rintro (_ | c)
  · simp [Nat.ne_of_gt <| clog_pos hb hn]
  · simp only [clog_le_iff_le_pow, Nat.pow_add_one, Nat.add_le_add_iff_right, Nat.zero_lt_of_lt hb,
      div_le_iff_le_mul, hb]
    grind

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

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

Tactic:
log_zero_right,

Goal state after:
case inl
b y : Ordinal.{u_1}
xy : 0 ≤ y
⊢ 0 ≤ log b y
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ 0 < 1

Tactic:
exact zero_lt_one

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

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

Tactic:
cases o using inductionOnWellOrder with | type α
  rw [cof_type, ← type_lt_ulift, cof_type, ← Cardinal.lift_id'.{u, v} (Order.cof (ULift _)),
    ← Cardinal.lift_umax, ← ULift.orderIso.lift_cof_congr]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (preBeth o).IsStrongLimit ↔ IsSuccLimit o

Tactic:
rw [isStrongLimit_iff, isSuccLimit_iff, preBeth_eq_zero.ne, isStrongPrelimit_preBeth]

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

Goal state before:
pp: case refine_1
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
⊢ o ≤ 2 ∨ o ∈ Set.range fun x ↦ ω ^ ω ^ x

Tactic:
rcases le_or_gt o 2 with ho₂ | ho₂
    · exact Or.inl ho₂
    · rcases isPrincipal_add_iff_zero_or_omega0_opow.1
        (isPrincipal_add_of_isPrincipal_mul ho ho₂.ne') with (rfl | ⟨a, rfl⟩)
      · exact (not_lt_zero ho₂).elim
      · rcases isPrincipal_add_iff_zero_or_omega0_opow.1
          (isPrincipal_add_of_isPrincipal_mul_opow one_lt_omega0 ho) with (rfl | ⟨b, rfl⟩)
        · simp
        · exact Or.inr ⟨b, rfl⟩

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

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

Tactic:
← h

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

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

Tactic:
← h

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

Goal state before:
pp: β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ #↑(sSup (range ((fun x ↦ A ↑x) ∘ ⇑ToType.mk.symm))) ≤ c

Tactic:
rw [← lift_le.{u}]

Goal state after:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ lift.{u, v} #↑(sSup (range ((fun x ↦ A ↑x) ∘ ⇑ToType.mk.symm))) ≤ lift.{u, v} c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ 2 ^ c ≤ c ^ c

pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ (2 ^ c) ^ c ≤ 2 ^ c

Tactic:
· exact power_le_power_right (natCast_le_aleph0.trans h)

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ (2 ^ c) ^ c ≤ 2 ^ c
Module: Mathlib.SetTheory.Cardinal.Regular

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

Tactic:
apply Ordinal.lift_iSup_lt_of_lt_cof _ hf

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c.ord
⊢ lift.{max u v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof
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) = f i 0

Tactic:
← h

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 (x i)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case mpr.inr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
hi : xi = 0
hj : xj = 0
⊢ single i 0 = single j 0

Tactic:
DFinsupp.single_zero,

Goal state after:
case mpr.inr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
hi : xi = 0
hj : xj = 0
⊢ 0 = single j 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case h.cons
ι : 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
⊢ p { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }

Tactic:
| cons i s ih =>

Goal state after:
case h.cons
ι : 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
⊢ p { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
⊢ (fun f ↦ mapRange (fun i ↦ ⇑(Equiv.cast ⋯)) ⋯ (comapDomain' ⇑h ⋯ f)) (comapDomain' ⇑h.symm ⋯ f) = f

Tactic:
by
    ext i
    rw [mapRange_apply, comapDomain'_apply, comapDomain'_apply, Equiv.cast_eq_iff_heq,
      h.symm_apply_apply]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
i : ι
x : β i
⊢ ∑ i_1 ∈ {i}, (φ i_1) (Pi.single i x i_1) = (φ i) x

Tactic:
Finset.sum_singleton,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
i : ι
x : β i
⊢ (φ i) (Pi.single i x i) = (φ i) x