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

Goal state before:
pp: G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
h : G
hh : h ∈ ↑H
n : G
hy : (fun x1 x2 ↦ x1 * x2) h n ∈ H ⊔ N
hn : n ∈ N
⊢ ∃ a, φ a = Quotient.mk'' ⟨(fun x1 x2 ↦ x1 * x2) h n, hy⟩

Tactic:
use ⟨h, hh⟩

Goal state after:
case h
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := ⋯
this : (N.subgroupOf (H ⊔ N)).Normal := ⋯
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := ⋯
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
h : G
hh : h ∈ ↑H
n : G
hy : (fun x1 x2 ↦ x1 * x2) h n ∈ H ⊔ N
hn : n ∈ N
⊢ φ ⟨h, hh⟩ = Quotient.mk'' ⟨(fun x1 x2 ↦ x1 * x2) h n, hy⟩
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one, Finite.mem_toFinset]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ 1 < s.ncard ↔ s.Nontrivial ∧ s.Finite

Tactic:
refine ⟨fun hs ↦ ?_, fun ⟨hs_nontrivial, hs_finite⟩ ↦ ?_⟩
  · have := finite_of_ncard_pos (Nat.zero_lt_of_lt hs)
    rw [← Set.finite_coe_iff] at this
    exact ⟨one_lt_ncard_iff_nontrivial.mp hs, this⟩
  · rw [← Set.finite_coe_iff] at hs_finite
    rwa [one_lt_ncard_iff_nontrivial]

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: case trans
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 x✝ y✝ z✝ : N
a✝¹ : ConGen.Rel rel x✝ y✝
a✝ : ConGen.Rel rel y✝ z✝
ih : ∀ ⦃a b : M⦄, f a = x✝ → f b = y✝ → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y✝ → f b = z✝ → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : f a = x✝
fb : f b = z✝
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b

Tactic:
exact Exists.casesOn (f.surjective _) fun c' hc' ↦ ConGen.Rel.trans (ih fa hc') (ih1 hc' fb)

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f✝ f : M →* P
g : P → M
hf : RightInverse g ⇑f
x : (ker f).Quotient
⊢ (kerLift f) ((toQuotient ∘ g) ((kerLift f) x)) = (kerLift f) x

Tactic:
rw [Function.comp_apply, kerLift_mk, hf]

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
h' : p ≤ comap (f ^ k) p
⊢ p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k

Tactic:
induction k with

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝⁷ : Semiring R
φ : ι → Type i
inst✝⁶ : (i : ι) → AddCommMonoid (φ i)
inst✝⁵ : (i : ι) → Module R (φ i)
inst✝⁴ : DecidableEq ι
S : Type u_1
inst✝³ : Fintype ι
inst✝² : Semiring S
inst✝¹ : (i : ι) → Module S (φ i)
inst✝ : ∀ (i : ι), SMulCommClass R S (φ i)
x : (i : ι) → φ i
⊢ ((lsum R φ S) (single R φ)) x = id x

Tactic:
by simp [Finset.univ_sum_single]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case h₁
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
m : M
n : M₂
⊢ (m, 0) ∈ fst R M M₂ ⊔ snd R M M₂

pp: case h₂
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
m : M
n : M₂
⊢ (0, n) ∈ fst R M M₂ ⊔ snd R M M₂

Tactic:
· exact Submodule.mem_sup_left (Submodule.mem_comap.mpr (by simp))

Goal state after:
case h₂
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
m : M
n : M₂
⊢ (0, n) ∈ fst R M M₂ ⊔ snd R M M₂
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case succ.hin.refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ succ^[n] i ≠ j

Tactic:
exact hn_lt_ne _ (Nat.lt_succ_self n)

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A✝ : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid A
inst✝³ : PartialOrder A
inst✝² : CanonicallyOrderedMul A
inst✝¹ : LocallyFiniteOrderBot A
inst✝ : DecidableEq A
n : A
a : A × A
h : a.1 * a.2 = n
⊢ a ∈ Iic n ×ˢ Iic n

Tactic:
simp [← h]

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

Goal state before:
pp: case mk
ι : 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
x✝ : (ι → R) ⧸ pi fun x ↦ I
x : ι → R
⊢ (fun x ↦ (Quotient.mk (pi fun x ↦ I)) fun x_1 ↦ Quotient.out (x x_1))
      ((fun x ↦ Quotient.liftOn' x (fun f i ↦ (Quotient.mk I) (f i)) ⋯)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) x)) =
    Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) x

Tactic:
exact Ideal.Quotient.eq.2 fun i ↦ Ideal.Quotient.eq.1 (Quotient.out_eq' _)

Goal state after:
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:
contrapose! h

Goal state after:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ∀ (p : Ideal R), p ≠ ⊥ → ¬p.IsMaximal
⊢ IsField R
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
B : FilterBasis α
this : Directed (fun x1 x2 ↦ x1 ≥ x2) fun s ↦ 𝓟 ↑s
U : Set α
⊢ U ∈ B.filter ↔ U ∈ ⨅ s, 𝓟 ↑s

Tactic:
simp [mem_filter_iff, mem_iInf_of_directed this]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst✝² : Fintype X
inst✝¹ : Finite Y
inst✝ : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ equivFunOnFinite (mapDomain f (equivFunOnFinite.symm (equivFunOnFinite s))) y = ∑ x with f x = y, equivFunOnFinite s x

Tactic:
simp only [Equiv.symm_apply_apply]

Goal state after:
M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst✝² : Fintype X
inst✝¹ : Finite Y
inst✝ : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ equivFunOnFinite (mapDomain f s) y = ∑ x with f x = y, equivFunOnFinite s x
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ range m ∈ map m f

Tactic:
by
  rw [← image_univ]
  exact image_mem_map univ_mem

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

Goal state before:
pp: α : Type u_1
⊢ ⨆ a, pure a = ⊤

Tactic:
← principal_univ,

Goal state after:
α : Type u_1
⊢ ⨆ a, pure a = 𝓟 univ
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ¬∀ᶠ (x : α) in atTop, ¬p x
a : α
⊢ ∃ b, a ≤ b ∧ p b

Tactic:
contrapose! h

Goal state after:
α : Type u_3
inst✝ : Preorder α
p : α → Prop
a : α
h : ∀ (b : α), a ≤ b → ¬p b
⊢ ∀ᶠ (x : α) in atTop, ¬p x
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂

Tactic:
apply le_antisymm h2.1

Goal state after:
α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ x₂ ≤ y₁
Module: Mathlib.Order.Filter.Map

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

Tactic:
← principal_univ,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ map f (𝓟 univ) = 𝓟 (range f)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl g ⊓ map inr f = ⊥

Tactic:
map_inl_inf_map_inr

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ ⊥ = ⊥
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : α → β
hl : l.HasBasis p s
t : Set β
⊢ t ∈ Filter.map f l ↔ ∃ i, p i ∧ f '' s i ⊆ t

Tactic:
simp only [mem_map, image_subset_iff, hl.mem_iff, preimage]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
⊢ (map f F).NeBot ↔ F.NeBot

Tactic:
by
  simp only [neBot_iff, Ne, map_eq_bot_iff]

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
H : ∀ᶠ (i : ι) in F, ∃ b, P i b
⊢ ∀ᶠ (i : ι) in F, P i ((fun i ↦ if h : ∃ b, P i b then h.choose else ⋯.some) i)

Tactic:
filter_upwards [H] with i hi

Goal state after:
ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
H : ∀ᶠ (i : ι) in F, ∃ b, P i b
i : ι
hi : ∃ b, P i b
⊢ P i (if h : ∃ b, P i b then h.choose else ⋯.some)
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case refine_1
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
c : β
⊢ ∃ a, c ≤ f a

Tactic:
rcases exists_ge_ge c b with ⟨d, hcd, hbd⟩

Goal state after:
case refine_1
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
c d : β
hcd : c ≤ d
hbd : b ≤ d
⊢ ∃ a, c ≤ f a
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
a : α
a✝ : True
c : β
hac : f a ≤ c
hbc : b ≤ c
⊢ c ∈ f '' Ici a

Tactic:
exact ⟨g c, (hgle _ hbc _).1 hac, hfg _ hbc⟩

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInaccOn D x
x : Set α
hx : x ∈ s
⊢ DirSupClosedOn D xᶜ

Tactic:
exact (hs x hx).compl

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupInaccOn D (f i)
⊢ DirSupInaccOn D (⋃ i, f i)

Tactic:
rw [← sUnion_range f]
  exact DirSupInaccOn.sUnion (by simpa)

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 • b) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
← neg_smul,

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 • b ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
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:
by
    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.SetTheory.Ordinal.Univ

Goal state before:
pp: case mpr.type.refine_1
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
⊢ β → α

Tactic:
exact fun b => enum r ⟨f b, (hf _).1 ⟨_, rfl⟩⟩

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

Goal state before:
pp: case inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), f (Sum.inl a) = Sum.inl a
a : α
x : γ
hx : f (Sum.inr a) = Sum.inl x
⊢ ∃ b, Sum.inl x = Sum.inr b

pp: case inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), f (Sum.inl a) = Sum.inl a
a : α
x : β
hx : f (Sum.inr a) = Sum.inr x
⊢ ∃ b, Sum.inr x = Sum.inr b

Tactic:
· rw [← H₁, f.inj] at hx
        contradiction

Goal state after:
case inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), f (Sum.inl a) = Sum.inl a
a : α
x : β
hx : f (Sum.inr a) = Sum.inr x
⊢ ∃ b, Sum.inr x = Sum.inr b
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 : β
⊢ (typein (Prod.Lex s r)).toRelEmbedding (b, a) < c

Tactic:
have := H _ (h.succ_lt (typein_lt_type s 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 : β
this : type r * succ ((typein s).toRelEmbedding b) ≤ c
⊢ (typein (Prod.Lex s r)).toRelEmbedding (b, a) < c
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: case mpr
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := ⋯
⊢ a ∈ s → a ∈ range (enumOrd s)

Tactic:
· intro ha
    refine ⟨sInf t, (enumOrd_le_of_forall_lt ha ?_).antisymm ?_⟩
    · intro b hb
      by_contra! hb'
      exact hb.not_ge (csInf_le' hb')
    · exact csInf_mem (s := t) ⟨a, (enumOrd_strictMono hs).id_le a⟩

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

Goal state before:
pp: o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ a < o.blsub f ↔ ∃ i, ∃ (hi : i < o), a ≤ f i hi

Tactic:
by
  simpa only [not_forall, not_lt, not_le] using not_congr (@blsub_le_iff.{_, v} _ f a)

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
⊢ (type r).blsub f ≤ o ↔ (lsub fun a ↦ f ((typein r).toRelEmbedding a) ⋯) ≤ o

Tactic:
by
    rw [blsub_le_iff, lsub_le_iff]
    exact ⟨fun H b => H _ _, fun H i h => by simpa only [typein_enum] using H (enum r ⟨i, h⟩)⟩

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

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

Tactic:
cases l with

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

Goal state before:
pp: case limit
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
⊢ 1 ^ b ≤ c ↔ 1 ≤ c

Tactic:
opow_le_of_isSuccLimit one_ne_zero l

Goal state after:
case limit
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
⊢ (∀ b' < b, 1 ^ b' ≤ c) ↔ 1 ≤ c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
⊢ Monotone (log b)

Tactic:
refine monotone_nat_of_le_succ fun n => ?_
  rcases le_or_gt b 1 with hb | hb
  · rw [log_of_left_le_one hb]
    exact zero_le _
  · exact le_log_of_pow_le hb (pow_log_le_add_one _ _)

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

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

Tactic:
induction k with

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

Goal state before:
pp: a b : Ordinal.{u_1}
h : a ^ b = 1
⊢ a = 1 ∨ b = 0

Tactic:
contrapose! h

Goal state after:
a b : Ordinal.{u_1}
h : a ≠ 1 ∧ b ≠ 0
⊢ a ^ b ≠ 1
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (∀ (i : ι), f i b ≤ nfpFamily f a) ↔ b ≤ nfpFamily f a

Tactic:
by
  refine ⟨fun h => ?_, fun h i => ?_⟩
  · obtain ⟨i⟩ := hι
    exact (H i).strictMono.le_apply.trans (h i)
  · rw [← nfpFamily_fp (H i)]
    exact (H i).monotone h

Goal state after:
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 * (1 + ↑n) + a % ω ^ log ω a - ω ^ log ω a < a

Tactic:
mul_one_add,

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

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
ha : a ∈ upperBounds {o | IsPrincipal op o}
⊢ False

Tactic:
exact ((le_nfp _ _).trans (ha (isPrincipal_nfp_iSup op (succ a)))).not_gt (lt_succ a)

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

Goal state before:
pp: ⊢ preOmega ω = ω

Tactic:
← apply_omega0_of_isNormal isNormal_preOmega,

Goal state after:
⊢ ⨆ n, preOmega ↑n = ω
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a : Ordinal.{u}
ha : ¬IsPrincipal (fun x1 x2 ↦ x1 + x2) a
⊢ ∃ b < a, ∃ c < a, b + c = a

Tactic:
rw [not_isPrincipal_iff] at ha

Goal state after:
a : Ordinal.{u}
ha : ∃ a_1 < a, ∃ b < a, a ≤ a_1 + b
⊢ ∃ b < a, ∃ c < a, b + c = a
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
rw [← o.card_preOmega, (isInitial_preOmega o).ord_card]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 0 < preAleph o ↔ 0 < o

Tactic:
rw [← preAleph_zero, preAleph_lt_preAleph]

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

Goal state before:
pp: case refine_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x ↦ a * x) c = a ^ ω * c
⊢ deriv (fun x ↦ a * x) (succ c) = a ^ ω * succ c

Tactic:
rw [deriv_succ, h]

Goal state after:
case refine_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x ↦ a * x) c = a ^ ω * c
⊢ nfp (fun x ↦ a * x) (succ (a ^ ω * c)) = a ^ ω * succ c
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x ↦ a * x) c = a ^ ω * c
⊢ deriv (fun x ↦ a * x) (succ c) = a ^ ω * succ c

Tactic:
· rw [deriv_succ, h]
    exact nfp_mul_opow_omega0_add c ha zero_lt_one (one_le_iff_pos.2 (opow_pos _ ha))

Goal state after:
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:
← mem_Iio,

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
⊢ #↑(⋃ j ∈ Iio o, A j) ≤ c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
this : Cardinal.lift.{u, max u v} (⨆ i, f i).card ≤ sum fun i ↦ (f i).card
⊢ (⨆ i, f i).card ≤ sum fun i ↦ (f i).card

Tactic:
rwa [Cardinal.lift_id'] at this

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

Goal state before:
pp: a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ (a + b).cof = b.cof

Tactic:
rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨c, rfl⟩ | hb)
  · contradiction
  · rw [succ_eq_add_one, ← add_assoc, cof_add_one, cof_add_one]
  · exact cof_map_of_isNormal (isNormal_add_right a) hb

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

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

Tactic:
Ordinal.lift_id',

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ c ^ ↑n ≤ max c ℵ₀

Tactic:
rcases le_or_gt ℵ₀ c with hc | hc

Goal state after:
case inl
c : Cardinal.{u}
n : ℕ
hc : ℵ₀ ≤ c
⊢ c ^ ↑n ≤ max c ℵ₀

case inr
c : Cardinal.{u}
n : ℕ
hc : c < ℵ₀
⊢ c ^ ↑n ≤ max c ℵ₀
Module: Mathlib.SetTheory.Cardinal.Regular

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

Tactic:
apply Ordinal.lift_iSup_lt_of_lt_cof _ hf
  rwa [lift_umax, Ordinal.lift_id', hc.cof_ord]

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

Goal state before:
pp: α : Type u
β' : Type v
⊢ #↑{f | Surjective f} ≠ 0 ↔ lift.{u, v} #β' ≤ lift.{v, u} #α ∧ (#α = 0 ∨ #β' ≠ 0)

Tactic:
lift_mk_le',

Goal state after:
α : Type u
β' : Type v
⊢ #↑{f | Surjective f} ≠ 0 ↔ Nonempty (β' ↪ α) ∧ (#α = 0 ∨ #β' ≠ 0)
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:
← 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 }