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

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
hs : Monotone s
f g : (a : α) → β a
a : α
i : ι
hi : a ∈ s i
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a

Tactic:
refine (eventually_ge_atTop i).mono fun j hij ↦ ?_
    simp only [Set.piecewise_eq_of_mem, hs hij hi, subset_iUnion _ _ hi]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t✝ : Set β
m : α → β
f : Filter α
t : Set β
s : Set α
hs : s ∈ f.sets
hst : kernImage m s ⊆ t
⊢ kernImage m (s ∪ m ⁻¹' t) = t

Tactic:
rw [kernImage_union_preimage, union_eq_right.mpr hst]

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

Goal state before:
pp: α : Type u_1
f : Filter α
U : Set α
h : U ∈ f
W : Set ↑U
W_in : W ∈ comap Subtype.val f
⊢ range Subtype.val ∈ f

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ map mab (map mba g) ≤ map mab f

Tactic:
exact map_mono h₂

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ Disjoint (𝓟 s) (𝓟 t) ↔ Disjoint s t

Tactic:
← subset_compl_iff_disjoint_left,

Goal state after:
α : Type u_1
s t : Set α
⊢ Disjoint (𝓟 s) (𝓟 t) ↔ t ⊆ sᶜ
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : Prop
q : α → Prop
h : p
⊢ (∀ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∀ᶠ (x : α) in f, q x

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
f : Filter α
p : Prop
q : α → Prop
h : ¬p
⊢ (∀ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∀ᶠ (x : α) in f, q x

Tactic:
simp [h]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
g : α → β
hg : g ∈ s
⊢ (fun g ↦ g a) g ∈ s.seq t

Tactic:
exact ⟨g, hg, a, ht, rfl⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
⊢ s.seq t ∈ (map (fun b a ↦ (a, b)) g).seq f

Tactic:
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.Algebra.Group.TransferInstance

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsLeftCancelMul β
this : Mul α := e.mul
⊢ IsLeftCancelMul α

Tactic:
exact e.injective.isLeftCancelMul _ fun _ _ ↦ e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.Shrink

Goal state before:
pp: α : Type u_2
inst✝¹ : Small.{v, u_2} α
inst✝ : Div α
x y : Shrink.{v, u_2} α
⊢ (equivShrink α).symm (x / y) = (equivShrink α).symm x / (equivShrink α).symm y

Tactic:
by
  simp [Equiv.div_def]

Goal state after:
Module: Mathlib.Algebra.Group.Shrink

Goal state before:
pp: α : Type u_2
inst✝¹ : Small.{v, u_2} α
inst✝ : Div α
x y : α
⊢ (equivShrink α) (x / y) = (equivShrink α) x / (equivShrink α) y

Tactic:
by
  simp [Equiv.div_def]

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:
rcases s.eq_empty_or_nonempty with rfl | hs

Goal state after:
case inl
α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
h : ∅.Finite
⊢ ∃ a, ∀ b ∈ ∅, f a ≤ f b

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ¬IsCofinal s
⊢ BddAbove s

Tactic:
not_isCofinal_iff

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ∃ x, ∀ y ∈ s, y < x
⊢ BddAbove s
Module: Mathlib.Order.Cofinal

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ BddAbove s → ¬IsCofinal s

Tactic:
not_isCofinal_iff

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ BddAbove s → ∃ x, ∀ y ∈ s, y < x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
h₂ : ∀ x ∈ s, ¬IsCofinal x
⊢ cof α ≤ #↑s

Tactic:
not_isCofinal_iff

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
h₂ : ∀ x ∈ s, ∃ x_1, ∀ y ∈ x, y < x_1
⊢ cof α ≤ #↑s
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_7
P : Type u_6
inst✝² : Semiring S
inst✝¹ : AddCommMonoid P
inst✝ : Module S P
σ : R →+* S
hM : Module.Finite R M
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
⊢ Module.Finite S P

Tactic:
Module.finite_def,

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_7
P : Type u_6
inst✝² : Semiring S
inst✝¹ : AddCommMonoid P
inst✝ : Module S P
σ : R →+* S
hM : ⊤.FG
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
⊢ ⊤.FG
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
⊢ Module.Finite R≥0 R

Tactic:
Module.finite_def,

Goal state after:
R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
⊢ ⊤.FG
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: c : Cardinal.{max (u + 1) v}
h✝ : c < Cardinal.univ.{u, v}
w : Cardinal.{u}
h : c = lift.{max (u + 1) v, u} w
⊢ 2 ^ c = lift.{max (u + 1) v, u} (2 ^ w)

Tactic:
simp [h]

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
a o : α
ho : o ∈ s
H : ∀ b < a, ↑((enum s hs) b) < o
⊢ ∀ c < a, c < (enum s hs).symm ⟨o, ho⟩

Tactic:
simpa [OrderIso.lt_symm_apply]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
hs : IsCofinal (range f)
H : StrictMono (Subtype.val ∘ ⇑(enum (range f) hs))
⊢ Subtype.val ∘ ⇑(enum (range f) hs) = f

Tactic:
rw [← StrictMono.range_inj H hf]

Goal state after:
case mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
hs : IsCofinal (range f)
H : StrictMono (Subtype.val ∘ ⇑(enum (range f) hs))
⊢ range (Subtype.val ∘ ⇑(enum (range f) hs)) = range f
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:
← Cardinal.lift_le.{max u v + 1},

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 u v) + 1, max u v} (Cardinal.lift.{v, u} #ι)
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: o a : Ordinal.{u}
s : Set Ordinal.{u}
ha : a ∈ s
H : ∀ b < o, enumOrd s b < a
⊢ enumOrd s o ≤ a

Tactic:
rw [enumOrd]
  exact csInf_le' ⟨ha, H⟩

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

Goal state before:
pp: case succ.inl
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      n < b ^ fuel →
        (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hnb : n < b
⊢ (go n b (fuel + 1)).fst = n / b ^ (go n b (fuel + 1)).snd ∧
    b ^ (go n b (fuel + 1)).snd ≤ n ∧ n < b ^ ((go n b (fuel + 1)).snd + 1)

Tactic:
| inl hnb =>

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u}
⊢ ∀ (a b : Type u), isEquivalent a b → ⨅ r, type ↑r = ⨅ r, type ↑r

Tactic:
rintro α β ⟨f⟩

Goal state after:
α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
⊢ ⨅ r, type ↑r = ⨅ r, type ↑r
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
H : 1 ≤ c
b' : Ordinal.{u_1}
h : b' < b
⊢ 1 ^ b' ≤ c

Tactic:
IH _ h

Goal state after:
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
H : 1 ≤ c
b' : Ordinal.{u_1}
h : b' < b
⊢ 1 ≤ c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case refine_2
a b : Ordinal.{u_1}
x✝ : 1 < a ∧ b ≠ 0
ha : 1 < a
hb : b ≠ 0
⊢ a ^ 0 < a ^ b

Tactic:
opow_lt_opow_iff_right ha,

Goal state after:
case refine_2
a b : Ordinal.{u_1}
x✝ : 1 < a ∧ b ≠ 0
ha : 1 < a
hb : b ≠ 0
⊢ 0 < b
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case inr.inl
s : Set Ordinal.{u_1}
hs : s.Nonempty
⊢ 0 * sSup s = sSup ((fun x ↦ 0 * x) '' s)

pp: case inr.inr
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)

Tactic:
· simp [hs.image_const]

Goal state after:
case inr.inr
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
rcases le_or_gt a 1 with a1 | a1

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

case inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : 1 < a
⊢ a ^ 1 ≤ a ^ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
by
  rw [add_comm, ← card_ord c, ← card_one, ← card_add, one_add_of_omega0_le]
  rwa [← ord_aleph0, ord_le_ord]

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

Goal state before:
pp: case inr
b x y : ℕ
h : x ≤ b ^ y
hb : 1 ≥ b
⊢ clog b x ≤ y

Tactic:
· grind [clog_of_left_le_one]

Goal state after:
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}
⊢ ⨆ i_1, f i (List.foldr f a i_1) ≤ ⨆ i, List.foldr f a i

Tactic:
refine Ordinal.iSup_le fun 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 ι
⊢ f i (List.foldr f a l) ≤ ⨆ i, List.foldr f a i
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}
⊢ ⨆ i, List.foldr f a i ≤ ⨆ i_1, f i (List.foldr f a i_1)

Tactic:
refine Ordinal.iSup_le fun 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: f : Ordinal.{u} → Ordinal.{u}
h : nfp f = id
⊢ deriv f ⊥ = id ⊥ ∧ ∀ (a : Ordinal.{u}), deriv f a = id a → deriv f (succ a) = id (succ a)

Tactic:
simp [h]

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

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun x ↦ a + x) c = b
⊢ deriv (fun x ↦ a + x) 0 ≤ deriv (fun x ↦ a + x) c

Tactic:
exact (isNormal_deriv _).monotone zero_le

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

Goal state before:
pp: o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ (⨆ a, f a).card ≤ sum fun i ↦ (f i.toOrd).card

Tactic:
by
  apply le_of_eq_of_le (congr_arg _ _).symm (card_iSup_le_sum_card _)
  simpa using ToType.mk.symm.iSup_comp (g := fun x ↦ f x)

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

Goal state before:
pp: case pos
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

pp: case neg
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : ¬BddAbove (range f)
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
swap

Goal state after:
case neg
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : ¬BddAbove (range f)
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

case pos
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
⊢ (⨆ i, f i) * c = ⨆ i, f i * c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u}
c : Cardinal.{v}
f : ↑(Iio o) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ Cardinal.lift.{v, u + 1} #↑(Iio o) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)

Tactic:
Cardinal.mk_Iio_ordinal,

Goal state after:
o : Ordinal.{u}
c : Cardinal.{v}
f : ↑(Iio o) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ Cardinal.lift.{v, u + 1} (Cardinal.lift.{u + 1, u} o.card) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
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.card + 1)

Tactic:
Cardinal.mul_eq_max_of_aleph0_le_right,

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
⊢ max (a ^ b).card a.card ≤ max a.card (b.card + 1)

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

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.Cardinal.Arithmetic

Goal state before:
pp: α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : β < α
⊢ β + γ < α + γ

Tactic:
lt_iff_le_and_ne,

Goal state after:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : β ≤ α ∧ β ≠ α
⊢ β + γ ≤ α + γ ∧ β + γ ≠ α + γ
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ⊢ Cardinal.lift.{v, u + 1} Cardinal.univ.{u, u + 1} = Cardinal.univ.{u, v}

Tactic:
Cardinal.lift_univ,

Goal state after:
⊢ Cardinal.univ.{u, max (u + 1) v} = Cardinal.univ.{u, v}
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl
c : Cardinal.{u}
n : ℕ
hc : ℵ₀ ≤ c
⊢ c ^ ↑n ≤ max c ℵ₀

pp: case inr
c : Cardinal.{u}
n : ℕ
hc : c < ℵ₀
⊢ c ^ ↑n ≤ max c ℵ₀

Tactic:
· exact le_max_of_le_left (power_nat_le hc)

Goal state after:
case inr
c : Cardinal.{u}
n : ℕ
hc : c < ℵ₀
⊢ c ^ ↑n ≤ max c ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

pp: case h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈ ↑⟨s, ⋯⟩ →
    x ∈
      ↑((fun f ↦ ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y ↦
          if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 })

Tactic:
· rintro ⟨y, h⟩
    dsimp only at h
    by_cases h' : ∃ z : s, g z = y
    · rw [dif_pos h'] at h
      cases Sum.inl.inj h
      exact (Classical.choose h').2
    · rw [dif_neg h'] at h
      cases h

Goal state after:
case h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈ ↑⟨s, ⋯⟩ →
    x ∈
      ↑((fun f ↦ ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y ↦
          if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 })
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
f : Π₀ (i : ι), β i
h : i' ≠ i
⊢ (erase i f) i' = f i'

Tactic:
simp [h]

Goal state after:
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]
  apply Finset.prod_subset hs
  intro i hi hi'
  simp only [DFinsupp.mem_support_toFun, ne_eq, not_not] at hi'
  rw [hi', map_zero]
  exact hi

Goal state after:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ ⟨i, a⟩ ≠ ⟨j, b⟩

Tactic:
simp [h]

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

Goal state before:
pp: case inl
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
⊢ i ∈ (f.update i b).support ↔ i ∈ insert i f.support

Tactic:
simp [h]

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

Goal state before:
pp: case mk
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s : Multiset ι
hf : ∀ (i : ι), i ∈ s ∨ f i = 0
⊢ ∑ i ∈ (↑⟨s, hf⟩).toFinset, (φ i) ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i) =
    ∑ i ∈ (↑⟨s, hf⟩).toFinset with { toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i ≠ 0,
      (fun x ↦ ⇑(φ x)) i ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i)

Tactic:
rw [Finset.sum_filter, Finset.sum_congr rfl]

Goal state after:
case mk
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s : Multiset ι
hf : ∀ (i : ι), i ∈ s ∨ f i = 0
⊢ ∀ x ∈ (↑⟨s, hf⟩).toFinset,
    (φ x) ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } x) =
      if { toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } x ≠ 0 then
        (fun x ↦ ⇑(φ x)) x ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } x)
      else 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
H2 : i ∉ sf
⊢ (φ i) (f i) = 0

Tactic:
rw [(hf i).resolve_left H2, map_zero]

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
x : X
⊢ x ∈ (k • a).support ↔ x ∈ a.support

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: case pos
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ψ = 0
⊢ ∑ a, ψ a = ↑(card A)

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: case neg
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : ψ x ≠ 1
⊢ ∑ i, ψ x * ψ i = ∑ a, ψ a

Tactic:
exact Fintype.sum_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul ..).symm

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

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
v : ι → V
hij : i ≠ j
hi : v i ≠ 0
⊢ LinearIndepOn K v {i, j} ↔ ∀ (c : K), c • v i ≠ v j

Tactic:
rw [pair_comm]
  convert! linearIndepOn_insert (s := { i }) (a := j) hij.symm
  simp [hi, mem_span_singleton]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Monoid α
n✝ n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a
a : α
s : Fin (n + 1) → Set α
⊢ (∃ x, x ∈ s 0 ∧ ∃ y, (∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = y) ∧ x * y = a) ↔
    ∃ a_1 v, ↑a_1 * (List.ofFn fun i ↦ ↑(v i)).prod = a

Tactic:
exists_exists_eq_and,

Goal state after:
case succ
α : Type u_1
inst✝ : Monoid α
n✝ n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a
a : α
s : Fin (n + 1) → Set α
⊢ (∃ x, x ∈ s 0 ∧ ∃ a_1, x * (List.ofFn fun i ↦ ↑(a_1 i)).prod = a) ↔
    ∃ a_1 v, ↑a_1 * (List.ofFn fun i ↦ ↑(v i)).prod = a
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t✝¹ : Finset V
hs : LinearIndepOn K id s
hst✝ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
h : b₁ ∈ s
⊢ False

Tactic:
have : b₁ ∈ s ∩ ↑(insert b₁ t) := ⟨h, Finset.mem_insert_self _ _⟩
        rwa [hst] at this

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
u : Finset γ
s : Set α
t : Set β
hu : ∃ s', ↑s' ⊆ s ×ˢ t ∧ image (fun x ↦ f x.1 x.2) s' = u
⊢ ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t'

Tactic:
rcases hu with ⟨u, hu, rfl⟩

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : ↑u ⊆ s ×ˢ t
⊢ ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ image (fun x ↦ f x.1 x.2) u ⊆ image₂ f s' t'
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
r : R
m : M
inst✝ : Mul M
hm : ∀ (m' : M), Commute m m'
hr : ∀ (r' : R), Commute r r'
x : R[M]
this : AddMonoidHom.mulLeft (single m r) = AddMonoidHom.mulRight (single m r)
⊢ Commute (single m r) x

Tactic:
exact congr($this x)

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ k = (s.sort fun a b ↦ a ≤ b).length

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p = 0
⊢ p.coeffs = ∅

Tactic:
simp [h]

Goal state after: