mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
⊢ ∃ p, p ≠ ⊥ ∧ p.IsMaximal

Tactic:
by
  contrapose! h
  simp only [← bot_lt_iff_ne_bot] at h
  refine isField_iff_maximal_bot.mpr ⟨⟨bot_ne_top, Ideal.maximal_of_no_maximal h⟩⟩

Goal state after:
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
⊢ ⋂ i, Iio (f i) = ∅

Tactic:
refine eq_empty_of_subset_empty ?_

Goal state after:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
⊢ ⋂ i, Iio (f i) ⊆ ∅
Module: Mathlib.Order.Filter.Tendsto

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

pp: case neg
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
h : ¬p x
⊢ g x ∈ s

Tactic:
exacts [hp₀ h, hp₁ h]

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

Goal state before:
pp: α : Type u_1
f g : Filter α
⊢ (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x

Tactic:
by
  rw [inf_comm]
  exact inf_neBot_iff_frequently_left

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

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
q : Prop
⊢ (∀ᶠ (x : α) in f, p x → q) ↔ (∃ᶠ (x : α) in f, p x) → q

Tactic:
by
  simp only [imp_iff_not_or, eventually_or_distrib_right, not_frequently]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → Filter α
m : α → β
hf : Directed (fun x1 x2 ↦ x1 ≥ x2) f
inst✝ : Nonempty ι
s : Set β
hs : m ⁻¹' s ∈ iInf f
i : ι
hi : m ⁻¹' s ∈ f i
⊢ map m (f i) ≤ 𝓟 s

Tactic:
by simpa only [le_principal_iff, mem_map]

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

Goal state before:
pp: α : Type u
β : Type v
p : α → Prop
fs : β → Filter α
⊢ (∃ᶠ (x : α) in ⨆ b, fs b, p x) ↔ ∃ b, ∃ᶠ (x : α) in fs b, p x

Tactic:
by
  simp only [Filter.Frequently, eventually_iSup, not_forall]

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ Group α

Tactic:
let zpow := e.pow ℤ

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
⊢ Group α
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ CommGroup α

Tactic:
let zpow := e.pow ℤ

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
⊢ CommGroup α
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
hb : 0 = b
⊢ a₁ • b ≤ a₂ • b

Tactic:
simp [← hb]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
⊢ a₁ • b ≤ a₂ • b

Tactic:
by
    obtain hb | hb := hb.eq_or_lt
    · simp [← hb]
    · exact h₀ _ hb _ _ h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ ≤ a₁
hb : b₂ ≤ b₁
⊢ a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂

Tactic:
by
  simp_rw [add_comm (a₁ • _)]; exact smul_add_smul_le_smul_add_smul ha hb

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : IsNormal f
a : α
ha : IsSuccLimit a
⊢ IsLUB (f '' Iio a) (f a)

Tactic:
refine ⟨?_, hf.2 ha⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : IsNormal f
a : α
ha : IsSuccLimit a
⊢ f a ∈ upperBounds (f '' Iio a)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case pos
s : Set Ordinal.{u_3}
hs : BddAbove s
hs' : BddAbove ((fun x ↦ x + 1) '' s)
⊢ ∀ x ∈ s, x ≤ sSup ((fun x ↦ x + 1) '' s)

Tactic:
exact fun x hx ↦ (lt_add_one _).le.trans (le_csSup hs' (mem_image_of_mem _ hx))

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 : α
⊢ ¬(enum fun x1 x2 ↦ x1 < x2) ⟨a, ⋯⟩ < (enum fun x1 x2 ↦ x1 < x2) ⟨(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding b, ⋯⟩

Tactic:
enum_le_enum (r := (· < ·)),

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, ⋯⟩ ≤ ⟨a, ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < b
⊢ IsSuccLimit (a * b)

Tactic:
rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨b, rfl⟩ | lb)

Goal state after:
case inl
a : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < 0
⊢ IsSuccLimit (a * 0)

case inr.inl
a : Ordinal.{u_4}
l : IsSuccLimit a
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ IsSuccLimit (a * succ b)

case inr.inr
a b : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < b
lb : IsSuccLimit b
⊢ IsSuccLimit (a * b)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case limit
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
l : IsSuccLimit c
IH : ∀ o' < c, (a + b) * (o' + 1) = a * (o' + 1) + b
⊢ (a + b) * c + (a + b) = a * (c + 1) + b

Tactic:
add_mul_limit_aux ba l IH,

Goal state after:
case limit
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
l : IsSuccLimit c
IH : ∀ o' < c, (a + b) * (o' + 1) = a * (o' + 1) + b
⊢ a * c + (a + b) = a * (c + 1) + b
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
h : c ≠ 0
⊢ c.ord ≠ 0

Tactic:
ne_eq,

Goal state after:
c : Cardinal.{u_1}
h : c ≠ 0
⊢ ¬c.ord = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b x y : ℕ
hy : y ≠ 0
h : x ≤ 0
hb : b ≤ 1
⊢ b ^ x ≤ y

Tactic:
Nat.le_zero

Goal state after:
b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
⊢ b ^ x ≤ y
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
a0 : a ≠ 0
b : Ordinal.{u_4}
⊢ a * (a * b / a) = a * b

Tactic:
by rw [mul_div_cancel _ a0]

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = log b (n + 1) ↔ b ^ log b (n + 1) ≠ n + 1

Tactic:
ne_eq,

Goal state after:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = log b (n + 1) ↔ ¬b ^ log b (n + 1) = n + 1
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.bsup fun x x_1 ↦ f x) = f o
⊢ (o.blsub fun x x_1 ↦ f x) = f o

Tactic:
rwa [← bsup_eq_blsub_of_lt_succ_limit ho fun a _ => h a] at *

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

Goal state before:
pp: case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.blsub fun x x_1 ↦ f x) = f o
⊢ (o.bsup fun x x_1 ↦ f x) = f o

Tactic:
rwa [← bsup_eq_blsub_of_lt_succ_limit ho fun a _ => h a] at *

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

Goal state before:
pp: case hbc
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * (v + 1) ≤ b ^ u * x

Tactic:
· grw [add_one_le_of_lt hv]

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
⊢ clog b n = clog b (n + 1) ↔ b ^ clog b n ≠ n

Tactic:
ne_eq,

Goal state after:
b n : ℕ
hb : 1 < b
⊢ clog b n = clog b (n + 1) ↔ ¬b ^ clog b n = n
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: a : Ordinal.{u_1}
ha : a ∈ upperBounds {x | x.IsInitial}
this : (succ a.card).ord ≤ a
⊢ False

Tactic:
rw [ord_le] at this

Goal state after:
a : Ordinal.{u_1}
ha : a ∈ upperBounds {x | x.IsInitial}
this : succ a.card ≤ a.card
⊢ False
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case ind.mk.hbc.inr
α : 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
hq : ℵ₀ ≤ #↑(Iio q)
⊢ #↑(Iio q) * #↑(Iio q) < #α

Tactic:
have := mk_Iio_lt q hα

Goal state after:
case ind.mk.hbc.inr
α : 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
hq : ℵ₀ ≤ #↑(Iio q)
this : #↑(Iio q) < #α
⊢ #↑(Iio q) * #↑(Iio q) < #α
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
by
  apply ((cof_le_card _).trans _).antisymm
  · rwa [aleph0_le_cof_iff, one_lt_cof_iff]
  · rwa [card_le_iff, succ_aleph0, ord_aleph]

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

Goal state before:
pp: case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
⊢ ∀ (i : ↑(Set.Iio b)), a * ↑i ≤ b ^ succ (log b a)

Tactic:
intro ⟨c, hcb⟩

Goal state after:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
⊢ a * ↑⟨c, hcb⟩ ≤ b ^ succ (log b a)
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case h₂
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a / b ^ log b a < b

Tactic:
← lt_mul_iff_div_lt hbo₀,

Goal state after:
case h₂
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a < b ^ log b a * b
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
⊢ #↑(⋃ x, A ↑x) ≤ c

Tactic:
iUnion,

Goal state after:
β : 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
⊢ #↑(⨆ x, A ↑x) ≤ c
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
⊢ lift.{v, u} #o.ToType * ⨆ i, lift.{u, v} #↑(((fun x ↦ A ↑x) ∘ ⇑ToType.mk.symm) i) ≤ lift.{u, v} c * lift.{u, v} c

Tactic:
rw [mk_toType]

Goal state after:
β : 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
⊢ lift.{v, u} o.card * ⨆ i, lift.{u, v} #↑(((fun x ↦ A ↑x) ∘ ⇑ToType.mk.symm) i) ≤ lift.{u, v} c * lift.{u, v} c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
g : ι' → Cardinal.{v}
⊢ (⨆ i, f i) * ⨆ j, g j = ⨆ i, ⨆ j, f i * g j

Tactic:
Cardinal.ciSup_mul f,

Goal state after:
ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
g : ι' → Cardinal.{v}
⊢ ⨆ i, f i * ⨆ j, g j = ⨆ i, ⨆ j, f i * g j
Module: Mathlib.SetTheory.Cardinal.Ordinal

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

Tactic:
ne_eq,

Goal state after:
case add_one.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ ¬(a ^ b).card = 0
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: 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'
⊢ ∃ o f, a.IsFundamentalSequence o f

Tactic:
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 _) ?_⟩

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 ≤ a.cof.ord

case refine_2
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'
i j : Ordinal.{u}
x✝¹ : i < type r'
h : j < type r'
x✝ : i < j
⊢ r ↑((enum r') ⟨i, x✝¹⟩) ↑((enum r') ⟨j, h⟩)

case refine_3
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'
⊢ a ≤ (type r').blsub fun i x ↦ f ↑((enum r') ⟨i, x⟩)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ a.card ≤ (a ^ b).card

Tactic:
apply card_le_card

Goal state after:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ a ≤ a ^ b
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ b.card ≤ (a ^ b).card

Tactic:
apply card_le_card

Goal state after:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ b ≤ a ^ b
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ a.card ≤ (a ^ b).card

Tactic:
apply card_le_card

Goal state after:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ a ≤ a ^ b
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ b.card ≤ (a ^ b).card

Tactic:
apply card_le_card

Goal state after:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ b ≤ a ^ b
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #↑(⋃ a, ⋃ (h : a ∈ s), t a h) < c
a : α
ha : a ∈ s
⊢ #↑(t a ha) < c

Tactic:
by
  rw [biUnion_eq_iUnion] at h
  have := card_lt_of_card_iUnion_lt h
  simp_all only [iUnion_coe_set, Subtype.forall]

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi : β i
⊢ single i xi = 0 ↔ xi = 0

Tactic:
← single_zero i,

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi : β i
⊢ single i xi = single i 0 ↔ xi = 0
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✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
j : ι
hi : i ≠ j
hj : j ∈ ↑s
⊢ j ∈ i ::ₘ ↑s ∨ Function.update (⇑f) i b j = 0

pp: case inr.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
j : ι
hi : i ≠ j
hj : f j = 0
⊢ j ∈ i ::ₘ ↑s ∨ Function.update (⇑f) i b j = 0

Tactic:
· exact Or.inl (Multiset.mem_cons_of_mem hj)

Goal state after:
case inr.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
j : ι
hi : i ≠ j
hj : f j = 0
⊢ j ∈ i ::ₘ ↑s ∨ Function.update (⇑f) i b j = 0
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
fs : (i : ↥(↑s).toFinset) → { s_1 // ∀ (i_1 : α ↑i), i_1 ∈ s_1 ∨ (f ↑i).toFun i_1 = 0 }
i : ι
a : α i
hi : f.toFun i = 0
⊢ (⟨i, a⟩ ∈ (↑s).toFinset.attach.val.bind fun i ↦ Multiset.map (Sigma.mk ↑i) ↑(fs i)) ∨ (f ⟨i, a⟩.fst) ⟨i, a⟩.snd = 0

Tactic:
| inr hi =>

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
γ : Type w
α : Type x
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∏ i ∈ ∅, (g i).prod h = (∑ i ∈ ∅, g i).prod h

Tactic:
simp [prod_zero_index]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ GaloisConnection (⇑OrderDual.toDual ∘ dualAnnihilator) (dualCoannihilator ∘ ⇑OrderDual.ofDual)

Tactic:
by
  intro a b
  induction b using OrderDual.rec
  simp only [Function.comp_apply, OrderDual.toDual_le_toDual, OrderDual.ofDual_toDual,
    SetLike.le_def, mem_dualAnnihilator, mem_dualCoannihilator]
  grind

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_3
U : ι → Submodule R M
⊢ ⨆ i, (U i).dualAnnihilator ≤ (⨅ i, U i).dualAnnihilator

Tactic:
by
  rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_iSup_eq]
  apply iInf_mono
  exact fun i : ι => le_dualAnnihilator_dualCoannihilator (U i)

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
i : ι
m : M
hm : (Finsupp.lsingle i) m ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), (fun i ↦ (Finsupp.lsingle i).range) j)
this : ⨆ j, ⨆ (_ : j ≠ i), (Finsupp.lsingle j).range ≤ Finsupp.supported M R {i}ᶜ
⊢ (Finsupp.lsingle i) m ∈ ⊥

Tactic:
have := (Finsupp.mem_supported ..).mp (this hm)

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
m : M
hm : (Finsupp.lsingle i) m ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), (fun i ↦ (Finsupp.lsingle i).range) j)
this✝ : ⨆ j, ⨆ (_ : j ≠ i), (Finsupp.lsingle j).range ≤ Finsupp.supported M R {i}ᶜ
this : ↑((Finsupp.lsingle i) m).support ⊆ {i}ᶜ
⊢ (Finsupp.lsingle i) m ∈ ⊥
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
f g : ι →₀ R
hsum : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
hc : IsChain r ∅
hfsupp : f ∈ Finsupp.supported R R (⋃ I ∈ ∅, ↑I)
hgsupp : g ∈ Finsupp.supported R R (⋃ I ∈ ∅, ↑I)
⊢ f = 0

Tactic:
simpa using! hfsupp

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : SMul S R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
inst✝¹² : Module S M
inst✝¹¹ : Module S N
inst✝¹⁰ : Module S P
inst✝⁹ : IsScalarTower S R M
inst✝⁸ : IsScalarTower S R N
inst✝⁷ : IsScalarTower S R P
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module S M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module S N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module S P'
inst✝ : SMulCommClass R S P
i : M' →ₗ[S] M
j : N' →ₗ[S] N
k : P' →ₗ[S] P
hk : Injective ⇑k
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ k.range
m : M'
n : N'
⊢ k (((i.restrictScalarsRange₂ j k hk B hB) m) n) = k 0 ↔ (B (i m)) (j n) = 0

Tactic:
restrictScalarsRange₂_apply,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : SMul S R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
inst✝¹² : Module S M
inst✝¹¹ : Module S N
inst✝¹⁰ : Module S P
inst✝⁹ : IsScalarTower S R M
inst✝⁸ : IsScalarTower S R N
inst✝⁷ : IsScalarTower S R P
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module S M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module S N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module S P'
inst✝ : SMulCommClass R S P
i : M' →ₗ[S] M
j : N' →ₗ[S] N
k : P' →ₗ[S] P
hk : Injective ⇑k
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ k.range
m : M'
n : N'
⊢ (B (i m)) (j n) = k 0 ↔ (B (i m)) (j n) = 0
Module: Mathlib.LinearAlgebra.Quotient.Card

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
⊢ Nat.card M = Nat.card ↥S * Nat.card (M ⧸ S)

Tactic:
by
  rw [mul_comm, ← Nat.card_prod]
  exact Nat.card_congr AddSubgroup.addGroupEquivQuotientProdAddSubgroup

Goal state after: