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 → G
hφ : RightInverse ψ ⇑φ
x : G ⧸ φ.ker
⊢ (kerLift φ) ↑(ψ ((kerLift φ) x)) = (kerLift φ) x

Tactic:
kerLift_mk,

Goal state after:
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 → G
hφ : RightInverse ψ ⇑φ
x : G ⧸ φ.ker
⊢ φ (ψ ((kerLift φ) x)) = (kerLift φ) x
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}

Tactic:
by
  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
  · exact iff_of_true (by simp) (Or.inl rfl)
  rw [ncard_le_one_iff hs]
  refine ⟨fun h ↦ Or.inr ⟨x, (singleton_subset_iff.mpr hx).antisymm' fun y hy ↦ h hy hx⟩, ?_⟩
  grind

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) ↑(g ((kerLift f) x)) = (kerLift f) x

Tactic:
kerLift_mk,

Goal state after:
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
⊢ f (g ((kerLift f) x)) = (kerLift f) x
Module: Mathlib.RingTheory.Congruence.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ (fun c ↦ c.toCon) c = (fun c ↦ c.toCon) d → c = d

Tactic:
cases c

Goal state after:
case mk
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
d : RingCon R
toCon✝ : Con R
add'✝ : ∀ {w x y z : R}, toCon✝.toSetoid w x → toCon✝.toSetoid y z → toCon✝.toSetoid (w + y) (x + z)
⊢ (fun c ↦ c.toCon) { toCon := toCon✝, add' := add'✝ } = (fun c ↦ c.toCon) d → { toCon := toCon✝, add' := add'✝ } = d
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 ι
I J : Set ι
hI : I.Finite
hIJ : Codisjoint I J
⊢ ⨅ i ∈ J, (proj i).ker ≤ ⨆ i ∈ I, (single R φ i).range

Tactic:
by
  lift I to Finset ι using hI
  intro b hb
  simp only [mem_iInf, mem_ker, proj_apply] at hb
  rw [←
    show (∑ i ∈ I, Pi.single i (b i)) = b by
      ext i
      rw [Finset.sum_apply, ← Pi.single_eq_same i (b i)]
      refine Finset.sum_eq_single i (fun j _ ne => Pi.single_eq_of_ne ne.symm _) ?_
      intro hiI
      rw [Pi.single_eq_same]
      exact hb _ ((hIJ.top_le trivial).resolve_left hiI)]
  exact sum_mem_biSup fun i _ => mem_range_self (single R φ i) (b i)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
⊢ Ico (succ a) b = Ioo a b

Tactic:
by_cases ha : IsMax a
  · rw [Ico_eq_empty (ha.mono <| le_succ _).not_lt, Ioo_eq_empty ha.not_lt]
  · ext x
    rw [mem_Ico, mem_Ioo, succ_le_iff_of_not_isMax ha]

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
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
hk : f.ker ≤ span R (⇑f ⁻¹' s)
⊢ comap f (span R₂ s) ≤ span R (⇑f ⁻¹' s)

Tactic:
← left_eq_sup

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ f.ker
⊢ comap f (span R₂ s) ≤ span R (⇑f ⁻¹' s)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
⊢ (update f i b j) c = update (fun i ↦ (f i) c) i (b c) j

Tactic:
by_cases h : j = i
  · rw [h, update_self, update_self]
  · rw [update_of_ne h, update_of_ne h]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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₂
p : Submodule R M
⊢ map (inl R M M₂) p = p.prod ⊥

Tactic:
by
  ext ⟨x, y⟩
  simp only [and_left_comm, eq_comm, mem_map, Prod.mk_inj, inl_apply, mem_bot, exists_eq_left',
    mem_prod]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ f.range), u ∘ₛₗ f = v ∘ₛₗ f → u = v
⊢ f.range = ⊤

Tactic:
by
  have h₁ : (0 : M₂ →ₗ[R₂] M₂ ⧸ (range f)).comp f = 0 := zero_comp _
  rw [← Submodule.ker_mkQ (range f), ← h 0 (range f).mkQ (Eq.trans h₁ (range_mkQ_comp _).symm)]
  exact ker_zero

Goal state after:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
⊢ ↑(Iio (succ b)) = ↑(Iic b)

Tactic:
by simpa using Set.Iio_succ_eq_Iic_of_not_isMax hb

Goal state after:
Module: Mathlib.Data.Fintype.Pigeonhole

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), Finite ↑(f ⁻¹' {y})
⊢ False

Tactic:
cases nonempty_fintype β

Goal state after:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), Finite ↑(f ⁻¹' {y})
val✝ : Fintype β
⊢ False
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mpr
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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ ↑p₁
h2 : (x1, x2).2 ∈ ↑p₂
⊢ (x1, x2) ∈ q

Tactic:
have h1' : (LinearMap.inl R _ _) x1 ∈ q := by
      apply hH
      simpa using h1

Goal state after:
case mpr
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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ ↑p₁
h2 : (x1, x2).2 ∈ ↑p₂
h1' : (inl R M M₂) x1 ∈ q
⊢ (x1, x2) ∈ q
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ.inl
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) < n + 1
⊢ (partialSups (disjointed f)) i = (partialSups f) i

Tactic:
exact ih _ <| Nat.le_of_lt_succ hn

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

Goal state before:
pp: A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
a b : A
this : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
⊢ (a, b) ∈ {x ∈ antidiagonal n | x.1 = m} ↔ (a, b) ∈ if m ≤ n then {(m, n - m)} else ∅

Tactic:
rw [mem_filter, mem_antidiagonal, apply_ite (fun n ↦ (a, b) ∈ n), mem_singleton,
      Prod.mk_inj, ite_prop_iff_or]
    simpa [← and_assoc, @and_right_comm _ (a = _), and_congr_left_iff]

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_2
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (∃ a, a + j = k ∧ a + (n - k) = i) → i + j = n ∧ j ≤ k

Tactic:
rintro ⟨l, hl, rfl⟩

Goal state after:
case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ l + (n - k) + j = n ∧ j ≤ k
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_2
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (∃ a, a + j = n - k ∧ a + k = i) → i + j = n ∧ k ≤ i

Tactic:
rintro ⟨l, hl, rfl⟩

Goal state after:
case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + k + j = n ∧ k ≤ l + k
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
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h1 : q * p * q = q * p
h2 : p * q + q * (p * q) - p * q = p * q
⊢ Commute p q

Tactic:
add_sub_cancel_left,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h1 : q * p * q = q * p
h2 : q * (p * q) = p * q
⊢ Commute p q
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 ^ (n + 1) * ↑x ^ (n + 1) ∈ span {↑x ^ (n + 1)}

Tactic:
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.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)
⊢ ↑x ^ (n + 1) ∣ f x ^ (n + 1) * ↑x ^ (n + 1)

Tactic:
exact ⟨f x ^ (n + 1), mul_comm _ _⟩

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

Goal state before:
pp: case inr.h
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
⊢ Finsupp.single 0 (f.prodOfFinsuppNat y).1 + mapDomain (fun x ↦ x + 1) ((comapDomain.addMonoidHom ⋯) x) =
    Finsupp.single 0 (f.prodOfFinsuppNat y).1 + mapDomain (fun x ↦ x + 1) ((comapDomain.addMonoidHom ⋯) y)

Tactic:
congr 2

Goal state after:
case inr.h.e_a.e_v
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
⊢ (comapDomain.addMonoidHom ⋯) x = (comapDomain.addMonoidHom ⋯) y
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:
by
  refine eq_empty_of_subset_empty ?_
  rw [← iInter_Iic_eq_empty_iff.mpr hf]
  gcongr
  exact Iio_subset_Iic_self

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

Goal state after:
case inl
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

case inr
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : Nonempty ((j : ι) → α j)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot
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 : ι
hi : ∃ b, P i b
⊢ P i (if h : ∃ b, P i b then h.choose else ⋯.some)

Tactic:
exact dif_pos hi ▸ hi.choose_spec

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
hm : Injective m
f₁ f₂ : Filter α
⊢ Disjoint (map m f₁) (map m f₂) ↔ Disjoint f₁ f₂

Tactic:
by
  simp only [disjoint_iff, ← map_inf hm, map_eq_bot_iff]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsRightCancelMul β
⊢ IsRightCancelMul α

Tactic:
by
  let := e.mul; exact e.injective.isRightCancelMul _ fun _ _ ↦ e.apply_symm_apply _

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬⟨N₀, h₁⟩ < x
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ x ∈ R ∙ x ⊔ N₀

Tactic:
exact (le_sup_left : R ∙ x ≤ _) (Submodule.mem_span_singleton_self _)

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ cof α ≠ 0 ↔ Nonempty α

Tactic:
by
  simpa using cof_eq_zero_iff.not

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ cof α ≠ 1 ↔ NoTopOrder α

Tactic:
rw [← not_iff_not, not_not, noTopOrder_iff, cof_eq_one_iff]
  simp

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
⊢ DirSupClosedOn D (s ∪ t)

Tactic:
intro d

Goal state after:
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
⊢ d ∈ D → d ⊆ s ∪ t → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s ∪ t
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
⊢ DirSupInaccOn D s

Tactic:
intro d

Goal state after:
α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
d : Set α
⊢ d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ DirSupClosed {a}

Tactic:
intro d

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : α
d : Set α
⊢ d ⊆ {a} → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a_4 : α⦄, IsLUB d a_4 → a_4 ∈ {a}
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case mpr.isMin
α : 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 : α
ha : IsMin a
⊢ f a = g a

Tactic:
rw [ha.eq_bot, H₁]

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

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a + b < a + c ↔ b < c

Tactic:
by
  rw [← not_le, ← not_le, add_le_add_iff_left]

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

Goal state before:
pp: case refine_4
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a < type r → a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯)

Tactic:
· refine inductionOn a ?_
    rintro β s wo ⟨g⟩
    exact ⟨_, g.subrelIso.ordinalType_congr⟩

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

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a + b - (a + c) = b - c

Tactic:
← sub_sub,

Goal state after:
a b c : Ordinal.{u_4}
⊢ a + b - a - c = b - c
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : Ordinal.{u}
hi : i < o
⊢ familyOfBFamily' r ho f ((enum r) ⟨i, ⋯⟩) = f i hi

Tactic:
simp only [familyOfBFamily', typein_enum]

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

Goal state before:
pp: o : Ordinal.{u}
⊢ #↑(Iio o) = Cardinal.lift.{u + 1, u} o.card

Tactic:
lift_card,

Goal state after:
o : Ordinal.{u}
⊢ #↑(Iio o) = (lift.{u + 1, u} o).card
Module: Mathlib.Data.Nat.Log

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

Tactic:
rw [← Nat.pow_two, ← Nat.pow_mul]

Goal state after:
n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
hfuel₀ : fuel ≠ 0
⊢ n < b ^ (2 * fuel)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
ha : IsSuccLimit a
⊢ IsSuccPrelimit (a * b)

Tactic:
obtain rfl | hb := eq_zero_or_pos b
  · rw [mul_zero]
    exact isSuccPrelimit_zero
  · exact (isSuccLimit_mul_left ha hb).isSuccPrelimit

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
⊢ a / c ≤ b / c

Tactic:
by
  obtain rfl | hc := eq_or_ne c 0
  · rw [div_zero, div_zero]
  · rw [← mul_le_iff_le_div hc]
    exact (mul_div_le a c).trans h

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
by
  by_cases a = 0 <;> by_cases b = 0 <;> simp_all [opow_ne_zero]

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

Goal state before:
pp: case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ x * y + z - (x * y + x * (z / x)) = z % x

pp: case inr.b0
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ x ≠ 0

Tactic:
← sub_sub,

Goal state after:
case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ x * y + z - x * y - x * (z / x) = z % x

case inr.b0
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ x ≠ 0
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
obtain ⟨i⟩ := hι

Goal state after:
case refine_1
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ nfpFamily f a
i : ι
⊢ b ≤ nfpFamily f a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : IsPrincipal op o
ho' : IsSuccLimit o
⊢ op a o ≤ o

Tactic:
H.apply_of_isSuccLimit ho',

Goal state after:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : IsPrincipal op o
ho' : IsSuccLimit o
⊢ ⨆ b, op a ↑b ≤ o
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 + (ω ^ log ω a * ↑n + a % ω ^ log ω a) - ω ^ log ω a < a

Tactic:
Ordinal.add_sub_cancel

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

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

Tactic:
by
  rw [range_preOmega, mem_ofPred]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ o)

Tactic:
by
  obtain rfl | ha' := eq_or_ne o 0
  · rw [opow_zero, isPrincipal_one_iff, add_zero]
  · rw [isPrincipal_add_iff_add_self_lt]
    intro a ha
    obtain ⟨c, hc, m, hm⟩ := (lt_omega0_opow ha').1 ha
    apply (add_lt_add_of_le_of_lt hm.le hm).trans_le
    rw [← mul_add, ← Nat.cast_add]
    exact (opow_mul_lt_opow (natCast_lt_omega0 _) hc).le

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

Goal state before:
pp: case ind.mk
α : 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
⊢ (typein s).toRelEmbedding p < typeLT α

Tactic:
← hα,

Goal state after:
case ind.mk
α : 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
⊢ (typein s).toRelEmbedding p < (#α).ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
hr',

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
⊢ typeLT ↑(Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a}) ≤ type r
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a b o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : ↑(Iio b) → ↑(Iio a)
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ IsCofinal (f '' range g)

Tactic:
exact hg.isCofinal_range.image hf.strictMono.monotone hf.isCofinal_range

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

Goal state before:
pp: c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #↑s ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
⊢ (sSup s).card ≤ c

Tactic:
sSup_eq_iSup'

Goal state after:
c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #↑s ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
⊢ (⨆ a, ↑a).card ≤ c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
c : Ordinal.{u_1}
hc : ℵ₀ < c.cof
hf : ∀ i < c, f i < c
a : Ordinal.{u_1}
⊢ Cardinal.lift.{u_1, 0} #Unit < c.cof

Tactic:
simpa using Cardinal.one_lt_aleph0.trans hc

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

Goal state before:
pp: c : Cardinal.{u_1}
H : c.IsRegular
⊢ 0 < c.ord

Tactic:
by
  rw [Cardinal.lt_ord, card_zero]
  exact H.pos

Goal state after: