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

Goal state before:
pp: case inl
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h✝ : IsEmpty ι
⊢ (iInf f).NeBot

Tactic:
constructor
    simp [iInf_of_empty f, top_ne_bot]

Goal state after:
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'
⊢ (∀ {i : ι ×' ι'}, p i.fst ∧ p' i.snd → (s i.fst ∩ s' i.snd).Nonempty) ↔
    ∀ ⦃i : ι⦄, p i → ∀ ⦃i' : ι'⦄, p' i' → (s i ∩ s' i').Nonempty

Tactic:
simp [@forall_comm _ ι']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
⊢ x ∈ (fun x ↦ if p x then f x else g x) ⁻¹' s

Tactic:
rw [mem_preimage]

Goal state after:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
⊢ (if p x then f x else g x) ∈ s
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
⊢ atTop.HasBasis (fun x ↦ a ≤ x) Ici

Tactic:
have : Nonempty α := ⟨a⟩
  refine atTop_basis.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩
  obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b
  exact ⟨c, hac, Ici_subset_Ici.2 hbc⟩

Goal state after:
Module: Mathlib.Order.Cofinal

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

Tactic:
isCofinal_iff_iUnion_Iic_eq_univ,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : ⋃ i ∈ s, Iio i = univ
⊢ ⋃ i ∈ s, Iic i = univ
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
⊢ s = ⨆ b ∈ ↑s, sp b

Tactic:
← span_eq_iSup_of_singleton_spans,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
⊢ s = span R ↑s
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
t : Finset M
huspan : ↑(Finset.image sp t) ⊆ sp '' ↑s
husup : s ≤ (Finset.image sp t).sup id
ssup : s = ⨆ x ∈ ↑t, sp x
⊢ s.FG

Tactic:
← span_eq_iSup_of_singleton_spans,

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
t : Finset M
huspan : ↑(Finset.image sp t) ⊆ sp '' ↑s
husup : s ≤ (Finset.image sp t).sup id
ssup : s = span R ↑t
⊢ s.FG
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := ⋯
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
⊢ IsCompactElement s → s.FG

Tactic:
intro h
    rw [CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup] at h
    -- s is the Sup of the spans of its elements.
    have sSup' : s = sSup (sp '' ↑s) := by
      rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]
    -- by h, s is then below (and equal to) the sup of the spans of finitely many elements.
    obtain ⟨u, ⟨huspan, husup⟩⟩ := h (sp '' ↑s) (le_of_eq sSup')
    have ssup : s = u.sup id := by
      suffices u.sup id ≤ s from le_antisymm husup this
      rw [sSup', Finset.sup_id_eq_sSup]
      exact sSup_le_sSup huspan
    obtain ⟨t, -, rfl⟩ := Finset.subset_set_image_iff.mp huspan
    rw [Finset.sup_image, Function.id_comp, Finset.sup_eq_iSup, supr_rw,
      ← span_eq_iSup_of_singleton_spans, eq_comm] at ssup
    exact ⟨t, ssup⟩

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α ≤i β
a✝ : α
ha : IsSuccLimit a✝
⊢ f a✝ ∈ lowerBounds (upperBounds (⇑f '' Iio a✝))

Tactic:
rw [f.image_Iio]
    exact (f.map_isSuccLimit ha).isLUB_Iio.2

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

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

Tactic:
refine le_antisymm (ord_card_le _) <| le_of_forall_lt fun o h => lt_ord.2 ?_
  have := Ordinal.liftPrincipalSeg.mem_range_of_rel_top (by simpa using h)
  rcases this with ⟨o, h'⟩
  rw [← h', Ordinal.liftPrincipalSeg_coe, ← Ordinal.lift_card]
  apply lift_lt_univ'

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

Goal state before:
pp: a b : Ordinal.{u_4}
n : ℕ
⊢ a + ↑(n + 1) ≤ b + ↑(n + 1) ↔ a ≤ b

Tactic:
simpa [← add_assoc] using add_le_add_iff_right n

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ Nonempty o.ToType ↔ o ≠ 0

Tactic:
← @type_ne_zero_iff_nonempty o.ToType (· < ·),

Goal state after:
o : Ordinal.{u_1}
⊢ typeLT o.ToType ≠ 0 ↔ o ≠ 0
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
s : Set Ordinal.{u_2}
hs : Small.{u_2, u_2 + 1} ↑s
⊢ BddAbove s

Tactic:
exact Ordinal.bddAbove_of_small

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

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a + b - a - c = b - c

Tactic:
add_sub_cancel

Goal state after:
a b c : Ordinal.{u_4}
⊢ b - c = b - c
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:
exact card_sInf_range_compl_le_lift f

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

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty

Tactic:
rw [not_bddAbove_iff] at hs

Goal state after:
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o : Ordinal.{u}
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: case refine_2
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
b : Ordinal.{u}
hb : b < o
⊢ enumOrd s (succ b) ≤ ⨆ b, enumOrd s ↑b

Tactic:
· exact Ordinal.le_iSup _ (⟨_, ho.succ_lt hb⟩ : Iio o)

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

Goal state before:
pp: case refine_1
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : succ (iSup f) ≤ lsub f
⊢ ∃ i, f i = iSup f

Tactic:
by_contra! hf
    have := forall_congr' fun i ↦ (Ordinal.le_iSup f i).lt_iff_ne.symm
    exact (succ_le_iff.1 h).ne ((iSup_le_lsub f).antisymm (lsub_le (this.1 hf)))

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

Goal state before:
pp: a c b : Ordinal.{u_4}
x✝ : a ∣ a * b + c
d : Ordinal.{u_4}
e : a * b + c = a * d
⊢ c = a * b + c - a * b

Tactic:
add_sub_cancel

Goal state after:
a c b : Ordinal.{u_4}
x✝ : a ∣ a * b + c
d : Ordinal.{u_4}
e : a * b + c = a * d
⊢ c = c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
⊢ a ≤ 1 ∨ b = 0 → a ^ b ≤ 1

Tactic:
rw [le_one_iff]

Goal state after:
case refine_1
a b : Ordinal.{u_1}
⊢ (a = 0 ∨ a = 1) ∨ b = 0 → a ^ b ≤ 1
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)

Tactic:
rw [csSup_of_not_bddAbove bdd, csSup_empty, csSup_of_not_bddAbove]

Goal state after:
case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ o * ⊥ = sSup ∅

case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ ¬BddAbove ((fun x ↦ o * x) '' s)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
h : a < ω
⊢ a + ω = ω

Tactic:
obtain ⟨n, rfl⟩ := lt_omega0.1 h
  exact natCast_add_omega0 n

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

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

Tactic:
exact (H i).strictMono.le_apply.trans (h i)

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

Goal state before:
pp: case right.refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), a ∈ fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a

Tactic:
rwa [← fp_iff_derivFamily H]

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

Goal state before:
pp: a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑n
| a

Tactic:
rw [← div_add_mod a (ω ^ log ω a), hn]

Goal state after:
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑n
| ω ^ log ω a * ↑n + a % ω ^ log ω a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ a < ⨆ n, f^[n] b ↔ ∃ n, a < f^[n] b

Tactic:
exact Ordinal.lt_iSup_iff

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

Goal state before:
pp: case succ
a : Ordinal.{u_1}
n✝ : ℕ
⊢ 0^[n✝ + 1] a ≤ 0^[0] a

Tactic:
rw [Function.iterate_succ']
    simp

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ preAleph ω ≤ preAleph o ↔ ω ≤ o

Tactic:
preAleph_le_preAleph

Goal state after:
o : Ordinal.{u_1}
⊢ ω ≤ o ↔ ω ≤ o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
i : α
h : (#α).ord = typeLT α
hα : ℵ₀ ≤ #α
⊢ #↑(Iic i) < #α

Tactic:
← Iio_insert,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
i : α
h : (#α).ord = typeLT α
hα : ℵ₀ ≤ #α
⊢ #↑(insert i (Iio i)) < #α
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: o : Ordinal.{u_1}
⊢ IsCofinal (range fun x ↦ ⟨o, ⋯⟩)

Tactic:
by simp [IsTop]

Goal state after:
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 ↑((enum r') ⟨i, x✝¹⟩) ↑((enum r') ⟨j, h⟩)

pp: case refine_3
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'
⊢ a ≤ (type r').blsub fun i x ↦ f ↑((enum r') ⟨i, x⟩)

Tactic:
· change r (hrr'.1 _) (hrr'.1 _)
    rwa [hrr'.2, @enum_lt_enum _ r']

Goal state after:
case refine_3
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'
⊢ a ≤ (type r').blsub fun i x ↦ f ↑((enum r') ⟨i, x⟩)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inl
b : Ordinal.{u_1}
n : ℕ
⊢ (↑n ^ b).card ≤ max ℵ₀ (max (↑n).card b.card)

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

Tactic:
· obtain ⟨m, rfl⟩ | hb := eq_natCast_or_omega0_le b
    · rw [opow_natCast, ← natCast_pow, card_nat]
      exact le_max_of_le_left natCast_le_aleph0
    · exact (card_opow_le_of_omega0_le_right _ hb).trans (le_max_right _ _)

Goal state after:
case inr
a b : Ordinal.{u_1}
ha : ω ≤ a
⊢ (a ^ b).card ≤ max ℵ₀ (max a.card b.card)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
⊢ #{ s // Bounded r s } ≤ #α

Tactic:
have : { s : Set α | Bounded r s } = ⋃ i, 𝒫 { j | r j i } := ofPred_exists _
    rw [← coe_ofPred, this]
    refine mk_iUnion_le_sum_mk.trans ((sum_le_mk_mul_iSup (fun i => #(𝒫 { j | r j i }))).trans
      ((mul_le_max_of_aleph0_le_left ha).trans ?_))
    rw [max_eq_left]
    apply ciSup_le' _
    intro i
    rw [mk_powerset]
    exact (h (card_typein_lt _ hr)).le

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

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

Tactic:
obtain ⟨e⟩ : Nonempty (α ≃ α × Bool) := by simp [← Cardinal.eq, mul_two]
      simp only [← le_def, mk_pi, mk_fintype, Fintype.card_bool, Nat.cast_ofNat,
        prod_const, lift_ofNat, lift_uzero] at this
      rwa [← power_def, power_self_eq (aleph0_le_mk α), e.permCongr.cardinal_eq]

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

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : 1 < b
⊢ a < (b ^ a).ord.cof

Tactic:
apply lt_imp_lt_of_le_imp_le (power_le_power_left <| power_ne_zero a hb.ne_bot)

Goal state after:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : 1 < b
⊢ (b ^ a) ^ a < (b ^ a) ^ (b ^ a).ord.cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case mk.f
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
⊢ { t // #↑t ≤ #β }

Tactic:
use Sum.inl ⁻¹' range f

Goal state after:
case property
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
⊢ #↑(Sum.inl ⁻¹' range f) ≤ #β
Module: Mathlib.Data.DFinsupp.Defs

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

Tactic:
eq_of_heq hxi

Goal state after:
case mpr.inl
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi xj : β i
hxi : xi ≍ xj
⊢ single i xj = single i xj
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 : ι
⊢ (mk s (x + y)) i = (mk s x + mk s y) i

Tactic:
by simp only [add_apply, mk_apply]; split_ifs <;> [rfl; rw [zero_add]]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∑ x ∈ (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩).support, ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = a

Tactic:
Finset.sum_subset support_mk_subset,

Goal state after:
case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∑ x ∈ s, ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = a

case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∀ x ∈ s, x ∉ (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩).support → ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 0
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
⊢ map S.mkQ T = ⊥ ⊔ map S.mkQ T

Tactic:
bot_sup_eq

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
⊢ map S.mkQ T = map S.mkQ T
Module: Mathlib.Tactic.Module

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring R
inst✝⁴ : Algebra S R
inst✝³ : AddMonoid M
inst✝² : SMul S M
inst✝¹ : MulAction R M
inst✝ : IsScalarTower S R M
l : NF S M
⊢ (algebraMap R l).eval = l.eval

Tactic:
by
  simp only [NF.eval, algebraMap, map_map]
  congr
  ext
  simp [IsScalarTower.algebraMap_smul]

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

Goal state before:
pp: case h.insert
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn R id (⋃ i ∈ s, f i)
⊢ LinearIndepOn R id (⋃ i_1 ∈ insert i s, f i_1)

Tactic:
rw [Finset.set_biUnion_insert]
    refine (hl _).id_union ih ?_
    rw [span_iUnion₂]
    exact hd i s s.finite_toSet his

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s x✝ : R
⊢ (ψ.mulShift r * ψ.mulShift s) x✝ = ψ (r * x✝ + s * x✝)

Tactic:
map_add_eq_mul

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s x✝ : R
⊢ (ψ.mulShift r * ψ.mulShift s) x✝ = ψ (r * x✝) * ψ (s * x✝)
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
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a ↦ ⟨v ↑a, ⋯⟩
x y : ↑t
hij : ↑x = ↑y
⊢ ⟨(fun a ↦ f ⋯) x, ⋯⟩ = ⟨(fun a ↦ f ⋯) y, ⋯⟩

Tactic:
simp [hij]

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ ↑(image g (image₂ f s t)) = ↑(image₂ f' (image g₁ s) (image g₂ t))

Tactic:
by
    push_cast
    exact image_image2_distrib h_distrib

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
⊢ ∀ (x : G × G),
    x ∈ A ×ˢ B ∧ x.1 * x.2 = a0 * b0 → (∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = x) → UniqueMul A B a0 b0

Tactic:
rintro ⟨x1, x2⟩ _ J x y hx hy l
        rcases Prod.mk_inj.mp (J (a0, b0) ⟨Finset.mk_mem_product aA bB, rfl⟩) with ⟨rfl, rfl⟩
        exact Prod.mk_inj.mp (J (x, y) ⟨Finset.mk_mem_product hx hy, l⟩)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n

Tactic:
rcases p with ⟨f⟩

Goal state after:
R : Type u
inst✝ : Semiring R
q : R[X]
f : R[ℕ]
⊢ { toFinsupp := f } = q ↔ ∀ (n : ℕ), { toFinsupp := f }.coeff n = q.coeff n
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ (p.update n a).support = if a = 0 then p.support.erase n else insert n p.support

Tactic:
simp [support, update, Finsupp.support_update]

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
⊢ ∃ s, φ = Pi.evalAlgHom k (fun i ↦ k) s

Tactic:
obtain ⟨s, hs⟩ : ∃ (s : G), φ (Pi.single s 1) ≠ 0 := by
    by_contra
    simp_all

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
⊢ ∃ s, φ = Pi.evalAlgHom k (fun i ↦ k) s
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2.right
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
y : P
hy : y ∈ l.support
⊢ l y • y = l y • f (g y)

Tactic:
(hg y (hl1 hy)).2

Goal state after:
case a.refine_2.right
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
y : P
hy : y ∈ l.support
⊢ l y • y = l y • y
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
⊢ a + ⨆ i, f i = ⨆ i, a + f i

Tactic:
by
  obtain rfl | ha := eq_or_ne a ⊤
  · simp
  refine le_antisymm ?_ <| iSup_le fun i ↦ by grw [← le_iSup]
  refine add_le_of_le_tsub_left_of_le (le_iSup_of_le (Classical.arbitrary _) le_self_add) ?_
  exact iSup_le fun i ↦ ENat.le_sub_of_add_le_left ha <| le_iSup (a + f ·) i

Goal state after: