mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Icc a b) = Icc (c + a) (c + b)

Tactic:
by
  rw [← map_add_left_Icc, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁶ : CommMonoid M
inst✝⁵ : LinearOrder α
inst✝⁴ : LocallyFiniteOrderBot α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
f : α → M
⊢ ∏ i < a + 1, f i = (∏ i < a, f i) * f a

Tactic:
by
  simp_rw [prod_Iio_add_one_comm, mul_comm]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n k : ℕ
⊢ (Iic k).sup (s ∘ id) = s k

Tactic:
← apply_sup_eq_sup_comp_of_nonempty hs nonempty_Iic,

Goal state after:
case refine_2
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n k : ℕ
⊢ s ((Iic k).sup id) = s k
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i < 0

Tactic:
by
  refine lt_of_le_of_ne ?_ ?_
  · rw [toZ_of_lt hi]
    lia
  · by_contra h
    have h_eq := iterate_pred_toZ i hi
    rw [← h_eq, h] at hi
    simp only [neg_zero, Int.toNat_zero, Function.iterate_zero, id, lt_self_iff_false] at hi

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
⊢ univ.sup (disjointed f) = univ.sup f

Tactic:
have hun : univ.biUnion Iic = (univ : Finset ι) := by
    ext r; simpa only [mem_biUnion, mem_univ, mem_Iic, true_and, iff_true] using ⟨r, le_rfl⟩

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
⊢ univ.sup (disjointed f) = univ.sup f
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
hn : ¬IsMax i
⊢ f (succ i) \ (partialSups f) i = f (succ i) \ f i

pp: case hi
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
hn : ¬IsMax i
⊢ ¬IsMax i

Tactic:
hf.partialSups_eq

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
hn : ¬IsMax i
⊢ f (succ i) \ f i = f (succ i) \ f i

case hi
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
hn : ¬IsMax i
⊢ ¬IsMax i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
⊢ (toZ ⊥ (succ^[↑n] ⊥)).toNat ≤ ↑n

Tactic:
Int.toNat_le

Goal state after:
case refine_1
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
⊢ toZ ⊥ (succ^[↑n] ⊥) ≤ ↑↑n
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ k ≤ i
⊢ i + j - k = n - k

Tactic:
hi.1

Goal state after:
case refine_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ k ≤ i
⊢ n - k = n - k
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: case isUnit_or_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
u v : α
ha : a = u * v
huv : ¬IsUnit u ∧ ¬IsUnit v
⊢ False

Tactic:
have hu : span {u} ≤ span {a} :=
      (max.eq_of_le (span_singleton_ne_top huv.1)
        (span_singleton_le_span_singleton.2 ((dvd_mul_right u v).trans ha.symm.dvd))).ge

Goal state after:
case isUnit_or_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
u v : α
ha : a = u * v
huv : ¬IsUnit u ∧ ¬IsUnit v
hu : span {u} ≤ span {a}
⊢ False
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: case isUnit_or_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
v : α
hv : a ∣ v
c : α
ha : a = a * c * v
huv : ¬IsUnit (a * c) ∧ ¬IsUnit v
⊢ False

Tactic:
obtain ⟨d, rfl⟩ := hv

Goal state after:
case isUnit_or_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ False
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: R : Type u_5
inst✝ : CommRing R
x y : R
⊢ y ∈ span {x} ↔ x ∣ y

Tactic:
Ideal.mem_span_singleton

Goal state after:
R : Type u_5
inst✝ : CommRing R
x y : R
⊢ x ∣ y ↔ x ∣ y
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case a
α : Type u_1
B : FilterBasis α
⊢ B.filter ≤ generate B.sets

Tactic:
rw [le_generate_iff]
    apply mem_filter_of_mem

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 α
hl : l.HasBasis p s
⊢ (∀ {i : ι}, p i → (s i).Nonempty) ↔ ¬∃ i, p i ∧ s i = ∅

Tactic:
by simp only [not_exists, not_and, nonempty_iff_ne_empty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
⊢ comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂

Tactic:
sup_eq_iSup,

Goal state after:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
⊢ comap m (⨆ b, bif b then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
⊢ s ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥

Tactic:
refine not_iff_not.1 ((inf_principal_neBot_iff.trans ?_).symm.trans neBot_iff)
  exact
    ⟨fun h hs => by simpa [Set.not_nonempty_empty] using h s hs, fun hs t ht =>
      inter_compl_nonempty_iff.2 fun hts => hs <| mem_of_superset ht hts⟩

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

Goal state before:
pp: α : Type u
f : Filter α
inst✝ : f.NeBot
p : α → Prop
q : Prop
⊢ (∃ᶠ (x : α) in f, p x → q) ↔ (∀ᶠ (x : α) in f, p x) → q

Tactic:
simp only [frequently_imp_distrib, frequently_const]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ (map Prod.mk f).seq g = (map (fun b a ↦ (a, b)) g).seq f

Tactic:
by
  refine le_antisymm (le_seq fun s hs t ht => ?_) (le_seq fun s hs t ht => ?_)
  · rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩
    grw [← hs]
    rw [← Set.prod_image_seq_comm]
    exact seq_mem_seq (image_mem_map ht) hu
  · rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩
    grw [← hs]
    rw [Set.prod_image_seq_comm]
    exact seq_mem_seq (image_mem_map ht) hu

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 : ℕ → ℕ
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))

Tactic:
exact ⟨ns, h_tendsto.comp (tendsto_atTop_mono hge tendsto_id), hns⟩

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ cof α ≠ 1 ↔ NoTopOrder α

Tactic:
rw [← not_iff_not, not_not, noTopOrder_iff, cof_eq_one_iff]

Goal state after:
α : Type u
inst✝ : Preorder α
⊢ (∃ x, IsTop x) ↔ ¬∀ (x : α), ¬IsTop x
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ ⊤.FG ↔ N.FG

Tactic:
← fg_map_iff N.subtype Subtype.val_injective,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (map N.subtype ⊤).FG ↔ N.FG
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✝ : SMulPosMono α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ a₁ • _b ≤ a₂ • _b

Tactic:
by
    rw [← neg_le_neg_iff, ← smul_neg, ← smul_neg]
    exact smul_le_smul_of_nonneg_right (β := β) ha <| neg_nonneg.2 hb

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : LinearOrder α
⊢ DirSupInaccOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty

Tactic:
simp [DirSupInaccOn]

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝² : IsWellOrder α r
inst✝¹ : Nonempty α
inst✝ : Subsingleton α
⊢ type r = 1

Tactic:
cases nonempty_unique α
  exact (RelIso.ofUniqueOfIrrefl r _).ordinalType_congr

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
⊢ typeLT ↑s ≤ typeLT α

Tactic:
by
  rw [type_le_iff']
  refine ⟨⟨Embedding.subtype _, ?_⟩⟩
  simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
i : ι
⊢ bfamilyOfFamily' r f ((typein r).toRelEmbedding i) ⋯ = f i

Tactic:
by
  simp only [bfamilyOfFamily', enum_typein]

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

Goal state before:
pp: a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
⊢ IsSuccLimit (a - b)

Tactic:
isSuccLimit_iff,

Goal state after:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
⊢ a - b ≠ 0 ∧ IsSuccPrelimit (a - b)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
a : Ordinal.{u_4}
⊢ (n + 1) • a = a * ↑(n + 1)

Tactic:
rw [succ_nsmul, nsmul_eq_mul, Nat.cast_add_one, mul_add_one]

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

Goal state before:
pp: ⊢ IsSuccLimit ω

Tactic:
isSuccLimit_iff,

Goal state after:
⊢ ω ≠ 0 ∧ IsSuccPrelimit ω
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ IsSuccLimit a ↔ a ≠ 0 ∧ ω ∣ a

Tactic:
isSuccLimit_iff,

Goal state after:
a : Ordinal.{u_4}
⊢ a ≠ 0 ∧ IsSuccPrelimit a ↔ a ≠ 0 ∧ ω ∣ a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b c : Ordinal.{u_1}
hb : 1 < b
h : b = 0 ∧ c ≠ 0
⊢ c ≤ log b 0

Tactic:
exact (zero_lt_one.asymm <| h.1 ▸ hb).elim

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

Goal state before:
pp: case mpr.inl
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hab : a ≤ b
⊢ op a b < o

Tactic:
exact (h₂ b hab).trans_lt <| H b hb

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

Goal state before:
pp: o : Ordinal.{u}
ho₁ : 1 < o
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
⊢ IsSuccLimit o

Tactic:
isSuccLimit_iff,

Goal state after:
o : Ordinal.{u}
ho₁ : 1 < o
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
⊢ o ≠ 0 ∧ IsSuccPrelimit o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b c : Ordinal.{u}
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
hab : a < b
hbc : b ≤ c
⊢ a + c = c

Tactic:
← Ordinal.add_sub_cancel_of_le hbc,

Goal state after:
a b c : Ordinal.{u}
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
hab : a < b
hbc : b ≤ c
⊢ a + (b + (c - b)) = b + (c - b)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: n : ℕ
⊢ preAleph.symm ↑n = ↑n

Tactic:
by
  simp [OrderIso.symm_apply_eq]

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

Goal state before:
pp: ⊢ preAleph.symm ℵ₀ = ω

Tactic:
by
  simp [OrderIso.symm_apply_eq]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ_ 0 < ℵ_ o ↔ 0 < o

Tactic:
aleph_lt_aleph

Goal state after:
o : Ordinal.{u_1}
⊢ 0 < o ↔ 0 < o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof = 0 ∨ o.cof = 1 ↔ ¬IsSuccLimit o

Tactic:
isSuccLimit_iff,

Goal state after:
o : Ordinal.{u_1}
⊢ o.cof = 0 ∨ o.cof = 1 ↔ ¬(o ≠ 0 ∧ IsSuccPrelimit o)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ preBeth o ≠ 0 ∧ (preBeth o).IsStrongPrelimit ↔ IsSuccLimit o

Tactic:
isSuccLimit_iff,

Goal state after:
o : Ordinal.{u_1}
⊢ preBeth o ≠ 0 ∧ (preBeth o).IsStrongPrelimit ↔ o ≠ 0 ∧ IsSuccPrelimit o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1.inr
n m : ℕ
h : n + m = n
⊢ m = 0

Tactic:
rw [← add_right_inj, h, add_zero]

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

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

Tactic:
range_comp',

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

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

Tactic:
have hc : c < ℵ₀ := by
      rw [← not_le]
      intro hc
      apply lt_irrefl ℵ₀
      apply (hc.trans (self_le_add_left _ a)).trans_lt
      rw [← h]
      apply add_lt_aleph0 ha hb

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
⊢ a ≤ (g o).cof.ord

Tactic:
rw [cof_map_of_isNormal hg ho, hf.ord_cof]

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

Goal state before:
pp: o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : typeLT ↑s = o.cof.ord
g : ↑(Iio o.cof.ord) ≃o ↑s :=
  (OrderIso.setCongr (Iio o.cof.ord) (Iio (typeLT ↑s)) ⋯).trans (OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2))
⊢ IsCofinal (range fun i ↦ (↑(g i)).toOrd)

Tactic:
range_comp',

Goal state after:
o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : typeLT ↑s = o.cof.ord
g : ↑(Iio o.cof.ord) ≃o ↑s :=
  (OrderIso.setCongr (Iio o.cof.ord) (Iio (typeLT ↑s)) ⋯).trans (OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2))
⊢ IsCofinal (ToType.toOrd '' range fun i ↦ ↑(g i))
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : typeLT ↑s = o.cof.ord
g : ↑(Iio o.cof.ord) ≃o ↑s :=
  (OrderIso.setCongr (Iio o.cof.ord) (Iio (typeLT ↑s)) ⋯).trans (OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2))
⊢ IsCofinal (range fun i ↦ ↑(g i))

Tactic:
range_comp',

Goal state after:
o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : typeLT ↑s = o.cof.ord
g : ↑(Iio o.cof.ord) ≃o ↑s :=
  (OrderIso.setCongr (Iio o.cof.ord) (Iio (typeLT ↑s)) ⋯).trans (OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2))
⊢ IsCofinal (Subtype.val '' range ⇑g)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ a ≤ a ^ b

Tactic:
exact left_le_opow a (omega0_pos.trans_le hb)

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < ℵ_ o
hb : b.card < ℵ_ o
⊢ ℵ_ 0 < ℵ_ o

Tactic:
aleph_lt_aleph

Goal state after:
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < ℵ_ o
hb : b.card < ℵ_ o
⊢ 0 < o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ lift.{u, max u v} (prod c) = 2 ^ lift.{v, u} #ι

Tactic:
lift_prod,

Goal state after:
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ (prod fun i ↦ lift.{u, v} (c i)) = 2 ^ lift.{v, u} #ι
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ ((fun x1 x2 ↦ x1 * x2) a b).card < c

Tactic:
card_mul

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

Goal state before:
pp: case neg
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : ¬IsMin o
⊢ (preOmega o).cof = o.cof

Tactic:
· exact cof_map_of_isNormal isNormal_preOmega ⟨h, ho⟩

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

Goal state before:
pp: case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #↑Set.univ ≤ #↑(⋃ i, Iio ↑i)

Tactic:
← isCofinal_iff_iUnion_Iio_eq_univ.1 hs,

Goal state after:
case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #↑(⋃ i ∈ s, Iio i) ≤ #↑(⋃ i, Iio ↑i)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case neg
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) = Sum.inl x
h' : ¬∃ z, g z = y
⊢ x ∈ ↑⟨s, ⋯⟩

Tactic:
· rw [dif_neg h'] at h
      cases h

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

Goal state before:
pp: ⊢ preAleph.symm univ.{u, v} = Ordinal.univ.{u, v}

Tactic:
by
  simp [OrderIso.symm_apply_eq]

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

Goal state before:
pp: case mpr.inl
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi xj : β i
hxi : xi ≍ xj
⊢ single i xi = single i xj

Tactic:
rw [eq_of_heq hxi]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
⊢ (single i✝ (c • x)) i = (c • single i✝ x) i

Tactic:
simp only [smul_apply, single_apply]
    split_ifs with h
    · cases h; rfl
    · rw [smul_zero]

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (mk s (-x)) i = (-mk s x) i

Tactic:
simp only [neg_apply, mk_apply]; split_ifs <;> [rfl; rw [neg_zero]]

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

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

Tactic:
rintro ⟨sx, hx⟩ ⟨sy, hy⟩

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
⊢ {i ∈ (↑⟨sx, hx⟩).toFinset | f i ≠ 0} = {i ∈ (↑⟨sy, hy⟩).toFinset | f i ≠ 0}
Module: Mathlib.Data.Fintype.Quotient

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

Tactic:
intro as

Goal state after:
case a
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
C : ((i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)) → Prop
f : ∀ (a : (i_1 : ι) → i_1 ∈ i :: l → α i_1), C fun x1 x2 ↦ ⟦a x1 x2⟧
q : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a : α i
as : (i : ι) → i ∈ l → α i
⊢ C (List.Pi.cons i l ⟦a⟧ fun x1 x2 ↦ ⟦as x1 x2⟧)
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
⊢ ∀ (a b : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }),
    ∑ i ∈ (↑a).toFinset, (φ i) (f i) = ∑ i ∈ (↑b).toFinset, (φ i) (f i)

Tactic:
rintro ⟨sx, hx⟩ ⟨sy, hy⟩

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
⊢ ∑ i ∈ (↑⟨sx, hx⟩).toFinset, (φ i) (f i) = ∑ i ∈ (↑⟨sy, hy⟩).toFinset, (φ i) (f i)
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_6
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f g : M →ₗ[R] M'
h : Injective ⇑(Dual.eval R M')
⊢ f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g

Tactic:
simp only [← Dual.eval_comp_comp_evalEquiv_eq]
  refine ⟨fun hfg => ?_, fun a ↦ congrArg (Dual.eval R M').comp
    (congrFun (congrArg LinearMap.comp a) (evalEquiv R M).symm.toLinearMap)⟩
  rw [propext (cancel_left h), LinearEquiv.eq_comp_toLinearMap_iff] at hfg
  exact hfg

Goal state after: