mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
x : φ i
hx : x ∈ p i
⊢ (single R φ i) x ∈ pi I p

Tactic:
Submodule.mem_pi

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
x : φ i
hx : x ∈ p i
⊢ ∀ i_1 ∈ I, (single R φ i) x i_1 ∈ p i_1
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ map (snd R M M₂) (fst R M M₂) = ⊥

Tactic:
aesop (add simp fst)

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Icc a (b - 1) = Ico a b

Tactic:
by
  simpa [pred_eq_sub_one] using Icc_pred_right_eq_Ico a b

Goal state after:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
a : α
f : ι → α
inst✝¹ : Nonempty ι
inst✝ : Finite ι
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
ha : a ≤ ⨆ i, f i
i : ι
hi : ∀ (i_1 : ι), f (id i_1) ≤ f i
⊢ ∃ i, a ≤ f i

Tactic:
exact ⟨i, ha.trans <| iSup_le hi⟩

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
by
  by_cases h : BddAbove (Set.range f)
  · exact ciSup_partialSups_eq h
  · rw [iSup, iSup, ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ h,
      ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _
        (bddAbove_range_partialSups.not.mpr h)]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' Set.Icc a b = Set.Icc (c + a) (c + b)

Tactic:
exact Set.image_const_add_Icc _ _ _

Goal state after:
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
⊢ x ∈ ↑(List.Nat.antidiagonal n) ↔ x.1 + x.2 = n

Tactic:
mem_coe,

Goal state after:
n : ℕ
x : ℕ × ℕ
⊢ x ∈ List.Nat.antidiagonal n ↔ x.1 + x.2 = n
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
f : ℕ → M
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
⊢ (∏ k ∈ range n, f (k + 1) / f k) / ∏ k ∈ range m, f (k + 1) / f k = f n / f m

Tactic:
prod_range_div,

Goal state after:
M : Type u_4
f : ℕ → M
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
⊢ f n / f 0 / ∏ k ∈ range m, f (k + 1) / f k = f n / f m
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
f : ℕ → M
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
⊢ f n / f 0 / ∏ k ∈ range m, f (k + 1) / f k = f n / f m

Tactic:
prod_range_div,

Goal state after:
M : Type u_4
f : ℕ → M
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
⊢ f n / f 0 / (f m / f 0) = f n / f m
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
f : ℕ → M
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
⊢ f n / f 0 / (f m / f 0) = f n / f m

Tactic:
div_div_div_cancel_right

Goal state after:
M : Type u_4
f : ℕ → M
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
⊢ f n / f m = f n / f m
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), t n m

Tactic:
have h_middle :
      ∀ n i : ℕ, i ∈ range n.succ → (t n.succ i.succ) = x * t n i + y * t n i.succ := by
    intro n i h_mem
    have h_le : i ≤ n := le_of_lt_succ (mem_range.mp h_mem)
    dsimp only [t]
    rw [choose_succ_succ, cast_add, mul_add]
    congr 1
    · rw [pow_succ' x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
    · rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq]
      by_cases h_eq : i = n
      · rw [h_eq, choose_succ_self, cast_zero, mul_zero, mul_zero]
      · rw [succ_sub (lt_of_le_of_ne h_le h_eq)]
        rw [pow_succ' y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
hx : ¬Disjoint ↑(I ⊔ span {x}) ↑S
hy : ¬Disjoint ↑(I ⊔ span {y}) ↑S
⊢ False

Tactic:
simp only [Set.not_disjoint_iff, SetLike.mem_coe, Submodule.mem_sup,
      mem_span_singleton] at hx hy

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
hx : ∃ x_1, (∃ y ∈ I, ∃ z, x ∣ z ∧ y + z = x_1) ∧ x_1 ∈ S
hy : ∃ x, (∃ y_1 ∈ I, ∃ z, y ∣ z ∧ y_1 + z = x) ∧ x ∈ S
⊢ False
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ
d n : ℕ
hn : ∑ ij ∈ antidiagonal n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
⊢ ∑ ij ∈ antidiagonal (n + 1), (d + ij.2).choose d = (d + (n + 1) + 1).choose (d + 1)

Tactic:
rw [Nat.sum_antidiagonal_succ, hn, Nat.choose_succ_succ (d + (n + 1)), ← add_assoc]

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

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ico (max a₁ b₁) (min a₂ b₂) = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
Ico_eq_empty_iff,

Goal state after:
α : Type v
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ ¬max a₁ b₁ < min a₂ b₂ ↔ min a₂ b₂ ≤ max a₁ b₁
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p q : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
hq : ∀ᶠ (x : α) in f, q x
⊢ ∃ᶠ (x : α) in f, p x ∧ q x

Tactic:
refine mt (fun h => hq.mp <| h.mono ?_) hp

Goal state after:
α : Type u
p q : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
hq : ∀ᶠ (x : α) in f, q x
h : ∀ᶠ (x : α) in f, ¬(fun x ↦ p x ∧ q x) x
⊢ ∀ (x : α), ¬(fun x ↦ p x ∧ q x) x → q x → ¬(fun x ↦ p x) x
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
q : α → Prop
⊢ (∃ᶠ (x : α) in f, p → q x) ↔ p → ∃ᶠ (x : α) in f, q x

Tactic:
simp [frequently_imp_distrib]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : m x = m y
⊢ x = y

Tactic:
rwa [← pure_injective.eq_iff, ← map_pure, ← map_pure, hm.eq_iff, pure_injective.eq_iff]
      at hxy <;> rwa [mem_Iic, pure_le_principal]

Goal state after:
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
N₁ N₂ : Submodule R M
hN₁ : N₁.FG
hN₂ : N₂.FG
t₁ : Set M
ht₁ : t₁.Finite
span_t₁ : span R t₁ = N₁
t₂ : Set M
ht₂ : t₂.Finite
span_t₂ : span R t₂ = N₂
⊢ span R (t₁ ∪ t₂) = N₁ ⊔ N₂

Tactic:
by rw [span_union, span_t₁, span_t₂]

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
hs : DirSupInacc s
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
⊢ a ∈ s ↔ b ∈ s

Tactic:
by
  simpa [not_iff_not] using hs.compl.mem_iff_of_antisymmRel h

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ ¬IsMin (f a)

Tactic:
obtain ⟨b, hb⟩ := not_isMin_iff.1 ha.not_isMin

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : α
hb : b < a
⊢ ¬IsMin (f a)
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mpr.type.refine_3
b✝ : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
a' : α
b : β
e : f b = (typein r).toRelEmbedding a'
⊢ (RelEmbedding.ofMonotone (fun b ↦ (enum r) ⟨f b, ⋯⟩) ⋯) b = a'

Tactic:
simp only [RelEmbedding.ofMonotone_coe]

Goal state after:
case mpr.type.refine_3
b✝ : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
a' : α
b : β
e : f b = (typein r).toRelEmbedding a'
⊢ (enum r) ⟨f b, ⋯⟩ = a'
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case e'_1
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ x = (enum r) ?h.convert_4

pp: case h.convert_4
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ↑(Iio (type r))

pp: case h.convert_6
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ?h.convert_4 < ⟨succ ((typein r).toRelEmbedding x), ⋯⟩

Tactic:
· rw [enum_typein]

Goal state after:
case h.convert_6
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ⟨(typein r).toRelEmbedding x, ⋯⟩ < ⟨succ ((typein r).toRelEmbedding x), ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{?u.38}
ho : 0 < o
⊢ o ≠ 0

Tactic:
rintro rfl; simp at ho

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

Goal state before:
pp: case type
α : Type u_4
r✝ : α → α → Prop
inst✝¹ : IsWellOrder α r✝
β : Type u_4
s✝ : β → β → Prop
inst✝ : IsWellOrder β s✝
⊢ type (Prod.Lex s✝ r✝) = 0 ↔ type r✝ = 0 ∨ type s✝ = 0

Tactic:
type_eq_zero_iff_isEmpty,

Goal state after:
case type
α : Type u_4
r✝ : α → α → Prop
inst✝¹ : IsWellOrder α r✝
β : Type u_4
s✝ : β → β → Prop
inst✝ : IsWellOrder β s✝
⊢ IsEmpty (β × α) ↔ IsEmpty α ∨ IsEmpty β
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) < lift.{max u w, v} (type s) ↔ Nonempty (r ≺i s)

Tactic:
by
  constructor <;> refine fun ⟨f⟩ ↦ ⟨?_⟩
  · exact (f.relIsoTrans (RelIso.preimage Equiv.ulift r).symm).transInitial
      (RelIso.preimage Equiv.ulift s).toInitialSeg
  · exact (f.relIsoTrans (RelIso.preimage Equiv.ulift r)).transInitial
      (RelIso.preimage Equiv.ulift s).symm.toInitialSeg

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

Goal state before:
pp: case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
w✝ : ι
hf : f w✝ = iSup f
⊢ succ (iSup f) ≤ lsub f

Tactic:
rw [succ_le_iff, ← hf]

Goal state after:
case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
w✝ : ι
hf : f w✝ = iSup f
⊢ f w✝ < lsub f
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_2
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w✝¹ : Ordinal.{u}
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = o.bsup f
⊢ succ (o.bsup f) ≤ o.blsub f

Tactic:
rw [succ_le_iff, ← hf]

Goal state after:
case refine_2
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w✝¹ : Ordinal.{u}
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = o.bsup f
⊢ f w✝¹ w✝ < o.blsub f
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / c ≤ b / c

Tactic:
· rw [← mul_le_iff_le_div hc]
    exact (mul_div_le a c).trans h

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

Goal state before:
pp: b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
⊢ log b y < x

Tactic:
by
  rcases eq_or_ne y 0 with rfl | hy
  · grind [log_zero_right]
  · exact log_lt_of_lt_pow hy hlt

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

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ (b + 1) = a ^ b * a

Tactic:
rw [opow_of_ne_zero h, opow_of_ne_zero h]
    exact limitRecOn_add_one ..

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

Goal state before:
pp: case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ log b (n + 1)

pp: case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ log b (n + 1)

Tactic:
· rw [log_of_left_le_one hb]
    exact zero_le _

Goal state after:
case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ log b (n + 1)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ
b n k : ℕ
hk : log b (n / b ^ k) = log b n - k
⊢ log b (n / b ^ k) - 1 = log b n - (k + 1)

Tactic:
hk,

Goal state after:
case succ
b n k : ℕ
hk : log b (n / b ^ k) = log b n - k
⊢ log b n - k - 1 = log b n - (k + 1)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a c d : Ordinal.{u_4}
⊢ a % (c * d) % c = (c * d * (a / (c * d)) + a % (c * d)) % c

Tactic:
rw [mul_assoc, mul_add_mod_self]

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

Goal state before:
pp: case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b * b) = log b n

Tactic:
log_mul_base hb (Nat.div_pos h (by lia)).ne',

Goal state after:
case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b) + 1 = log b n
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inr.inr.hb
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ b ^ k ≤ 1

Tactic:
rwa [Nat.pow_le_one_iff (Nat.ne_of_gt hk)]

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

Goal state before:
pp: x : ℕ
this : Fintype ↑(Iio x)
⊢ (typein LT.lt).toRelEmbedding x = ↑x

Tactic:
rw [← type_Iio_lt, type_fintype, Nat.cast_inj]

Goal state after:
x : ℕ
this : Fintype ↑(Iio x)
⊢ Fintype.card ↑(Iio x) = x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
x : Fin n
⊢ (typein LT.lt).toRelEmbedding x = ↑↑x

Tactic:
rw [← type_Iio_lt, type_fintype, Nat.cast_inj]

Goal state after:
n : ℕ
x : Fin n
⊢ Fintype.card ↑(Iio x) = ↑x
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ clog b n

pp: case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ clog b n

Tactic:
· rw [log_of_left_le_one hb]
    exact zero_le _

Goal state after:
case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ clog b n
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ι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ nfpFamily f a
⊢ b ≤ nfpFamily f a

Tactic:
obtain ⟨i⟩ := hι
    exact (H i).strictMono.le_apply.trans (h i)

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

Goal state before:
pp: n : ℕ
IH : preOmega ↑n = ↑n
⊢ ↑n < ↑(n + 1)

Tactic:
Nat.cast_lt

Goal state after:
n : ℕ
IH : preOmega ↑n = ↑n
⊢ n < n + 1
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.Countable ↔ #↑s < ℵ_ 1

Tactic:
lt_aleph_one_iff,

Goal state after:
α : Type u_1
s : Set α
⊢ s.Countable ↔ #↑s ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
by_cases h2a : a = 0

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

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

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

Tactic:
apply le_antisymm
  · rw [← h]
    apply self_le_add_left
  rw [← not_lt]; intro hb
  have : a + b < c := add_lt_of_lt hc ha hb
  simp [h] at this

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

Goal state before:
pp: case refine_2.inl
a b : Cardinal.{u_1}
h1 : ℵ₀ ≤ a
h2 : b ≤ a
⊢ a + b = a

Tactic:
rw [add_eq_max h1, max_eq_left h2]

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
⊢ o.cof.ord = a

Tactic:
apply hf.le_ord_cof.antisymm'
  rw [← hf.iSup_add_one_eq, cof_iSup_Iio_add_one hf.strictMono]
  exact ord_cof_le a

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

Goal state before:
pp: case pos
ι : Type u
f : ι → Ordinal.{v}
n : ℕ
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} ↑n
hf : ∀ (i : ι), (f i).card ≤ ↑n
hc : ↑n < ℵ₀
⊢ ⨆ i, f i ≤ ↑n

Tactic:
refine ciSup_le' fun i ↦ ?_

Goal state after:
case pos
ι : Type u
f : ι → Ordinal.{v}
n : ℕ
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} ↑n
hf : ∀ (i : ι), (f i).card ≤ ↑n
hc : ↑n < ℵ₀
i : ι
⊢ f i ≤ ↑n
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:
rw [← 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.Cofinality.Ordinal

Goal state before:
pp: s : Set Cardinal.{u}
a : Cardinal.{u}
ha : #↑s < (Cardinal.lift.{u + 1, u} a).ord.cof
hs : ∀ i ∈ s, i < a
⊢ sSup s < a

Tactic:
by
  rw [← ord_lt_ord, sSup_ord]
  apply Ordinal.sSup_lt_of_lt_cof
  · simpa [mk_image_eq ord_injective]
  · simpa

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

Goal state before:
pp: case refine_2
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #↑S = Order.cof o.ToType
f : ↑S → Ordinal.{u} := fun s ↦ (typein LT.lt).toRelEmbedding ↑s
⊢ o.cof ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}

Tactic:
refine ⟨S, f, le_antisymm (lsub_le fun i => typein_lt_self (o := o) i)
      (le_of_forall_lt fun a ha => ?_), by rwa [cof_toType] at hS'⟩

Goal state after:
case refine_2
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #↑S = Order.cof o.ToType
f : ↑S → Ordinal.{u} := fun s ↦ (typein LT.lt).toRelEmbedding ↑s
a : Ordinal.{u}
ha : a < o
⊢ a < lsub f
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_2
o : Ordinal.{u}
⊢ o.cof ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}

Tactic:
rcases Order.cof_eq (α := o.ToType) with ⟨S, hS, hS'⟩
    let f : S → Ordinal := fun s => typein LT.lt s.val
    refine ⟨S, f, le_antisymm (lsub_le fun i => typein_lt_self (o := o) i)
      (le_of_forall_lt fun a ha => ?_), by rwa [cof_toType] at hS'⟩
    rw [← type_toType o] at ha
    rcases hS (enum (· < ·) ⟨a, ha⟩) with ⟨b, hb, hb'⟩
    rw [← not_lt, ← typein_le_typein, typein_enum] at hb'
    exact hb'.trans_lt (lt_lsub.{u, u} f ⟨b, hb⟩)

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ iSup f < c

Tactic:
apply lift_iSup_lt_of_lt_cof _ hf
  rwa [Cardinal.lift_umax, lift_id']

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:
by
  apply lt_imp_lt_of_le_imp_le (power_le_power_left <| power_ne_zero a hb.ne_bot)
  rw [← power_mul, mul_eq_self ha]
  exact lt_power_cof_ord (ha.trans <| (cantor' _ hb).le)

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

Goal state before:
pp: case neg
ι : 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 : ι
a✝ : i ∈ s.toFinset
h : ¬{ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i ≠ 0
⊢ (φ i) ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i) = 0

Tactic:
rw [not_not.mp h, map_zero]

Goal state after:
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
p : ι → Submodule R N
x : N
⊢ x ∈ iSup p ↔ ∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi ↦ xi) = x

Tactic:
rw [mem_iSup_iff_exists_dfinsupp']

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
x : N
⊢ (∃ f, (f.sum fun x xi ↦ ↑xi) = x) ↔ ∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi ↦ xi) = x
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![-x, y] ↔ LinearIndependent R ![x, y]

Tactic:
rw [pair_iff, pair_iff]
  refine ⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩ <;> simpa using h (-s) t (by simpa using hst)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝² : Monoid S
inst✝¹ : Semiring R
inst✝ : DistribMulAction S R
f : M → N
s : S
x : R[M]
⊢ mapDomain f (s • x) = s • mapDomain f x

Tactic:
by
  ext; simp [Finsupp.mapDomain_smul]

Goal state after:
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
⊢ a ∈ ↑s ∧ b ∈ ↑t ↔ a ∈ s ∧ b ∈ t

Tactic:
mem_coe,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
b : β
hf : Injective2 f
⊢ a ∈ s ∧ b ∈ ↑t ↔ a ∈ s ∧ b ∈ t
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 β
⊢ image₂ f s t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
by
  contrapose!; exact image₂_nonempty_iff

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

Goal state before:
pp: ι : Type u_14
α : ι → Type u_15
β : ι → Type u_16
γ : ι → Type u_17
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → α i → β i → γ i
s : (i : ι) → Finset (α i)
t : (i : ι) → Finset (β i)
a✝ : (a : ι) → γ a
⊢ (a✝ ∈ piFinset fun i ↦ image₂ (f i) (s i) (t i)) ↔ a✝ ∈ image₂ (fun a b i ↦ f i (a i) (b i)) (piFinset s) (piFinset t)

Tactic:
simp only [mem_piFinset, mem_image₂, Classical.skolem, forall_and, funext_iff]

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

Goal state before:
pp: case neg
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
p : M × M
hps : p ∈ s
hp : p ∈ s → x.coeff p.1 ≠ 0 → y.coeff p.2 = 0
h1 : ¬x.coeff p.1 = 0
⊢ x.coeff p.1 * y.coeff p.2 = 0

Tactic:
rw [hp hps h1, mul_zero]

Goal state after: