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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ ∃ j ≤ i, (partialSups f) i = f j

Tactic:
use j, hj_mem

Goal state after:
case right
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ (partialSups f) i = f j
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝¹ : CancelMonoid A
inst✝ : HasMulAntidiagonal A
p q : A × A
n : A
hp : p ∈ mulAntidiagonal n
hq : q ∈ mulAntidiagonal n
h : p.1 = q.1
⊢ q.1 * p.2 = q.1 * q.2

Tactic:
rw [mem_mulAntidiagonal] at hp hq

Goal state after:
A : Type u_1
inst✝¹ : CancelMonoid A
inst✝ : HasMulAntidiagonal A
p q : A × A
n : A
hp : p.1 * p.2 = n
hq : q.1 * q.2 = n
h : p.1 = q.1
⊢ q.1 * p.2 = q.1 * q.2
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
⊢ mulAntidiagonal 1 = {(1, 1)}

Tactic:
by
  ext ⟨x, y⟩
  simp

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: case mpr
A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n a : A
inst✝¹ : DecidablePred fun x ↦ x = a
inst✝ : Decidable (a ≤ n)
h : a ≤ n
⊢ a + (n - a) = n

Tactic:
exact add_tsub_cancel_of_le h

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
⊢ ∃ g ≤ f, univ.sup g = univ.sup f ∧ Pairwise (Disjoint on g)

Tactic:
let R : ι ≃ Fin _ := equivFin ι

Goal state after:
case inr
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
⊢ ∃ g ≤ f, univ.sup g = univ.sup f ∧ Pairwise (Disjoint on g)
Module: Mathlib.Algebra.BigOperators.Intervals

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

Tactic:
rw [prod_Ico_eq_div _ hmn, prod_range_div, prod_range_div, div_div_div_cancel_right]

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

Goal state before:
pp: n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (i, j) ∈ {a ∈ antidiagonal n | a.2 ≤ k} ↔
    (i, j) ∈ map ({ toFun := fun x ↦ x + (n - k), inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal k)

Tactic:
suffices i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i by simpa

Goal state after:
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : Finite ι
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
⊢ f x i ∈ I

Tactic:
by
  classical
    cases nonempty_fintype ι
    rw [pi_eq_sum_univ x]
    simp only [Finset.sum_apply, smul_eq_mul, map_sum, Pi.smul_apply, map_smul]
    exact I.sum_mem fun j _ => I.mul_mem_right _ (hi j)

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

Goal state before:
pp: case a
α : Type u_1
B : FilterBasis α
⊢ B.sets ⊆ B.filter.sets

Tactic:
apply mem_filter_of_mem

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
x✝ : s ∈ comap f l
t : Set β
ht : t ∈ l
hts : f ⁻¹' t ⊆ s
y : β
hy : y ∈ t
x : α
hx : f x = y
⊢ f x ∈ t

Tactic:
by rwa [hx]

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

Goal state before:
pp: α : Type u
f g : Filter α
⊢ f ⊓ g = ⊥ ↔ ∃ U ∈ f, ∃ V ∈ g, U ∩ V = ∅

Tactic:
by
  simp only [← disjoint_iff, Filter.disjoint_iff, Set.disjoint_iff_inter_eq_empty]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
la : Filter α
lb : Filter β
h : la.NeBot → Tendsto f la lb
hla : la.NeBot
⊢ Tendsto f la lb

Tactic:
· exact h hla

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:
simp_rw [iInf_subtype', mem_iInf_of_directed h.directed_val, Subtype.exists, exists_prop]

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

Goal state before:
pp: α : Type u_1
f g : Filter α
⊢ (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in g, p x

Tactic:
simp only [inf_neBot_iff, frequently_iff, and_comm]; rfl

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) → ∀ B ∈ F, f x ∈ B

Tactic:
intro h U U_in

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A
U : Set β
U_in : U ∈ F
⊢ f x ∈ U
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
⊢ a • b₁ ≤ a • b₂

Tactic:
by
    obtain ha | ha := ha.eq_or_lt
    · simp [← ha]
    · exact h₀ _ ha _ _ h

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α✝ : Type u_1
s✝ t✝ : Set α✝
D✝ : Set (Set α✝)
inst✝¹ : Preorder α✝
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s)
⊢ a ∈ s ∪ t

Tactic:
obtain ⟨hds, hcof⟩ := h

Goal state after:
α✝ : Type u_1
s✝ t✝ : Set α✝
D✝ : Set (Set α✝)
inst✝¹ : Preorder α✝
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s)
hcof : IsCofinalFor (d ∩ t) (d ∩ s)
⊢ a ∈ s ∪ t
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
⊢ typeLT Ordinal.{u_2} ≤ (cof Ordinal.{u_2}).ord

Tactic:
rw [type_lt_ordinal, ← ord_univ, ord_le_ord, le_cof_iff]
    intro s hs
    contrapose! hs
    rw [← Cardinal.lift_id (#s), ← small_iff_lift_mk_lt_univ] at hs
    rw [not_isCofinal_iff_bddAbove]
    exact Ordinal.bddAbove_of_small

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

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a - b ≠ 0 ↔ b < a

Tactic:
simpa using Ordinal.sub_eq_zero_iff_le.not

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

Goal state before:
pp: case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≼i s)
f : r ≼i s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≼i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r

Tactic:
· exact (RelIso.preimage Equiv.ulift r).toInitialSeg.trans
      (f.trans (RelIso.preimage Equiv.ulift s).symm.toInitialSeg)

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
h : iSup f = 0
i : ι
⊢ f i = 0

Tactic:
← nonpos_iff_eq_zero,

Goal state after:
ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
h : iSup f = 0
i : ι
⊢ f i ≤ 0
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
⊢ a ≤ b + a

Tactic:
simpa using add_le_add_left bot_le a

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

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
h : o.bsup f = 0
i : Ordinal.{u_3}
hi : i < o
⊢ f i hi = 0

Tactic:
← nonpos_iff_eq_zero,

Goal state after:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
h : o.bsup f = 0
i : Ordinal.{u_3}
hi : i < o
⊢ f i hi ≤ 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : IsSuccLimit b
⊢ a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c

Tactic:
by
  refine ⟨fun h _ l ↦ (mul_le_mul_right l.le _).trans h, fun H ↦ le_of_not_gt ?_⟩
  induction a, b using inductionOn₂ with | type α r β s
  exact mul_le_of_limit_aux h H

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

Goal state before:
pp: ι : Type u_3
h : IsEmpty ι
f : ι → Ordinal.{max u_4 u_3}
⊢ lsub f = 0

Tactic:
← nonpos_iff_eq_zero,

Goal state after:
ι : Type u_3
h : IsEmpty ι
f : ι → Ordinal.{max u_4 u_3}
⊢ lsub f ≤ 0
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
h : IsEmpty ι
f : ι → Ordinal.{max u_4 u_3}
⊢ lsub f = 0

Tactic:
by
  rw [← nonpos_iff_eq_zero, lsub_le_iff]
  exact h.elim

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

Goal state before:
pp: b n : ℕ
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1

Tactic:
rcases Nat.lt_or_ge 1 b with hb | hb

Goal state after:
case inl
b n : ℕ
hb : 1 < b
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1

case inr
b n : ℕ
hb : 1 ≥ b
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
a b : Ordinal.{u_4}
h : a ≤ b
⊢ a / 0 ≤ b / 0

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

Tactic:
· rw [div_zero, div_zero]

Goal state after:
case inr
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / c ≤ b / c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
h : a < b
⊢ a / b = 0

Tactic:
← nonpos_iff_eq_zero,

Goal state after:
a b : Ordinal.{u_4}
h : a < b
⊢ a / b ≤ 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
hy : y ≠ 0
⊢ x ≤ log b y

pp: case inr
b x : ℕ
hb : 1 < b
h : b ^ x ≤ 0
⊢ x ≤ log b 0

Tactic:
exacts [(le_log_iff_pow_le hb hy).2 h, (h.not_gt (Nat.pow_pos (Nat.zero_lt_one.trans hb))).elim]

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

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

Tactic:
rw [log_of_left_le_one hb, log_of_left_le_one hb]

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

Goal state before:
pp: case inr.inr
b k n : ℕ
hn : n ≠ 0
hk : k > 0
⊢ log (b ^ k) n = log b n / k

Tactic:
rcases Nat.lt_or_ge 1 b with hb | hb

Goal state after:
case inr.inr.inl
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
⊢ log (b ^ k) n = log b n / k

case inr.inr.inr
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ log (b ^ k) n = log b n / k
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
have : Fintype <| Iio x := Nat.fintypeIio x

Goal state after:
x : ℕ
this : Fintype ↑(Iio x)
⊢ (typein LT.lt).toRelEmbedding x = ↑x
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b x y : ℕ
h : x ≤ b ^ y
⊢ clog b x ≤ y

Tactic:
rcases Nat.lt_or_ge 1 b with hb | hb

Goal state after:
case inl
b x y : ℕ
h : x ≤ b ^ y
hb : 1 < b
⊢ clog b x ≤ y

case inr
b x y : ℕ
h : x ≤ b ^ y
hb : 1 ≥ b
⊢ clog b x ≤ y
Module: Mathlib.Data.Nat.Log

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

Tactic:
rcases Nat.lt_or_ge 1 b with hb | hb

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

case inr.inr
b k n : ℕ
hk : k > 0
hb : 1 ≥ b
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b x : Ordinal.{u_1}
hx : 1 ≤ x
hb : b ≤ 1
⊢ b ^ log b x ≤ x

Tactic:
obtain rfl | rfl := le_one_iff.1 hb <;> simpa

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

Goal state before:
pp: case inr.inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ log b o = 0

Tactic:
← nonpos_iff_eq_zero,

Goal state after:
case inr.inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ log b o ≤ 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inr
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
hb : b ≤ 1
⊢ log b x ≤ log b y

Tactic:
rw [log_of_left_le_one hb, log_of_left_le_one hb]

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

Goal state before:
pp: o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ ¬IsPrincipal op o ↔ ∃ a < o, ∃ b < o, o ≤ op a b

Tactic:
simp [IsPrincipal]

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

Goal state before:
pp: b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ (u + log b v) ≤ b ^ u * v + w ∧ b ^ u * v + w < b ^ (u + log b v + 1)

pp: case hx
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v + w ≠ 0

Tactic:
· constructor
    · grw [opow_add, opow_log_le_self b hv, ← le_self_add]
    · grw [hw, ← mul_add_one, add_assoc, opow_add]
      gcongr
      rw [add_one_le_iff]
      exact lt_opow_succ_log_self hb _

Goal state after:
case hx
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v + w ≠ 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 0 < o / b ^ log b o

Tactic:
rcases eq_zero_or_pos b with (rfl | hb)

Goal state after:
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 0 < o / 0 ^ log 0 o

case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ 0 < o / b ^ log b o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
⊢ IsPrincipal op 0

Tactic:
simp [IsPrincipal]

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

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
⊢ IsPrincipal op 1 ↔ op 0 0 = 0

Tactic:
simp [IsPrincipal]

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

Goal state before:
pp: a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ a < ω ^ ω ^ b ↔ ∃ c < b, ∃ n, a < ω ^ (ω ^ c * ↑n)

Tactic:
simp_rw [lt_omega0_opow (opow_ne_zero _ omega0_ne_zero), lt_omega0_opow hb]

Goal state after:
a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ (∃ c, (∃ c_1 < b, ∃ n, c < ω ^ c_1 * ↑n) ∧ ∃ n, a < ω ^ c * ↑n) ↔ ∃ c < b, ∃ n, a < ω ^ (ω ^ c * ↑n)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
⊢ nfp (fun x ↦ a * x) 0 = 0

Tactic:
← nonpos_iff_eq_zero,

Goal state after:
a : Ordinal.{u_1}
⊢ nfp (fun x ↦ a * x) 0 ≤ 0
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case isSuccPrelimit
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
⊢ ⨆ i, lift.{v, u_1} (preBeth ↑i) = ⨆ a, preBeth ↑a

Tactic:
apply congrArg sSup

Goal state after:
case isSuccPrelimit
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
⊢ (range fun i ↦ lift.{v, u_1} (preBeth ↑i)) = range fun a ↦ preBeth ↑a
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:
← iSup_Iio_add_one hf.strictMono,

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

a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
ha : 1 < a
⊢ IsSuccPrelimit a
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) c.ord

Tactic:
by
  intro a b ha hb
  rw [lt_ord, card_add] at *
  exact add_lt_of_lt hc ha hb

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

Goal state before:
pp: o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o

Tactic:
rw [← h.ord_card]

Goal state after:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o.card.ord
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) o

Tactic:
rw [← h.ord_card]

Goal state after:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) o.card.ord
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) o.card.ord

Tactic:
apply isPrincipal_mul_ord

Goal state after:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ ℵ₀ ≤ o.card
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
exact le_max_of_le_right (power_lt_aleph0 hc natCast_lt_aleph0).le

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

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

Tactic:
intro f
    use Sum.inl ⁻¹' range f
    refine le_trans (mk_preimage_of_injective _ _ fun x y => Sum.inl.inj) ?_
    apply mk_range_le

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

Goal state before:
pp: ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, (sumAddHom fun i ↦ (S i).subtype) f = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x

Tactic:
simp_rw [sumAddHom_apply]

Goal state after:
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, (f.sum fun x ↦ ⇑(S x).subtype) = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : ⟨i, xi⟩ = ⟨j, xj⟩
⊢ single i xi = single j xj

Tactic:
cases h
  rfl

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

Goal state before:
pp: case mk.mk.e_a
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
⊢ ∑ x ∈ (sf + sg).toFinset, (φ x) (f x) = ∑ x ∈ sf.toFinset, (φ x) (f x)

pp: case mk.mk.e_a
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
⊢ ∑ x ∈ (sf + sg).toFinset, (φ x) (g x) = ∑ x ∈ sg.toFinset, (φ x) (g x)

Tactic:
· refine (Finset.sum_subset ?_ ?_).symm
      · intro i
        simp only [Multiset.mem_toFinset, Multiset.mem_add]
        exact Or.inl
      · intro i _ H2
        simp only [Multiset.mem_toFinset] at H2
        rw [(hf i).resolve_left H2, map_zero]

Goal state after:
case mk.mk.e_a
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
⊢ ∑ x ∈ (sf + sg).toFinset, (φ x) (g x) = ∑ x ∈ sg.toFinset, (φ x) (g x)
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
i : ι
y : N
hy : y ∈ p i
⊢ y ∈ ((lsum ℕ) fun i ↦ (p i).subtype).range

Tactic:
simp only [LinearMap.mem_range, lsum_apply_apply]

Goal state after:
ι : 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
i : ι
y : N
hy : y ∈ p i
⊢ ∃ y_1, (sumAddHom fun i ↦ (p i).subtype.toAddMonoidHom) y_1 = y
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
i : ι
hi : p i
y : N
hy : y ∈ S i
⊢ ((lsum ℕ) fun i ↦ (S i).subtype) ((filterLinearMap R (fun i ↦ ↥(S i)) p) (single i ⟨y, hy⟩)) = y

Tactic:
filterLinearMap_apply,

Goal state after:
case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
i : ι
hi : p i
y : N
hy : y ∈ S i
⊢ ((lsum ℕ) fun i ↦ (S i).subtype) (filter p (single i ⟨y, hy⟩)) = y
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: case mp
R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝¹¹ : AddCommMonoid Mₗ
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid Pₗ
inst✝⁸ : AddCommMonoid Qₗ
inst✝⁷ : AddCommMonoid Qₗ'
inst✝⁶ : Module R₁ Mₗ
inst✝⁵ : Module R₂ N
inst✝⁴ : Module R₂ Pₗ
inst✝³ : Module R₁ Pₗ
inst✝² : Module R₁ Qₗ
inst✝¹ : Module R₂ Qₗ'
inst✝ : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
x' : Qₗ
y' : Qₗ'
⊢ (f₁ (g x')) (g' y') = (f₂ (g x')) (g' y')

Tactic:
convert! LinearMap.congr_fun₂ h x' y' using 0

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mp
ι : 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
⊢ (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0) →
    ∀ (s : Finset ι) (v w : ι → N), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i

Tactic:
intro h s v w hvw
    simpa [sub_eq_zero] using h s (v - w) fun i hi => (p i).sub_mem (hvw i hi).1 (hvw i hi).2

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
    exact fun t₁ t₂ ht => iUnion_mono fun i => iUnion_subset_iUnion_const fun h => ht h

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
a : α
inst✝ : DecidableEq β
t₁ t₂ : Finset β
hf : Injective (f a)
⊢ image₂ f {a} (t₁ ∩ t₂) = image₂ f {a} t₁ ∩ image₂ f {a} t₂

Tactic:
by
  simp_rw [image₂_singleton_left, image_inter _ _ hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
f : α → β → γ
g : γ → δ
⊢ ↑(image g (image₂ f s t)) = ↑(image₂ (fun a b ↦ g (f a b)) s t)

Tactic:
by
    push_cast
    exact image_image2 _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst✝ : DecidableEq β
h : s.Nonempty
⊢ image2 (fun x y ↦ y) ↑s ↑t = ↑t

Tactic:
exact image2_right h

Goal state after: