mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ insert a ↑t = s

pp: case refine_2
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ (↑t).ncard = t.card

Tactic:
· simp [Set.ext_iff, hts]

Goal state after:
case refine_2
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ (↑t).ncard = t.card
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: case mk
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x : P
w✝ : c.Quotient
y : M
hy : (c.lift f H) (Quot.mk (⇑c.toSetoid) y) = x
⊢ x ∈ MonoidHom.mrange f

Tactic:
exact ⟨y, hy⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_5
N : ι → Type u_6
inst✝¹ : (i : ι) → AddCommGroup (N i)
inst✝ : (i : ι) → Module R (N i)
f : (i : ι) → M →ₗ[R] N i
p : Submodule R M
h : ∀ (i : ι), p ≤ (f i).ker
⊢ (LinearMap.pi fun i ↦ p.liftQ (f i) ⋯) = p.liftQ (LinearMap.pi f) ⋯

Tactic:
ext x i

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_5
N : ι → Type u_6
inst✝¹ : (i : ι) → AddCommGroup (N i)
inst✝ : (i : ι) → Module R (N i)
f : (i : ι) → M →ₗ[R] N i
p : Submodule R M
h : ∀ (i : ι), p ≤ (f i).ker
x : M
i : ι
⊢ ((LinearMap.pi fun i ↦ p.liftQ (f i) ⋯) ∘ₗ p.mkQ) x i = (p.liftQ (LinearMap.pi f) ⋯ ∘ₗ p.mkQ) x i
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ ↑(insert (succ b) (Ioc a b)) = ↑(Ioc a (succ b))

Tactic:
simpa using Set.insert_Ioc_right_eq_Ioc_succ_of_not_isMax h hb

Goal state after:
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 (fst R M M₂) (⊤.prod ⊤) = ⊤

Tactic:
prod_map_fst

Goal state after:
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₂
⊢ ⊤ = ⊤
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
g : ι →o α
⊢ partialSups f ≤ g ↔ f ≤ ⇑g

Tactic:
refine ⟨(le_partialSups f).trans, fun h ↦ ?_⟩
    convert! partialSups_mono h
    exact OrderHom.ext _ _ g.monotone.partialSups_eq.symm

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a + d + c ∈ Ioi (a + d)
⊢ a + d + c ∈ (fun x ↦ x + d) '' Ioi a

Tactic:
rw [mem_Ioi, add_right_comm, add_lt_add_iff_right] at h

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a < a + c
⊢ a + d + c ∈ (fun x ↦ x + d) '' Ioi a
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: δ : Type u_4
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k ∈ Ico m n, f k) * ∏ k ∈ range m, f k = ∏ k ∈ range n, f k

Tactic:
rw [mul_comm]

Goal state after:
δ : Type u_4
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k ∈ range m, f k) * ∏ k ∈ Ico m n, f k = ∏ k ∈ range n, f k
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ ↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 1, 0)]) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)

Tactic:
← coe_add,

Goal state after:
n : ℕ
⊢ ↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) + ↑[(n + 1, 0)] =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
⊢ a + b * a + (a * b + b * b) = a + b

Tactic:
hb.eq,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
⊢ a + b * a + (a * b + b) = a + b
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
⊢ b * b - a - (a - a) = b - a

Tactic:
hb.eq,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
⊢ b - a - (a - a) = b - a
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
⊢ span (range fun i ↦ Pi.single i 1) = ⊤

Tactic:
rw [_root_.eq_top_iff]

Goal state after:
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
⊢ ⊤ ≤ span (range fun i ↦ Pi.single i 1)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
⊢ span (range fun i ↦ Pi.single i 1) = ⊤

Tactic:
by
  rw [_root_.eq_top_iff]
  rintro x -
  induction x using Pi.single_induction with
  | zero => simp
  | add f g hf hg => exact Ideal.add_mem _ hf hg
  | single i r =>
      rw [show Pi.single i r = Pi.single i r * Pi.single i 1 by simp [← Pi.single_mul_left]]
      exact Ideal.mul_mem_left _ _ (Ideal.subset_span ⟨i, rfl⟩)

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht : t ∈ l
⊢ ∃ i, p' i ∧ s' i ⊆ t

Tactic:
rcases hl.mem_iff.1 ht with ⟨i, hi, ht⟩

Goal state after:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht✝ : t ∈ l
i : ι
hi : p i
ht : s i ⊆ t
⊢ ∃ i, p' i ∧ s' i ⊆ t
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
s : Set α
x✝ : s ∈ ⊥
⊢ m ⁻¹' ∅ ⊆ s

Tactic:
simp only [empty_subset, preimage_empty]

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

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

Tactic:
filter_upwards [h₀ s hs, h₁ s hs] with x hp₀ hp₁

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

Goal state before:
pp: α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst✝ : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ y, r x y
this : Nonempty β
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)

Tactic:
choose! f hf using fun x (hx : ∃ y, r x y) => hx

Goal state after:
α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst✝ : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ y, r x y
this : Nonempty β
f : α → β
hf : ∀ (x : α), (∃ y, r x y) → r x (f x)
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsLeftCancelMul β
⊢ IsLeftCancelMul α

Tactic:
let := e.mul

Goal state after:
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsLeftCancelMul β
this : Mul α := e.mul
⊢ IsLeftCancelMul α
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsRightCancelMul β
⊢ IsRightCancelMul α

Tactic:
let := e.mul

Goal state after:
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsRightCancelMul β
this : Mul α := e.mul
⊢ IsRightCancelMul α
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsCancelMul β
⊢ IsCancelMul α

Tactic:
let := e.mul

Goal state after:
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsCancelMul β
this : Mul α := e.mul
⊢ IsCancelMul α
Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst✝¹ : AddZeroClass B
inst✝ : DistribSMul M B
⊢ DistribSMul M A

Tactic:
by
  letI := e.addZeroClass
  exact {
    e.smulZeroClass M with
    smul_add := by simp [add_def, smul_def, smul_add]
  }

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : Ring α
inst✝⁵ : AddCommGroup β
inst✝⁴ : Module α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : IsOrderedAddMonoid α
inst✝ : IsOrderedAddMonoid β
h : ∀ (a : α), 0 ≤ a → ∀ (b : β), 0 ≤ b → 0 ≤ a • b
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
⊢ a₁ ≤ a₂ → a₁ • _b ≤ a₂ • _b

Tactic:
simpa [sub_nonneg, sub_smul] using (h (a₂ - a₁) · _ hb)

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
⊢ N (S.attach.sup f) ≤ M'

Tactic:
rw [← H]

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
⊢ N (S.attach.sup f) ≤ iSup ⇑N
Module: Mathlib.RingTheory.Finiteness.Basic

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

Tactic:
exact fun n _ => singleton_span_isCompactElement n

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
⊢ ∀ x ∈ {s, t}, DirSupClosedOn D x

Tactic:
simpa [hs]

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₁
⊢ ∀ (a₂ : Submodule R V), Module.Finite R ↥a₂ → Module.Finite R ↥(S₁ ⊔ a₂)

Tactic:
S₂

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
⊢ Module.Finite R ↥S₂ → Module.Finite R ↥(S₁ ⊔ S₂)
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
exact ⟨_, _, bfamilyOfFamily'_typein _ _ _⟩

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

Goal state before:
pp: s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
⊢ IsNormal (enumOrd s)

Tactic:
refine isNormal_iff.2 ⟨enumOrd_strictMono hs, fun o ho a ha ↦ ?_⟩
  trans ⨆ b : Iio o, enumOrd s b
  · refine enumOrd_le_of_forall_lt ?_ (fun b hb ↦ (enumOrd_strictMono hs (lt_succ b)).trans_le ?_)
    · have : Nonempty (Iio o) := ⟨0, ho.bot_lt⟩
      apply H _ _ (range_nonempty _) bddAbove_of_small
      rintro _ ⟨c, rfl⟩
      exact enumOrd_mem hs c
    · exact Ordinal.le_iSup _ (⟨_, ho.succ_lt hb⟩ : Iio o)
  · exact Ordinal.iSup_le fun x ↦ ha _ x.2

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

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

Tactic:
rw [← nonpos_iff_eq_zero, div_le h.ne_bot]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ b ^ (clog b x).pred < x

Tactic:
rw [← lt_clog_iff_pow_lt hb]
  exact pred_lt (clog_pos hb hx).ne'

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

Goal state before:
pp: ⊢ IsInitial 1

Tactic:
by
  exact_mod_cast isInitial_natCast 1

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

Goal state before:
pp: case mpr
x : Ordinal.{u_1}
⊢ x ∈ {x | ω ≤ x ∧ x.IsInitial} → x ∈ range ⇑ω_

Tactic:
rintro ⟨ha', ha⟩

Goal state after:
case mpr
x : Ordinal.{u_1}
ha' : ω ≤ x
ha : x.IsInitial
⊢ x ∈ range ⇑ω_
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : ℵ₀ ≤ max a b
⊢ max a b * max a b < c

Tactic:
rw [mul_eq_self h]

Goal state after:
case inr
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : ℵ₀ ≤ max a b
⊢ max a b < c
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
exact le_self_add

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

Goal state before:
pp: o : Ordinal.{u_1}
| o.cof

Tactic:
rw [← type_toType o, cof_type]

Goal state after:
o : Ordinal.{u_1}
| Order.cof o.ToType
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof = 0 ↔ o = 0

Tactic:
← cof_toType,

Goal state after:
o : Ordinal.{u_1}
⊢ Order.cof o.ToType = 0 ↔ o = 0
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ range ⇑ℵ_ = Ici ℵ₀

Tactic:
ext c
  refine ⟨fun ⟨o, e⟩ => e ▸ aleph0_le_aleph _, fun hc ↦ ⟨preAleph.symm c - ω, ?_⟩⟩
  rw [aleph_eq_preAleph, Ordinal.add_sub_cancel_of_le, preAleph.apply_symm_apply]
  rwa [← aleph0_le_preAleph, preAleph.apply_symm_apply]

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

Goal state before:
pp: a b : Ordinal.{u_1}
h : a < b
| preBeth b

Tactic:
rw [preBeth]

Goal state after:
a b : Ordinal.{u_1}
h : a < b
| ⨆ a, 2 ^ preBeth ↑a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preBeth 0 = 0

Tactic:
rw [preBeth]

Goal state after:
⊢ ⨆ a, 2 ^ preBeth ↑a = 0
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
rw [preBeth]

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ ⨆ a, 2 ^ preBeth ↑a = ⨆ a, preBeth ↑a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ a * b

Tactic:
rw [mul_comm]

Goal state after:
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ b * a
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
⊢ ⨆ i, f i + 1 < a

Tactic:
rw [iSup, range_comp' (· + 1)]
  apply sSup_add_one_lt_of_lt_cof _ (by simpa)
  rw [← Cardinal.lift_lt.{_, v}]
  apply mk_range_le_lift.trans_lt
  rw [← Cardinal.lift_lt.{_, u + 1}] at ha
  simpa [← lift_cof] using ha

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

Goal state before:
pp: a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ a.IsFundamentalSequence o' fun i hi ↦ f (g i hi) ⋯

Tactic:
by
  refine ⟨?_, @fun i j _ _ h => hf.2.1 _ _ (hg.2.1 _ _ h), ?_⟩
  · rw [hf.cof_eq]
    exact hg.1.trans (ord_cof_le o)
  · rw [@blsub_comp.{u, u, u} o _ f (@IsFundamentalSequence.monotone _ _ f hf)]
    · exact hf.2.2
    · exact hg.2.2

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

Goal state before:
pp: case refine_2
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
l : List ι
⊢ List.foldr f a l < c

Tactic:
induction l with
    | nil => exact ha
    | cons i l H => exact hf _ _ H

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

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a < ω_ o
hb : b < ω_ o
⊢ (fun x1 x2 ↦ x1 ^ x2) a b < ω_ o

Tactic:
lt_omega_iff_card_lt

Goal state after:
case inr
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < ℵ_ o
hb : b.card < ℵ_ o
⊢ ((fun x1 x2 ↦ x1 ^ x2) a b).card < ℵ_ o
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c.IsRegular ∨ ℵ₀ ≤ c ∧ c.ord.cof ≠ c

Tactic:
← (cof_ord_le c).lt_iff_ne,

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:
rw [isSingular_iff, ← (cof_ord_le _).lt_iff_ne]

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.SetTheory.Cardinal.Regular

Goal state before:
pp: case ind
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ preBeth a < c

Tactic:
rw [preBeth]

Goal state after:
case ind
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ ⨆ a_1, 2 ^ preBeth ↑a_1 < c
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case mk
ι : 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 ∈ (↑⟨s, hf⟩).toFinset, (φ i) ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i) =
    ∑ a ∈ (↑⟨s, hf⟩).toFinset,
      if { toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } a ≠ 0 then
        (fun x ↦ ⇑(φ x)) a ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } a)
      else 0

Tactic:
Finset.sum_congr rfl

Goal state after:
case mk
ι : 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
⊢ (↑⟨s, hf⟩).toFinset.sum ?m.88 =
    ∑ a ∈ (↑⟨s, hf⟩).toFinset,
      if { toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } a ≠ 0 then
        (fun x ↦ ⇑(φ x)) a ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } a)
      else 0

case mk
ι : 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
⊢ ∀ x ∈ (↑⟨s, hf⟩).toFinset, (φ x) ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } x) = ?m.88 x

ι : 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
⊢ ι → γ
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₂ i
⊢ mapRange (fun i ↦ (fun x ↦ (e i) x) ∘ fun x ↦ (e i).symm x) ?h x = x

Tactic:
simp_rw [AddEquiv.self_comp_symm]
          simp

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

Goal state before:
pp: case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₂ i
⊢ ∀ (i : ι), ((fun x ↦ (e i) x) ∘ fun x ↦ (e i).symm x) 0 = 0

Tactic:
simp_rw [AddEquiv.self_comp_symm]
          simp

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
⊢ ∃ s, LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t

Tactic:
let indep : Set ι → Prop := fun s => LinearIndepOn R v s
  let X := { I : Set ι // indep I }
  let r : X → X → Prop := fun I J => I.1 ⊆ J.1
  have key : ∀ c : Set X, IsChain r c → indep (⋃ (I : X) (_ : I ∈ c), I) := by
    intro c hc
    dsimp [indep]
    rw [linearIndepOn_iffₛ]
    intro f hfsupp g hgsupp hsum
    rcases eq_empty_or_nonempty c with (rfl | hn)
    · rw [show f = 0 by simpa using! hfsupp, show g = 0 by simpa using! hgsupp]
    have : Std.Refl r := ⟨fun _ => Set.Subset.refl _⟩
    classical
    obtain ⟨I, _I_mem, hI⟩ : ∃ I ∈ c, (f.support ∪ g.support : Set ι) ⊆ I :=
      f.support.coe_union _ ▸ hc.directedOn.exists_mem_subset_of_finset_subset_biUnion hn <| by
        simpa using! And.intro hfsupp hgsupp
    exact linearIndepOn_iffₛ.mp I.2 f (subset_union_left.trans hI)
      g (subset_union_right.trans hI) hsum
  obtain ⟨⟨I, hli : indep I⟩, hmax : ∀ a, r ⟨I, hli⟩ a → r a ⟨I, hli⟩⟩ :=
    exists_maximal_of_chains_bounded (r := r)
      (fun c hc => ⟨⟨⋃ I ∈ c, (I : Set ι), key c hc⟩, fun I => Set.subset_biUnion_of_mem⟩)
      Set.Subset.trans
  exact ⟨I, hli, fun J hsub hli => Set.Subset.antisymm hsub (hmax ⟨J, hli⟩ hsub)⟩

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ (mapDomainRingHom R ↑e).comp (mapDomainRingHom R ↑e.symm) = RingHom.id R[N]

Tactic:
apply MonoidAlgebra.ringHom_ext <;> simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ (mapDomainRingHom R ↑e.symm).comp (mapDomainRingHom R ↑e) = RingHom.id R[M]

Tactic:
apply MonoidAlgebra.ringHom_ext <;> simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ (mapRingHom M ↑e).comp (mapRingHom M ↑e.symm) = RingHom.id S[M]

Tactic:
apply MonoidAlgebra.ringHom_ext <;> simp

Goal state after: