mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : LinearOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : AddRightReflectLE R
inst✝¹ : IsCancelAdd M
inst✝ : DecidableEq ι
s : Finset ι
⊢ ¬LinearIndepOn R v ↑s ↔ ∃ t ⊆ s, ∃ f, ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i ∧ ∃ i ∈ t, 0 < f i

Tactic:
by
  simp only [linearIndepOn_finset_iffₒₛ, not_forall, pos_iff_ne_zero]
  refine ⟨fun ⟨t, hst, f, heq, i, hi, hfi⟩ => ?_,
    fun ⟨t, hst, f, heq, i, hi, hfi⟩ => ⟨t, hst, f, heq, i, hst hi, hfi⟩⟩
  by_cases hi' : i ∈ t
  · exact ⟨t, hst, f, heq, i, hi', hfi⟩
  · refine ⟨s \ t, Finset.sdiff_subset, f, ?_, i, Finset.mem_sdiff.2 ⟨hi, hi'⟩, hfi⟩
    simpa [Finset.sdiff_sdiff_eq_self hst] using heq.symm

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case empty
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
x : (i : η) → f i
h1 : ∀ i ∉ ∅, x i = 1
h2 : ∀ i ∈ ∅, Pi.mulSingle i (x i) ∈ H
⊢ x ∈ H

Tactic:
| empty =>

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N✝ : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N✝), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
a✝ : N ≤ ⊥
x : M
x_mem : x ∈ ⊥
x_ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
⊢ False

Tactic:
rw [mem_bot] at x_mem

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N✝ : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N✝), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
a✝ : N ≤ ⊥
x : M
x_mem : x = 0
x_ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
⊢ False
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
⊢ α ≃ Fin (Nat.card α)

Tactic:
have := (Finite.exists_equiv_fin α).choose_spec.some
  rwa [Nat.card_eq_of_equiv_fin this]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s

Tactic:
mul_assoc

Goal state after:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : ↥(span R (range ⇑b))
i : ι
this :
  mapRange.linearMap (Algebra.linearMap R S) ∘ₗ ↑(restrictScalars R b).repr =
    (↑R ↑b.repr).domRestrict (span R (range ⇑b))
⊢ (algebraMap R S) (((restrictScalars R b).repr m) i) = (b.repr ↑m) i

Tactic:
by exact DFunLike.congr_fun (LinearMap.congr_fun this m) i

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x : α
⊢ orbitRel.Quotient.orbit ↑x = x • ↑s

Tactic:
by
  ext
  rw [orbitRel.Quotient.mem_orbit]
  simpa [mem_smul_set_iff_inv_smul_mem, ← leftRel_apply, Quotient.eq''] using Setoid.comm' _

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

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ insert a ↑t = s

Tactic:
simp [Set.ext_iff, hts]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1.mem
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x✝ : ι ⊕ ι' → R
k : ι'
x : ι ⊕ ι' → R
h : x ∈ Set.range fun i ↦ single (Sum.inl i) 1
⊢ x (Sum.inr k) = 0

Tactic:
| mem x h =>

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a ≤ a + c
⊢ (fun x ↦ x + d) (a + c) = a + d + c

Tactic:
rw [add_right_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a < a + c
⊢ (fun x ↦ x + d) (a + c) = a + d + c

Tactic:
rw [add_right_comm]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case empty
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
⊢ p (f i \ ∅.sup f)

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
hf' : f = f' ∘ ⇑R
⊢ disjointed f' ∘ ⇑R ≤ f

pp: case inr.refine_2
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
hf' : f = f' ∘ ⇑R
⊢ univ.sup (disjointed f' ∘ ⇑R) = univ.sup f

pp: case inr.refine_3
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
hf' : f = f' ∘ ⇑R
⊢ Pairwise (Disjoint on disjointed f' ∘ ⇑R)

Tactic:
· intro n
    simpa only [hf'] using! disjointed_le f' (R n)

Goal state after:
case inr.refine_2
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
hf' : f = f' ∘ ⇑R
⊢ univ.sup (disjointed f' ∘ ⇑R) = univ.sup f

case inr.refine_3
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
hf' : f = f' ∘ ⇑R
⊢ Pairwise (Disjoint on disjointed f' ∘ ⇑R)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x * (x ^ i * (y ^ (n - i) * ↑(n.choose i))) = x * (x ^ i * y ^ (n - i) * ↑(n.choose i))

Tactic:
mul_assoc

Goal state after:
case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x * (x ^ i * (y ^ (n - i) * ↑(n.choose i))) = x * (x ^ i * (y ^ (n - i) * ↑(n.choose i)))
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * (y * (y ^ (n - i.succ) * ↑(n.choose i.succ))) = x ^ i.succ * y * (y ^ (n - i.succ) * ↑(n.choose i.succ))

Tactic:
mul_assoc

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * (y * (y ^ (n - i.succ) * ↑(n.choose i.succ))) =
    x ^ i.succ * (y * (y ^ (n - i.succ) * ↑(n.choose i.succ)))
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
M✝ : Ideal α
hMmax : M✝.IsMaximal
⊢ ¬⊤ ≤ M✝

Tactic:
rw [top_le_iff]

Goal state after:
α : Type u
inst✝ : Semiring α
M✝ : Ideal α
hMmax : M✝.IsMaximal
⊢ ¬M✝ = ⊤
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y x✝ : α
⊢ x✝ ∈ span {x + y, y} ↔ x✝ ∈ span {x, y}

Tactic:
mem_span_pair

Goal state after:
α : Type u
inst✝ : Ring α
x y x✝ : α
⊢ (∃ a b, a * (x + y) + b * y = x✝) ↔ ∃ a b, a * x + b * y = x✝
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : b ∈ Submodule.span α ↑I
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ a * x * y + y * b ∈ I

Tactic:
mul_assoc

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : b ∈ Submodule.span α ↑I
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ a * (x * y) + y * b ∈ I
Module: Mathlib.RingTheory.Ideal.Span

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

Tactic:
mem_span_pair

Goal state after:
α : Type u
inst✝ : CommRing α
x y z x✝ : α
⊢ (∃ a b, a * (x + y * z) + b * y = x✝) ↔ ∃ a b, a * x + b * y = x✝
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : M ≠ ⊤
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Tactic:
rw [Ne, eq_top_iff, ← hs, span_le, Set.not_subset] at this

Goal state after:
α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : ∃ a ∈ s, a ∉ ↑M
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case empty
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
⊢ Multiset.sum 0 ^ (Multiset.card 0 * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) 0).toFinset

Tactic:
| empty =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
c : Set α
hc : c ∈ f
d : Set α
hd : d ∈ g
⊢ a ∩ b ∩ (c ∩ d) ∈ {s | ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b}

Tactic:
refine ⟨a ∩ c, inter_mem ha hc, b ∩ d, inter_mem hb hd, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
c : Set α
hc : c ∈ f
d : Set α
hd : d ∈ g
⊢ a ∩ b ∩ (c ∩ d) = a ∩ c ∩ (b ∩ d)
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
x✝ : Set α
⊢ x✝ ∈ l ↔ ∃ i, p i ∧ x✝ ∈ 𝓟 (s i)

Tactic:
simp only [h.mem_iff, mem_principal]

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

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

Tactic:
rcases isEmpty_or_nonempty (∀ j, α j) with H | H
  · rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]
    simp [← Classical.nonempty_pi]
  · have : ∀ j, Nonempty (α j) := Classical.nonempty_pi.1 H
    simp [comap_neBot_iff_frequently, *]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
⊢ (fun g ↦ g a) '' s ∈ f.seq (pure a)

Tactic:
rw [← seq_singleton]
    exact seq_mem_seq hs singleton_mem_pure

Goal state after:
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 : β
⊢ f a ≤ c → b ≤ c → c ∈ f '' Ici a

Tactic:
hac

Goal state after:
α : 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
⊢ b ≤ c → c ∈ f '' Ici a
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
a : α
ha : IsMax a
hs : IsCofinal s
⊢ a ∈ s

Tactic:
by
  obtain ⟨b, hb, hb'⟩ := hs a
  rwa [ha.eq_of_ge hb'] at hb

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

Goal state before:
pp: case empty
R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
singleton : ∀ (x : M), motive (R ∙ x) ⋯
sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯
⊢ motive (span R ↑∅) ⋯

Tactic:
| empty =>

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

Goal state before:
pp: case empty
R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
⊢ motive (span R ↑∅) ⋯

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : CompleteLattice α
⊢ DirSupInaccOn D s ↔
    ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → sSup d ∈ s → (d ∩ s).Nonempty

Tactic:
by
  simp [DirSupInaccOn, isLUB_iff_sSup_eq]

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
⊢ IsNormal (g ∘ f)

Tactic:
refine ⟨hg.strictMono.comp hf.strictMono, fun ha b hb ↦ ?_⟩
  simp_rw [Function.comp_apply, mem_upperBounds, forall_mem_image] at hb
  simpa [hg.le_iff_forall_le (hf.map_isSuccLimit ha), hf.lt_iff_exists_lt ha] using
    fun c d hd hc ↦ (hg.strictMono hc).le.trans (hb hd)

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

Goal state before:
pp: c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
c' : Cardinal.{u}
h' : lift.{u + 1, u} c' < univ.{u, u + 1}
e : lift.{v, u + 1} (lift.{u + 1, u} c') = c
⊢ ∃ c', c = lift.{max (u + 1) v, u} c'

Tactic:
exact ⟨c', by simp only [e.symm, lift_lift]⟩

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
⊢ a ≤ b → ∃ c, b = a + c

Tactic:
by
    refine inductionOn₂ a b fun α r _ β s _ ⟨f⟩ ↦ ?_
    obtain ⟨γ, t, _, ⟨g⟩⟩ := f.exists_sum_relIso
    exact ⟨type t, g.ordinalType_congr.symm⟩

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

Goal state before:
pp: case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
h : o < typeLT α
⊢ o ≤ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a

Tactic:
rw [← typein_enum _ h, typein_le_typein, not_lt]

Goal state after:
case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
h : o < typeLT α
⊢ (enum fun x1 x2 ↦ x1 < x2) ⟨o, h⟩ ≤ a
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ ↑n < o.card ↔ ↑n < o

Tactic:
by
  rw [← natCast_add_one_le_iff, ← succ_le_iff, ← Nat.cast_add_one, nat_le_card]
  rfl

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

Goal state before:
pp: b n : ℕ
⊢ ¬(n < b ∨ b ≤ 1) ↔ b ≤ n ∧ 1 < b

Tactic:
not_or,

Goal state after:
b n : ℕ
⊢ ¬n < b ∧ ¬b ≤ 1 ↔ b ≤ n ∧ 1 < b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * (c / b) ≤ c

Tactic:
apply mul_div_le

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

Goal state before:
pp: case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b + c < a * d * succ (b / d)

Tactic:
mul_assoc

Goal state after:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b + c < a * (d * succ (b / d))
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b x : ℕ
hx : x = 0
⊢ log b x ≤ x

Tactic:
by simp [hx]

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a ^ (b + 1) = a ^ b * a

Tactic:
by
  obtain rfl | h := eq_or_ne a 0
  · rw [zero_opow (add_pos_of_right zero_lt_one b).ne', mul_zero]
  · rw [opow_of_ne_zero h, opow_of_ne_zero h]
    exact limitRecOn_add_one ..

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

Goal state before:

Tactic:
c ^ log b n ≤ b ^ log b n := Nat.pow_le_pow_left hb _
    _ ≤ n := pow_log_le_self _ hn

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

Goal state before:
pp: case inr.inr.add_one
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b + c) = a ^ b * a ^ c
⊢ a ^ b * a ^ c * a = a ^ b * (a ^ c * a)

Tactic:
mul_assoc

Goal state after:
case inr.inr.add_one
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b + c) = a ^ b * a ^ c
⊢ a ^ b * (a ^ c * a) = a ^ b * (a ^ c * a)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ
b n : ℕ
hb : 1 < b
hn : 1 < n
c : ℕ
⊢ clog b n ≤ c + 1 ↔ clog b ((n + b - 1) / b) + 1 ≤ c + 1

Tactic:
simp only [clog_le_iff_le_pow, Nat.pow_add_one, Nat.add_le_add_iff_right, Nat.zero_lt_of_lt hb,
      div_le_iff_le_mul, hb]
    grind

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

Goal state before:
pp: b o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 0 < o / b ^ log b o

Tactic:
rcases eq_zero_or_pos b with (rfl | hb)
  · simpa using pos_iff_ne_zero.2 ho
  · rw [div_pos (opow_ne_zero _ hb.ne')]
    exact opow_log_le_self b ho

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ derivFamily f = enumOrd (⋂ i, fixedPoints (f i))

Tactic:
rw [eq_comm, eq_enumOrd _ (not_bddAbove_fp_family H)]

Goal state after:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ StrictMono (derivFamily f) ∧ Set.range (derivFamily f) = ⋂ i, fixedPoints (f i)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case right
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ Set.range (derivFamily f) = ⋂ i, fixedPoints (f i)

Tactic:
Set.range_eq_iff

Goal state after:
case right
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ (∀ (a : Ordinal.{u}), derivFamily f a ∈ ⋂ i, fixedPoints (f i)) ∧
    ∀ b ∈ ⋂ i, fixedPoints (f i), ∃ a, derivFamily f a = b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ⊢ nfp 0 = id

Tactic:
by
  ext
  exact nfp_zero_left _

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

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ a * ω ≤ b

Tactic:
rw [← nfp_add_zero a, ← 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.Ordinal.FixedPoint

Goal state before:
pp: case inl
b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ 0 ^ ω
⊢ nfp (fun x ↦ 0 * x) b = 0 ^ ω

Tactic:
zero_opow omega0_ne_zero

Goal state after:
case inl
b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ 0
⊢ nfp (fun x ↦ 0 * x) b = 0 ^ ω
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inl
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ 0 ^ ω ≤ b

Tactic:
zero_opow omega0_ne_zero

Goal state after:
case inl
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ 0 ≤ b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: x : Ordinal.{u_1}
⊢ x ∈ range ⇑preOmega ↔ x.IsInitial

Tactic:
range_preOmega,

Goal state after:
x : Ordinal.{u_1}
⊢ x ∈ {x | x.IsInitial} ↔ x.IsInitial
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case mpr
o : Ordinal.{u}
⊢ (o = 0 ∨ o ∈ Set.range fun x ↦ ω ^ x) → IsPrincipal (fun x1 x2 ↦ x1 + x2) o

Tactic:
rintro (rfl | ⟨a, rfl⟩)
    exacts [isPrincipal_zero, isPrincipal_add_omega0_opow a]

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

Goal state before:
pp: a b : Ordinal.{u_1}
h : a < b
⊢ preBeth a < preBeth b

Tactic:
conv_rhs => rw [preBeth]

Goal state after:
a b : Ordinal.{u_1}
h : a < b
⊢ preBeth a < ⨆ a, 2 ^ preBeth ↑a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inl
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ ω ^ c * n * b < ω ^ c * ω

Tactic:
mul_assoc

Goal state after:
case inr.inl
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ ω ^ c * (n * b) < ω ^ c * ω
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
t : Set ↑s
ht : IsCofinal t
ht' : typeLT ↑t = (Order.cof α).ord
⊢ typeLT ↑(Subtype.val '' t) = typeLT ↑t

Tactic:
exact ((Subtype.strictMono_coe _).strictMonoOn _).orderIso.ordinalType_congr.symm

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

Goal state before:
pp: case inr
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b

Tactic:
· apply le_antisymm
    · obtain ⟨x, xb, ax⟩ :=
        (lt_opow_of_isSuccLimit omega0_ne_zero (isSuccLimit_opow_left isSuccLimit_omega0 b0)).1 h
      grw [ax, ← opow_add, add_omega0_opow xb]
    · conv_lhs => rw [← one_mul (ω ^ _)]
      grw [one_le_iff_pos.2 a0]

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

Goal state before:
pp: case refine_1
a b : Cardinal.{u_1}
h : a * b = a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
rcases le_or_gt ℵ₀ a with ha | ha
    · have : a ≠ 0 := by
        rintro rfl
        exact ha.not_gt aleph0_pos
      left
      rw [and_assoc]
      use ha
      constructor
      · rw [← not_lt]
        exact fun hb => ne_of_gt (hb.trans_le (le_mul_left this)) h
      · rintro rfl
        apply this
        rw [mul_zero] at h
        exact h.symm
    right
    by_cases h2a : a = 0
    · exact Or.inr h2a
    have hb : b ≠ 0 := by
      rintro rfl
      apply h2a
      rw [mul_zero] at h
      exact h.symm
    left
    rw [← h, mul_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
    rcases ha with (rfl | rfl | ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩)
    · contradiction
    · contradiction
    rw [← Ne] at h2a
    rw [← Cardinal.one_le_iff_ne_zero] at h2a hb
    norm_cast at h2a hb h ⊢
    apply le_antisymm _ hb
    rw [← not_lt]
    apply fun h2b => ne_of_gt _ h
    conv_rhs => left; rw [← mul_one n]
    rw [Nat.mul_lt_mul_left]
    · exact id
    apply Nat.lt_of_succ_le h2a

Goal state after: