mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
x : ℕ
hx : x ∈ Ioc m n
⊢ x ∈ Ioc n k → False

Tactic:
h'x

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
x : ℕ
hx : x ∈ Ioc m n
h'x : x ∈ Ioc n k
⊢ False
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
⊢ ∏ k ∈ Ioc a (b + 1), f k = (∏ k ∈ Ioc a b, f k) * f (b + 1)

Tactic:
by
  rw [← prod_Ioc_consecutive _ hab (Nat.le_succ b), Nat.Ioc_succ_singleton, prod_singleton]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: n : ℕ
⊢ (∏ k ∈ Ico (succ 0) n.succ, k) * n.succ = (n + 1)!

Tactic:
Nat.factorial_succ,

Goal state after:
n : ℕ
⊢ (∏ k ∈ Ico (succ 0) n.succ, k) * n.succ = (n + 1) * n !
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (↑(List.Nat.antidiagonal n)).card = n + 1

Tactic:
coe_card,

Goal state after:
n : ℕ
⊢ (List.Nat.antidiagonal n).length = n + 1
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
⊢ r ∈ I → r ∈ ⊥

Tactic:
hr

Goal state after:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
⊢ r ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : x ∈ (LinearMap.toSpanSingleton R R e).ker
⊢ x * 1 - x * e = x

Tactic:
show x * e = 0 from h,

Goal state after:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : x ∈ (LinearMap.toSpanSingleton R R e).ker
⊢ x * 1 - 0 = x
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
⊢ (quotEquivOfEq h).symm = quotEquivOfEq ⋯

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : c ∈ I
abc : c = 1 - b * a
⊢ b * a - 1 ∈ I

Tactic:
abc,

Goal state after:
case mk
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : 1 - b * a ∈ I
abc : c = 1 - b * a
⊢ b * a - 1 ∈ I
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ map f ⊤ = 𝓟 (range f)

Tactic:
rw [← principal_univ, map_principal, image_univ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
ι' : Sort u_5
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hla : la.HasBasis pa sa
hlb : lb.HasBasis pb sb
⊢ Tendsto f la lb ↔ ∀ (ib : ι'), pb ib → ∃ ia, pa ia ∧ ∀ x ∈ sa ia, f x ∈ sb ib

Tactic:
simp [hlb.tendsto_right_iff, hla.eventually_iff]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
R : Type u_4
inst✝³ : Zero R
inst✝² : Zero β
inst✝¹ : SMul R β
inst✝ : NoZeroSMulDivisors R β
⊢ let this := e.zero;
  let this_1 := Equiv.smul R e;
  NoZeroSMulDivisors R α

Tactic:
by
  extract_lets
  refine ⟨fun {r} m ↦ ?_⟩
  simpa [smul_def, zero_def, Equiv.eq_symm_apply] using eq_zero_or_eq_zero_of_smul_eq_zero

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α < β
⊢ α.ToType <i β.ToType

Tactic:
apply Classical.choice (type_lt_iff.mp _)

Goal state after:
α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α < β
⊢ typeLT α.ToType < typeLT β.ToType
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: case h
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) := ⋯
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b : α
hb : ∀ b_1 < a, (Subtype.val ∘ ⇑(enum s hs)) b_1 ≤ b
⊢ ↑((enum s hs) a) ∈ upperBounds (Subtype.val ∘ ⇑(enum s hs) '' Iio a)

Tactic:
simpa [upperBounds] using fun x hx ↦ hx.le

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

Goal state before:
pp: case mpr
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
f : α ↪ { α := β, r := s, wo := x✝ }.α
g : ⇑f ⁻¹'o s ↪r s
⊢ (#α).ord ≤ type s

Tactic:
have := RelEmbedding.isWellOrder g

Goal state after:
case mpr
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
f : α ↪ { α := β, r := s, wo := x✝ }.α
g : ⇑f ⁻¹'o s ↪r s
this : IsWellOrder α (⇑f ⁻¹'o s)
⊢ (#α).ord ≤ type s
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_1
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : succ (o.bsup f) ≤ o.blsub f
⊢ ∃ i, ∃ (hi : i < o), f i hi = o.bsup f

Tactic:
by_contra! hf
    exact
      ne_of_lt (succ_le_iff.1 h)
        (le_antisymm (bsup_le_blsub f) (blsub_le (lt_bsup_of_ne_bsup.1 hf)))

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

Goal state before:
pp: o : Ordinal.{u_1}
ι : Sort u_2
f : ι → Ordinal.{u_1}
⊢ o * sSup (range fun i ↦ f i) = ⨆ i, o * f i

Tactic:
mul_sSup,

Goal state after:
o : Ordinal.{u_1}
ι : Sort u_2
f : ι → Ordinal.{u_1}
⊢ sSup ((fun x ↦ o * x) '' range fun i ↦ f i) = ⨆ i, o * f i
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
⊢ log2 0 = log 2 0

Tactic:
log2_zero,

Goal state after:
case inl
⊢ 0 = log 2 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case left
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

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

Tactic:
· grw [opow_add, opow_log_le_self b hv, ← le_self_add]

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

Goal state before:
pp: a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = ↑n
⊢ ∃ n, a < ω ^ log ω a * ↑n

Tactic:
use n + 1

Goal state after:
case h
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = ↑n
⊢ a < ω ^ log ω a * ↑(n + 1)
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inl
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ ∃ n, op a b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o

Tactic:
use n + 1

Goal state after:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ op a b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n + 1] o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1.inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
⊢ a + o = o

Tactic:
· cases le_one_iff.1 ho₁ <;> simp_all

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

Goal state before:
pp: a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ b + c
hab : a - b = a
⊢ False

Tactic:
← sub_le,

Goal state after:
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a - b ≤ c
hab : a - b = a
⊢ False
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case mp
o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o → o = 0 ∨ o ∈ Set.range fun x ↦ ω ^ x

Tactic:
rw [or_iff_not_imp_left]
    refine fun H ho ↦ ⟨log ω o, (opow_log_le_self ω ho).eq_of_not_lt ?_⟩
    obtain ⟨n, hn⟩ := lt_omega0_opow_succ.1 (lt_opow_succ_log_self one_lt_omega0 o)
    exact fun h ↦ hn.not_gt <| H.mul_natCast_lt h n

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

Goal state before:
pp: case mp
o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o → o = 0 ∨ o ∈ Set.range fun x ↦ ω ^ x

pp: case mpr
o : Ordinal.{u}
⊢ (o = 0 ∨ o ∈ Set.range fun x ↦ ω ^ x) → IsPrincipal (fun x1 x2 ↦ x1 + x2) o

Tactic:
· rw [or_iff_not_imp_left]
    refine fun H ho ↦ ⟨log ω o, (opow_log_le_self ω ho).eq_of_not_lt ?_⟩
    obtain ⟨n, hn⟩ := lt_omega0_opow_succ.1 (lt_opow_succ_log_self one_lt_omega0 o)
    exact fun h ↦ hn.not_gt <| H.mul_natCast_lt h n

Goal state after:
case mpr
o : Ordinal.{u}
⊢ (o = 0 ∨ o ∈ Set.range fun x ↦ ω ^ x) → IsPrincipal (fun x1 x2 ↦ x1 + x2) o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ preOmega o = preOmega (ω + o)

Tactic:
add_of_omega0_opow_le _ ho

Goal state after:
o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ preOmega o = preOmega o

o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ ω < ω ^ ↑2
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: x o : Ordinal.{u_1}
⊢ x.card < (ω_ o).card ↔ x.card < ℵ_ o

Tactic:
card_omega

Goal state after:
x o : Ordinal.{u_1}
⊢ x.card < ℵ_ o ↔ x.card < ℵ_ o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ ≤ o.cof ↔ IsSuccLimit o

Tactic:
aleph0_le_cof_iff,

Goal state after:
o : Ordinal.{u_1}
⊢ 1 < o.cof ↔ IsSuccLimit o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < ω_ 1
⊢ ℵ₀ ≤ o.cof

Tactic:
aleph0_le_cof_iff,

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < ω_ 1
⊢ 1 < o.cof
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)
⊢ lift.{v, u_1} (⨆ a, preBeth ↑a) = ⨆ a, preBeth ↑a

Tactic:
lift_iSup bddAbove_of_small

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)
⊢ ⨆ i, lift.{v, u_1} (preBeth ↑i) = ⨆ a, preBeth ↑a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ preBeth o = preBeth (ω + o)

Tactic:
add_of_omega0_opow_le _ ho

Goal state after:
o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ preBeth o = preBeth o

o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ ω < ω ^ ↑2
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_2.inr
a : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) ((fun x ↦ ω ^ ω ^ x) a)

Tactic:
exact isPrincipal_mul_omega0_opow_opow a

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

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

Tactic:
have : a < b := ha.trans_le hb
    rw [add_eq_right hb this.le, eq_comm] at h
    rw [eq_of_add_eq_of_aleph0_le h this hb]

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
ha : 1 < a
⊢ ℵ₀ ≤ o.cof

Tactic:
aleph0_le_cof_iff,

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

Goal state before:
pp: ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ lift.{u, v} (⨆ i, f i)
⊢ sum f = lift.{u, v} (⨆ i, f i)

Tactic:
lift_iSup bddAbove_of_small

Goal state after:
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, lift.{u, v} (f i)
⊢ sum f = lift.{u, v} (⨆ i, f i)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case e'_4
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, lift.{u, v} (f i)
⊢ lift.{u, v} (⨆ i, f i) = ⨆ i, lift.{u, v} (f i)

Tactic:
lift_iSup bddAbove_of_small

Goal state after:
case e'_4
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, lift.{u, v} (f i)
⊢ ⨆ i, lift.{u, v} (f i) = ⨆ i, lift.{u, v} (f i)
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_1
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
⊢ type r ≤ (#ι).ord

Tactic:
hr

Goal state after:
case refine_1
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
⊢ type r ≤ type r
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a : Ordinal.{u}
⊢ ∃ f, a.IsFundamentalSequence a.cof.ord f

Tactic:
by
  suffices h : ∃ o f, IsFundamentalSequence a o f by
    rcases h with ⟨o, f, hf⟩
    exact ⟨_, hf.ord_cof⟩
  rcases exists_lsub_cof a with ⟨ι, f, hf, hι⟩
  rcases ord_eq ι with ⟨r, wo, hr⟩
  let r' := Subrel r fun i ↦ ∀ j, r j i → f j < f i
  let hrr' : r' ↪r r := Subrel.relEmbedding _ _
  have := hrr'.isWellOrder
  refine
    ⟨_, _, hrr'.ordinal_type_le.trans ?_, @fun i j _ h _ => (enum r' ⟨j, h⟩).prop _ ?_,
      le_antisymm (blsub_le fun i hi => lsub_le_iff.1 hf.le _) ?_⟩
  · rw [← hι, hr]
  · change r (hrr'.1 _) (hrr'.1 _)
    rwa [hrr'.2, @enum_lt_enum _ r']
  · rw [← hf, lsub_le_iff]
    intro i
    suffices h : ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f i) i' hi' by
      rcases h with ⟨i', hi', hfg⟩
      exact hfg.trans_lt (lt_blsub _ _ _)
    by_cases! h : ∀ j, r j i → f j < f i
    · refine ⟨typein r' ⟨i, h⟩, typein_lt_type _ _, ?_⟩
      rw [bfamilyOfFamily'_typein]
    · obtain ⟨hji, hij⟩ := wo.wf.min_mem _ h
      refine ⟨typein r' ⟨_, fun k hkj => lt_of_lt_of_le ?_ hij⟩, typein_lt_type _ _, ?_⟩
      · by_contra! H
        exact (wo.wf.not_lt_min {j | r j i ∧ f i ≤ f j} ⟨IsTrans.trans _ _ _ hkj hji, H⟩) hkj
      · rwa [bfamilyOfFamily'_typein]

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

Goal state before:
pp: c : Cardinal.{u_1}
H : c.IsRegular
⊢ 0 < c

Tactic:
exact H.pos

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

Goal state before:
pp: o : Ordinal.{u_1}
h : IsSuccLimit o
⊢ ℵ₀ ≤ o.cof

Tactic:
aleph0_le_cof_iff,

Goal state after:
o : Ordinal.{u_1}
h : IsSuccLimit o
⊢ 1 < o.cof
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (ℵ_ (o + 1)).IsRegular

Tactic:
by
  rw [← succ_aleph]
  exact isRegular_succ (aleph0_le_aleph o)

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

Goal state before:
pp: case inl
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ ≤ max c ℵ₀

pp: case inr
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ c ^< ℵ₀ ≤ max c ℵ₀

Tactic:
· rw [powerlt_aleph0 h]
    apply le_max_left

Goal state after:
case inr
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ c ^< ℵ₀ ≤ max c ℵ₀
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : #↑s < (#α).ord.cof
⊢ Bounded r s

Tactic:
hr

Goal state after:
case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : #↑s < (type r).cof
⊢ Bounded r s
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
rw [hα, cof_type, ← card_ord (Order.cof _), ← hs', card_type, ← prod_const']

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ ∀ (i : ↑(Iio a)), 2 ^ preBeth ↑i < c

Tactic:
· rintro ⟨b, hb⟩
    exact hc.isStrongPrelimit <| IH _ hb (hb.trans ha)

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
f₁ f₂ : Π₀ (i : ι), β i
x✝ : ι
⊢ (erase i (f₁ + f₂)) x✝ = (erase i f₁ + erase i f₂) x✝

Tactic:
by simp [ite_zero_add]

Goal state after:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : (f g.fst) g.snd ≠ 0
h : f g.fst = 0
⊢ False

Tactic:
dsimp at hg

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : ¬(f g.fst) g.snd = 0
h : f g.fst = 0
⊢ False
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case mk.mk.e_a.refine_2
ι : 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
i : ι
a✝ : i ∈ (sf + sg).toFinset
H2 : i ∉ sg
⊢ (φ i) (g i) = 0

Tactic:
rw [(hg i).resolve_left H2, map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
e : ι ≃ ι'
x✝¹ x✝ : Π₀ (i : ι), M i
⊢ (equivCongrLeft e).toFun (x✝¹ + x✝) = (equivCongrLeft e).toFun x✝¹ + (equivCongrLeft e).toFun x✝

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
e : ι ≃ ι'
x✝¹ : R
x✝ : Π₀ (i : ι), M i
⊢ (equivCongrLeft e).toFun (x✝¹ • x✝) = (RingHom.id R) x✝¹ • (equivCongrLeft e).toFun x✝

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M✝ : ι → Type u_5
N : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → AddCommMonoid (M✝ i)
inst✝⁵ : (i : ι) → Module R (M✝ i)
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : DecidableEq ι
α : ι → Type u_7
M : (i : ι) → α i → Type u_8
inst✝¹ : (i : ι) → (j : α i) → AddCommMonoid (M i j)
inst✝ : (i : ι) → (j : α i) → Module R (M i j)
x✝¹ x✝ : Π₀ (i : (x : ι) × α x), M i.fst i.snd
⊢ __spread✝⁻⁰.toFun (x✝¹ + x✝) = __spread✝⁻⁰.toFun x✝¹ + __spread✝⁻⁰.toFun x✝

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M✝ : ι → Type u_5
N : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → AddCommMonoid (M✝ i)
inst✝⁵ : (i : ι) → Module R (M✝ i)
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : DecidableEq ι
α : ι → Type u_7
M : (i : ι) → α i → Type u_8
inst✝¹ : (i : ι) → (j : α i) → AddCommMonoid (M i j)
inst✝ : (i : ι) → (j : α i) → Module R (M i j)
x✝¹ : R
x✝ : Π₀ (i : (x : ι) × α x), M i.fst i.snd
⊢ __spread✝⁻⁰.toFun (x✝¹ • x✝) = (RingHom.id R) x✝¹ • __spread✝⁻⁰.toFun x✝

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝¹ x✝ : Π₀ (i : ι), M i
⊢ equivFunOnFintype.toFun (x✝¹ + x✝) = equivFunOnFintype.toFun x✝¹ + equivFunOnFintype.toFun x✝

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝¹ : R
x✝ : Π₀ (i : ι), M i
⊢ equivFunOnFintype.toFun (x✝¹ • x✝) = (RingHom.id R) x✝¹ • equivFunOnFintype.toFun x✝

Tactic:
ext; rfl

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
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : f ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I)
g : ι →₀ R
hgsupp : g ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I)
hsum : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
hn : c.Nonempty
this : Std.Refl r
⊢ ↑f.support ∪ ↑g.support ⊆ ⋃ i ∈ c, ↑i

Tactic:
by
        simpa using! And.intro hfsupp hgsupp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
⊢ iSupIndep p

Tactic:
rw [iSupIndep_iff_forall_dfinsupp]

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
⊢ ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid N
p : ι → AddSubmonoid N
h : Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)
⊢ iSupIndep (⇑AddSubmonoid.toNatSubmodule ∘ p)

Tactic:
exact iSupIndep_of_dfinsupp_lsum_injective _ h

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)
⊢ iSupIndep (⇑AddSubgroup.toIntSubmodule ∘ p)

Tactic:
exact iSupIndep_of_dfinsupp_lsum_injective _ h

Goal state after: