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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosStrictMono α γ
⊢ ∀ ⦃b : β × γ⦄,
    0.1 < b.1 ∧ 0.2 ≤ b.2 ∨ 0.1 ≤ b.1 ∧ 0.2 < b.2 →
      ∀ ⦃a₁ a₂ : α⦄,
        a₁ < a₂ → (a₁ • b).1 < (a₂ • b).1 ∧ (a₁ • b).2 ≤ (a₂ • b).2 ∨ (a₁ • b).1 ≤ (a₂ • b).1 ∧ (a₁ • b).2 < (a₂ • b).2

Tactic:
rintro a (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩) _b₁ _b₂ hb

Goal state after:
case inl
α : Type u_1
β : Type u_2
a✝ a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosStrictMono α γ
a : β × γ
h₁ : 0.1 < a.1
h₂ : 0.2 ≤ a.2
_b₁ _b₂ : α
hb : _b₁ < _b₂
⊢ (_b₁ • a).1 < (_b₂ • a).1 ∧ (_b₁ • a).2 ≤ (_b₂ • a).2 ∨ (_b₁ • a).1 ≤ (_b₂ • a).1 ∧ (_b₁ • a).2 < (_b₂ • a).2

case inr
α : Type u_1
β : Type u_2
a✝ a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosStrictMono α γ
a : β × γ
h₁ : 0.1 ≤ a.1
h₂ : 0.2 < a.2
_b₁ _b₂ : α
hb : _b₁ < _b₂
⊢ (_b₁ • a).1 < (_b₂ • a).1 ∧ (_b₁ • a).2 ≤ (_b₂ • a).2 ∨ (_b₁ • a).1 ≤ (_b₂ • a).1 ∧ (_b₁ • a).2 < (_b₂ • a).2
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α ≤i β
a✝ : α
ha : IsSuccLimit a✝
⊢ f a✝ ∈ lowerBounds (upperBounds (⇑f '' Iio a✝))

Tactic:
f.image_Iio

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α ≤i β
a✝ : α
ha : IsSuccLimit a✝
⊢ f a✝ ∈ lowerBounds (upperBounds (Iio (f 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

Tactic:
rw [enum_typein]

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

Goal state before:
pp: α : Type u_1
s : Set Ordinal.{u_2}
hs : Small.{u_2, u_2 + 1} ↑s
⊢ ¬IsCofinal s

Tactic:
rw [not_isCofinal_iff_bddAbove]

Goal state after:
α : Type u_1
s : Set Ordinal.{u_2}
hs : Small.{u_2, u_2 + 1} ↑s
⊢ BddAbove s
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a : α
⊢ (typein s).toRelEmbedding (f a) = (typein r).toRelEmbedding a

Tactic:
rw [← f.transPrincipal_apply _ a, (f.transPrincipal _).eq]

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

Goal state before:
pp: case h
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : s ≺i r
⊢ lift.{v, max u v} (type s) = type s

Tactic:
lift_id'

Goal state after:
case h
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : s ≺i r
⊢ type s = type s
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : Sum.Lex r emptyRelation ≼i s
⊢ type r < type s

Tactic:
refine ⟨((InitialSeg.leAdd _ _).trans f).toPrincipalSeg fun h ↦ ?_⟩
    simpa using h (f (Sum.inr PUnit.unit))

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

Goal state before:
pp: case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ b ≤ (enum fun x1 x2 ↦ x1 < x2) ⟨a, ⋯⟩

Tactic:
rw [← enum_typein (α := α) (· < ·) b, ← not_lt, enum_le_enum (r := (· < ·)),
        Subtype.mk_le_mk, ← lt_succ_iff, ha]

Goal state after:
case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding b < typeLT α
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl.inl
b : ℕ
hb : 1 < b
⊢ log b 0 = 0 ↔ 0 < b ∨ b ≤ 1

Tactic:
grind [log_of_lt]

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}
⊢ o.blsub f = 0 ↔ o = 0

Tactic:
by
  rw [← lsub_eq_blsub, lsub_eq_zero_iff]
  exact isEmpty_toType_iff

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
h : i ≤ a
⊢ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

Tactic:
refine lt_of_le_of_lt ?_ (hlt a mem_cons_self); simpa

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
by_cases a = 0 <;> by_cases b = 0

Goal state after:
case pos
a b : Ordinal.{u_1}
h✝¹ : a = 0
h✝ : b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

case neg
a b : Ordinal.{u_1}
h✝¹ : a = 0
h✝ : ¬b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

case pos
a b : Ordinal.{u_1}
h✝¹ : ¬a = 0
h✝ : b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

case neg
a b : Ordinal.{u_1}
h✝¹ : ¬a = 0
h✝ : ¬b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ 1 < a ^ b ↔ 1 < a ∧ b ≠ 0

Tactic:
by
  refine ⟨?_, fun ⟨ha, hb⟩ ↦ ?_⟩
  · contrapose! +distrib
    rw [le_one_iff]
    rintro ((rfl | rfl) | rfl)
    · exact zero_opow_le b
    · simp
    · simp
  · rwa [← opow_zero a, opow_lt_opow_iff_right ha, pos_iff_ne_zero]

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

Goal state before:
pp: case inl
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
rw [tsub_eq_zero_iff_le.2 h, Ordinal.sub_eq_zero_iff_le.2 (Nat.cast_le.2 h), Nat.cast_zero]

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

Goal state before:
pp: case case1.inr.hb
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
hy : (clog.go x b x).snd ≥ y
⊢ x > b ^ y

Tactic:
exact Nat.lt_of_le_of_lt (Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) hy) H₁

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

Goal state before:
pp: case add_one
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o✝ : Ordinal.{u}
a✝ : f i (derivFamily f o✝) = derivFamily f o✝
⊢ f i (derivFamily f (o✝ + 1)) = derivFamily f (o✝ + 1)

Tactic:
derivFamily_add_one

Goal state after:
case add_one
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o✝ : Ordinal.{u}
a✝ : f i (derivFamily f o✝) = derivFamily f o✝
⊢ f i (nfpFamily f (derivFamily f o✝ + 1)) = nfpFamily f (derivFamily f o✝ + 1)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case add_one.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : derivFamily f o < a
⊢ derivFamily f (o + 1) ≤ a

Tactic:
derivFamily_add_one

Goal state after:
case add_one.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : derivFamily f o < a
⊢ nfpFamily f (derivFamily f o + 1) ≤ a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ha : a < o
n : ℕ
⊢ a * ↑n < o

Tactic:
induction n with
  | zero => simpa using ha.pos
  | succ n h =>
    rw [Nat.cast_add_one, mul_add_one]
    exact ho h ha

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ c * c = c

Tactic:
induction c using WellFoundedLT.induction with

Goal state after:
case ind
c : Cardinal.{u_1}
IH : ∀ y < c, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ c
⊢ c * c = c
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inl
b : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (0 ^ b)

pp: case inr
b c : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) c)
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) c ^ b)

Tactic:
· rcases eq_or_ne b 0 with (rfl | hb)
    · rw [opow_zero]
      exact isPrincipal_add_one
    · rwa [zero_opow hb]

Goal state after:
case inr
b c : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) c)
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) c ^ b)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (preOmega o).card.ord = preOmega o

Tactic:
(isInitial_preOmega o).ord_card

Goal state after:
o : Ordinal.{u_1}
⊢ preOmega o = preOmega o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case a
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ 1 ≤ a

Tactic:
· rwa [one_le_iff_pos]

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

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

Tactic:
one_mul

Goal state after:
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a = a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
this : b ^ (x + y) < b ^ o
⊢ x + y < o

Tactic:
opow_lt_opow_iff_right hb

Goal state after:
b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
this : x + y < o
⊢ x + y < o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → 1 < m

pp: n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 0 < n

Tactic:
· exact id

Goal state after:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 0 < n
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 ≤ a.cof.ord

Tactic:
← hι,

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 ≤ (#ι).ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
lift_id'

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < iSup f
hf : Cardinal.lift.{v, u} #ι < (iSup f).cof
⊢ Cardinal.lift.{v, u} #ι < (iSup f).cof
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
⊢ Cardinal.lift.{v, u} #ι < (lift.{u, max u v} c).cof

Tactic:
lift_id'

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{v, u} #ι < c.cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
| (↑n + 1) * a + 1 * a

Tactic:
one_mul

Goal state after:
n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
| (↑n + 1) * a + a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
| (↑n + 1) * μ + 1 * μ

Tactic:
one_mul

Goal state after:
n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
| (↑n + 1) * μ + μ
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = o
hι' : (#ι).ord = type r
⊢ ∃ f, o.cof.ord.blsub f = o

Tactic:
← hι,

Goal state after:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = o
hι' : (#ι).ord = type r
⊢ ∃ f, (#ι).ord.blsub f = o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Ordinal.{max u v}
ho : Cardinal.lift.{v, u} o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c
h : o.blsub f = c
⊢ c.cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
by simpa [← iSup_ord, hf, h] using cof_blsub_le_lift.{u, v} f

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

Goal state before:
pp: c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
⊢ #↑(⋃ i, t i) < c ↔ ∀ (i : ι), #↑(t i) < c

Tactic:
refine ⟨card_lt_of_card_iUnion_lt, fun h ↦ ?_⟩
  apply lt_of_le_of_lt (Cardinal.mk_sUnion_le _)
  apply Cardinal.mul_lt_of_lt hc.aleph0_le (mk_range_le.trans_lt hι)
  apply Cardinal.iSup_lt_of_lt_cof_ord (mk_range_le.trans_lt _)
  · simpa
  · rwa [hc.cof_ord]

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

Goal state before:
pp: case add_one
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b < c.ord → derivFamily f b < c.ord
hb' : b + 1 < c.ord
⊢ derivFamily f (b + 1) < c.ord

Tactic:
derivFamily_add_one

Goal state after:
case add_one
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b < c.ord → derivFamily f b < c.ord
hb' : b + 1 < c.ord
⊢ nfpFamily f (derivFamily f b + 1) < c.ord
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : Infinite α
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ (#α + 1) ^ c

Tactic:
induction c using Cardinal.inductionOn with | _ β

Goal state after:
case mk
α : Type u
inst✝ : Infinite α
β : Type u
⊢ #{ t // #↑t ≤ #β } ≤ (#α + 1) ^ #β
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
i : ↑↑s
⊢ x i = y i

Tactic:
have h1 : (mk s x : ∀ i, β i) i = (mk s y : ∀ i, β i) i := by grind

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
i : ↑↑s
h1 : (mk s x) ↑i = (mk s y) ↑i
⊢ x i = y i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
j i : ι
x : β i
⊢ erase j (single i x) = if i = j then 0 else single i x

Tactic:
rw [← filter_ne_eq_erase, filter_single, ite_not]

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

Goal state before:

Tactic:
i ∈ support (mk s fun i ↦ (f i).1) ↔ ∃ h : i ∈ s, (f ⟨i, h⟩).1 ≠ 0 := by simp
      _ ↔ ∃ _ : i ∈ s, True := exists_congr fun h ↦ (iff_true _).mpr (f _).2
      _ ↔ i ∈ s := by simp

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: case h0
ι : 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✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
c : R
f : Π₀ (i : ι), M i
⊢ (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • 0) = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) 0

Tactic:
rw [smul_zero, map_zero, smul_zero]

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : Finsupp.single 0 s + Finsupp.single 1 t = 0
⊢ t = 0

Tactic:
by simpa using congr($h 1)

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
hx : x ∉ s
⊢ ¬μ x ≠ 0

Tactic:
not_ne_iff

Goal state after:
case h.h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
hx : x ∉ s
⊢ μ x = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.hf
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
a✝ : x ∈ s
hx : ¬μ x ≠ 0
⊢ (fun x xi ↦ ↑xi) x (μ x) = 0

Tactic:
not_ne_iff

Goal state after:
case h.hf
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
a✝ : x ∈ s
hx : μ x = 0
⊢ (fun x xi ↦ ↑xi) x (μ x) = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx : ¬(DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x ≠ 0
⊢ ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 0

Tactic:
not_ne_iff

Goal state after:
case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx : (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x = 0
⊢ ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 0
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ ((r₁, x) ::ᵣ l₁).eval - ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval

Tactic:
simp only [← h, eval_cons, sub_eq_add_neg, neg_add, add_smul, neg_smul, add_assoc]

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ r₁ • x + (l₁.eval + (-(r₂ • x) + -l₂.eval)) = r₁ • x + (-(r₂ • x) + (l₁.eval + -l₂.eval))
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
a : FreeAbelianGroup X
| a

Tactic:
← toFreeAbelianGroup_toFinsupp a,

Goal state after:
X : Type u_1
a : FreeAbelianGroup X
| toFreeAbelianGroup (toFinsupp a)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
hf : ∀ (l : ι →₀ R), (linearCombination R f) l = 0 → l = 0
i : ι
m : M
r : R
hr : r ∈ nonZeroDivisors R
l : ι →₀ R
hl : l i ∈ nonZeroDivisors R
hg : r • m = (linearCombination R f) l
l' : ι →₀ R
hl' :
  r •
      ((linearCombination R f - linearCombination R (Pi.single i (f i))) l' +
        (linearCombination R (Pi.single i m)) l') =
    r • 0
⊢ l' = 0

Tactic:
LinearMap.sub_apply,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
hf : ∀ (l : ι →₀ R), (linearCombination R f) l = 0 → l = 0
i : ι
m : M
r : R
hr : r ∈ nonZeroDivisors R
l : ι →₀ R
hl : l i ∈ nonZeroDivisors R
hg : r • m = (linearCombination R f) l
l' : ι →₀ R
hl' :
  r •
      ((linearCombination R f) l' - (linearCombination R (Pi.single i (f i))) l' +
        (linearCombination R (Pi.single i m)) l') =
    r • 0
⊢ l' = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
hf : ∀ (l : ι →₀ R), (linearCombination R f) l = 0 → l = 0
i : ι
m : M
r : R
hr : r ∈ nonZeroDivisors R
l : ι →₀ R
hl : l i ∈ nonZeroDivisors R
hg : r • m = (linearCombination R f) l
l' : ι →₀ R
hl' : r • ((linearCombination R f) l' - l' i • f i) + r • l' i • m = r • 0
⊢ l' = 0

Tactic:
smul_sub,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
hf : ∀ (l : ι →₀ R), (linearCombination R f) l = 0 → l = 0
i : ι
m : M
r : R
hr : r ∈ nonZeroDivisors R
l : ι →₀ R
hl : l i ∈ nonZeroDivisors R
hg : r • m = (linearCombination R f) l
l' : ι →₀ R
hl' : r • (linearCombination R f) l' - r • l' i • f i + r • l' i • m = r • 0
⊢ l' = 0
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ ψ (-x✝) = ψ (-(1 * x✝))

Tactic:
one_mul

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ ψ (-x✝) = ψ (-x✝)
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ ψ (1 * x✝) = ψ x✝

Tactic:
one_mul

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ ψ x✝ = ψ x✝
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
y : R
⊢ y = 1 * y

Tactic:
one_mul

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
y : R
⊢ y = y