mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
⊢ (fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i

Tactic:
by
    rcases le_or_gt hι.some i with hi | hi
    · have h_nonneg : 0 ≤ toZ hι.some i := toZ_nonneg hi
      simp_rw [if_pos h_nonneg]
      exact iterate_succ_toZ i hi
    · have h_neg : toZ hι.some i < 0 := toZ_neg hi
      simp_rw [if_neg (not_le.mpr h_neg)]
      exact iterate_pred_toZ i hi

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
hf' : f = f' ∘ ⇑R
⊢ disjointed f' ∘ ⇑R ≤ f

Tactic:
intro n

Goal state after:
case inr.refine_1
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
hf' : f = f' ∘ ⇑R
n : ι
⊢ (disjointed f' ∘ ⇑R) n ≤ f n
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
⊢ ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ

Tactic:
intro n

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n : ℕ
⊢ ∀ i ∈ range n.succ, t n.succ i.succ = x * t n i + y * t n i.succ
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
x : α
⊢ span {x} = ⊤ ↔ x ∣ 1

Tactic:
← span_singleton_le_span_singleton,

Goal state after:
α : Type u
inst✝ : CommSemiring α
x : α
⊢ span {x} = ⊤ ↔ span {1} ≤ span {x}
Module: Mathlib.Algebra.Order.SuccPred.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁶ : SemilatticeSup α
inst✝⁵ : LinearOrder ι
inst✝⁴ : Add ι
inst✝³ : One ι
inst✝² : OrderBot ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
⊢ (partialSups f) (i + 1) = f ⊥ ⊔ (partialSups (f ∘ fun k ↦ k + 1)) i

Tactic:
by
  simpa [← Order.succ_eq_add_one] using partialSups_succ' f i

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ 0 • ⋯.choose = 0

Tactic:
rw [zero_smul]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ l = generate {U | ∃ i, p i ∧ s i = U}

Tactic:
rw [← h.isBasis.filter_eq_generate, h.filter_eq]

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

Goal state before:
pp: α : Type u
p q : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
hq : ∀ᶠ (x : α) in f, q x
⊢ ∃ᶠ (x : α) in f, p x ∧ q x

Tactic:
by
  refine mt (fun h => hq.mp <| h.mono ?_) hp
  exact fun x hpq hq hp => hpq ⟨hp, hq⟩

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

Goal state before:
pp: case h.left
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∀ (n : ℕ), (Nat.recOn n (u 0 0) fun n v ↦ u (n + 1) v) < Nat.recOn (n + 1) (u 0 0) fun n v ↦ u (n + 1) v

Tactic:
intro n

Goal state after:
case h.left
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n : ℕ
⊢ (Nat.recOn n (u 0 0) fun n v ↦ u (n + 1) v) < Nat.recOn (n + 1) (u 0 0) fun n v ↦ u (n + 1) v
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case h.right
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∀ (n : ℕ), P n (Nat.recOn n (u 0 0) fun n v ↦ u (n + 1) v)

Tactic:
intro n

Goal state after:
case h.right
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n : ℕ
⊢ P n (Nat.recOn n (u 0 0) fun n v ↦ u (n + 1) v)
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : Directed (fun x1 x2 ↦ x1 ≤ x2) Subtype.val
⊢ IsDirectedOrder ↑s

Tactic:
rwa [IsDirectedOrder, ← directed_id_iff]

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

Goal state before:
pp: A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
R : Type u_7
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
hS : (restrictScalars R S).FG
⊢ S.FG

Tactic:
by
  obtain ⟨s, e⟩ := hS
  refine ⟨s, restrictScalars_injective R _ _ (le_antisymm ?_ ?_)⟩
  · have := span_le.mp e.le
    rwa [restrictScalars_le, span_le]
  · rw [← e]
    exact span_le_restrictScalars ..

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupInaccOn D (s ∪ t)

Tactic:
rw [← dirSupClosedOn_compl, compl_union]; exact hs.compl.inter ht.compl

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

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

Tactic:
simpa only [smul_zero] using smul_lt_smul_iff_of_neg_left ha (b₁ := (0 : β))

Goal state after:
Module: Mathlib.Order.IsNormal

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

Tactic:
refine ⟨?_, fun b hb ↦ ?_⟩
  · simpa [mem_upperBounds, hf.strictMono.le_iff_le] using hs.1
  · 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.SetTheory.Ordinal.Univ

Goal state before:
pp: o✝ : Ordinal.{max (u + 1) v}
h : o✝ < Ordinal.univ.{u, v}
o : Ordinal.{u}
h' : Ordinal.liftPrincipalSeg.toRelEmbedding o = o✝
⊢ o✝.card < univ.{u, v}

Tactic:
rw [← h', Ordinal.liftPrincipalSeg_coe, ← Ordinal.lift_card]

Goal state after:
o✝ : Ordinal.{max (u + 1) v}
h : o✝ < Ordinal.univ.{u, v}
o : Ordinal.{u}
h' : Ordinal.liftPrincipalSeg.toRelEmbedding o = o✝
⊢ lift.{max (u + 1) v, u} o.card < univ.{u, v}
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:
by
  refine inductionOn o ?_; rintro γ t wo ⟨g⟩ ⟨h⟩
  rw [enum_type g, enum_type (g.transRelIso f)]; rfl

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

Goal state before:
pp: case mpr
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a < b + d
⊢ ∃ d < c, a ≤ b + d

Tactic:
· exact ⟨d, hd, ha.le⟩

Goal state after:
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 (range (g ∘ f))

Tactic:
rw [range_comp]

Goal state after:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
g : Ordinal.{v} → Ordinal.{max v w}
⊢ BddAbove (g '' range f)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case type
α : Type u_4
r✝ : α → α → Prop
inst✝¹ : IsWellOrder α r✝
β : Type u_4
s✝ : β → β → Prop
inst✝ : IsWellOrder β s✝
⊢ type r✝ * type s✝ = 0 ↔ type r✝ = 0 ∨ type s✝ = 0

Tactic:
| _ α _ β _
   => 

Goal state after:
case type
α : Type u_4
r✝ : α → α → Prop
inst✝¹ : IsWellOrder α r✝
β : Type u_4
s✝ : β → β → Prop
inst✝ : IsWellOrder β s✝
⊢ type r✝ * type s✝ = 0 ↔ type r✝ = 0 ∨ type s✝ = 0
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ :
  isEquivalent
    { α := ULift.{max v w, u} { α := α, r := r, wo := inst✝¹ }.α,
      r := ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r, wo := ⋯ }
    { α := ULift.{max u w, v} { α := β, r := s, wo := inst✝ }.α, r := ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r,
      wo := ⋯ }
f : ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≃r ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
⊢ r ≃r s

pp: case refine_2
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≃r s)
f : r ≃r s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≃r ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r

Tactic:
· exact (RelIso.preimage Equiv.ulift r).symm.trans <| f.trans (RelIso.preimage Equiv.ulift s)

Goal state after:
case refine_2
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≃r s)
f : r ≃r s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≃r ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: s : Set Ordinal.{u_3}
⊢ BddAbove ((fun x ↦ x + 1) '' s) ↔ BddAbove s

Tactic:
constructor <;> rintro ⟨a, ha⟩

Goal state after:
case mp
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : a ∈ upperBounds ((fun x ↦ x + 1) '' s)
⊢ BddAbove s

case mpr
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : a ∈ upperBounds s
⊢ BddAbove ((fun x ↦ x + 1) '' s)
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 ≤ a + b

Tactic:
by simpa using add_le_add_right bot_le a

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ typeLT α ∈ range succ ↔ ∃ x, IsMax x

Tactic:
← isTop_iff_isMax

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ typeLT α ∈ range succ ↔ ∃ x, IsTop x
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}
⊢ o.bsup f = 0 ↔ ∀ (i : Ordinal.{u_3}) (hi : i < o), f i hi = 0

Tactic:
refine
    ⟨fun h i hi => ?_, fun h =>
      le_antisymm (bsup_le fun i hi => nonpos_iff_eq_zero.2 (h i hi)) zero_le⟩
  rw [← nonpos_iff_eq_zero, ← h]
  exact le_bsup f i hi

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

Goal state before:
pp: α : Type u_1
β : Type u_2
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
a : Ordinal.{max u v}
ha : a < o'
⊢ g a ha < o

Tactic:
← hg

Goal state after:
α : Type u_1
β : Type u_2
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
a : Ordinal.{max u v}
ha : a < o'
⊢ g a ha < o'.blsub g
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
⊢ x ≤ log b y

Tactic:
rcases ne_or_eq y 0 with (hy | rfl)

Goal state after:
case inl
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
hy : y ≠ 0
⊢ x ≤ log b y

case inr
b x : ℕ
hb : 1 < b
h : b ^ x ≤ 0
⊢ x ≤ log b 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
⊢ x ≤ log b y

Tactic:
by
  rcases ne_or_eq y 0 with (hy | rfl)
  exacts [(le_log_iff_pow_le hb hy).2 h, (h.not_gt (Nat.pow_pos (Nat.zero_lt_one.trans hb))).elim]

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : IsSuccLimit a
⊢ IsSuccLimit (a + b) ↔ IsSuccPrelimit b

Tactic:
by
  rw [isSuccLimit_add_iff]
  obtain rfl | hb := eq_or_ne b 0
  · simpa
  · simp [hb, isSuccLimit_iff]

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

Goal state before:
pp: a b : Ordinal.{u_4}
h₁ : a ∣ b
h₂ : b ∣ a
a0 : ¬a = 0
b0 : b = 0
⊢ a = b

Tactic:
subst b; exact eq_zero_of_zero_dvd h₂

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
⊢ (∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o) ↔
    ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o

Tactic:
constructor <;> intro H o ho

Goal state after:
case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
⊢ (o.blsub fun x x_1 ↦ f x) = f o

case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
⊢ (o.bsup fun x x_1 ↦ f x) = f o
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ log b n ≤ log c n

Tactic:
apply le_log_of_pow_le hc

Goal state after:
case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ c ^ log b n ≤ n
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b n : ℕ
hb : 1 < b
⊢ log b (n / b) = log b n - 1

Tactic:
rcases lt_or_ge n b with h | h

Goal state after:
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b) = log b n - 1

case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b) = log b n - 1
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b n : ℕ
hb : 1 < b
⊢ log b (n / b * b) = log b n

Tactic:
rcases lt_or_ge n b with h | h

Goal state after:
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b * b) = log b n

case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b * b) = log b n
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
⊢ a ^ 1 ≤ a ^ b

Tactic:
rcases lt_or_eq_of_le a1 with a0 | a1
    · rw [lt_one_iff] at a0
      rw [a0, zero_opow one_ne_zero]
      exact zero_le
    rw [a1, one_opow, one_opow]

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 + 1)) = (a ^ b) ^ (c + 1)

Tactic:
rw [mul_add_one, opow_add, IH, opow_add_one]

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

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ NoMaxOrder c.ord.ToType

Tactic:
← isSuccPrelimit_type_lt_iff,

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ IsSuccPrelimit (typeLT c.ord.ToType)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case right.refine_1
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ∀ (a : Ordinal.{u}), derivFamily f a ∈ ⋂ i, fixedPoints (f i)

Tactic:
rintro a S ⟨i, hi⟩
    rw [← hi]
    exact derivFamily_fp (H i) a

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

Goal state before:
pp: case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ∀ (i : ℕ), f^[i] a ≤ nfp f a

Tactic:
intro n

Goal state after:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ f^[n] a ≤ nfp f a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
⊢ ∀ (i : ℕ), 0^[i] a ≤ 0^[0] a

Tactic:
intro n

Goal state after:
a : Ordinal.{u_1}
n : ℕ
⊢ 0^[n] a ≤ 0^[0] a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ NoMaxOrder α

Tactic:
← isSuccPrelimit_type_lt_iff,

Goal state after:
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ IsSuccPrelimit (typeLT α)
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
rw [← aleph_zero, succ_aleph, zero_add]

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

Goal state before:
pp: a : Ordinal.{u}
a0 : 0 < a
ha : a < ω
b : Ordinal.{u}
⊢ a * (ω * b) = ω * b

Tactic:
by rw [← mul_assoc, mul_omega0 a0 ha]

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

Goal state before:
pp: a b o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : ↑(Iio b) → ↑(Iio a)
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ IsCofinal (range (f ∘ g))

Tactic:
rw [range_comp]

Goal state after:
a b o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : ↑(Iio b) → ↑(Iio a)
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ IsCofinal (f '' range g)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x✝¹ x✝ : Cardinal.{u_1}
hlt : x✝¹ < x✝
⊢ (fun a ↦ a * ↑n) x✝¹ < (fun a ↦ a * ↑n) x✝

Tactic:
simpa [mul_comm] using natCast_mul_strictMono hn hlt

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

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := ⋯
⊢ #{ s // #↑s < (#α).ord.cof } ≤ #α

Tactic:
conv_rhs => rw [← mk_bounded_subset h hr]
    apply mk_subtype_le_of_subset
    intro s hs
    rw [hr] at hs
    contrapose! hs
    rw [not_bounded_iff] at hs
    apply cof_le
    simp_rw [IsCofinal, ← not_lt]
    exact hs

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
⊢ #(Perm α) = 2 ^ #α

Tactic:
by
  rw [mk_perm_eq_self_power, power_self_eq (aleph0_le_mk α)]

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

Goal state before:
pp: α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ NoMaxOrder α

Tactic:
← isSuccPrelimit_type_lt_iff,

Goal state after:
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ IsSuccPrelimit (typeLT α)
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
h : ∃ a, ∀ (x : κ), (b.repr (v x)) a = 0
⊢ False

Tactic:
obtain ⟨i, w⟩ := h

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
⊢ False
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ (ω ^ 2).card < c

Tactic:
pow_two,

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ (ω * ω).card < c
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : xi = 0
hcj : (single i xi) j = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
DFinsupp.single_eq_of_ne (Ne.symm hij)

Goal state after:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : xi = 0
hcj : 0 = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
fs : (i : ↥(↑s).toFinset) → { s_1 // ∀ (i_1 : α ↑i), i_1 ∈ s_1 ∨ (f ↑i).toFun i_1 = 0 }
⊢ ∀ (i : (x : ι) × α x),
    (i ∈ (↑s).toFinset.attach.val.bind fun i ↦ Multiset.map (Sigma.mk ↑i) ↑(fs i)) ∨ (f i.fst) i.snd = 0

Tactic:
rintro ⟨i, a⟩
          cases s.prop i with
          | inl hi =>
            cases (fs ⟨i, Multiset.mem_toFinset.mpr hi⟩).prop a with
            | inl ha =>
              left; rw [Multiset.mem_bind]
              use ⟨i, Multiset.mem_toFinset.mpr hi⟩
              constructor
              case right => simp [ha]
              case left => apply Multiset.mem_attach
            | inr ha => right; simp [toFun_eq_coe (f i) ▸ ha]
          | inr hi => right; simp [toFun_eq_coe f ▸ hi]

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝⁵ : DecidableEq ι
ι₁ : Type u₁
inst✝⁴ : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst✝³ : (i₁ : ι₁) → Zero (β₁ i₁)
inst✝² : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
this : ∀ (i₁ : ι), (f.sum fun i b ↦ (g i b) i₁) ≠ 0 → ∃ i, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0
⊢ (f.sum g).support ⊆ f.support.biUnion fun i ↦ (g i (f i)).support

Tactic:
simpa [Finset.subset_iff, mem_support_iff, Finset.mem_biUnion, sum_apply] using this

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

Goal state before:
pp: case refine_2.mk.refine_1
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
y : (i : ι) → β₁ i
hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)
i : ι
⊢ i ∈ s ∨ y i = 0

pp: case refine_2.mk.refine_2
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
y : (i : ι) → β₁ i
hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)
i : ι
⊢ (mapRange f hf { toFun := y, support' := Trunc.mk ⟨s, ⋯⟩ }) i =
    { toFun := x, support' := Quot.mk ⇑trueSetoid ⟨s, hs⟩ } i

Tactic:
· exact (hs i).imp_right (hy i).2

Goal state after:
case refine_2.mk.refine_2
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
y : (i : ι) → β₁ i
hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)
i : ι
⊢ (mapRange f hf { toFun := y, support' := Trunc.mk ⟨s, ⋯⟩ }) i =
    { toFun := x, support' := Quot.mk ⇑trueSetoid ⟨s, hs⟩ } i
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
⊢ (sumZeroHom φ) (single i x) = (φ i) x

Tactic:
dsimp [sumZeroHom, single, Trunc.lift_mk]
  rw [Multiset.toFinset_singleton, Finset.sum_singleton, Pi.single_eq_same]

Goal state after: