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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulMono α β
ha : 0 ≤ a
hb : b ≤ 0
⊢ a • b ≤ 0

Tactic:
simpa only [smul_zero] using smul_le_smul_of_nonneg_left hb ha

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ¬IsCofinal s
⊢ BddAbove s

Tactic:
rw [not_isCofinal_iff] at h

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ∃ x, ∀ y ∈ s, y < x
⊢ BddAbove s
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ -a • -b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Tactic:
smul_nonneg_iff_pos_imp_nonneg

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ a • -b ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
smul_nonneg_iff_pos_imp_nonneg

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ -a • b ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
smul_nonneg_iff_pos_imp_nonneg

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ f a = ⨆ b, f ↑b

Tactic:
convert! map_iSup hf _
  · exact ha.iSup_Iio.symm
  · exact ⟨⊥, ha.bot_lt⟩
  · use a
    rintro _ ⟨⟨x, hx⟩, rfl⟩
    exact hx.le

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

Goal state before:
pp: b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

Tactic:
constructor <;> intro h

Goal state after:
case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding
⊢ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
⊢ (typein r).toRelEmbedding a ≤ (typein r).toRelEmbedding b ↔ ¬r b a

Tactic:
by
  rw [← not_lt, typein_lt_typein]

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

Goal state before:
pp: a : Ordinal.{u_1}
o₁ o₂ : ↑(Iio (typeLT a.ToType))
⊢ (enum fun x1 x2 ↦ x1 < x2) o₁ ≤ (enum fun x1 x2 ↦ x1 < x2) o₂ ↔ o₁ ≤ o₂

Tactic:
← enum_le_enum,

Goal state after:
a : Ordinal.{u_1}
o₁ o₂ : ↑(Iio (typeLT a.ToType))
⊢ (enum fun x1 x2 ↦ x1 < x2) o₁ ≤ (enum fun x1 x2 ↦ x1 < x2) o₂ ↔
    ¬(enum fun x1 x2 ↦ x1 < x2) o₂ < (enum fun x1 x2 ↦ x1 < x2) o₁
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Sort u_3
f : ι → Cardinal.{u_4}
⊢ (⨆ i, f i).ord = ⨆ i, (f i).ord

Tactic:
rw [iSup, iSup, sSup_ord, range_comp']

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ IsNormal (Subtype.val ∘ ⇑(enum s hs)) ↔ DirSupClosed s

Tactic:
let H := (Subtype.strictMono_coe _).comp (enum s hs).strictMono
  refine ⟨fun he ↦ by simpa using he.dirSupClosed_range, ?_⟩
  rw [isNormal_iff, dirSupClosed_iff_of_linearOrder]
  refine fun hs' ↦ ⟨H, fun a ha b hb ↦ ?_⟩
  have bdd : BddAbove (Subtype.val ∘ enum s hs '' Iio a) := by
    use enum s hs a
    simpa [upperBounds] using fun x hx ↦ hx.le
  have : Nonempty α := ⟨a⟩
  let := WellFoundedLT.toOrderBot α
  let := WellFoundedLT.conditionallyCompleteLinearOrderBot α
  trans sSup ((Subtype.val ∘ enum s hs) '' Iio a)
  · refine enum_le_of_forall_lt (hs' ?_ ?_ (isLUB_csSup' bdd)) fun b hb ↦ ?_
    · grind
    · simpa using ha.ne_bot
    · obtain ⟨c, hca, hbc⟩ := ha.lt_iff_exists_lt.1 hb
      refine (H hbc).trans_le <| le_csSup bdd ⟨c, ?_⟩
      simpa
  · apply csSup_le'
    simpa [upperBounds]

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

Goal state before:
pp: case mp
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
⊢ ∃ x, IsTop x

Tactic:
refine ⟨enum (α := α) (· < ·) ⟨a, ?_⟩, fun b ↦ ?_⟩
    · rw [mem_Iio, ← ha, lt_succ_iff]
    · rw [← enum_typein (α := α) (· < ·) b, ← not_lt, enum_le_enum (r := (· < ·)),
        Subtype.mk_le_mk, ← lt_succ_iff, ha]
      exact typein_lt_type ..

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
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ enumOrd s o ≤ ⨆ b, enumOrd s ↑b

pp: s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ ⨆ b, enumOrd s ↑b ≤ a

Tactic:
· 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)

Goal state after:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ ⨆ b, enumOrd s ↑b ≤ a
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: 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
⊢ (#α).ord ≤ type s ↔ #α ≤ (type s).card

Tactic:
constructor <;> intro h

Goal state after:
case mp
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
h : (#α).ord ≤ type s
⊢ #α ≤ (type s).card

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
h : #α ≤ (type s).card
⊢ (#α).ord ≤ type s
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
rw [le_antisymm_iff, ← Nat.lt_succ_iff, le_log_iff_pow_le, log_lt_iff_lt_pow,
      and_comm]

Goal state after:
case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0

case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
⊢ 0 ^ 0 = 1

pp: case inr
a : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ 0 = 1

Tactic:
· rw [zero_opow', Ordinal.sub_zero]

Goal state after:
case inr
a : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ 0 = 1
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

Tactic:
by
  obtain ho | ho := lt_or_ge o ω
  · exact Or.inl <| lt_omega0.1 ho
  · exact Or.inr ho

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

Goal state before:
pp: o : Ordinal.{u_4}
H : ∀ (n : ℕ), ↑n ≤ o
a : Ordinal.{u_4}
h : a < ω
n : ℕ
e : a = ↑n
⊢ a < o

Tactic:
rw [e, ← succ_le_iff]

Goal state after:
o : Ordinal.{u_4}
H : ∀ (n : ℕ), ↑n ≤ o
a : Ordinal.{u_4}
h : a < ω
n : ℕ
e : a = ↑n
⊢ succ ↑n ≤ o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ∀ (a : Ordinal.{u_1}), a.card < c → (a + 1).card < c

Tactic:
card_add_one

Goal state after:
case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ∀ (a : Ordinal.{u_1}), a.card < c → a.card + 1 < c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀ ≤ (a + 1).card

pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ IsSuccLimit ℵ₀.ord

Tactic:
card_add_one

Goal state after:
case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀ ≤ a.card + 1

case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ IsSuccLimit ℵ₀.ord
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a * ↑(n + 1) + a % ω ^ log ω a - ω ^ log ω a < a

Tactic:
rw [add_comm, Nat.cast_add, Nat.cast_one, mul_one_add, add_assoc, Ordinal.add_sub_cancel]

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

Goal state before:
pp: case refine_1
a : Ordinal.{u}
⊢ deriv (fun x ↦ a + x) ⊥ = a * ω + ⊥

pp: case refine_2
a✝ a : Ordinal.{u}
h : deriv (fun x ↦ a✝ + x) a = a✝ * ω + a
⊢ deriv (fun x ↦ a✝ + x) (succ a) = a✝ * ω + succ a

Tactic:
· rw [bot_eq_zero, deriv_zero_right, add_zero]
    exact nfp_add_zero a

Goal state after:
case refine_2
a✝ a : Ordinal.{u}
h : deriv (fun x ↦ a✝ + x) a = a✝ * ω + a
⊢ deriv (fun x ↦ a✝ + x) (succ a) = a✝ * ω + succ a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * succ b ≤ nfp (fun x ↦ a * x) (a ^ ω * b + c)

Tactic:
obtain ⟨d, hd⟩ :=
      mul_eq_right_iff_opow_omega0_dvd.1 (nfp_fp (isNormal_mul_right ha) (a ^ ω * b + c))

Goal state after:
case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * succ b ≤ nfp (fun x ↦ a * x) (a ^ ω * b + c)
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inr
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ ω ^ succ x < ω ^ c

Tactic:
opow_lt_opow_iff_right one_lt_omega0

Goal state after:
case inr.inr
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ succ x < c
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
⊢ y < o → (fun x1 x2 ↦ x1 + x2) x y < o

Tactic:
hy

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
⊢ (fun x1 x2 ↦ x1 + x2) x y < o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1.inl
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂ : o ≤ 2
⊢ o ≤ 2 ∨ o ∈ Set.range fun x ↦ ω ^ ω ^ x

pp: case refine_1.inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂ : 2 < o
⊢ o ≤ 2 ∨ o ∈ Set.range fun x ↦ ω ^ ω ^ x

Tactic:
· exact Or.inl ho₂

Goal state after:
case refine_1.inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂ : 2 < o
⊢ o ≤ 2 ∨ o ∈ Set.range fun x ↦ ω ^ ω ^ x
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ #↑(⋃ j, ⋃ (_ : j < o), A j) ≤ c

Tactic:
by
  simp_rw [← mem_Iio, biUnion_eq_iUnion, iUnion, iSup, ← ToType.mk.symm.surjective.range_comp]
  rw [← lift_le.{u}]
  apply ((mk_iUnion_le_lift _).trans _).trans_eq (mul_eq_self (aleph0_le_lift.2 hc))
  rw [mk_toType]
  refine mul_le_mul' ho (ciSup_le' ?_)
  intro i
  simpa using hA _ i.toOrd.prop

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

Goal state before:
pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ #↑(?m.44 ⁻¹' Set.univ) < #?m.42

pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ Type ?u.40

pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ Type ?u.39

pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ ?m.42 → ?m.43

Tactic:
← iUnion_of_singleton,

Goal state after:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ #↑(?m.44 ⁻¹' ⋃ x, {x}) < #?m.42

β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ Type ?u.41

β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ Type ?u.40

β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ ?m.42 → ?m.46
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β : Type u
⊢ #(α ↪ β) = 0 ↔ #β < #α

Tactic:
by
  rw [mk_embedding_eq_zero_iff_lift_lt, lift_lt]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Set M
hs : s.Finite
hsspan : span R s = ⊤
ι : Type w
b : Basis ι R M
this : span R (⇑↑b.repr '' s) = (↑b.repr).range
⊢ Finite ι

Tactic:
LinearEquiv.range

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Set M
hs : s.Finite
hsspan : span R s = ⊤
ι : Type w
b : Basis ι R M
this : span R (⇑↑b.repr '' s) = ⊤
⊢ Finite ι
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsSingular
⊢ ∀ (b : Cardinal.{u_1}), succ b ≠ c

Tactic:
rintro c rfl

Goal state after:
c : Cardinal.{u_1}
hc : (succ c).IsSingular
⊢ False
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
y : γ
⊢ y ∈ S i → y ∈ AddMonoidHom.mrange (sumAddHom fun i ↦ (S i).subtype)

Tactic:
hy

Goal state after:
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
y : γ
hy : y ∈ S i
⊢ y ∈ AddMonoidHom.mrange (sumAddHom fun i ↦ (S i).subtype)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
h : ¬p i
⊢ (if p i then single i x else 0) = 0

Tactic:
if_neg h

Goal state after:
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
h : ¬p i
⊢ 0 = 0
Module: Mathlib.Data.DFinsupp.Defs

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

Tactic:
if_neg h

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
x : β i
h : i ≠ j
⊢ single i x = single i x
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
δ : Type u_1
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : (i : ι) → SMulZeroClass γ (β i)
inst✝² : (i : ι) → SMulZeroClass δ (β i)
inst✝¹ : SMul γ δ
inst✝ : ∀ (i : ι), IsScalarTower γ δ (β i)
r : γ
s : δ
m : Π₀ (i : ι), β i
i : ι
⊢ ((r • s) • m) i = (r • s • m) i

Tactic:
by simp only [smul_apply, smul_assoc r s (m i)]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
P : (Fin 0 → α) → Prop
⊢ Exists P ↔ ∃ x, P x

Tactic:
simp only [Exists, Fin.exists_fin_zero_pi, Matrix.vecEmpty]
    rfl

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

Goal state before:
pp: ι : 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
⊢ (sumZeroHom φ) f = f.sum fun x ↦ ⇑(φ x)

Tactic:
by
  rcases f with ⟨f, s, hf⟩
  change (∑ i ∈ _, _) = ∑ i ∈ _ with _, _
  rw [Finset.sum_filter, Finset.sum_congr rfl]
  intro i _
  dsimp only [coe_mk', Subtype.coe_mk] at *
  split_ifs with h
  · rfl
  · rw [not_not.mp h, map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

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

Tactic:
hy

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 ∈ ((lsum ℕ) fun i ↦ (p i).subtype).range
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: 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'
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂

Tactic:
constructor <;> intro h

Goal state after:
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'
⊢ f₁ = f₂

case mpr
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₁ = f₂
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ Function.Injective ⇑(quotientInfToSupQuotient p p')

Tactic:
← ker_eq_bot,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ (quotientInfToSupQuotient p p').ker = ⊥
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ s • u • x + u • t • y = 0

Tactic:
smul_comm u t,

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ s • u • x + t • u • y = 0
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝¹ : AddMonoid M
inst✝ : SMul R M
r₁ r₂ : R
m : M
l₁ l₂ : NF R M
h1 : r₁ = r₂
h2 : l₁.eval = l₂.eval
⊢ ((r₁, m) ::ᵣ l₁).eval = ((r₂, m) ::ᵣ l₂).eval

Tactic:
simp [h1, h2]

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
r : R
m n : M
l : NF R M
h1 : r = 0
h2 : l.eval = n
⊢ ((r, m) ::ᵣ l).eval = n

Tactic:
simp [h1, h2]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
ι : Type u_4
c : R
x✝ : ι
⊢ (⇑f ∘ (algebraMap R (ι → A)) c) x✝ = (algebraMap R (ι → B)) c x✝

Tactic:
exact f.commutes' c

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ (toFinsupp a) x ≠ 0 ↔ (coeff x) a ≠ 0

Tactic:
exact Iff.rfl

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ (toFinsupp a) x = 0 ↔ (coeff x) a = 0

Tactic:
exact Iff.rfl

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
a : A
⊢ (∑ i ∈ s, ψ i) a = ∏ i ∈ s, (ψ i) a

Tactic:
by rw [coe_sum, Finset.prod_apply]

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
n : ℤ
ψ : AddChar A M
a : A
⊢ (n • ψ) a = ψ a ^ n

Tactic:
by
  cases n <;> simp [-neg_apply, neg_apply']

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

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
⊢ LinearIndepOn K v (insert x s)

Tactic:
rw [← union_singleton]
  have x0 : v x ≠ 0 := fun h => hx (h ▸ zero_mem _)
  apply hs.union (LinearIndepOn.singleton x0)
  rwa [image_singleton, disjoint_span_singleton' x0]

Goal state after: