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✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
h₁ : 0 < b₁
ha : a₁ ≤ a₁
h₂ : 0 < a₁
hb : b₁ ≤ b₁
⊢ a₁ • b₁ = a₁ • b₁

Tactic:
rfl

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

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

Tactic:
simpa [sub_nonneg, smul_sub] using h _ ha (b₂ - b₁)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
t : Finset M
⊢ ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
⊢ (∀ ⦃d : Set α⦄, d ∈ D → d ⊆ sᶜ → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ sᶜ) ↔
    ∀ ⦃d : Set α⦄,
      d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ¬Disjoint d s

Tactic:
grind

Goal state after:
Module: Mathlib.Order.DirSupClosed

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

Tactic:
grind

Goal state after:
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 ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

Tactic:
grind

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

Goal state before:
pp: R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
hM : Module.Finite R M
⊢ Module.Finite A M

Tactic:
rw [finite_def, fg_def] at hM ⊢

Goal state after:
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
hM : ∃ S, S.Finite ∧ span R S = ⊤
⊢ ∃ S, S.Finite ∧ span A S = ⊤
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
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : PartialOrder α
inst✝² : (i : ι) → PartialOrder (β i)
inst✝¹ : (i : ι) → SMulWithZero α (β i)
inst✝ : ∀ (i : ι), SMulPosStrictMono α (β i)
⊢ ∀ ⦃b : (i : ι) → β i⦄, 0 < b → ∀ ⦃a₁ a₂ : α⦄, a₁ < a₂ → a₁ • b < a₂ • b

Tactic:
simp_rw [lt_def]
    rintro a ⟨ha, i, hi⟩ _b₁ _b₂ hb
    exact ⟨smul_le_smul_of_nonneg_right hb.le ha, i, smul_lt_smul_of_pos_right hb hi⟩

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : α
hb : b < a
⊢ ¬IsMin (f a)

Tactic:
exact not_isMin_iff.2 ⟨_, hf.strictMono hb⟩

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
n : ℕ
⊢ (range fun n ↦ f^[n.succ] a) ⊆ range fun n ↦ f^[n] a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
x : α
⊢ OrderIso.Set.univ.symm x = ⟨x, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
hs : IsCofinal (range f)
H : StrictMono (Subtype.val ∘ ⇑(enum (range f) hs))
⊢ {x | ∃ y, f y = x} = range f

Tactic:
rfl

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

Goal state before:
pp: α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ f g.top = (g.transRelIso f).top

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
inst✝² : ConditionallyCompleteLinearOrderBot α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
this✝ : Bot ↑s := { bot := ⟨sInf s, ⋯⟩ }
this : OrderBot ↑s := { toBot := this✝, bot_le := ⋯ }
⊢ ↑⊥ = sInf s

Tactic:
rfl

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (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
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
⊢ Subtype.val ∘ ⇑(enum s hs) '' Iio a ⊆ s

Tactic:
grind

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

Goal state before:
pp: o : Ordinal.{u}
⊢ #↑(Iio o) = ((typein LT.lt).toRelEmbedding o).card

Tactic:
rfl

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

Goal state before:
pp: o₁ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
⊢ o₁.bsup f = o₁.bsup fun a h ↦ f a ⋯

Tactic:
rfl

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

Goal state before:
pp: f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ ⨆ i, f (familyOfBFamily' r ?ho✝ g i) = iSup (familyOfBFamily' r ?ho fun a h ↦ f (g a h))

Tactic:
rfl

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

Goal state before:
pp: case ho
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ type r = type r

Tactic:
rfl

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

Goal state before:
pp: α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h✝ : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : ¬b = b'
⊢ s b' b

Tactic:
grind

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

Goal state before:
pp: case case1
b n : ℕ
hb : n < b
h✝ : b ≤ 1
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case case2.case1
b : ℕ
h✝ : ¬b ≤ 1
hb : 0 < b
⊢ (0, 0).snd = 0

Tactic:
grind

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

Goal state before:
pp: case case2.case2
b : ℕ
h✝¹ : ¬b ≤ 1
fuel✝ : ℕ
hb h✝ : fuel✝.succ < b
⊢ (fuel✝.succ, 0).snd = 0

Tactic:
grind

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

Goal state before:
pp: case case2.case3
b : ℕ
h✝² : ¬b ≤ 1
fuel✝ q✝ e✝ : ℕ
h✝¹ : q✝ < b
hb : fuel✝.succ < b
h✝ : ¬fuel✝.succ < b
x✝ : log.go fuel✝.succ (b * b) fuel✝ = (q✝, e✝)
⊢ (q✝, 2 * e✝).snd = 0

Tactic:
grind

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

Goal state before:
pp: case case2.case4
b : ℕ
h✝² : ¬b ≤ 1
fuel✝ q✝ e✝ : ℕ
h✝¹ : ¬q✝ < b
hb : fuel✝.succ < b
h✝ : ¬fuel✝.succ < b
x✝ : log.go fuel✝.succ (b * b) fuel✝ = (q✝, e✝)
⊢ (q✝ / b, 2 * e✝ + 1).snd = 0

Tactic:
grind

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

Goal state before:
pp: n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
hfuel₀ : fuel ≠ 0
⊢ b > 0

Tactic:
grind

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

Goal state before:
pp: n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
hfuel₀ : fuel ≠ 0
⊢ fuel + 1 ≤ 2 * fuel

Tactic:
grind

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

Goal state before:
pp: o₁ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
⊢ o₁.blsub f = o₁.blsub fun a h ↦ f a ⋯

Tactic:
rfl

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

Goal state before:
pp: a : Cardinal.{u_1}
ha : IsSuccLimit a
⊢ a.ord ∈ {x | ∀ ⦃a_1 : Ordinal.{u_1}⦄, a_1 ∈ {x | ∀ ⦃a_2 : Ordinal.{u_1}⦄, a_2 ∈ ord '' Iio a → a_2 ≤ x} → x ≤ a_1}

Tactic:
mem_ofPred,

Goal state after:
a : Cardinal.{u_1}
ha : IsSuccLimit a
⊢ ∀ ⦃a_1 : Ordinal.{u_1}⦄, (∀ ⦃a_2 : Ordinal.{u_1}⦄, a_2 ∈ ord '' Iio a → a_2 ≤ a_1) → a.ord ≤ a_1
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ ↑(n + 1) ≤ o ↔ succ ↑n ≤ o

Tactic:
rfl

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

Goal state before:
pp: case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 0 < b

Tactic:
grind

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

Goal state before:
pp: case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

Tactic:
grind

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

Goal state before:
pp: case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n / b ≠ 0

Tactic:
grind

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

Goal state before:
pp: case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n ≠ 0

Tactic:
grind

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

Goal state before:
pp: case inl
a : Ordinal.{u_4}
h : IsSuccLimit (a + 0)
⊢ IsSuccLimit 0 ∨ 0 = 0 ∧ IsSuccLimit a

Tactic:
grind

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

Goal state before:
pp: a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : IsSuccLimit b
⊢ (∀ (a_1 : Ordinal.{u_1}) (b_1 : a_1 ∈ Iio b), a ^ ↑⟨a_1, b_1⟩ ≤ c) ↔ ∀ b' < b, a ^ b' ≤ c

Tactic:
rfl

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

Goal state before:
pp: case zero
b n : ℕ
⊢ log b (n / b ^ 0) = log b n - 0

Tactic:
grind

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

Goal state before:
pp: case succ
b n : ℕ
hb : 1 < b
hn : 1 < n
c : ℕ
⊢ n ≤ b ^ c * b ↔ n + b - 1 ≤ b ^ c * b + b - 1

Tactic:
grind

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

Goal state before:
pp: b n : ℕ
⊢ log b n ≤ clog b n

Tactic:
by
  obtain hb | hb := le_or_gt b 1
  · rw [log_of_left_le_one hb]
    exact zero_le _
  cases n with
  | zero =>
    rw [log_zero_right]
    exact zero_le _
  | succ n =>
    exact (Nat.pow_le_pow_iff_right hb).1
      ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)

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

