mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
⊢ ∀ (a : R ⧸ I) (x y : (ι → R) ⧸ pi fun x ↦ I), a • (x + y) = a • x + a • y

Tactic:
rintro ⟨a⟩ ⟨b⟩ ⟨c⟩

Goal state after:
case mk.mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a✝¹ b✝ : R
inst✝ : I.IsTwoSided
a✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ pi fun x ↦ I
b : ι → R
y✝ : (ι → R) ⧸ pi fun x ↦ I
c : ι → R
⊢ Quot.mk (⇑(Submodule.quotientRel I)) a •
      (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) b + Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c) =
    Quot.mk (⇑(Submodule.quotientRel I)) a • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) b +
      Quot.mk (⇑(Submodule.quotientRel I)) a • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
⊢ ∀ (r s : R ⧸ I) (x : (ι → R) ⧸ pi fun x ↦ I), (r + s) • x = r • x + s • x

Tactic:
rintro ⟨a⟩ ⟨b⟩ ⟨c⟩

Goal state after:
case mk.mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a✝ b✝ : R
inst✝ : I.IsTwoSided
r✝ : R ⧸ I
a : R
s✝ : R ⧸ I
b : R
x✝ : (ι → R) ⧸ pi fun x ↦ I
c : ι → R
⊢ (Quot.mk (⇑(Submodule.quotientRel I)) a + Quot.mk (⇑(Submodule.quotientRel I)) b) •
      Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c =
    Quot.mk (⇑(Submodule.quotientRel I)) a • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c +
      Quot.mk (⇑(Submodule.quotientRel I)) b • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
a : α
⊢ ⋃ i, Ico (f i) a = Iio a ↔ ∀ x < a, ∃ i, f i ≤ x

Tactic:
simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]

Goal state after:
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: ι : Sort u
α : Type v
inst✝ : LinearOrder α
p : ι → Prop
f : (i : ι) → p i → α
a : α
⊢ ⋃ i, ⋃ (hi : p i), Ico (f i hi) a = Iio a ↔ ∀ x < a, ∃ i, ∃ (hi : p i), f i hi ≤ x

Tactic:
simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) s
ne : s.Nonempty
t : Set α
this : Nonempty ↑s
⊢ t ∈ ⨅ i ∈ s, f i ↔ ∃ i ∈ s, t ∈ f i

Tactic:
iInf_subtype',

Goal state after:
α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) s
ne : s.Nonempty
t : Set α
this : Nonempty ↑s
⊢ t ∈ ⨅ x, f ↑x ↔ ∃ i ∈ s, t ∈ f i
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
t : f.NeBot
p : Prop
⊢ (∀ᶠ (x : α) in f, p) ↔ p

Tactic:
by_cases h : p <;> simp [h, t.ne]

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

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

Tactic:
rw [← map_le_iff_le_comap, le_generate_iff]
  exact fun u hu ↦ mem_generate_of_mem ⟨u, hu, rfl⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ cof α ≤ 1 ↔ ∃ x, IsTop x

Tactic:
rw [le_iff_lt_or_eq, Cardinal.lt_one_iff, cof_eq_one_iff]

Goal state after:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ (cof α = 0 ∨ ∃ x, IsTop x) ↔ ∃ x, IsTop x
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosMono α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ -(a₂ • _b) ≤ -(a₁ • _b)

Tactic:
← smul_neg,

Goal state after:
α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosMono α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ a₂ • -_b ≤ -(a₁ • _b)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosStrictMono α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ -(a₂ • _b) < -(a₁ • _b)

Tactic:
← smul_neg,

Goal state after:
α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosStrictMono α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₂ • -_b < -(a₁ • _b)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosReflectLT α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
h : -(a₂ • _b) < -(a₁ • _b)
⊢ a₁ < a₂

Tactic:
← smul_neg,

Goal state after:
α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosReflectLT α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
h : a₂ • -_b < -(a₁ • _b)
⊢ a₁ < a₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosReflectLE α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
h : -(a₂ • _b) ≤ -(a₁ • _b)
⊢ a₁ ≤ a₂

Tactic:
← smul_neg,

Goal state after:
α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosReflectLE α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
h : a₂ • -_b ≤ -(a₁ • _b)
⊢ a₁ ≤ a₂
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ DirSupInacc Set.univ

Tactic:
by simp [← compl_empty]

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosedOn D (f i)
⊢ DirSupClosedOn D (⋂ i, f i)

Tactic:
by
  rw [← sInter_range f]
  exact DirSupClosedOn.sInter (by simpa)

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 : β
⊢ 0 ≤ -(a • b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
← smul_neg,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ a • -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
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 : β
⊢ 0 ≤ -(a • b) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
← smul_neg,

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

Goal state before:
pp: b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type s < univ.{u, v}

Tactic:
rw [univ, ← lift_umax]

Goal state after:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s t : Set α
h : s ⊆ t
⊢ Nonempty ((fun x1 x2 ↦ x1 < x2) ↪r fun x1 x2 ↦ x1 < x2)

Tactic:
refine ⟨⟨embeddingOfSubset _ _ h, ?_⟩⟩

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s t : Set α
h : s ⊆ t
⊢ ∀ {a b : ↑s}, (s.embeddingOfSubset t h) a < (s.embeddingOfSubset t h) b ↔ a < b
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : Ordinal.{u}
hi : i < o
⊢ i ∈ Iio (type r)

Tactic:
by rwa [ho]

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

Goal state before:
pp: α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
⊢ range (familyOfBFamily' r ho f) = o.brange f

Tactic:
refine Set.ext fun a => ⟨?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
a : α
⊢ a ∈ range (familyOfBFamily' r ho f) → a ∈ o.brange f

case refine_2
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
a : α
⊢ a ∈ o.brange f → a ∈ range (familyOfBFamily' r ho f)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
⊢ (type r).brange (bfamilyOfFamily' r f) = range f

Tactic:
refine Set.ext fun a => ⟨?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ (type r).brange (bfamilyOfFamily' r f) → a ∈ range f

case refine_2
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ range f → a ∈ (type r).brange (bfamilyOfFamily' r 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:
rw [← Cardinal.lift_le.{max u v + 1}, Cardinal.lift_lift]
  apply (lift_card_sInf_compl_le _).trans
  rw [← Cardinal.lift_id'.{u, max u v + 1} #(range _)]
  exact mk_range_le_lift

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a + 1 ≤ b ↔ a < b

Tactic:
refine inductionOn₂ a b fun α r _ β s _ ↦ ⟨?_, ?_⟩

Goal state after:
case refine_1
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ type r + 1 ≤ type s → type r < type s

case refine_2
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ type r < type s → type r + 1 ≤ type s
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
ha : IsSuccLimit a
⊢ ∀ ⦃a_1 : Ordinal.{u_1}⦄, (∀ ⦃a_2 : Ordinal.{u_1}⦄, a_2 ∈ ord '' Iio a → a_2 ≤ a_1) → a.ord ≤ a_1

Tactic:
forall_mem_image,

Goal state after:
a : Cardinal.{u_1}
ha : IsSuccLimit a
⊢ ∀ ⦃a_1 : Ordinal.{u_1}⦄, (∀ ⦃x : Cardinal.{u_1}⦄, x ∈ Iio a → x.ord ≤ a_1) → a.ord ≤ a_1
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
grw [hc, ← mul_succ]
        gcongr
        rw [succ_le_iff]
        exact lt_mul_succ_div b hd

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

Goal state before:
pp: case inr
a : Ordinal.{u_1}
h : a ≠ 0
⊢ (limitRecOn 0 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯) = 1

Tactic:
limitRecOn_zero

Goal state after:
case inr
a : Ordinal.{u_1}
h : a ≠ 0
⊢ 1 = 1
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
h : IsSuccLimit a
⊢ IsSuccLimit (a + b) ↔ IsSuccPrelimit b

Tactic:
rw [isSuccLimit_add_iff]

Goal state after:
a b : Ordinal.{u_4}
h : IsSuccLimit a
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : log b n < log b (n + 1)
⊢ b ^ log b (n + 1) ≤ n + 1

Tactic:
exact Nat.pow_log_le_self b (Ne.symm (Nat.zero_ne_add_one n))

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

Goal state before:
pp: case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c

Tactic:
zero_opow hc.ne',

Goal state after:
case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ 0 ^ (b + c) = 0 ^ b * 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl
b k n : ℕ
hk : k > 0
hb : 1 < b
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
refine eq_of_forall_lt_iff fun c ↦ ?_

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

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

Tactic:
simp [pow_succ, natCast_pow m n]

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ preOmega b < a.card.ord

Tactic:
← (isInitial_ord _).card_lt_card,

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ (preOmega b).card < a.card.ord.card
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ preAleph o = ⨆ a, preAleph ↑a

Tactic:
by
  obtain rfl | h := eq_or_ne o 0
  · simp
  · exact isNormal_preAleph.apply_of_isSuccLimit ⟨by simpa, ho⟩

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ∈ range ⇑ℵ_ ↔ ℵ₀ ≤ c

Tactic:
range_aleph,

Goal state after:
c : Cardinal.{u_1}
⊢ c ∈ Ici ℵ₀ ↔ ℵ₀ ≤ c
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
⊢ ord 1 < o.cof.ord

Tactic:
hf.ord_cof,

Goal state after:
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
ha : 1 < a
⊢ ord 1 < a
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a b o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : ↑(Iio b) → ↑(Iio a)
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ b ≤ o.cof.ord

Tactic:
hf.ord_cof,

Goal state after:
a b o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : ↑(Iio b) → ↑(Iio a)
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ b ≤ a
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
⊢ ∃ a, #α < #↑(f ⁻¹' {a})

Tactic:
simp_rw [← succ_le_iff]

Goal state after:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
⊢ ∃ a, succ #α ≤ #↑(f ⁻¹' {a})
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
⊢ #β ≤ #↑(range f)

Tactic:
by_contra h

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : ¬#β ≤ #↑(range f)
⊢ False
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u_1
h : (#α).IsStrongPrelimit
⊢ #{ s // #↑s < (#α).ord.cof } = #α

Tactic:
by
  rcases eq_or_ne #α 0 with (ha | ha)
  · simp [ha]
  have h' : IsStrongLimit #α := ⟨ha, @h⟩
  rcases exists_ord_eq α with ⟨r, wo, hr⟩
  classical
  let := linearOrderOfSTO r
  apply le_antisymm
  · conv_rhs => rw [← mk_bounded_subset h hr]
    apply mk_subtype_le_of_subset
    intro s hs
    rw [hr] at hs
    contrapose! hs
    rw [not_bounded_iff] at hs
    apply cof_le
    simp_rw [IsCofinal, ← not_lt]
    exact hs
  · refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
    · rw [mk_singleton, one_lt_cof_iff]
      exact isSuccLimit_ord h'.aleph0_le
    · intro a b hab
      simpa [singleton_eq_singleton_iff] using hab

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Set M
hs : s.Finite
hsspan : span R s = ⊤
ι : Type w
b : Basis ι R M
this : Submodule.map (↑b.repr) (span R s) = Submodule.map ↑b.repr ⊤
⊢ Finite ι

Tactic:
← span_image,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Set M
hs : s.Finite
hsspan : span R s = ⊤
ι : Type w
b : Basis ι R M
this : span R (⇑↑b.repr '' s) = Submodule.map ↑b.repr ⊤
⊢ Finite ι
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
⊢ ⋃ k, ↑(b.repr (v k)).support = Set.univ

Tactic:
by_contra h

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
h : ¬⋃ k, ↑(b.repr (v k)).support = Set.univ
⊢ False
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsSingular
⊢ c ≠ 0 ∧ ∀ (b : Cardinal.{u_1}), succ b ≠ c

Tactic:
refine ⟨hc.pos.ne', ?_⟩

Goal state after:
c : Cardinal.{u_1}
hc : c.IsSingular
⊢ ∀ (b : Cardinal.{u_1}), succ b ≠ c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c.IsRegular ∨ c.IsSingular

Tactic:
isSingular_iff,

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c.IsRegular ∨ ℵ₀ ≤ c ∧ c.ord.cof ≠ c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case inr.inr
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ (ℵ_ o).IsSingular ↔ IsSuccLimit o ∧ o.cof < ℵ_ o

Tactic:
isSingular_iff,

Goal state after:
case inr.inr
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ ℵ₀ ≤ ℵ_ o ∧ (ℵ_ o).ord.cof ≠ ℵ_ o ↔ IsSuccLimit o ∧ o.cof < ℵ_ o
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : xi = 0
hcj : (single i xi) j = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
rw [DFinsupp.single_eq_of_ne (Ne.symm hij)] at hcj

Goal state after:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : xi = 0
hcj : 0 = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
f_eq : ∏ i ∈ f.support ∪ g.support, h i (f i) = f.prod h
g_eq : ∏ i ∈ f.support ∪ g.support, h i (g i) = g.prod h
⊢ ∏ i ∈ f.support ∪ g.support, h i ((f + g) i) =
    (∏ i ∈ f.support ∪ g.support, h i (f i)) * ∏ i ∈ f.support ∪ g.support, h i (g i)

Tactic:
by
      { simp [h_add, Finset.prod_mul_distrib] }

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊤.dualAnnihilator = ⊥

Tactic:
simp [eq_bot_iff, SetLike.le_def, LinearMap.ext_iff]

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

Goal state before:
pp: ι : 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)
⊢ LinearIndepOn R v (⋃ i, s i)

Tactic:
by_cases hη : Nonempty η
  · refine linearIndepOn_of_finite (⋃ i, s i) fun t ht ft => ?_
    rcases finite_subset_iUnion ft ht with ⟨I, fi, hI⟩
    rcases hs.finset_le fi.toFinset with ⟨i, hi⟩
    exact (h i).mono (Subset.trans hI <| iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))
  · refine (linearIndepOn_empty R v).mono (t := iUnion (s ·)) ?_
    rintro _ ⟨_, ⟨i, _⟩, _⟩
    exact hη ⟨i⟩

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h : (f.sum fun _i xi ↦ xi) ≠ 0
⊢ ∑ i_1 ∈ insert i f.support, (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) i_1 = 0

Tactic:
· specialize hf i
      simp at hf
      grind [Finsupp.sum, Finset.sum_congr]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : MulOneClass M
s : Set M
m : M
inst✝ : Nontrivial R
h : (of R M) m ∈ Submodule.span R ↑(Submonoid.closure (⇑(of R M) '' s))
⊢ m ∈ Submonoid.closure s

Tactic:
← MonoidHom.map_mclosure

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : MulOneClass M
s : Set M
m : M
inst✝ : Nontrivial R
h : (of R M) m ∈ Submodule.span R ↑(Submonoid.map (of R M) (Submonoid.closure s))
⊢ m ∈ Submonoid.closure s
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
b : β
hf : Injective2 f
⊢ f a b ∈ image₂ f s t ↔ a ∈ s ∧ b ∈ t

Tactic:
rw [← mem_coe, coe_image₂, mem_image2_iff hf, mem_coe, mem_coe]

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
inst✝¹ : Mul M
inst✝ : Mul N
e : M ≃ N
x : R[M]
a✝ : N
⊢ ((mapDomainAddEquiv R e) x).coeff a✝ = (equivMapDomain e x.coeff) a✝

Tactic:
simp [mapDomainAddEquiv]

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
inst✝¹ : Mul M
inst✝ : Mul N
e : M ≃ N
r : R
m : M
⊢ (mapDomainAddEquiv R e) (single m r) = single (e m) r

Tactic:
simp [mapDomainAddEquiv]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (↑s ∪ ↑t) (↑s ∩ ↑t) ⊆ image2 f ↑s ↑t

Tactic:
exact image2_union_inter_subset hf

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
⊢ ∑ n ∈ ∅, Polynomial.C (p.coeff n) * X ^ n = Polynomial.C 0

Tactic:
exact C_0.symm

Goal state after: