mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
F : Filter α
⊢ map ψ (map φ F) = map ρ (map θ F)

Tactic:
rw [Filter.map_map, H, ← Filter.map_map]

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
s t✝ : Set α
hqs : q s
hqt : q t✝
x✝ y✝ : Set α
ha : x✝ ∈ {s | ∀ (t : Set α), q t → q (s ∩ t)}
hb : y✝ ∈ {s | ∀ (t : Set α), q t → q (s ∩ t)}
t : Set α
ht : q t
⊢ q (x✝ ∩ y✝ ∩ t)

Tactic:
by simpa [inter_assoc] using ha _ (hb _ ht)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ s ∈ kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ

Tactic:
rw [mem_kernMap, compl_surjective.exists]

Goal state after:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ (∃ x, xᶜ ∈ f ∧ kernImage m xᶜ = s) ↔ ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ t ∈ l ⊔ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∪ s' i.snd ⊆ t

Tactic:
simp_rw [mem_sup, hl.mem_iff, hl'.mem_iff, PProd.exists, union_subset_iff,
       ← exists_and_right, ← exists_and_left]

Goal state after:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ (∃ x x_1, (p x ∧ s x ⊆ t) ∧ p' x_1 ∧ s' x_1 ⊆ t) ↔ ∃ a b, (p a ∧ p' b) ∧ s a ⊆ t ∧ s' b ⊆ t
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : Directed (fun x1 x2 ↦ x1 ⊇ x2) (s ∘ Subtype.val)
ne : S.Nonempty
t : Set α
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) ((fun i ↦ 𝓟 (s i)) ∘ Subtype.val)

Tactic:
refine h.mono_comp _ ?_

Goal state after:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : Directed (fun x1 x2 ↦ x1 ⊇ x2) (s ∘ Subtype.val)
ne : S.Nonempty
t : Set α
⊢ ∀ ⦃x y : Set α⦄, x ⊇ y → 𝓟 x ≥ 𝓟 y
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
h : f = ⊥
⊢ map m f = ⊥

Tactic:
simp only [h, map_bot]

Goal state after:
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : s.Finite
⊢ ∃ a, ∀ b ∈ s, f a ≤ f b

Tactic:
by
  rcases s.eq_empty_or_nonempty with rfl | hs
  · exact ‹Nonempty α›.elim fun a => ⟨a, fun _ => False.elim⟩
  · rcases Set.exists_min_image s f h hs with ⟨x₀, _, hx₀⟩
    exact ⟨x₀, fun x hx => hx₀ x hx⟩

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), (t i).Finite
hts : ∀ (i : ι), span R (t i) = p i
⊢ ⨆ i, map (LinearMap.single R M i) (p i) = pi univ p

Tactic:
iSup_map_single

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
A : Type u_3
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
S : Submodule A M
inst✝ : Module.Finite R A
hS : S.FG
⊢ (Submodule.restrictScalars R S).FG

Tactic:
← Module.Finite.iff_fg

Goal state after:
R : Type u_1
inst✝⁷ : Semiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
A : Type u_3
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
S : Submodule A M
inst✝ : Module.Finite R A
hS : Module.Finite A ↥S
⊢ Module.Finite R ↥(Submodule.restrictScalars R S)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : PartialOrder α
inst✝² : (i : ι) → PartialOrder (β i)
inst✝¹ : (i : ι) → SMulWithZero α (β i)
inst✝ : ∀ (i : ι), SMulPosStrictMono α (β i)
⊢ ∀ ⦃b : (i : ι) → β i⦄,
    (0 ≤ b ∧ ∃ i, 0 i < b i) → ∀ ⦃a₁ a₂ : α⦄, a₁ < a₂ → a₁ • b ≤ a₂ • b ∧ ∃ i, (a₁ • b) i < (a₂ • b) i

Tactic:
rintro a ⟨ha, i, hi⟩ _b₁ _b₂ hb

Goal state after:
α : Type u_1
β✝ : Type u_2
a✝ a₁ a₂ : α
b b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : PartialOrder α
inst✝² : (i : ι) → PartialOrder (β i)
inst✝¹ : (i : ι) → SMulWithZero α (β i)
inst✝ : ∀ (i : ι), SMulPosStrictMono α (β i)
a : (i : ι) → β i
ha : 0 ≤ a
i : ι
hi : 0 i < a i
_b₁ _b₂ : α
hb : _b₁ < _b₂
⊢ _b₁ • a ≤ _b₂ • a ∧ ∃ i, (_b₁ • a) i < (_b₂ • a) i
Module: Mathlib.Order.DirSupClosed

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

Tactic:
by
  simp [DirSupClosed, isLUB_iff_sSup_eq]

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case isSuccLimit
α : Type u_1
β : Type u_2
f : α → β
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : SuccOrder α
inst✝ : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
hb : IsSuccLimit b
IH : ∀ b_1 < b, a < b_1 → f a < f b_1
hab : a < b
⊢ f a < f b

Tactic:
have hab' := hb.succ_lt hab

Goal state after:
case isSuccLimit
α : Type u_1
β : Type u_2
f : α → β
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : SuccOrder α
inst✝ : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
hb : IsSuccLimit b
IH : ∀ b_1 < b, a < b_1 → f a < f b_1
hab : a < b
hab' : succ a < b
⊢ f a < f b
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
a : Ordinal.{u}
e : liftInitialSeg.toRelEmbedding a = type s
α : Type u
⊢ ∀ (r : α → α → Prop) [inst : IsWellOrder α r],
    liftInitialSeg.toRelEmbedding (type r) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

Tactic:
r

Goal state after:
case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
a : Ordinal.{u}
e : liftInitialSeg.toRelEmbedding a = type s
α : Type u
r : α → α → Prop
⊢ ∀ [inst : IsWellOrder α r], liftInitialSeg.toRelEmbedding (type r) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ cof α ≤ #α

Tactic:
exact cof_le_cardinalMk α

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h0 : 0 < type r
a : α
⊢ ¬r ((enum r) ⟨(typein r).toRelEmbedding a, ⋯⟩) ((enum r) ⟨0, h0⟩)

Tactic:
enum_le_enum r

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h0 : 0 < type r
a : α
⊢ ⟨0, h0⟩ ≤ ⟨(typein r).toRelEmbedding a, ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
isSuccPrelimit_iff_succ_lt

Goal state after:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
⊢ b < a ∧ ∀ a_1 < a - b, succ a_1 < a - b
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case inr
α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
i : β
⊢ f (Sum.inr i) ≤ max (⨆ a, f (Sum.inl a)) (⨆ b, f (Sum.inr b))

Tactic:
exact le_max_of_le_right (Ordinal.le_iSup (fun x ↦ f (Sum.inr x)) i)

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

Goal state before:
pp: case pos
s : Set Ordinal.{u_3}
hs : BddAbove s
hs' : BddAbove ((fun x ↦ x + 1) '' s)
⊢ sSup s ≤ sSup ((fun x ↦ x + 1) '' s)

Tactic:
rw [csSup_le_iff' hs]

Goal state after:
case pos
s : Set Ordinal.{u_3}
hs : BddAbove s
hs' : BddAbove ((fun x ↦ x + 1) '' s)
⊢ ∀ x ∈ s, x ≤ sSup ((fun x ↦ x + 1) '' s)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
lt_add_iff hb

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

Goal state before:
pp: o : Ordinal.{u}
ho : ∀ a < o, succ a < o
⊢ IsSuccPrelimit o

Tactic:
isSuccPrelimit_iff_succ_lt

Goal state after:
o : Ordinal.{u}
ho : ∀ a < o, succ a < o
⊢ ∀ a < o, succ a < o
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
i : c.ord.ToType
⊢ #↑(Iio i) < c

Tactic:
simpa using mk_Iio_lt i

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

Goal state before:
pp: c : Cardinal.{u_1}
h : c ≠ 0
⊢ Nonempty c.ord.ToType

Tactic:
rwa [Ordinal.nonempty_toType_iff, ne_eq, ord_eq_zero]

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

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ ↑n ≤ o.card ↔ ↑n ≤ o

Tactic:
rw [← Cardinal.ord_le, Cardinal.ord_natCast]

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ (#↑s).ord < (#α).ord

Tactic:
ord_lt_ord,

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ #↑s < #α
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ #↑s < #α

Tactic:
← mk_univ (α := α)

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ #↑s < #↑univ
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case limit
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
⊢ (∀ b' < b, 1 ^ b' ≤ c) ↔ 1 ≤ c

Tactic:
exact ⟨fun H => by simpa only [opow_zero] using H 0 l.bot_lt, fun H b' h => by rwa [IH _ h]⟩

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

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

Tactic:
contrapose! +distrib
    rw [le_one_iff]
    rintro ((rfl | rfl) | rfl)
    · exact zero_opow_le b
    · simp
    · simp

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

Goal state before:
pp: case neg.limit
a b : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ o' ≤ b ^ o'
⊢ a ^ c ≤ b ^ c

Tactic:
exact (opow_le_of_isSuccLimit ha l).2 fun b' h ↦
        (IH _ h).trans (opow_le_opow_right ((pos_iff_ne_zero.2 ha).trans_le ab) h.le)

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

Goal state before:
pp: ⊢ ω ≠ 0 ∧ IsSuccPrelimit ω

Tactic:
isSuccPrelimit_iff_succ_lt

Goal state after:
⊢ ω ≠ 0 ∧ ∀ a < ω, succ a < ω
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a

Tactic:
refine ⟨fun h ↦ ?_, apply_lt_nfpFamily H⟩
  let ⟨l, hl⟩ := lt_nfpFamily_iff.1 (h (Classical.arbitrary ι))
  exact lt_nfpFamily_iff.2 <| ⟨l, (H _).strictMono.le_apply.trans_lt hl⟩

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

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

Tactic:
exact (isSuccLimit_ord h).isSuccPrelimit

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

Goal state before:
pp: case mpr
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
⊢ b ^ y ≤ x ∧ x < b ^ (y + 1) → log b x = y

Tactic:
· rintro ⟨hx₁, hx₂⟩
    apply le_antisymm
    · rwa [← lt_add_one_iff, ← lt_opow_iff_log_lt hb hx]
    · rwa [← opow_le_iff_le_log hb hx]

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

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ nfp f a

Tactic:
rw [← iSup_iterate_eq_nfp]
  exact Ordinal.le_iSup (fun n ↦ f^[n] a) n

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

Goal state before:
pp: x✝ : Ordinal.{u_1}
⊢ nfp id x✝ = id x✝

Tactic:
simp_rw [← iSup_iterate_eq_nfp, iterate_id]

Goal state after:
x✝ : Ordinal.{u_1}
⊢ ⨆ n, id x✝ = id x✝
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a.IsInitial
⊢ a.card ≤ b.card ↔ a ≤ b

Tactic:
refine ⟨fun h ↦ ?_, Ordinal.card_le_card⟩

Goal state after:
a b : Ordinal.{u_1}
ha : a.IsInitial
h : a.card ≤ b.card
⊢ a ≤ b
Module: Mathlib.SetTheory.Ordinal.Principal

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

Tactic:
isSuccPrelimit_iff_succ_lt

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

Goal state before:
pp: a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ b + c
hab : a - b = a
⊢ False

Tactic:
rw [← sub_le, hab] at H

Goal state after:
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ c
hab : a - b = a
⊢ False
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hc : c < a * b
hd : d < a * b
⊢ (fun x1 x2 ↦ x1 + x2) c d < a * b

Tactic:
lt_mul_iff_of_isSuccLimit
        (isSuccLimit_of_isPrincipal_add (lt_of_le_of_ne hb₁' hb₁.symm) hb)

Goal state after:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hc : ∃ c' < b, c < a * c'
hd : ∃ c' < b, d < a * c'
⊢ ∃ c' < b, (fun x1 x2 ↦ x1 + x2) c d < a * c'
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
⊢ ((typein s).toRelEmbedding p).card < #α

Tactic:
apply lt_of_le_of_lt (b := #(Iio q) * #(Iio q))

Goal state after:
case ind.mk.hab
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := ⋯
f : α × α ↪ Lex (α × Lex (α × α)) := ⋯
s : α × α → α × α → Prop := ⋯
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
⊢ ((typein s).toRelEmbedding p).card ≤ #↑(Iio q) * #↑(Iio q)

case ind.mk.hbc
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := ⋯
f : α × α ↪ Lex (α × Lex (α × α)) := ⋯
s : α × α → α × α → Prop := ⋯
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
⊢ #↑(Iio q) * #↑(Iio q) < #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
by
  rw [add_comm, max_comm, add_eq_max ha]

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

Goal state before:
pp: case refine_2.inr
a b : Cardinal.{u_1}
h3 : b = 0
⊢ a + b = a

Tactic:
rw [h3, add_zero]

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

Goal state before:
pp: case refine_2
a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0 → a + b = a

Tactic:
rintro (⟨h1, h2⟩ | h3)
    · rw [add_eq_max h1, max_eq_left h2]
    · rw [h3, add_zero]

Goal state after:
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
⊢ False

Tactic:
apply lt_irrefl ℵ₀

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

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

Tactic:
rw [← hf]

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

Goal state before:
pp: case refine_2
α : Type u
s : Set α
c : Cardinal.{u}
⊢ ∀ (a : { t // t ⊆ s ∧ #↑t ≤ c }),
    { toFun := fun t ↦ Subtype.val ⁻¹' ↑t, inj' := ⋯ } a ∈ fun t ↦ Quot.lift ((fun α β ↦ Nonempty (α ↪ β)) ↑t) ⋯ c

Tactic:
rintro ⟨t, _, h2t⟩

Goal state after:
case refine_2
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
left✝ : t ⊆ s
h2t : #↑t ≤ c
⊢ { toFun := fun t ↦ Subtype.val ⁻¹' ↑t, inj' := ⋯ } ⟨t, ⋯⟩ ∈ fun t ↦ Quot.lift ((fun α β ↦ Nonempty (α ↪ β)) ↑t) ⋯ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
s : Set α
h2 : #↑s < #α
⊢ #↑s + #↑sᶜ = #α

Tactic:
exact mk_sum_compl s

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

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
s t : Set α
hs : #↑s < #α
ht : #↑t < #α
⊢ #↑sᶜ = #↑tᶜ

Tactic:
mk_compl_of_infinite s hs,

Goal state after:
α : Type u_1
inst✝ : Infinite α
s t : Set α
hs : #↑s < #α
ht : #↑t < #α
⊢ #α = #↑tᶜ
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift.{u_2, u_1} #↑sᶜ = lift.{u_1, u_2} #↑(range ⇑f)ᶜ

Tactic:
mk_compl_of_infinite s hs,

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift.{u_2, u_1} #α = lift.{u_1, u_2} #↑(range ⇑f)ᶜ
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
b : β i
⊢ (if h : i' = i then ⋯ ▸ b else 0 i') = if h : i = i' then Eq.recOn h b else 0

Tactic:
simp [@eq_comm _ i i']

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f✝ : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (f + single i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : f i = 0
h2 : b ≠ 0
h3 : p f
⊢ f + single i b = single i b + f

Tactic:
by
      ext j; by_cases H : i = j
      · subst H
        simp [h1]
      · simp [H]

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

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

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

Tactic:
case mpr => rintro rfl _ _; rfl

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

Goal state before:
pp: case refine_1
ι : 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
H1✝ : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sx.toFinset
⊢ i ∉ sx.toFinset ∩ sy.toFinset → (φ i) (f i) = 0

Tactic:
H2

Goal state after:
case refine_1
ι : 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
H1✝ : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2✝ : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sx.toFinset
H2 : i ∉ sx.toFinset ∩ sy.toFinset
⊢ (φ i) (f i) = 0
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
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1✝ : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2✝ : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sx
H2 : ¬(i ∈ sx ∧ i ∈ sy)
⊢ f i = 0

Tactic:
exact (hy i).resolve_left (mt (And.intro H1) H2)

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

Goal state before:
pp: case refine_3
ι : 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
H1✝ : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sy.toFinset
⊢ i ∉ sx.toFinset ∩ sy.toFinset → (φ i) (f i) = 0

Tactic:
H2

Goal state after:
case refine_3
ι : 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
H1✝ : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2✝ : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sy.toFinset
H2 : i ∉ sx.toFinset ∩ sy.toFinset
⊢ (φ i) (f i) = 0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case mk.mk.e_a.refine_2
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
i : ι
a✝ : i ∈ (sf + sg).toFinset
⊢ i ∉ sf.toFinset → (φ i) (f i) = 0

Tactic:
H2

Goal state after:
case mk.mk.e_a.refine_2
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
i : ι
a✝ : i ∈ (sf + sg).toFinset
H2 : i ∉ sf.toFinset
⊢ (φ i) (f i) = 0