mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocRing R
N : AddSubgroup R
inst✝ : N.Normal
n : ℤ
a : R
⊢ ↑(n • a) = n • ↑a

Tactic:
mk_zsmul N a n

Goal state after:
R : Type u_1
inst✝¹ : NonAssocRing R
N : AddSubgroup R
inst✝ : N.Normal
n : ℤ
a : R
⊢ n • ↑a = n • ↑a
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
⊢ ∀ (a b : α), f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
intro a b

Goal state after:
case inr.refine_1
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : IsField R
a : R
ha : a ≠ 0
⊢ (a * if ha : a = 0 then 0 else Classical.choose ⋯) = 1

Tactic:
by convert! Classical.choose_spec (h.mul_inv_cancel ha); exact dif_neg ha

Goal state after:
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: case hex
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃ x_1, x * x_1 = 1

pp: case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂

Tactic:
· exact hf.mul_inv_cancel hx

Goal state after:
case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case pos
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∈ I
⊢ b i = 0 i

Tactic:
by_cases hiJ : i ∈ J
      · exact (h.le_bot ⟨hiI, hiJ⟩).elim
      · exact hJ i hiJ

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ toZ i0 (succ^[n] i0) = ↑n

Tactic:
← hmn

Goal state after:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ toZ i0 (succ^[n] i0) = ↑m
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ toZ i0 (pred^[n + 1] i0) = -↑(n + 1)

Tactic:
← hmn

Goal state after:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ toZ i0 (pred^[n + 1] i0) = -↑m
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 1) = (0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n)

Tactic:
simp only [antidiagonal, range_succ_eq_map, map_cons, Nat.add_succ_sub_one,
    Nat.add_zero, id, Nat.sub_zero, map_map, Prod.map_apply]

Goal state after:
n : ℕ
⊢ (0, n + 1) :: (Nat.succ 0, n) :: map ((fun i ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n) =
    (0, n + 1) :: (Nat.succ 0, n) :: map (Prod.map Nat.succ id ∘ (fun i ↦ (i, n - i)) ∘ Nat.succ) (range n)
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 1) =
    cons (0, n + 1)
      (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (antidiagonal n)) ⋯

Tactic:
by
  apply eq_of_veq
  rw [cons_val, map_val]
  apply Multiset.Nat.antidiagonal_succ

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
⊢ IsIdempotentElem (q - p) ↔ p * q = p ∧ q * p = p

Tactic:
by
  refine ⟨fun hqp ↦ ?_, fun ⟨h1, h2⟩ => hp.sub hq h1 h2⟩
  have h : p * (q - p) + (q - p) * p = 0 := hp.add_iff hqp |>.mp ((add_sub_cancel p q).symm ▸ hq)
  have hpq : Commute p q := by
    simp_rw [IsIdempotentElem, mul_sub, sub_mul,
    hp.eq, hq.eq, ← sub_add_eq_sub_sub, sub_right_inj, add_sub] at hqp
    have h1 := congr_arg (q * ·) hqp
    have h2 := congr_arg (· * q) hqp
    simp_rw [mul_sub, mul_add, ← mul_assoc, hq.eq, add_sub_cancel_right] at h1
    simp_rw [sub_mul, add_mul, mul_assoc, hq.eq, add_sub_cancel_left, ← mul_assoc] at h2
    exact h2.symm.trans h1
  rw [hpq.eq, and_self, ← nsmul_right_inj (by simp : 2 ≠ 0), ← zero_add (2 • p)]
  convert congrArg (· + 2 • p) h
  simp [sub_mul, mul_sub, hp.eq, hpq.eq, two_nsmul, sub_add, sub_sub]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: case mpr
α : Type u
inst✝ : Semiring α
y : α
I : Ideal α
a b : α
hb : b ∈ I
⊢ ∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = a * y + b

Tactic:
exact ⟨a * y, Ideal.mem_span_singleton'.mpr ⟨a, rfl⟩, b, hb, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {y * z + x, y} = span {x, y}

Tactic:
by
  rw [add_comm, span_pair_add_right_mul]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x y : R
⊢ (mk I) x = (mk I) y ↔ x - y ∈ I

Tactic:
rw [← eq_zero_iff_mem, map_sub, sub_eq_zero]

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

Goal state before:
pp: case zero.inl
α : Type u_2
inst✝ : CommSemiring α
hs : span ∅ = ⊤
⊢ 1 ∈ span ∅

Tactic:
hs

Goal state after:
case zero.inl
α : Type u_2
inst✝ : CommSemiring α
hs : span ∅ = ⊤
⊢ 1 ∈ ⊤
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
⊢ ∀ (r s : R ⧸ I) (x : (ι → R) ⧸ pi fun x ↦ I), (r + s) • x = r • x + s • x

Tactic:
by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; exact congr_arg _ (add_smul _ _ _)

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

Goal state before:
pp: case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this✝ : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
this : span {↑x ^ (n + 1)} ≤ span ((fun x ↦ x ^ (n + 1)) '' s)
⊢ (f x * ↑x) ^ (n + 1) ∈ span {↑x ^ (n + 1)}

Tactic:
rw [mul_pow, mem_span_singleton]

Goal state after:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this✝ : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
this : span {↑x ^ (n + 1)} ≤ span ((fun x ↦ x ^ (n + 1)) '' s)
⊢ ↑x ^ (n + 1) ∣ f x ^ (n + 1) * ↑x ^ (n + 1)
Module: Mathlib.Order.Filter.Defs

Goal state before:
pp: case hs
α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t✝ : Set α
f g : Filter α
x✝ y✝ : Set α
hx : x✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
hy : y✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
t : Set α
htg : t ∈ g
ht : x✝ ∩ y✝ ⊆ t
⊢ x✝ ∪ t ∈ f

Tactic:
exact hx (mem_of_superset htg subset_union_right) subset_union_left

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t

Tactic:
rcases h.mem_iff.1 ht with ⟨i, hpi, hti⟩

Goal state after:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
i : ι
hpi : p i
hti : s i ⊆ t
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t
Module: Mathlib.Order.Filter.Map

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

Tactic:
by
  rw [← principal_univ, map_principal, image_univ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hm : Surjective m
⊢ comap m f = ⊥ ↔ f = ⊥

Tactic:
comap_eq_bot_iff_compl_range,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hm : Surjective m
⊢ (range m)ᶜ ∈ f ↔ f = ⊥
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f₁ f₂ : Filter (Filter α)
x : Set α
⊢ x ∈ f₁.join ⊔ f₂.join ↔ x ∈ (f₁ ⊔ f₂).join

Tactic:
by simp only [mem_sup, mem_join]

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

Goal state before:
pp: α : 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 β
⊢ s ∈ l₂ → (fun x ↦ if p x then f x else g x) ⁻¹' s ∈ l₁

Tactic:
hs

Goal state after:
α : 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₂
⊢ (fun x ↦ if p x then f x else g x) ⁻¹' s ∈ l₁
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : g₂ ⁻¹' {t | s ∈ t} ∈ f₁
a✝ : α
hx : g₁ a✝ ≤ g₂ a✝
⊢ a✝ ∈ g₂ ⁻¹' {t | s ∈ t} → s ∈ g₁ a✝

Tactic:
hs

Goal state after:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs✝ : g₂ ⁻¹' {t | s ∈ t} ∈ f₁
a✝ : α
hx : g₁ a✝ ≤ g₂ a✝
hs : a✝ ∈ g₂ ⁻¹' {t | s ∈ t}
⊢ s ∈ g₁ a✝
Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst✝¹ : AddZeroClass B
inst✝ : DistribSMul M B
this : AddZeroClass A := e.addZeroClass
⊢ ∀ (a : M) (x y : A), a • (x + y) = a • x + a • y

Tactic:
simp [add_def, smul_def, smul_add]

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

Goal state before:
pp: case mpr
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
⊢ (∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N) → N.FG

Tactic:
rintro ⟨G, _, g, hg⟩
    have := Fintype.ofFinite (range g)
    exact ⟨(range g).toFinset, by simpa⟩

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ ∃ s, IsCofinal s ∧ #↑s = cof α

Tactic:
by
  obtain ⟨s, hs⟩ := ciInf_mem fun s : {s : Set α // IsCofinal s} ↦ #s
  exact ⟨s.1, s.2, hs⟩

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

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
⊢ IsCofinal s → lift.{v, u} (cof α) ≤ lift.{u, v} #↑s

Tactic:
hs

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #↑s
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set α
⊢ IsCofinal s → lift.{u, v} (cof β) ≤ lift.{v, u} #↑s

Tactic:
hs

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set α
hs : IsCofinal s
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} #↑s
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case h.a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
s : M
⊢ s ∈ ↑S → s ∈ ↑(N (S.attach.sup f))

Tactic:
hs

Goal state after:
case h.a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
s : M
hs : s ∈ ↑S
⊢ s ∈ ↑(N (S.attach.sup f))
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
⊢ s.FG ↔ IsCompactElement s

Tactic:
(Tactic.tacticLet__
 "let"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId `sp)
   []
   [(Term.typeSpec ":" (Term.arrow `M "→" (Term.app `Submodule [`R `M])))]
   ":="
   (Term.fun
    "fun"
    (Term.basicFun
     [`a]
     []
     "=>"
     (Term.app
      `span
      [`R
       (choice
        («term{_}» "{" [`a] "}")
        (Term.structInst
         "{"
         []
         (Term.structInstFields [(Term.structInstField (Term.structInstLVal `a []) [])])
         (Term.optEllipsis [])
         []
         "}"))]))))))

Goal state after:
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
⊢ s.FG ↔ IsCompactElement s
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosMono α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ a₁ • _b ≤ a₂ • _b

Tactic:
← neg_le_neg_iff,

Goal state after:
α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosMono α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ -(a₂ • _b) ≤ -(a₁ • _b)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosReflectLE α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
h : a₁ • _b ≤ a₂ • _b
⊢ a₁ ≤ a₂

Tactic:
← neg_le_neg_iff,

Goal state after:
α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosReflectLE α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
h : -(a₂ • _b) ≤ -(a₁ • _b)
⊢ a₁ ≤ a₂
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst✝⁶ : CommSemiring A₁
inst✝⁵ : CommSemiring B₁
inst✝⁴ : CommSemiring A₂
inst✝³ : Semiring B₂
inst✝² : Algebra A₁ B₁
inst✝¹ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
inst✝ : Module.Finite A₁ B₁
this✝¹ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this✝ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
this : IsScalarTower A₁ A₂ B₁
r : A₂
⊢ e₂.toFun ((algebraMap A₂ B₁) r) = (algebraMap A₂ B₂) r

Tactic:
simpa [RingHom.algebraMap_toAlgebra] using DFunLike.congr_fun he.symm (e₁.symm r)

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
inst✝⁴ : LinearOrder α
inst✝³ : WellFoundedLT α
inst✝² : SuccOrder α
inst✝¹ : LinearOrder β
inst✝ : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
a : α
⊢ f a = g a

Tactic:
induction a using SuccOrder.limitRecOn with

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
⊢ s ⊆ range f → s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → ∀ ⦃a : α⦄, IsLUB s a → a ∈ range f

Tactic:
hs

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
⊢ s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → ∀ ⦃a : α⦄, IsLUB s a → a ∈ range f
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
s : Set Ordinal.{u_2}
⊢ IsCofinal s → Cardinal.univ.{u_2, u_2 + 1} ≤ #↑s

Tactic:
hs

Goal state after:
α : Type u_1
s : Set Ordinal.{u_2}
hs : IsCofinal s
⊢ Cardinal.univ.{u_2, u_2 + 1} ≤ #↑s
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 : β), Prod.Lex s r (b, a) ((enum (Prod.Lex s r)) ⟨c, l⟩)

Tactic:
intro a b

Goal state after:
α β : 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 : β
⊢ Prod.Lex s r (b, a) ((enum (Prod.Lex s r)) ⟨c, l⟩)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
w✝ : ι
hf : f w✝ = iSup f
⊢ f w✝ < lsub f

Tactic:
exact lt_lsub _ _

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

Goal state before:
pp: ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ lsub (familyOfBFamily' r ho f) = lsub (familyOfBFamily' r' ho' f)

Tactic:
rw [lsub_eq_blsub', lsub_eq_blsub']

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

Goal state before:
pp: ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ (type r).blsub (bfamilyOfFamily' r f) = (type r').blsub (bfamilyOfFamily' r' f)

Tactic:
blsub_eq_lsub',

Goal state after:
ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ lsub f = (type r').blsub (bfamilyOfFamily' r' f)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : c ≠ 0
⊢ a < b / c ↔ c * succ a ≤ b

Tactic:
rw [← not_le, div_le h, not_lt]

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

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

Tactic:
← ord_le,

Goal state after:
o : Ordinal.{u_1}
⊢ ℵ₀.ord ≤ o ↔ ω ≤ o
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
⊢ b ^ log b 0 ≤ 0 + 1

Tactic:
by rw [log_zero_right, Nat.pow_zero]

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

Goal state before:
pp: case inl
x : Ordinal.{u_1}
h : 0 ≤ 1
⊢ log 0 x = 0

Tactic:
apply (csSup_of_not_bddAbove _).trans csSup_empty
    by_contra! hb
    refine not_bddAbove_Ici 1 (hb.mono fun a ↦ ?_)
    simp +contextual [one_le_iff_ne_zero]

Goal state after:
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.card

Tactic:
← ord_le,

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

Goal state before:
pp: case inr
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
⊢ log b x ≤ log b y

Tactic:
obtain hb | hb := lt_or_ge 1 b

Goal state after:
case inr.inl
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
hb : 1 < b
⊢ log b x ≤ log b y

case inr.inr
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
hb : b ≤ 1
⊢ log b x ≤ log b y
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:
| add_one =>

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

Goal state before:
pp: case inr
b x : Ordinal.{u_1}
hx : x ≠ 0
⊢ log b x ≤ x

Tactic:
obtain hb | hb := lt_or_ge 1 b

Goal state after:
case inr.inl
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : 1 < b
⊢ log b x ≤ x

case inr.inr
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : b ≤ 1
⊢ log b x ≤ x
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b : Ordinal.{u_1}
⊢ log b 1 = 0

Tactic:
obtain hb | hb := lt_or_ge 1 b

Goal state after:
case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ log b 1 = 0

case inr
b : Ordinal.{u_1}
hb : b ≤ 1
⊢ log b 1 = 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
⊢ log b x + log b y ≤ log b (x * y)

Tactic:
obtain hb | hb := lt_or_ge 1 b

Goal state after:
case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ log b x + log b y ≤ log b (x * y)

case inr
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : b ≤ 1
⊢ log b x + log b y ≤ log b (x * y)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ nfp (fun x ↦ a + x) 0 ≤ b

Tactic:
← deriv_zero_right

Goal state after:
case refine_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ deriv (fun x ↦ a + x) 0 ≤ b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
⊢ a.cof ≤ (f a).cof

Tactic:
cases a using limitRecOn with
  | zero => simp
  | add_one a =>
    rw [cof_add_one, Cardinal.one_le_iff_ne_zero, cof_eq_zero.ne]
    exact (hf.strictMono (lt_succ a)).ne_zero
  | limit a ha => rw [cof_map_of_isNormal hf ha]

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
⊢ a ≤ o.cof.ord

Tactic:
hf.ord_cof

Goal state after:
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
⊢ a ≤ a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ a + c < b + c ↔ a < b

Tactic:
constructor <;> contrapose!

Goal state after:
case mp
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ b ≤ a → b + c ≤ a + c

case mpr
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ b + c ≤ a + c → b ≤ a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = b → a ≤ #ι
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
hf : o.blsub f = b
⊢ a ≤ o.card

Tactic:
by simpa using H _ hf

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

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

Tactic:
nonempty_coe_sort,

Goal state after:
α : Type u
β' : Type v
⊢ {f | Surjective f}.Nonempty ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: case inl
β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : #α < ℵ₀
⊢ ∃ a, ℵ_ 1 ≤ #↑(f ⁻¹' {a})

pp: case inr
β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : ℵ₀ ≤ #α
⊢ ∃ a, ℵ_ 1 ≤ #↑(f ⁻¹' {a})

Tactic:
· exact infinite_pigeonhole_card f ℵ₁ (by simp) aleph0_lt_aleph_one.le
      (by rw [isRegular_aleph_one.cof_ord]; exact hα.trans aleph0_lt_aleph_one)

Goal state after:
case inr
β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : ℵ₀ ≤ #α
⊢ ∃ a, ℵ_ 1 ≤ #↑(f ⁻¹' {a})