Goal state before:
pp: case inr.inr
b k n : ℕ
hk : k > 0
hb : 1 ≥ b
⊢ k - 1 < k

Tactic:
grind

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

Goal state before:
pp: case zero
a : Ordinal.{u_1}
⊢ 0^[0] a ≤ 0^[0] a

Tactic:
rfl

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

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

Tactic:
by
  rw [← omega_zero, omega_le_omega]
  exact zero_le

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

Goal state before:
pp: case ind
c : Cardinal.{u_1}
IH : ∀ y < c, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ c
⊢ c * c ≤ c

Tactic:
induction c using Cardinal.inductionOn with | mk α

Goal state after:
case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
⊢ #α * #α ≤ #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
⊢ ∀ (a b : α), g (a, b) < g p ∨ g (a, b) = g p ∧ (a < p.1 ∨ a = p.1 ∧ b < p.2) → a < q ∧ b < q

Tactic:
grind

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

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

Tactic:
by
  rw [← Cardinal.mul_eq_self hc]
  exact mul_le_mul' ha hb

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

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

Tactic:
by
  rw [aleph_eq_preAleph, succ_preAleph, add_assoc, aleph_eq_preAleph]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ ≤ ℵ_ o

Tactic:
by
  rw [aleph_eq_preAleph, aleph0_le_preAleph]
  exact le_self_add

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

Goal state before:
pp: case refine_1
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
x : ↑(Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
⊢ ↑x ∈ s

Tactic:
grind

Goal state after:
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 : (fun x1 x2 ↦ x1 * x2) (b ^ x) (b ^ y) < b ^ o
⊢ (fun x1 x2 ↦ x1 + x2) x y < o

Tactic:
dsimp only at *

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 : b ^ x * b ^ y < b ^ o
⊢ x + y < o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr.inr
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
by_cases hf : BddAbove (range f)

Goal state after:
case pos
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

case neg
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : ¬BddAbove (range f)
⊢ (⨆ i, f i) * c = ⨆ i, f i * c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
f : α → Ordinal.{u}
⊢ (⨆ i, f i + 1).cof ≤ #α

Tactic:
simpa using cof_lift_iSup_add_one_le f

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

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

Tactic:
have H := hf.cof_eq
  subst H
  exact hf

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

Goal state before:
pp: case refine_2
o i j : Ordinal.{u}
hi : i < 1
hj : j < 1
h : i < j
⊢ (fun x x_1 ↦ o) i hi < (fun x x_1 ↦ o) j hj

Tactic:
lt_one_iff_zero

Goal state after:
case refine_2
o i j : Ordinal.{u}
hi✝ : i < 1
hi : i = 0
hj✝ : j < 1
hj : j = 0
h : i < j
⊢ (fun x x_1 ↦ o) i hi✝ < (fun x x_1 ↦ o) j hj✝
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case inr
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i : Ordinal.{u}
hi hj : i < o
hij : i ≤ i
⊢ f i hi ≤ f i hj

Tactic:
rfl

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

Goal state before:
pp: a✝¹ : Ordinal.{?u.2}
b : Ordinal.{?u.4}
o✝¹ : Ordinal.{?u.6}
a✝ o✝ : Ordinal.{u}
f✝ : (b : Ordinal.{u}) → b < o✝ → Ordinal.{u}
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
i : Ordinal.{u}
hi : i < o'
⊢ g i hi < o

Tactic:
← hg.2.2

Goal state after:
a✝¹ : Ordinal.{?u.2}
b : Ordinal.{?u.4}
o✝¹ : Ordinal.{?u.6}
a✝ o✝ : Ordinal.{u}
f✝ : (b : Ordinal.{u}) → b < o✝ → Ordinal.{u}
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
i : Ordinal.{u}
hi : i < o'
⊢ g i hi < o'.blsub g
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case add_one
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ max a.card (a ^ b).card ≤ max a.card (b.card + 1)

Tactic:
grw [IH]

Goal state after:
case add_one
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ max a.card (max a.card b.card) ≤ max a.card (b.card + 1)
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_1
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
⊢ o ≤ (f a).cof.ord

Tactic:
grind [Ordinal.IsFundamentalSequence, cof_map_of_isNormal]

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

Goal state before:
pp: case refine_2
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ { x // ∃ (h : x ∈ s), f ⟨x, h⟩ = a } ≃ { a_1 // ∃ (h : a_1 ∈ s), f ⟨a_1, ⋯⟩ = a }

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β' : Type v
⊢ (∃ x, x ∈ {f | Surjective f}) ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)

Tactic:
mem_ofPred,

Goal state after:
α : Type u
β' : Type v
⊢ (∃ f, Surjective f) ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
| #α

Tactic:
rw [← mk_bounded_subset h hr]

Goal state after:
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
| #{ s // Bounded r s }
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ c < c ^ c.ord.cof

Tactic:
induction c using Cardinal.inductionOn with | mk α

Goal state after:
case mk
α : Type u_1
hc : ℵ₀ ≤ #α
⊢ #α < #α ^ (#α).ord.cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
c : Cardinal.{u}
⊢ #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ (ℵ₀ + #α) ^ c

Tactic:
rfl

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
⊢ ℵ₀ ≤ ℵ₀

Tactic:
rfl

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift.{u_2, u_1} #α = lift.{u_1, u_2} #↑(range ⇑f)ᶜ

Tactic:
mk_compl_of_infinite

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift.{u_2, u_1} #α = lift.{u_1, u_2} #β

case inr.h2
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ #↑(range ⇑f) < #β
Module: Mathlib.Data.DFinsupp.Submonoid

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

Tactic:
rintro x ⟨v, rfl⟩
    exact dfinsuppSumAddHom_mem _ v _ fun i _ => (le_iSup S i : S i ≤ _) (v i).prop

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

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
inst✝ : (i : ι) → Zero (β₁ i)
h : ∀ (i : ι), id 0 = 0
g : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ (mapRange (fun i ↦ id) h g) i✝ = g i✝

Tactic:
rfl

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

Goal state before:
pp: ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
f₂ : (i : ι) → β i → β₁ i
hf : ∀ (i : ι), f i 0 = 0
hf₂ : ∀ (i : ι), f₂ i 0 = 0
h : ∀ (i : ι), (f i ∘ f₂ i) 0 = 0
g : Π₀ (i : ι), β i
i✝ : ι
⊢ (f i✝ ∘ f₂ i✝) (g i✝) = f i✝ (f₂ i✝ (g i✝))

Tactic:
rfl

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

Goal state before:
pp: case inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : i ∈ ↑xs
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0

Tactic:
grind

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

Goal state before:
pp: case inr.inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : x i = 0
h2 : i ∈ ↑ys
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0

Tactic:
grind

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

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

Tactic:
rfl

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

Goal state before:
pp: case inr.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : x i = 0
h2 : y i = 0
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0

Tactic:
grind

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

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

Tactic:
by
  rw [AddSubmonoid.mem_iSup_iff_exists_dfinsupp]
  simp_rw [sumAddHom_apply]
  rfl

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : ι
h : p i
⊢ (filter p f) i = f i

Tactic:
grind

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : ι
h : ¬p i
⊢ (filter p f) i = 0

Tactic:
grind

Goal state after:
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
⊢ (mk s x) ↑i = (mk s y) ↑i

Tactic:
grind

Goal state after: