mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b

Tactic:
encard_le_one_iff_eq,

Goal state after:
α : Type u_1
s : Set α
⊢ (s = ∅ ∨ ∃ x, s = {x}) ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case insert
η : 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
i : η
I : Finset η
hnotMem : i ∉ I
ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
⊢ x ∈ H

Tactic:
| insert i I hnotMem ih =>

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

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ ({a} \ {b} ∪ s \ {b}).ncard = ({a} ∪ s \ {b}).ncard

Tactic:
sdiff_singleton_eq_self fun h ↦ ha (by rwa [← mem_singleton_iff.mp h])

Goal state after:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ ({a} ∪ s \ {b}).ncard = ({a} ∪ s \ {b}).ncard
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:
by cases c; congr!

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
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : p ≤ comap 0 q
⊢ p.mapQ q 0 h = 0

Tactic:
by
  ext
  simp

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
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
R₃ : Type u_5
M₃ : Type u_6
inst✝³ : Ring R₃
inst✝² : AddCommGroup M₃
inst✝¹ : Module R₃ M₃
p₂ : Submodule R₂ M₂
p₃ : Submodule R₃ M₃
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : p ≤ comap f p₂
hg : p₂ ≤ comap g p₃
h : p ≤ comap f (comap g p₃)
⊢ p.mapQ p₃ (g ∘ₛₗ f) h = p₂.mapQ p₃ g hg ∘ₛₗ p.mapQ p₂ f hf

Tactic:
by
  ext
  simp

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
h : p ≤ comap LinearMap.id p
⊢ p.mapQ p LinearMap.id h = LinearMap.id

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
S : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : Semiring S
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid M₄
inst✝⁷ : AddCommMonoid M₅
inst✝⁶ : AddCommMonoid M₆
inst✝⁵ : Module R M
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M₄
inst✝¹ : Module R M₅
inst✝ : Module R M₆
f✝ f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
c : R
x : M
⊢ Function.prod (⇑f) (⇑g) (c • x) = (RingHom.id R) c • Function.prod (⇑f) (⇑g) x

Tactic:
simp only [Function.prod_apply, Prod.smul_mk, map_smul, RingHom.id_apply]

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 p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
⊢ factor H2 ∘ₗ factor H1 = factor ⋯

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' P Q : Submodule R M
hf : map (↑(LinearEquiv.refl R M)) P = Q
⊢ P = Q

Tactic:
by simpa using hf

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

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

Tactic:
by
  refine ⟨fun hx k ↦ ?_, fun hx ↦ ?_⟩
  · induction hx using span_induction with
    | mem x h => obtain ⟨i, rfl⟩ := h; simp
    | zero => simp
    | add u v _ _ hu hv => simp [hu, hv]
    | smul t u _ hu => simp [hu]
  · have := Fintype.ofFinite ι
    suffices x = ∑ i : ι, x (Sum.inl i) • Pi.single (M := fun _ ↦ R) (Sum.inl i) (1 : R) by
      rw [this]
      exact sum_mem <| fun i _ ↦ SMulMemClass.smul_mem _ <| subset_span <| Set.mem_range_self i
    ext (i | i)
    · simp [single_apply]
    · simp [hx i]

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₂
m : M
n : M₂
⊢ (m, n) ∈ fst R M M₂ ⊔ snd R M M₂

Tactic:
rw [show (m, n) = (m, 0) + (0, n) by simp]

Goal state after:
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) + (0, n) ∈ fst R M M₂ ⊔ snd R M M₂
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : ConditionallyCompleteLattice β
inst✝¹ : Finite ι
inst✝ : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : MonotoneOn g s
hs : ∀ (i : ι), f i ∈ s
j : ι
hj : f j = ⨆ i, f i
⊢ g (⨆ i, f i) = ⨆ i, g (f i)

Tactic:
rw [← hj]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : ConditionallyCompleteLattice β
inst✝¹ : Finite ι
inst✝ : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : MonotoneOn g s
hs : ∀ (i : ι), f i ∈ s
j : ι
hj : f j = ⨆ i, f i
⊢ g (f j) = ⨆ i, g (f i)
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ x_1, f x_1 = x) ↔ f' x.1 = x.2
s : S
h : H
⊢ (h, f' h) ∈ f.range

Tactic:
LinearMap.mem_range,

Goal state after:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ x_1, f x_1 = x) ↔ f' x.1 = x.2
s : S
h : H
⊢ ∃ y, f y = (h, f' h)
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n k : ℕ
⊢ (Iic k).sup (s ∘ id) = s k

Tactic:
rw [← apply_sup_eq_sup_comp_of_nonempty hs nonempty_Iic, sup_Iic]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ.inr.hab
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iio x) < #(Iic x)

pp: case succ.inr.hbc
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iic x) ≤ #(Iio i)

Tactic:
· simpa only [Iic_eq_cons_Iio, card_cons] using Nat.lt_succ_self _

Goal state after:
case succ.inr.hbc
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iic x) ≤ #(Iio i)
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ f (succ i) \ (Iio (succ i)).sup f = f (succ i) \ (Iic i).sup f

Tactic:
congr 2 with m

Goal state after:
case e_a.e_s
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
m : ι
⊢ m ∈ Iio (succ i) ↔ m ∈ Iic i
Module: Mathlib.Data.Multiset.NatAntidiagonal

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

Tactic:
rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal,
    map_coe, coe_add, List.singleton_append, cons_coe]

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

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
⊢ ∀ {a b : ι},
    { toFun := fun i ↦ (toZ ⊥ i).toNat, invFun := fun n ↦ succ^[n] ⊥, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun i ↦ (toZ ⊥ i).toNat, invFun := fun n ↦ succ^[n] ⊥, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
intro i j

Goal state after:
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
i j : ι
⊢ { toFun := fun i ↦ (toZ ⊥ i).toNat, invFun := fun n ↦ succ^[n] ⊥, left_inv := ⋯, right_inv := ⋯ } i ≤
      { toFun := fun i ↦ (toZ ⊥ i).toNat, invFun := fun n ↦ succ^[n] ⊥, left_inv := ⋯, right_inv := ⋯ } j ↔
    i ≤ j
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
⊢ ∀ {a b : ι},
    { toFun := fun i ↦ ⟨(toZ ⊥ i).toNat, ⋯⟩, invFun := fun n ↦ succ^[↑n] ⊥, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun i ↦ ⟨(toZ ⊥ i).toNat, ⋯⟩, invFun := fun n ↦ succ^[↑n] ⊥, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
intro i j

Goal state after:
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
i j : ι
⊢ { toFun := fun i ↦ ⟨(toZ ⊥ i).toNat, ⋯⟩, invFun := fun n ↦ succ^[↑n] ⊥, left_inv := ⋯, right_inv := ⋯ } i ≤
      { toFun := fun i ↦ ⟨(toZ ⊥ i).toNat, ⋯⟩, invFun := fun n ↦ succ^[↑n] ⊥, left_inv := ⋯, right_inv := ⋯ } j ↔
    i ≤ j
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + k + j = n

Tactic:
rw [add_right_comm, hl]

Goal state after:
case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ n - k + k = n
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: α : Type u
inst✝² : Semiring α
inst✝¹ : Nontrivial α
inst✝ : NoZeroDivisors α
⊢ ⊥.primeCompl = nonZeroDivisors α

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ a * b * a = 0

Tactic:
rw [← nsmul_right_inj ((Nat.zero_ne_add_one 1).symm), nsmul_zero]

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ (1 + 1) • (a * b * a) = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
S : Ideal R
inst✝ : S.IsTwoSided
⊢ factor ⋯ = RingHom.id (R ⧸ S)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S T U : Ideal R
inst✝² : S.IsTwoSided
inst✝¹ : T.IsTwoSided
inst✝ : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
⊢ (factor H2).comp (factor H1) = factor ⋯

Tactic:
by
  ext
  simp

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

Goal state before:
pp: ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
⊢ span (range fun i ↦ Pi.single i 1) = ⊤

Tactic:
_root_.eq_top_iff

Goal state after:
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
⊢ ⊤ ≤ span (range fun i ↦ Pi.single i 1)
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
⊢ (submodule fun x ↦ ⊤) = ⊤

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
G : Filter δ
⊢ comap φ (comap ψ G) = comap θ (comap ρ G)

Tactic:
Filter.comap_comap,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
G : Filter δ
⊢ comap (ψ ∘ φ) G = comap θ (comap ρ G)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
⊢ map (g ∘ f) F = F

Tactic:
hfg.comp_eq_id,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
⊢ map id F = F
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
⊢ comap (g ∘ f) F = F

Tactic:
hfg.comp_eq_id,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
⊢ comap id F = F
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
⊢ (comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β

Tactic:
by
  cases isEmpty_or_nonempty β
  · rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]; simp [*]
  · simp [comap_neBot_iff_frequently, *]

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

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o.pred < o ↔ ¬IsSuccPrelimit o

Tactic:
rw [(pred_le_self o).lt_iff_ne]
  exact pred_eq_iff_isSuccPrelimit.not

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

Goal state before:
pp: s : Set Ordinal.{u}
⊢ #↑(Iio (sInf sᶜ)) ≤ #↑s

Tactic:
refine mk_le_mk_of_subset fun x (hx : x < _) ↦ ?_

Goal state after:
s : Set Ordinal.{u}
x : Ordinal.{u}
hx : x < sInf sᶜ
⊢ x ∈ s
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o : Ordinal.{u}
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty

Tactic:
obtain ⟨a, ha⟩ := bddAbove_of_small (s := enumOrd s '' Iio o)

Goal state after:
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o a : Ordinal.{u}
ha : a ∈ upperBounds (enumOrd s '' Iio o)
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.card ≤ 1 ↔ o ≤ 1

Tactic:
simpa using card_le_nat (n := 1)

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ (#↑s).ord < type r

Tactic:
by
  grw [← ord_le_type, ord_lt_ord, ← mk_univ (α := α)]
  exact card_lt_card_of_left_finite hfin h.ssubset_univ

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

Goal state before:
pp: a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
⊢ (a * b + c) / (a * d) = b / d

Tactic:
obtain rfl | hd := eq_or_ne d 0
  · rw [mul_zero, div_zero, div_zero]
  · have H := mul_ne_zero hc.ne_zero hd
    apply le_antisymm
    · rw [← lt_succ_iff, ← lt_mul_iff_div_lt H, mul_assoc]
      · grw [hc, ← mul_succ]
        gcongr
        rw [succ_le_iff]
        exact lt_mul_succ_div b hd
    · grw [← mul_le_iff_le_div H, mul_assoc, mul_div_le b d, ← le_self_add]

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

Goal state before:
pp: case inl
b n : ℕ
h₁ : b ^ 0 ≤ n
h₂ : n < b ^ (0 + 1)
⊢ log b n = 0

Tactic:
Nat.pow_one

Goal state after:
case inl
b n : ℕ
h₁ : b ^ 0 ≤ n
h₂ : n < b
⊢ log b n = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
⊢ b ^ 1 ≤ n ∧ n < b ^ 1 * b ^ 1 ↔ b ≤ n ∧ n < b * b

Tactic:
Nat.pow_one

Goal state after:
b n : ℕ
⊢ b ≤ n ∧ n < b * b ↔ b ≤ n ∧ n < b * b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
contrapose!; exact apply_lt_nfpFamily_iff H

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

Goal state before:
pp: case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ (n + b - 1) / b ≤ 1

Tactic:
rw [← Nat.lt_succ_iff, Nat.div_lt_iff_lt_mul] <;> lia

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

Goal state before:
pp: case refine_2
a✝ a : Ordinal.{u}
h : deriv (fun x ↦ a✝ + x) a = a✝ * ω + a
⊢ deriv (fun x ↦ a✝ + x) (succ a) = a✝ * ω + succ a

Tactic:
rw [succ_eq_add_one, deriv_add_one, h, ← add_assoc]
    exact nfp_eq_self (add_eq_right_iff_mul_omega0_le.2 (le_self_add.trans (le_succ _)))

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

Goal state before:
pp: case mp
a : Ordinal.{u_1}
⊢ ω_ a ∈ {x | ω ≤ x ∧ x.IsInitial}

Tactic:
exact ⟨omega0_le_omega a, isInitial_omega a⟩

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

Goal state before:
pp: case ind.mk.hbc
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := ⋯
f : α × α ↪ Lex (α × Lex (α × α)) := ⋯
s : α × α → α × α → Prop := ⋯
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
⊢ #↑(Iio q) * #↑(Iio q) < #α

Tactic:
rcases lt_or_ge #(Iio q) ℵ₀ with hq | hq

Goal state after:
case ind.mk.hbc.inl
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
hq : #↑(Iio q) < ℵ₀
⊢ #↑(Iio q) * #↑(Iio q) < #α

case ind.mk.hbc.inr
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
hq : ℵ₀ ≤ #↑(Iio q)
⊢ #↑(Iio q) * #↑(Iio q) < #α
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof = 0 ↔ o = 0

Tactic:
by
  rw [← cof_toType, cof_eq_zero_iff, isEmpty_toType_iff]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof = 1 ↔ o ∈ range succ

Tactic:
cases o using inductionOnWellOrder with | type α
  rw [cof_type, Order.cof_eq_one_iff, type_lt_mem_range_succ_iff]
  simp_rw [isTop_iff_isMax]

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

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

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

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

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
rcases le_or_gt ℵ₀ a with ha | ha
  · rw [add_eq_max ha]
    exact le_max_left _ _
  · rcases le_or_gt ℵ₀ b with hb | hb
    · rw [add_comm, add_eq_max hb, max_comm]
      exact le_max_left _ _
    · exact le_max_of_le_right (add_lt_aleph0 ha hb).le

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x✝¹ x✝ : Cardinal.{u_1}
hlt : x✝¹ < x✝
⊢ (fun a ↦ a * ↑n) x✝¹ < (fun a ↦ a * ↑n) x✝

Tactic:
by simpa [mul_comm] using natCast_mul_strictMono hn hlt

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

Goal state before:
pp: o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hι' : (#ι).ord = type r
⊢ ∃ f, o.cof.ord.blsub f = o

Tactic:
rw [← @blsub_eq_lsub' ι r hr] at hf

Goal state after:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = o
hι' : (#ι).ord = type r
⊢ ∃ f, o.cof.ord.blsub f = o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
rw [← @blsub_eq_lsub' ι r hr] at hf

Goal state after:
b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = b
hι' : (#ι).ord = type r
⊢ a ≤ #ι
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : o.bsup f = o.blsub f
⊢ (o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
rw [H]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : o.bsup f = o.blsub f
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
by_cases hb' : IsMin b

Goal state after:
case pos
a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccPrelimit b
hb' : IsMin b
⊢ (a * b).cof = b.cof

case neg
a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccPrelimit b
hb' : ¬IsMin b
⊢ (a * b).cof = b.cof
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b ↦
    Eq.mp (Eq.trans mem_iUnion._simp_1 (congrArg Exists (funext fun i ↦ SetLike.mem_coe._simp_1)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b ↦ ⟨f ⋯.choose, ⋯⟩
a : α
p : β
m✝ : p ∈ u' ⁻¹' {⟨f a, ⋯⟩}
m : f ⋯.choose = f a
⊢ p ∈ ↑(f a)

Tactic:
rw [← m]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b ↦
    Eq.mp (Eq.trans mem_iUnion._simp_1 (congrArg Exists (funext fun i ↦ SetLike.mem_coe._simp_1)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b ↦ ⟨f ⋯.choose, ⋯⟩
a : α
p : β
m✝ : p ∈ u' ⁻¹' {⟨f a, ⋯⟩}
m : f ⋯.choose = f a
⊢ p ∈ ↑(f ⋯.choose)