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

Goal state before:
pp: case inl
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

Tactic:
rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]

Goal state after:
case inl
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ ¬⊥.NeBot ↔ ¬((∀ (j : ι), Nonempty (α j)) ∧ f.NeBot)
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PartialOrder β
l : Filter α
f g : α → β
⊢ f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f

Tactic:
by
  simp only [EventuallyEq, EventuallyLE, le_antisymm_iff, eventually_and]

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

Goal state before:
pp: α : Type u_6
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ atTop = pure ⊤

Tactic:
rw [isTop_top.atTop_eq, Ici_top, principal_singleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : α → Filter β
s✝ s : Set β
⊢ (s ∈ f.bind fun x ↦ g x ⊓ 𝓟 s✝) ↔ s ∈ f.bind g ⊓ 𝓟 s✝

Tactic:
simp only [mem_bind, mem_inf_principal]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
u : α → β
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
⊢ ∃ a', a ≤ a' ∧ b < u a'

Tactic:
rcases exists_le_of_tendsto_atTop h a b' with ⟨a', ha', ha''⟩

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
u : α → β
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
a' : α
ha' : a ≤ a'
ha'' : b' ≤ u a'
⊢ ∃ a', a ≤ a' ∧ b < u a'
Module: Mathlib.Data.Set.Finite.Lemmas

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

Tactic:
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.Order.Cofinal

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : ⋃ i ∈ s, Iio i = univ
i : α
h✝ : i ∈ s
⊢ Iio i ⊆ Iic i

Tactic:
exact Iio_subset_Iic_self

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupInacc (f i)
⊢ DirSupInacc (⋃₀ range f)

Tactic:
exact DirSupInacc.sUnion (by simpa)

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₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosStrictMono α γ
⊢ ∀ ⦃b : β × γ⦄, 0 < b → ∀ ⦃a₁ a₂ : α⦄, a₁ < a₂ → a₁ • b < a₂ • b

Tactic:
by
    simp_rw [lt_iff]
    rintro a (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩) _b₁ _b₂ hb
    · exact .inl ⟨smul_lt_smul_of_pos_right hb h₁, smul_le_smul_of_nonneg_right hb.le h₂⟩
    · exact .inr ⟨smul_le_smul_of_nonneg_right hb.le h₁, smul_lt_smul_of_pos_right hb h₂⟩

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

Goal state before:
pp: c : Cardinal.{u}
this : lift.{max (u + 1) v, u + 1} (lift.{u + 1, u} c) < lift.{max (u + 1) v, u + 1} univ.{u, u + 1}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}

Tactic:
rw [lift_lift, lift_univ, univ_umax.{u, v}] at this

Goal state after:
c : Cardinal.{u}
this : lift.{max (u + 1) v, u} c < univ.{u, v}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: ⊢ ℵ₀ < univ.{u, v}

Tactic:
simpa using lift_lt_univ' ℵ₀

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (enum s hs))
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b : α
hb : ∀ b_1 < a, (Subtype.val ∘ ⇑(enum s hs)) b_1 ≤ b
⊢ BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)

Tactic:
use enum s hs a

Goal state after:
case h
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) := ⋯
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b : α
hb : ∀ b_1 < a, (Subtype.val ∘ ⇑(enum s hs)) b_1 ≤ b
⊢ ↑((enum s hs) a) ∈ upperBounds (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
⊢ (sInf (range f)ᶜ).card ≤ Cardinal.lift.{v, u} #ι

Tactic:
rw [← Cardinal.lift_le.{max u v + 1}, Cardinal.lift_lift]

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ Cardinal.lift.{(max u v) + 1, max u v} (sInf (range f)ᶜ).card ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
⊢ ⨆ i, f i + 1 = ⨆ i, f i

Tactic:
apply (iSup_le_iSup_add_one f).antisymm'

Goal state after:
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
⊢ ⨆ i, f i + 1 ≤ ⨆ i, f i
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}
⊢ IsEmpty o.ToType ↔ o = 0

Tactic:
exact isEmpty_toType_iff

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

Goal state before:
pp: a b c : Ordinal.{u_4}
hle : b * c ≤ a
hlt : a < b * (c + 1)
⊢ a / b = c

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Goal state after:
case inl
a c : Ordinal.{u_4}
hle : 0 * c ≤ a
hlt : a < 0 * (c + 1)
⊢ a / 0 = c

case inr
a b c : Ordinal.{u_4}
hle : b * c ≤ a
hlt : a < b * (c + 1)
hb : b ≠ 0
⊢ a / b = c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / b = c ↔ b * c ≤ a ∧ a < b * (c + 1)

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Goal state after:
case inl
a c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / 0 = c ↔ 0 * c ≤ a ∧ a < 0 * (c + 1)

case inr
a b c : Ordinal.{u_4}
hc : c ≠ 0
hb : b ≠ 0
⊢ a / b = c ↔ b * c ≤ a ∧ a < b * (c + 1)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: b c : Ordinal.{u_4}
⊢ b * c % b = 0

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Goal state after:
case inl
c : Ordinal.{u_4}
⊢ 0 * c % 0 = 0

case inr
b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ b * c % b = 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * z * (y / z) + (x * (y % z) + w) = x * y + w

Tactic:
rw [← add_assoc, mul_assoc, ← mul_add, div_add_mod]

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{v}
hf : IsNormal f
⊢ ⨆ n, f ↑n = f ω

Tactic:
by
  rw [← iSup_natCast, hf.map_iSup bddAbove_of_small]

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

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
m : ℕ
⊢ m ≤ n.log2 ↔ m ≤ log 2 n

Tactic:
Nat.le_log2 hn,

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
m : ℕ
⊢ 2 ^ m ≤ n ↔ m ≤ log 2 n
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ succ c < b ^ succ c

Tactic:
rw [opow_succ, opow_succ]

Goal state after:
a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ c * a < b ^ c * b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ sSup (if 1 ∈ Iic x then univ else ∅) = 0

Tactic:
split_ifs

Goal state after:
case pos
x : Ordinal.{u_1}
h : 1 ≤ 1
h✝ : 1 ∈ Iic x
⊢ sSup univ = 0

case neg
x : Ordinal.{u_1}
h : 1 ≤ 1
h✝ : 1 ∉ Iic x
⊢ sSup ∅ = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case refine_2
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
⊢ clog b n < clog b (n + 1)

Tactic:
lt_clog_iff_pow_lt hb,

Goal state after:
case refine_2
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
⊢ b ^ clog b n < n + 1
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl
b k n : ℕ
hk : k > 0
hb : 1 < b
c : ℕ
⊢ (b ^ k) ^ c < n ↔ c * k < clog b n

Tactic:
lt_clog_iff_pow_lt hb,

Goal state after:
case inr.inl
b k n : ℕ
hk : k > 0
hb : 1 < b
c : ℕ
⊢ (b ^ k) ^ c < n ↔ b ^ (c * k) < n
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
by
  obtain rfl | hx := eq_or_ne x 0
  · simp_rw [log_zero_right, zero_le]
  · obtain hb | hb := lt_or_ge 1 b
    · exact (opow_le_iff_le_log hb (hx.bot_lt.trans_le xy).ne').1 <|
        (opow_log_le_self _ hx).trans xy
    · rw [log_of_left_le_one hb, log_of_left_le_one hb]

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

Goal state before:
pp: b o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o % b ^ log b o < o

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Goal state after:
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o % 0 ^ log 0 o < o

case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : b ≠ 0
⊢ o % b ^ log b o < o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case succ
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
n : ℕ
hn : (op a)^[n] a < o
⊢ (op a ∘ (op a)^[n]) a < o

Tactic:
exact ho hao hn

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

Goal state before:
pp: ⊢ ω.IsInitial

Tactic:
by
  rw [IsInitial, card_omega0, ord_aleph0]

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

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ o)

Tactic:
rw [isPrincipal_add_iff_add_self_lt]
    intro a ha
    obtain ⟨c, hc, m, hm⟩ := (lt_omega0_opow ha').1 ha
    apply (add_lt_add_of_le_of_lt hm.le hm).trans_le
    rw [← mul_add, ← Nat.cast_add]
    exact (opow_mul_lt_opow (natCast_lt_omega0 _) hc).le

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

Goal state before:
pp: case inl
b : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (0 ^ b)

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Goal state after:
case inl.inl
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (0 ^ 0)

case inl.inr
b : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
hb : b ≠ 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (0 ^ b)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b ≤ b ↔ a ^ ω ∣ b

Tactic:
rw [← mul_eq_right_iff_opow_omega0_dvd]
  exact (isNormal_mul_right ha).strictMono.le_apply.ge_iff_eq'

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

Goal state before:
pp: a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ a * b = max a b

Tactic:
by
  rw [mul_comm, max_comm]
  exact mul_eq_max_of_aleph0_le_left h h'

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

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

Tactic:
rw [add_eq_right hb this.le, eq_comm] at h

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ (⨆ i, f i) + c = ⨆ i, f i + c

Tactic:
by
  have (i : ι) : f i + c ≤ (⨆ i, f i) + c := by grw [le_ciSup hf i]
  refine le_antisymm ?_ (ciSup_le' this)
  have bdd : BddAbove (range (f · + c)) := ⟨_, forall_mem_range.mpr this⟩
  obtain hs | hs := lt_or_ge (⨆ i, f i) ℵ₀
  · obtain ⟨i, hi⟩ := exists_eq_ciSup_of_not_isSuccLimit hf (not_isSuccLimit_of_lt_aleph0 hs)
    exact hi ▸ le_ciSup bdd i
  rw [add_eq_max hs, max_le_iff]
  exact ⟨ciSup_mono bdd fun i ↦ self_le_add_right _ c,
    (self_le_add_left _ _).trans (le_ciSup bdd <| Classical.arbitrary ι)⟩

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

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

Tactic:
exact ha.not_ge (cof_le_cardinalMk _)

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

Goal state before:
pp: case add_one
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ (a ^ b).card * a.card ≤ max a.card (b + 1).card

Tactic:
card_add_one,

Goal state after:
case add_one
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ (a ^ b).card * a.card ≤ max a.card (b.card + 1)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case add_one.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ (a ^ b).card ≠ 0

pp: case add_one.h
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ ℵ₀ ≤ a.card

Tactic:
· rw [ne_eq, card_eq_zero, opow_eq_zero]
      rintro ⟨rfl, -⟩
      cases omega0_pos.not_ge ha

Goal state after:
case add_one.h
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ ℵ₀ ≤ a.card
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_2
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i j : Ordinal.{u}
x✝¹ : i < type r'
h : j < type r'
x✝ : i < j
⊢ r (hrr'.toEmbedding ((enum r') ⟨i, x✝¹⟩)) (hrr'.toEmbedding ((enum r') ⟨j, h⟩))

Tactic:
rwa [hrr'.2, @enum_lt_enum _ r']

Goal state after:
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
⊢ lsub f < c.ord

Tactic:
by
  apply lift_iSup_add_one_lt_of_lt_cof _ hf
  rwa [lift_umax, c.ord.lift_id', hc.cof_ord]

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

Goal state before:
pp: α : Type u
β' : Type v
⊢ #↑{f | Surjective f} ≠ 0 ↔ (#α = 0 ∨ #β' ≠ 0) ∧ Nonempty (β' ↪ α)

Tactic:
simp_rw [mk_ne_zero_iff, mk_eq_zero_iff, nonempty_coe_sort,
    Set.Nonempty, mem_ofPred, exists_surjective_iff, nonempty_fun]

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

Goal state before:
pp: c : Cardinal.{u}
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
hc : c.IsRegular
hs : #↑s < c
⊢ #↑(⋃ x, t ↑x ⋯) < c ↔ ∀ (a : α) (ha : a ∈ s), #↑(t a ha) < c

Tactic:
card_iUnion_lt_iff_forall_of_isRegular hc hs,

Goal state after:
c : Cardinal.{u}
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
hc : c.IsRegular
hs : #↑s < c
⊢ (∀ (i : ↑s), #↑(t ↑i ⋯) < c) ↔ ∀ (a : α) (ha : a ∈ s), #↑(t a ha) < c
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
i : ι
⊢ ((if p i then f i else 0) + if ¬p i then f i else 0) = f i

Tactic:
split_ifs

Goal state after:
case pos
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
i : ι
h✝ : p i
⊢ f i + 0 = f i

case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
i : ι
h✝ : ¬p i
⊢ 0 + f i = f i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case inr.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
j : ι
hi : i ≠ j
hj : f j = 0
⊢ j ∈ i ::ₘ ↑s ∨ Function.update (⇑f) i b j = 0

Tactic:
· exact Or.inr ((Function.update_of_ne hi.symm b _).trans hj)

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)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (c • x) ⟨i, H⟩ else 0) = c • if H : i ∈ s then x ⟨i, H⟩ else 0

Tactic:
split_ifs

Goal state after:
case pos
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
h✝ : i ∈ s
⊢ (c • x) ⟨i, h✝⟩ = c • x ⟨i, h✝⟩

case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
h✝ : i ∉ s
⊢ 0 = c • 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ f.update i b = f - single i (f i) + single i b

Tactic:
by
  rw [update_eq_erase_add_single f i b, erase_eq_sub_single f i]

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (x + y) ⟨i, H⟩ else 0) = (if H : i ∈ s then x ⟨i, H⟩ else 0) + if H : i ∈ s then y ⟨i, H⟩ else 0

Tactic:
split_ifs

Goal state after:
case pos
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
h✝ : i ∈ s
⊢ (x + y) ⟨i, h✝⟩ = x ⟨i, h✝⟩ + y ⟨i, h✝⟩

case neg
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
h✝ : i ∉ s
⊢ 0 = 0 + 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
i : ι
⊢ (if H : i ∈ s then 0 ⟨i, H⟩ else 0) = 0 i

Tactic:
split_ifs

Goal state after:
case pos
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
i : ι
h✝ : i ∈ s
⊢ 0 ⟨i, h✝⟩ = 0 i

case neg
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
i : ι
h✝ : i ∉ s
⊢ 0 = 0 i
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 : ι
⊢ (if H : i ∈ s then (-x) ⟨i, H⟩ else 0) = -if H : i ∈ s then x ⟨i, H⟩ else 0

Tactic:
split_ifs

Goal state after:
case pos
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i : ι
h✝ : i ∈ s
⊢ (-x) ⟨i, h✝⟩ = -x ⟨i, h✝⟩

case neg
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i : ι
h✝ : i ∉ s
⊢ 0 = -0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
s : Finset ι
hs : f.support ⊆ s
map_zero : ∀ i ∈ s, g i 0 = 1
⊢ f.prod g = ∏ i ∈ s, g i (f i)

Tactic:
simp only [DFinsupp.prod]

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
s : Finset ι
hs : f.support ⊆ s
map_zero : ∀ i ∈ s, g i 0 = 1
⊢ ∏ i ∈ f.support, g i (f i) = ∏ i ∈ s, g i (f i)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (x - y) ⟨i, H⟩ else 0) = (if H : i ∈ s then x ⟨i, H⟩ else 0) - if H : i ∈ s then y ⟨i, H⟩ else 0

Tactic:
split_ifs

Goal state after:
case pos
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
h✝ : i ∈ s
⊢ (x - y) ⟨i, h✝⟩ = x ⟨i, h✝⟩ - y ⟨i, h✝⟩

case neg
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
h✝ : i ∉ s
⊢ 0 = 0 - 0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case refine_1
ι : Type u
γ : Type w
inst✝⁵ : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : (i : ι) → Zero (β₁ i)
inst✝³ : (i : ι) → Zero (β₂ i)
inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
i : ι
⊢ i ∈ g.support → i ∉ (mk g.support fun i ↦ f (↑i) (g ↑i)).support → h i ((mk g.support fun i ↦ f (↑i) (g ↑i)) i) = 1

Tactic:
h1

Goal state after:
case refine_1
ι : Type u
γ : Type w
inst✝⁵ : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : (i : ι) → Zero (β₁ i)
inst✝³ : (i : ι) → Zero (β₂ i)
inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
i : ι
h1 : i ∈ g.support
⊢ i ∉ (mk g.support fun i ↦ f (↑i) (g ↑i)).support → h i ((mk g.support fun i ↦ f (↑i) (g ↑i)) i) = 1
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)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
⊢ δ ⟨i, j⟩.fst ⟨i, j⟩.snd

Tactic:
by exact x

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

Goal state before:
pp: case refine_2
ι : Type u
γ : Type w
inst✝⁵ : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : (i : ι) → Zero (β₁ i)
inst✝³ : (i : ι) → Zero (β₂ i)
inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
i : ι
⊢ i ∈ g.support → h i ((mk g.support fun i ↦ f (↑i) (g ↑i)) i) = (fun i b ↦ h i (f i b)) i (g i)

Tactic:
h1

Goal state after:
case refine_2
ι : Type u
γ : Type w
inst✝⁵ : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : (i : ι) → Zero (β₁ i)
inst✝³ : (i : ι) → Zero (β₂ i)
inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
i : ι
h1 : i ∈ g.support
⊢ h i ((mk g.support fun i ↦ f (↑i) (g ↑i)) i) = (fun i b ↦ h i (f i b)) i (g i)
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁸ : CommSemiring K
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module K V
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ (Dual.eval R M) m₁ = (Dual.eval R M) m₂

Tactic:
by ext n; simpa [hr.1.eq_iff] using congr(n $hm)

Goal state after: