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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t : Set β
m : α → β
f : Filter α
⊢ ∀ {x y : Set β}, x ∈ kernImage m '' f.sets → y ∈ kernImage m '' f.sets → x ∩ y ∈ kernImage m '' f.sets

Tactic:
rintro _ _ ⟨s₁, h₁, rfl⟩ ⟨s₂, h₂, rfl⟩

Goal state after:
α : 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 α
s₁ : Set α
h₁ : s₁ ∈ f.sets
s₂ : Set α
h₂ : s₂ ∈ f.sets
⊢ kernImage m s₁ ∩ kernImage m s₂ ∈ kernImage m '' f.sets
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι' : Sort u_5
la : Filter α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hlb : lb.HasBasis pb sb
⊢ Tendsto f la lb ↔ ∀ (i : ι'), pb i → ∀ᶠ (x : α) in la, f x ∈ sb i

Tactic:
simp only [Tendsto, hlb.ge_iff, mem_map', Filter.Eventually]

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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f (F ⊓ comap f G) ≤ map f F ⊓ G

pp: case a
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f F ⊓ G ≤ map f (F ⊓ comap f G)

Tactic:
· calc
      map f (F ⊓ comap f G) ≤ map f F ⊓ (map f <| comap f G) := map_inf_le
      _ ≤ map f F ⊓ G := inf_le_inf_left (map f F) map_comap_le

Goal state after:
case a
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f F ⊓ G ≤ map f (F ⊓ comap f G)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
U : Set (Set β)
f : β → α
⊢ map f (generate U) ≤ generate ((fun x ↦ f ⁻¹' x) ⁻¹' U)

Tactic:
rw [le_generate_iff]
  exact fun u hu ↦ mem_generate_of_mem hu

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
⊢ upperBounds (range (f ∘ g)) = upperBounds (range f)

Tactic:
refine Subset.antisymm ?_ (upperBounds_mono_set <| range_comp_subset_range _ _)

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
⊢ upperBounds (range (f ∘ g)) ⊆ upperBounds (range f)
Module: Mathlib.RingTheory.Finiteness.Basic

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

Tactic:
span_image _,

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ ∃ s, IsCofinal s ∧ #↑s = cof α

Tactic:
obtain ⟨s, hs⟩ := ciInf_mem fun s : {s : Set α // IsCofinal s} ↦ #s
  exact ⟨s.1, s.2, hs⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
x : ↑s
⊢ ∃ y, ↑x ≤ f y

Tactic:
simpa using hf' x

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite M
⊢ Module.Finite R M

Tactic:
by
  cases nonempty_fintype M
  exact ⟨⟨Finset.univ, by rw [Finset.coe_univ, span_univ]⟩⟩

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
rw [← neg_nonneg, ← neg_smul, smul_nonneg_iff_pos_imp_nonneg]; simp only [neg_pos, neg_nonneg]

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

Goal state before:
pp: R : Type u_2
V : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
S₁ : Submodule R V
hS₁ : Module.Finite R ↥S₁
S₂ : Submodule R V
⊢ Module.Finite R ↥S₂ → Module.Finite R ↥(S₁ ⊔ S₂)

Tactic:
hS₂

Goal state after:
R : Type u_2
V : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
S₁ : Submodule R V
hS₁ : Module.Finite R ↥S₁
S₂ : Submodule R V
hS₂ : Module.Finite R ↥S₂
⊢ Module.Finite R ↥(S₁ ⊔ S₂)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
obtain h' | h' := le_or_gt b a

Goal state after:
case inl
a b c : Ordinal.{u_4}
h : a ≤ b + c
h' : b ≤ a
⊢ a - b ≤ c

case inr
a b c : Ordinal.{u_4}
h : a ≤ b + c
h' : a < b
⊢ a - b ≤ c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
x : α
⊢ ↑((enum (range f) ⋯) x) = ↑((StrictMono.orderIso f hf) x)

Tactic:
apply congrFun (enum_eq_iff.2 ⟨?_, ?_⟩)

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
x : α
⊢ StrictMono fun x ↦ ↑((StrictMono.orderIso f hf) x)

α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
x : α
⊢ (range fun x ↦ ↑((StrictMono.orderIso f hf) x)) = range f
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 : c < a - b
⊢ succ c < a - b

Tactic:
lt_sub

Goal state after:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
c : Ordinal.{u_4}
hc : b + c < a
⊢ b + succ c < a
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
exact le_max_of_le_left (Ordinal.le_iSup (fun x ↦ f (Sum.inl x)) i)

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

Goal state before:
pp: case succ.inr
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:
rcases ih (Nat.one_mul 1 ▸ Nat.mul_lt_mul_of_lt_of_lt hb hb) (go_aux hb hfuel hnb)
        with ⟨ih₁, ih₂, ih₃⟩
      simp_all only [go, if_neg (Nat.not_lt_of_le hnb), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul, Nat.pow_pos (Nat.zero_lt_of_lt hb), Nat.div_div_eq_div_mul,
        ← Nat.pow_add_one, ← Nat.pow_add_one', Nat.mul_add_one]
      split <;> simp_all

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

Goal state before:
pp: a : Cardinal.{u}
b : Ordinal.{max u v}
h : b < (Cardinal.lift.{v, u} (succ a)).ord
⊢ b ∈ range lift.{v, u}

Tactic:
← lift_ord

Goal state after:
a : Cardinal.{u}
b : Ordinal.{max u v}
h : b < lift.{v, u} (succ a).ord
⊢ b ∈ range lift.{v, u}
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ b / d ≤ (a * b + c) / (a * d)

Tactic:
grw [← mul_le_iff_le_div H, mul_assoc, mul_div_le b d, ← le_self_add]

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

Goal state before:
pp: a : Ordinal.{u_1}
⊢ a ^ 0 = 1

Tactic:
obtain rfl | h := eq_or_ne a 0
  · rw [zero_opow', Ordinal.sub_zero]
  · rw [opow_of_ne_zero h, limitRecOn_zero]

Goal state after:
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:
csSup_of_not_bddAbove bdd,

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 ∅ = sSup ((fun x ↦ o * x) '' s)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: m n : ℕ
⊢ ↑(m * n) + ↑m = ↑m * ↑(n + 1)

Tactic:
natCast_mul m n,

Goal state after:
m n : ℕ
⊢ ↑m * ↑n + ↑m = ↑m * ↑(n + 1)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
← natCast_mul,

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

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

Tactic:
← natCast_mul,

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

Goal state before:
pp: m n : ℕ
⊢ ↑n * ↑(m / n) + ↑(m % n) = ↑m

Tactic:
← natCast_mul,

Goal state after:
m n : ℕ
⊢ ↑(n * (m / n)) + ↑(m % n) = ↑m
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
hab : a * b = b
⊢ b = 0 ∨ a ^ ω ≤ b

Tactic:
rcases eq_zero_or_pos a with ha | ha
  · rw [ha, zero_opow omega0_ne_zero]
    exact .inr zero_le
  rw [or_iff_not_imp_left]
  intro hb
  rw [← nfp_mul_one ha]
  rw [← Ne, ← one_le_iff_ne_zero] at hb
  exact nfp_le_fp (isNormal_mul_right ha).monotone hb (le_of_eq hab)

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

Goal state before:
pp: case pos
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : a = 0
⊢ b = 1 ∨ a = 0

pp: case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
⊢ b = 1 ∨ a = 0

Tactic:
· exact Or.inr h2a

Goal state after:
case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
⊢ b = 1 ∨ a = 0
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * succ (a / b ^ log b a) * c ≤ b ^ succ (log b a)

Tactic:
rw [mul_assoc, opow_succ]

Goal state after:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * (succ (a / b ^ log b a) * c) ≤ b ^ log b a * b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
exact Cardinal.eq_of_add_eq_add_left h hb

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
ha : 1 < a
⊢ ⨆ i, ↑(f i) = o

Tactic:
rw [← iSup_Iio_add_one hf.strictMono, hf.iSup_add_one_eq]
  rw [← hf.ord_cof]
  apply (isSuccLimit_ord _).isSuccPrelimit
  rwa [aleph0_le_cof_iff, ← ord_lt_ord, hf.ord_cof, ord_one]

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

Goal state before:
pp: β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ #↑(range f) < (lift.{u + 1, u} a).cof

Tactic:
← Cardinal.lift_lt.{_, v}

Goal state after:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ Cardinal.lift.{v, u + 1} #↑(range f) < Cardinal.lift.{v, u + 1} (lift.{u + 1, u} a).cof
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
⊢ (⨆ i, f i).card ≤ c

Tactic:
by
  apply card_iSup_le_lift _ hf
  conv_rhs => rw [← Cardinal.lift_lift.{u, u + 1}]
  rwa [Cardinal.mk_Iio_ordinal, Cardinal.lift_lift, ← Cardinal.lift_lift.{v, u + 1},
    Cardinal.lift_le]

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

Goal state before:
pp: f : (b : Ordinal.{u_1}) → b < 0 → Ordinal.{u_1}
⊢ 0 ≤ (cof 0).ord

Tactic:
by rw [cof_zero, ord_zero]

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⟩)

Tactic:
@enum_lt_enum _ r'

Goal state after:
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
⊢ ⟨i, x✝¹⟩ < ⟨j, h⟩
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
⊢ ∃ f, o.cof.ord.blsub f = o

Tactic:
by
  rcases exists_lsub_cof o with ⟨ι, f, hf, hι⟩
  rcases Cardinal.exists_ord_eq ι with ⟨r, hr, hι'⟩
  rw [← @blsub_eq_lsub' ι r hr] at hf
  rw [← hι, hι']
  exact ⟨_, hf⟩

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

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : o.bsup f = o.blsub f
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
exact cof_blsub_le_lift.{u, v} f

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

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ (2 ^ c) ^ c ≤ 2 ^ c

Tactic:
rw [← power_mul, mul_eq_self h]

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

Goal state before:
pp: case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #α < prod fun x ↦ #α

Tactic:
refine (mk_iUnion_le_sum_mk.trans' ?_).trans_lt (sum_lt_prod _ _ fun i ↦ mk_Iio_lt i.1 hα)

Goal state after:
case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #α ≤ #↑(⋃ i, Iio ↑i)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
rwa [← lift_lt, mk_range_eq_of_injective f.injective, ← h, lift_lt]

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

Goal state after:
case nil
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
⊢ Multiset.Pi.empty α = Pi.nil α
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 : ι
⊢ (mk s (-x)) i = (-mk s x) i

Tactic:
simp only [neg_apply, mk_apply]

Goal state after:
ι : 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
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Submodule R N
inst✝ : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)
x : N
⊢ (∃ f, ((lsum ℕ) fun i ↦ (p i).subtype) f = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x

Tactic:
simp_rw [DFinsupp.lsum_apply_apply, DFinsupp.sumAddHom_apply,
    LinearMap.toAddMonoidHom_coe, coe_subtype]

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
⊢ LinearIndependent R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v'))

Tactic:
have : linearCombination R (Sum.elim (inl R M M' ∘ v) (inr R M M' ∘ v')) =
      .prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
      (sumFinsuppLEquivProdFinsupp R).toLinearMap := by ext (_ | _) <;> simp
  rw [LinearIndependent, this]
  simpa [LinearMap.coe_prodMap] using ⟨hv, hv'⟩

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

Goal state before:
pp: case hs
ι : 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))
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) fun i ↦ ⋃ i_1 ∈ i, f i_1

Tactic:
apply directed_of_isDirected_le

Goal state after:
case hs
ι : 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 j : Finset ι⦄, i ⊆ j → ⋃ i_1 ∈ i, f i_1 ⊆ ⋃ i ∈ j, f i
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
i : ι
hs : LinearIndepOn R v s
hx : ∀ (r : R), r • v i ∈ span R (v '' s) → r = 0
⊢ LinearIndepOn R v (insert i s)

Tactic:
← Set.union_singleton

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
i : ι
hs : LinearIndepOn R v s
hx : ∀ (r : R), r • v i ∈ span R (v '' s) → r = 0
⊢ LinearIndepOn R v (s ∪ {i})
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f f' : α → β → γ
s : Finset α
t : Finset β
h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b
⊢ ↑(image₂ f s t) = ↑(image₂ f' s t)

Tactic:
push_cast
    exact image2_congr h

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
hf : Injective f
x : R[N]
⊢ (comapDomain f hf x).coeff = Finsupp.comapDomain f x.coeff ⋯

Tactic:
by simp [comapDomain]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : MulOneClass M
inst✝ : Nontrivial R
a b : M
h : (of R M) a = (of R M) b
⊢ a = b

Tactic:
simpa [← coeff_inj, Finsupp.single_eq_single_iff] using h

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x : R[G]
r : R
g h : G
⊢ ∀ m' ∈ x.coeff.support, m' * g = h ↔ m' = h * g⁻¹

Tactic:
simp [eq_mul_inv_iff_mul_eq]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Ring R
inst✝ : MulOneClass M
n : ℕ
⊢ single 1 ↑(Int.negSucc n) = -↑(n + 1)

Tactic:
by simp [natCast_def, one_def]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : AddZeroClass M
a b : Multiplicative M
h : (of R M) a = (of R M) b
⊢ a = b

Tactic:
simpa [← coeff_inj, Finsupp.single_eq_single_iff] using h

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
n : ℕ
a : α
s : Fin n → Finset α
⊢ a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a

Tactic:
rw [← mem_coe, coe_list_prod, List.map_ofFn, Set.mem_prod_list_ofFn]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
n : ℕ
a : α
s : Fin n → Finset α
⊢ (∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a) ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ {i}ᶜ.orderEmbOfFin h = RelEmbedding.trans (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb

Tactic:
apply DFunLike.coe_injective
  rw [eq_comm]
  convert!
    orderEmbOfFin_unique _ (fun x ↦ ?_) ((Fin.strictMono_succAbove _).comp (Fin.cast_strictMono _))
  · simp
  · simp [← h, card_compl]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
s t : Finset α
⊢ 1 ∈ ↑(s / t) ↔ ¬Disjoint s t

Tactic:
← disjoint_coe,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
s t : Finset α
⊢ 1 ∈ ↑(s / t) ↔ ¬Disjoint ↑s ↑t
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R[ℕ]
⊢ { toFinsupp := a } = 1 ↔ a = 1

Tactic:
← ofFinsupp_one,

Goal state after:
R : Type u
inst✝ : Semiring R
a : R[ℕ]
⊢ { toFinsupp := a } = { toFinsupp := 1 } ↔ a = 1
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type u_1
inst✝² : SMulZeroClass S R
inst✝¹ : SMulZeroClass Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
⊢ ∀ (m : S) (a : R[X]), MulOpposite.op m • a = m • a

Tactic:
rintro _ ⟨⟩
    simp_rw [← ofFinsupp_smul, op_smul_eq_smul]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ n * X * p = p * X ^ (n + 1)

Tactic:
rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ]

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

Goal state before:
pp: case 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 : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), f (g y a) = y
y : P
H : y ∈ t1
⊢ f ((fun y ↦ if H : y ∈ t1 then g y H else 0) y) = y

Tactic:
· simp only [dif_pos H]
      apply hg2

Goal state after: