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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ IsCofinal s ↔ ⋃ i ∈ s, Iic i = univ

Tactic:
simp [IsCofinal, eq_univ_iff_forall]

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∈ s
⊢ f a ≤ b

pp: case neg
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
⊢ f a ≤ b

Tactic:
· simp_all [mem_upperBounds]

Goal state after:
case neg
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
⊢ f a ≤ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
succ_eq_add_one,

Goal state after:
case mp
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ a < b + (d + 1)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ IsNormal fun x ↦ a + x

Tactic:
by
  rw [isNormal_iff]
  exact ⟨add_right_strictMono, fun _ l _ ↦ (add_le_iff_of_isSuccLimit l).2⟩

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

Goal state before:
pp: a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
c : Ordinal.{u_4}
hc : b + c < a
⊢ b + succ c < a

Tactic:
succ_eq_add_one,

Goal state after:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
c : Ordinal.{u_4}
hc : b + c < a
⊢ b + (c + 1) < a
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
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
⊢ (Subtype.val ∘ ⇑(enum s hs)) a ≤ b

Tactic:
trans sSup ((Subtype.val ∘ enum s hs) '' Iio a)

Goal state after:
α : 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
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := ⋯
this : ConditionallyCompleteLinearOrderBot α := ⋯
⊢ (Subtype.val ∘ ⇑(enum s hs)) a ≤ sSup (Subtype.val ∘ ⇑(enum s hs) '' Iio a)

α : 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
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := ⋯
this : ConditionallyCompleteLinearOrderBot α := ⋯
⊢ sSup (Subtype.val ∘ ⇑(enum s hs) '' Iio a) ≤ b
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: s : Set Cardinal.{u_3}
⊢ (sSup s).ord = sSup (ord '' s)

Tactic:
obtain rfl | hn := s.eq_empty_or_nonempty
  · simp
  · by_cases hs : BddAbove s
    · exact isNormal_ord.map_sSup hn hs
    · rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (bddAbove_ord_image_iff.not.2 hs)]
      simp

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

Goal state before:
pp: o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
i : Ordinal.{u}
hi : i < o
j : Ordinal.{v}
hj : j < o'
hj' : g j hj = f i hi
⊢ f i hi ≤ o'.bsup g

Tactic:
rw [← hj']

Goal state after:
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
i : Ordinal.{u}
hi : i < o
j : Ordinal.{v}
hj : j < o'
hj' : g j hj = f i hi
⊢ g j hj ≤ o'.bsup g
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b : Ordinal.{u_4}
hb : IsSuccLimit b
ha : 0 < a
⊢ IsSuccPrelimit (a * b)

Tactic:
· exact (isSuccLimit_mul_right ha hb).isSuccPrelimit

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

Goal state before:
pp: a b : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ IsSuccPrelimit (a * b)

Tactic:
by
  obtain rfl | ha := eq_zero_or_pos a
  · rw [zero_mul]
    exact isSuccPrelimit_zero
  · exact (isSuccLimit_mul_right ha hb).isSuccPrelimit

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

Goal state before:
pp: ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ (type r).blsub (bfamilyOfFamily' r f) = (type r').blsub (bfamilyOfFamily' r' f)

Tactic:
rw [blsub_eq_lsub', blsub_eq_lsub']

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

Goal state before:
pp: case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑m < ↑n * succ ↑(m / n)

Tactic:
succ_eq_add_one,

Goal state after:
case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑m < ↑n * (↑(m / n) + 1)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ∀ a < c.ord, succ a < c.ord

Tactic:
succ_eq_add_one,

Goal state after:
case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ∀ a < c.ord, a + 1 < c.ord
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀.ord ≤ succ a

pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ IsSuccLimit ℵ₀.ord

Tactic:
succ_eq_add_one,

Goal state after:
case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀.ord ≤ a + 1

case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ IsSuccLimit ℵ₀.ord
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ f i (List.foldr f a l) ≤ ⨆ i, List.foldr f a i

pp: case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ List.foldr f a l ≤ ⨆ i_1, f i (List.foldr f a i_1)

Tactic:
· exact Ordinal.le_iSup _ (i::l)

Goal state after:
case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ List.foldr f a l ≤ ⨆ i_1, f i (List.foldr f a i_1)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
rw [← nfpFamily_fp (H i)]
    exact (H i).monotone h

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

Goal state before:
pp: case inr
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b (o % b ^ log b o) < log b o

Tactic:
← lt_opow_iff_log_lt hb h

Goal state after:
case inr
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ o % b ^ log b o < b ^ log b o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : b ≤ 1
⊢ log b x + log b y ≤ log b (x * y)

Tactic:
simpa only [log_of_left_le_one hb, zero_add] using le_rfl

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

Goal state before:
pp: case neg
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : ¬BddAbove s
⊢ IsPrincipal op (sSup s)

Tactic:
csSup_of_not_bddAbove hs

Goal state after:
case neg
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : ¬BddAbove s
⊢ IsPrincipal op (sSup ∅)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ a % ω ^ log ω a < ω ^ log ω a

Tactic:
· exact mod_lt _ (opow_ne_zero _ omega0_ne_zero)

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
⊢ f b < nfp f a ↔ b < nfp f a

Tactic:
unfold nfp
  rw [← @apply_lt_nfpFamily_iff Unit (fun _ => f) _ _ (fun _ => H) a b]
  exact ⟨fun h _ => h, fun h => h Unit.unit⟩

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

Goal state before:
pp: case refine_2
a✝ a : Ordinal.{u}
h : deriv (fun x ↦ a✝ + x) a = a✝ * ω + a
⊢ deriv (fun x ↦ a✝ + x) (succ a) = a✝ * ω + succ a

Tactic:
succ_eq_add_one,

Goal state after:
case refine_2
a✝ a : Ordinal.{u}
h : deriv (fun x ↦ a✝ + x) a = a✝ * ω + a
⊢ deriv (fun x ↦ a✝ + x) (a + 1) = a✝ * ω + (a + 1)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: n : ℕ
⊢ preOmega ↑n = ↑n

Tactic:
by
  induction n with
  | zero => exact preOmega_zero
  | succ n IH =>
    apply (le_preOmega_self _).antisymm'
    apply enumOrd_succ_le not_bddAbove_isInitial (isInitial_natCast _) (IH.trans_lt _)
    rw [Nat.cast_lt]
    exact lt_succ n

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

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ IsPrincipal op (nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o)

Tactic:
intro a b ha hb
  rw [lt_nfp_iff] at *
  obtain ⟨m, ha⟩ := ha
  obtain ⟨n, hb⟩ := hb
  obtain h | h := le_total
    ((fun x ↦ ⨆ y : Set.Iio x ×ˢ Set.Iio x, succ (op y.1.1 y.1.2))^[m] o)
    ((fun x ↦ ⨆ y : Set.Iio x ×ˢ Set.Iio x, succ (op y.1.1 y.1.2))^[n] o)
  · use n + 1
    rw [Function.iterate_succ']
    apply (lt_succ _).trans_le
    exact Ordinal.le_iSup (fun y : Set.Iio _ ×ˢ Set.Iio _ ↦ succ (op y.1.1 y.1.2))
      ⟨_, Set.mk_mem_prod (ha.trans_le h) hb⟩
  · use m + 1
    rw [Function.iterate_succ']
    apply (lt_succ _).trans_le
    exact Ordinal.le_iSup (fun y : Set.Iio _ ×ˢ Set.Iio _ ↦ succ (op y.1.1 y.1.2))
      ⟨_, Set.mk_mem_prod ha (hb.trans_le h)⟩

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

Goal state before:
pp: case a
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a ≤ 1

Tactic:
rw [← lt_add_one_iff, one_add_one_eq_two]

Goal state after:
case a
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a < 2
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
⊢ ((typein fun x1 x2 ↦ x1 < x2).toRelEmbedding o).cof = (lift.{u + 1, u} o).cof

Tactic:
typein_ordinal

Goal state after:
o : Ordinal.{u}
⊢ (lift.{u + 1, u} o).cof = (lift.{u + 1, u} o).cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_1
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
i : β
⊢ f i ∈ Iio (⨆ i, f i + 1)

Tactic:
· rw [mem_Iio]
    exact (lt_add_one _).trans_le <| le_ciSup bddAbove_of_small _

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

Goal state before:
pp: case neg.refine_1
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 : ι
h : ∃ j, r j i ∧ f i ≤ f j
hji : r (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h)
k : ι
hkj : r k (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h)
⊢ f k < f i

pp: case neg.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 : ι
h : ∃ j, r j i ∧ f i ≤ f j
hji : r (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h)
⊢ f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) ((typein r').toRelEmbedding ⟨⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h, ⋯⟩) ⋯

Tactic:
· by_contra! H
        exact (wo.wf.not_lt_min {j | r j i ∧ f i ≤ f j} ⟨IsTrans.trans _ _ _ hkj hji, H⟩) hkj

Goal state after:
case neg.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 : ι
h : ∃ j, r j i ∧ f i ≤ f j
hji : r (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h)
⊢ f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) ((typein r').toRelEmbedding ⟨⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h, ⋯⟩) ⋯
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.inl
a c : Ordinal.{u_1}
hb : succ c ≠ 0
⊢ (a + succ c).cof = (succ c).cof

Tactic:
succ_eq_add_one,

Goal state after:
case inr.inl
a c : Ordinal.{u_1}
hb : succ c ≠ 0
⊢ (a + (c + 1)).cof = (c + 1).cof
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: κ : Cardinal.{v}
h : κ.IsRegular
⊢ (Cardinal.lift.{u, v} κ).IsRegular

Tactic:
obtain ⟨h₁, h₂⟩ := h
  constructor
  · simpa
  · rwa [← Cardinal.lift_ord, ← Ordinal.lift_cof, lift_le]

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

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

Tactic:
by
  apply le_antisymm
  · rw [powerlt_le]
    exact fun _ a ↦ pow_le h a
  convert! le_powerlt c one_lt_aleph0; rw [power_one]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
b : β
⊢ ∃ a, b ∈ f a

Tactic:
by simpa using (w.ge :) (Set.mem_univ b)

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
e : α ≃ α × Bool
this : 2 ^ #α ≤ #(Perm (α × Bool))
⊢ #(α → α) ≤ #(α ≃ α)

Tactic:
← power_def,

Goal state after:
α : Type u
inst✝ : Infinite α
e : α ≃ α × Bool
this : 2 ^ #α ≤ #(Perm (α × Bool))
⊢ #α ^ #α ≤ #(α ≃ α)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case pos
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h' : ∃ z, g z = y
h : Sum.inl ↑(Classical.choose h') = Sum.inl x
⊢ x ∈ ↑⟨s, ⋯⟩

Tactic:
cases Sum.inl.inj h

Goal state after:
case pos.refl
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
y : β
h' : ∃ z, g z = y
h : Sum.inl ↑(Classical.choose h') = Sum.inl ↑(Classical.choose h')
⊢ ↑(Classical.choose h') ∈ ↑⟨s, ⋯⟩
Module: Mathlib.Data.List.Pi

Goal state before:
pp: case nil
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
⊢ ((↑[]).pi fun x ↦ ↑(fs x)) = ↑([].pi fs)

Tactic:
simp only [Multiset.coe_nil, Multiset.pi_zero, pi_nil, Multiset.coe_singleton,
      Multiset.singleton_inj]
    ext i hi
    simp at hi

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

Goal state before:
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)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
i : ι
⊢ i ∈ {i ∈ sy.toFinset | f i ≠ 0} → i ∈ {i ∈ sx.toFinset | f i ≠ 0}

Tactic:
· intro H
      rcases Finset.mem_filter.1 H with ⟨_, h⟩
      exact Finset.mem_filter.2 ⟨Multiset.mem_toFinset.2 <| (hx i).resolve_right h, h⟩

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

Goal state before:
pp: case inl.inr
ι : 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 : ι
a : α i
hi : i ∈ ↑s
ha : (f ↑⟨i, ⋯⟩).toFun a = 0
⊢ (f ⟨i, a⟩.fst) ⟨i, a⟩.snd = 0

Tactic:
simp [toFun_eq_coe (f i) ▸ ha]

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddGroup (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ (-f).support = f.support

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
x : (i : ι) → β i →+ γ
⊢ (fun F i ↦ F.comp (singleAddHom β i)) (sumAddHom x) = x

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
ψ : (Π₀ (i : ι), β i) →+ γ
⊢ sumAddHom ((fun F i ↦ F.comp (singleAddHom β i)) ψ) = ψ

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
F G : (i : ι) → β i →+ γ
⊢ sumAddHom (F + G) = sumAddHom F + sumAddHom G

Tactic:
ext; simp

Goal state after:
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
⊢ ↑(evalEquiv R M).symm.dualMap = Dual.eval R (Dual R M)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i : ι
⊢ lapply i ∘ₗ lsingle i = LinearMap.id

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case neg
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : ¬Nonempty η
⊢ LinearIndepOn R v (⋃ i, s i)

Tactic:
· refine (linearIndepOn_empty R v).mono (t := iUnion (s ·)) ?_
    rintro _ ⟨_, ⟨i, _⟩, _⟩
    exact hη ⟨i⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inr
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : f ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I)
g : ι →₀ R
hgsupp : g ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I)
hsum : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
hn : c.Nonempty
this : Std.Refl r
⊢ f = g

Tactic:
classical
    obtain ⟨I, _I_mem, hI⟩ : ∃ I ∈ c, (f.support ∪ g.support : Set ι) ⊆ I :=
      f.support.coe_union _ ▸ hc.directedOn.exists_mem_subset_of_finset_subset_biUnion hn <| by
        simpa using! And.intro hfsupp hgsupp
    exact linearIndepOn_iffₛ.mp I.2 f (subset_union_left.trans hI)
      g (subset_union_right.trans hI) hsum

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: A : Type u_1
R : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝³⁴ : Semiring A
inst✝³³ : CommSemiring R
inst✝³² : Semiring R₁
inst✝³¹ : Semiring R₂
M : Type u_5
Mₗ : Type u_6
N : Type u_7
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝³⁰ : AddCommMonoid M
inst✝²⁹ : AddCommMonoid Mₗ
inst✝²⁸ : AddCommMonoid N
inst✝²⁷ : AddCommMonoid Nₗ
inst✝²⁶ : AddCommMonoid Pₗ
inst✝²⁵ : AddCommMonoid Qₗ
inst✝²⁴ : AddCommMonoid Qₗ'
inst✝²³ : Module R M
inst✝²² : Module R Mₗ
inst✝²¹ : Module R₁ Mₗ
inst✝²⁰ : Module R₂ N
inst✝¹⁹ : Module R Nₗ
inst✝¹⁸ : Module R Pₗ
inst✝¹⁷ : Module R₂ Pₗ
inst✝¹⁶ : Module R₁ Pₗ
inst✝¹⁵ : Module R Qₗ
inst✝¹⁴ : Module R₁ Qₗ
inst✝¹³ : Module R Qₗ'
inst✝¹² : Module R₂ Qₗ'
Tₗ : Type u_12
Tₗ' : Type u_13
inst✝¹¹ : AddCommMonoid Tₗ
inst✝¹⁰ : AddCommMonoid Tₗ'
inst✝⁹ : Module R₁ Tₗ
inst✝⁸ : Module R₂ Tₗ'
inst✝⁷ : Module A Pₗ
inst✝⁶ : SMulCommClass R A Pₗ
inst✝⁵ : Module R A
inst✝⁴ : Module A M
inst✝³ : Module A Qₗ
inst✝² : SMulCommClass R A Qₗ
inst✝¹ : IsScalarTower R A Qₗ
inst✝ : IsScalarTower R A Pₗ
f : M →ₗ[A] Nₗ →ₗ[R] Pₗ
g : Pₗ →ₗ[A] Qₗ
x✝¹ x✝ : M
⊢ ↑R g ∘ₗ f (x✝¹ + x✝) = ↑R g ∘ₗ f x✝¹ + ↑R g ∘ₗ f x✝

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: A : Type u_1
R : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝³⁴ : Semiring A
inst✝³³ : CommSemiring R
inst✝³² : Semiring R₁
inst✝³¹ : Semiring R₂
M : Type u_5
Mₗ : Type u_6
N : Type u_7
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝³⁰ : AddCommMonoid M
inst✝²⁹ : AddCommMonoid Mₗ
inst✝²⁸ : AddCommMonoid N
inst✝²⁷ : AddCommMonoid Nₗ
inst✝²⁶ : AddCommMonoid Pₗ
inst✝²⁵ : AddCommMonoid Qₗ
inst✝²⁴ : AddCommMonoid Qₗ'
inst✝²³ : Module R M
inst✝²² : Module R Mₗ
inst✝²¹ : Module R₁ Mₗ
inst✝²⁰ : Module R₂ N
inst✝¹⁹ : Module R Nₗ
inst✝¹⁸ : Module R Pₗ
inst✝¹⁷ : Module R₂ Pₗ
inst✝¹⁶ : Module R₁ Pₗ
inst✝¹⁵ : Module R Qₗ
inst✝¹⁴ : Module R₁ Qₗ
inst✝¹³ : Module R Qₗ'
inst✝¹² : Module R₂ Qₗ'
Tₗ : Type u_12
Tₗ' : Type u_13
inst✝¹¹ : AddCommMonoid Tₗ
inst✝¹⁰ : AddCommMonoid Tₗ'
inst✝⁹ : Module R₁ Tₗ
inst✝⁸ : Module R₂ Tₗ'
inst✝⁷ : Module A Pₗ
inst✝⁶ : SMulCommClass R A Pₗ
inst✝⁵ : Module R A
inst✝⁴ : Module A M
inst✝³ : Module A Qₗ
inst✝² : SMulCommClass R A Qₗ
inst✝¹ : IsScalarTower R A Qₗ
inst✝ : IsScalarTower R A Pₗ
f : M →ₗ[A] Nₗ →ₗ[R] Pₗ
g : Pₗ →ₗ[A] Qₗ
x✝¹ : A
x✝ : M
⊢ ↑R g ∘ₗ f (x✝¹ • x✝) = (RingHom.id A) x✝¹ • ↑R g ∘ₗ f x✝

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
this : (a * d) • s = (b * c) • s
⊢ s = 0

Tactic:
by_contra hs; exact h (_root_.smul_left_injective S hs ‹_›)

Goal state after: