mathlib-initiative/mathlib-tactics huggingface dataset:
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
Pbot : P ⊥
⊢ P N

Tactic:
induction n generalizing N with
  | zero =>
    suffices N = ⊥ by rwa [this]
    apply Basis.eq_bot_of_rank_eq_zero b _ fun m hv => Nat.le_zero.mp (rank_le _ hv)
  | succ n rank_ih =>
    apply ih
    intro N' N'_le x x_mem x_ortho
    apply rank_ih
    intro m v hli
    refine Nat.succ_le_succ_iff.mp (rank_le (Fin.cons ⟨x, x_mem⟩ fun i => ⟨v i, N'_le (v i).2⟩) ?_)
    convert! hli.finCons' x _ ?_
    · ext i
      refine Fin.cases ?_ ?_ i <;> simp
    · intro c y hy hc
      refine x_ortho c y (Submodule.span_le.mpr ?_ hy) hc
      rintro _ ⟨z, rfl⟩
      exact (v z).2

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

Goal state before:
pp: α : Type u_1
a : α
s : Set α
h : s.Infinite
⊢ s.ncard ≤ (insert a s).ncard

Tactic:
(rw [h.ncard]; exact Nat.zero_le _)

Goal state after:
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 : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
⊢ ((b.repr m).sum fun i a ↦ a • b i) ∈ span R (range ⇑b)

Tactic:
refine sum_mem fun i _ => ?_

Goal state after:
ι : 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 : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
i : ι
x✝ : i ∈ (b.repr m).support
⊢ (fun i a ↦ a • b i) i ((b.repr m) i) ∈ span R (range ⇑b)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
h₁ : {t | t ⊆ ↑s ∧ t.ncard = n} ⊆ range SetLike.coe
⊢ {t | t ⊆ ↑s ∧ t.ncard = n}.ncard = (↑s).ncard.choose n

Tactic:
have h₂ : (↑) ⁻¹' {t ⊆ (s : Set α) | t.ncard = n} = (s.powersetCard n : Set (Finset α)) := by
    ext t
    simp

Goal state after:
α : Type u_1
n : ℕ
s : Finset α
h₁ : {t | t ⊆ ↑s ∧ t.ncard = n} ⊆ range SetLike.coe
h₂ : SetLike.coe ⁻¹' {t | t ⊆ ↑s ∧ t.ncard = n} = ↑(Finset.powersetCard n s)
⊢ {t | t ⊆ ↑s ∧ t.ncard = n}.ncard = (↑s).ncard.choose n
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ.rangeRestrict a = φ.rangeRestrict b
⊢ (leftRel φ.ker) a b

Tactic:
rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h,
        φ.rangeRestrict.map_inv, inv_mul_cancel]

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

Goal state before:
pp: 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⟩

Tactic:
refine Quotient.eq.mpr ?_

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 := 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
⊢ (leftRel (N.subgroupOf (H ⊔ N))) ((inclusion ⋯) ⟨h, hh⟩) ⟨(fun x1 x2 ↦ x1 * x2) h n, hy⟩
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case pos
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
h : j = i
⊢ b c = update (fun i ↦ (f i) c) i (b c) i

Tactic:
update_self

Goal state after:
case pos
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
h : j = i
⊢ b c = b c
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
inst✝¹³ : Semiring R✝
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₄
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M →ₗ[R] M₂
C : Submodule R M
h : IsCompl C f.ker
⊢ Function.Surjective ⇑(codRestrict f.range f ⋯ ∘ₗ C.subtype)

Tactic:
rintro ⟨-, x, rfl⟩

Goal state after:
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
inst✝¹³ : Semiring R✝
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₄
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M →ₗ[R] M₂
C : Submodule R M
h : IsCompl C f.ker
x : M
⊢ ∃ a, (codRestrict f.range f ⋯ ∘ₗ C.subtype) a = ⟨f x, ⋯⟩
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' : AddMonoidHom.mrange ↑f = f'.mgraph
⊢ ∃ f', f.range = f'.graph

Tactic:
simp only [SetLike.ext_iff, AddMonoidHom.mem_mrange, AddMonoidHom.coe_coe,
    AddMonoidHom.mem_mgraph] at hf'

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
⊢ ∃ f', f.range = f'.graph
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 b c : M
⊢ (fun x ↦ a + x) '' Ioo b c = Ioo (a + b) (a + c)

Tactic:
by
  simp only [add_comm a, image_add_const_Ioo]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a < b
⊢ (∏ x ∈ Ioo a b, f x) * f a = ∏ x ∈ Ico a b, f x

Tactic:
by
  rw [mul_comm, mul_prod_Ioo_eq_prod_Ico h]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
⊢ toZ i0 (succ^[n] i0) ≤ ↑n

Tactic:
rw [toZ_of_ge (le_succ_iterate _ _)]
  norm_cast
  exact Nat.find_min' _ rfl

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
⊢ disjointed ⇑(partialSups f) = disjointed f

Tactic:
classical
  ext i
  have step1 : f i \ (Iio i).sup f = partialSups f i \ (Iio i).sup f := by
    rw [sdiff_eq_symm (sdiff_le.trans (le_partialSups f i))]
    simp only [funext (partialSups_apply f), sup'_eq_sup]
    rw [sdiff_sdiff_eq_sdiff_sup (sup_mono Iio_subset_Iic_self), sup_eq_right]
    simp only [Iic_eq_cons_Iio, sup_cons, sup_sdiff_left_self, sdiff_le_iff, le_sup_right]
  simp only [disjointed_apply, step1, funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion]
  congr 2 with r
  simpa only [mem_biUnion, mem_Iio, mem_Iic] using
    ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
a : α
m n : ℕ
ha : a ^ m ∈ I
h : m ≤ n
⊢ a ^ (n - m) * a ^ m ∈ I

Tactic:
exact I.mul_mem_left _ ha

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

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d ∈ I

Tactic:
show a * c - b * d = (a - b) * c + b * (c - d) by rw [sub_mul, mul_sub]; abel

Goal state after:
α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ (a - b) * c + b * (c - d) ∈ I
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: 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 ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) + ↑(n.choose i.succ)) =
    x * (x ^ i * y ^ (n - i) * ↑(n.choose i)) + y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))

Tactic:
mul_add

Goal state after:
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 ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i) + x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) =
    x * (x ^ i * y ^ (n - i) * ↑(n.choose i)) + y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
⊢ ∑ m ∈ Finset.range (k + 1), a ^ m * b ^ (k - m) * ↑(k.choose m) ∈ I

Tactic:
← Nat.cast_comm

Goal state after:
α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
⊢ ∑ x ∈ Finset.range (k + 1), ↑(k.choose x) * (a ^ x * b ^ (k - x)) ∈ I
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝¹ : Ring R
f : ι → R
inst✝ : (span (range f)).IsTwoSided
i : ι
⊢ (mk (span (range f))) (f i) = 0

Tactic:
Ideal.Quotient.eq_zero_iff_mem

Goal state after:
ι : Type u_1
R : Type u_3
inst✝¹ : Ring R
f : ι → R
inst✝ : (span (range f)).IsTwoSided
i : ι
⊢ f i ∈ span (range f)
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: 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
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
⊢ f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y

Tactic:
obtain eq | ne := s.eq_empty_or_nonempty

Goal state after:
case inl
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
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
eq : s = ∅
⊢ f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y

case inr
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
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne : s.Nonempty
⊢ f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋂ i, s i
hs : Antitone s
f g : (a : α) → β a
a : α
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise f g a = (⋂ i, s i).piecewise f g a

Tactic:
convert! ← (compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a using 3
  · convert! congr_fun (Set.piecewise_compl (s _) g f) a
  · simp only [(· ∘ ·), ← compl_iInter, Set.piecewise_compl]

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

Goal state before:
pp: α : Type v
inst✝ : Preorder α
a : α
⊢ ⋃ b, Icc a b = Ici a

Tactic:
simp only [← Ici_inter_Iic, ← inter_iUnion, iUnion_Iic, inter_univ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ g ≤ map φ (map ψ g)

Tactic:
rw [map_map, eq, map_id]

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

Goal state before:
pp: α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
⊢ ∃ x, p x

Tactic:
by_contra H
  replace H : ∀ᶠ x in f, ¬p x := Eventually.of_forall (not_exists.1 H)
  exact hp H

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z)

Tactic:
image_inter_preimage

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' V ∩ Z = f '' V ∩ Z
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : α
⊢ IsCofinal {x} ↔ IsTop x

Tactic:
by
  simp [IsCofinal, IsTop]

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : IsCofinal s
⊢ ⋃ i ∈ s, Iio i = univ

Tactic:
by
    simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop]
    intro x
    obtain ⟨y, hy⟩ := exists_gt x
    obtain ⟨z, hz, hz'⟩ := hs y
    exact ⟨z, hz, hy.trans_le hz'⟩

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

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #↑s = cof α
⊢ s.Finite

Tactic:
Set.Finite,

Goal state after:
α : Type u
inst✝ : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #↑s = cof α
⊢ Finite ↑s
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
inst✝⁹ : Zero α
inst✝⁸ : Preorder α
inst✝⁷ : Preorder β
inst✝⁶ : Preorder γ
inst✝⁵ : SMul α β
inst✝⁴ : SMul α γ
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : SMulPosReflectLE α β
inst✝ : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
⊢ _a₁ ≤ _a₂

Tactic:
rcases lt_iff.mp hb with ⟨h₁, -⟩ | ⟨-, h₁⟩

Goal state after:
case inl
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : Preorder α
inst✝⁷ : Preorder β
inst✝⁶ : Preorder γ
inst✝⁵ : SMul α β
inst✝⁴ : SMul α γ
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : SMulPosReflectLE α β
inst✝ : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
h₁ : 0.1 < _b.1
⊢ _a₁ ≤ _a₂

case inr
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : Preorder α
inst✝⁷ : Preorder β
inst✝⁶ : Preorder γ
inst✝⁵ : SMul α β
inst✝⁴ : SMul α γ
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : SMulPosReflectLE α β
inst✝ : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
h₁ : 0.2 < _b.2
⊢ _a₁ ≤ _a₂
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LinearOrder α
⊢ DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty

Tactic:
by
  simp [DirSupInacc]

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

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

Tactic:
by
  have := lift_lt.{_, max (u + 1) v}.2 (lift_lt_univ c)
  rw [lift_lift, lift_univ, univ_umax.{u, v}] at this
  exact this

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

Goal state before:
pp: case inr
o : Ordinal.{v}
ho : IsSuccPrelimit o
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred

Tactic:
rwa [ho.ordinalPred_eq, eq_comm, pred_eq_iff_isSuccPrelimit, isSuccPrelimit_lift]

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
⊢ #↑s ≤ #α

Tactic:
le_mk_iff_exists_set

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
⊢ ∃ p, #↑p = #↑s
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
rw [zero_opow (add_pos_of_right zero_lt_one b).ne', mul_zero]

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

Goal state before:
pp: case inl
⊢ log2 0 = log 2 0

Tactic:
rw [log2_zero, log_zero_right]

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

Goal state before:
pp: case mpr.a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
⊢ log b x ≤ y

pp: case a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
⊢ y ≤ log b x

Tactic:
· rwa [← lt_add_one_iff, ← lt_opow_iff_log_lt hb hx]

Goal state after:
case a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
⊢ y ≤ log b x
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a : Ordinal.{u_1}
ha : a ≠ 0
⊢ a - ω ^ log ω a < a

Tactic:
by
  obtain ⟨n, hn⟩ := lt_omega0.1 <| div_opow_log_lt a one_lt_omega0
  conv_lhs => left; rw [← div_add_mod a (ω ^ log ω a), hn]
  cases n with
  | zero =>
    simpa using ((div_pos (opow_ne_zero _ omega0_ne_zero)).2 (opow_log_le_self _ ha)).trans_eq hn
  | succ n =>
    rw [add_comm, Nat.cast_add, Nat.cast_one, mul_one_add, add_assoc, Ordinal.add_sub_cancel]
    apply (opow_mul_add_lt_opow_mul _ (lt_add_one _)).trans_le
    · rw [Ordinal.mul_le_iff_le_div, hn] <;> simp
    · exact mod_lt _ (opow_ne_zero _ omega0_ne_zero)

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ a ∈ Set.range (deriv f) ↔ f a = a

Tactic:
Set.mem_range,

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ (∃ y, deriv f y = a) ↔ f a = a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
⊢ nfp 0 a = a

Tactic:
by
  rw [← iSup_iterate_eq_nfp]
  apply (Ordinal.iSup_le ?_).antisymm (Ordinal.le_iSup _ 0)
  intro n
  cases n
  · rfl
  · rw [Function.iterate_succ']
    simp

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 : ℵ₀ ≤ #α
⊢ #α * #α ≤ #α

Tactic:
obtain ⟨_, _, hα⟩ := exists_ord_eq_type_lt α

Goal state after:
case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ #α * #α ≤ #α
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: n : ℕ
⊢ preAleph ↑n = ↑n

Tactic:
← card_preOmega,

Goal state after:
n : ℕ
⊢ (preOmega ↑n).card = ↑n
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preAleph ω = ℵ₀

Tactic:
← card_preOmega,

Goal state after:
⊢ (preOmega ω).card = ℵ₀
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case right
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
⊢ (fun x1 x2 ↦ x1 + x2) c d < a * (x + y)

Tactic:
mul_add

Goal state after:
case right
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
⊢ (fun x1 x2 ↦ x1 + x2) c d < a * x + a * y
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case h₂
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a / b ^ log b a < b

Tactic:
rw [← lt_mul_iff_div_lt hbo₀, ← opow_succ]

Goal state after:
case h₂
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a < b ^ succ (log b a)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case add_one
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ max a.card (a ^ b).card ≤ max a.card (b.card + 1)

Tactic:
grw [IH]
      rw [← max_assoc, max_self]
      grw [← le_self_add]

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

Goal state before:
pp: case refine_2
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ o.blsub f = a

Tactic:
exact hf.2.2

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

Goal state before:
pp: α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
⊢ α + γ ≤ β + γ ↔ α ≤ β

Tactic:
refine ⟨fun h => ?_, fun h => by gcongr⟩

Goal state after:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : α + γ ≤ β + γ
⊢ α ≤ β
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inl
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) (ω_ 0)

Tactic:
rw [omega_zero]
    exact isPrincipal_opow_omega0

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

Goal state before:
pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
x : α
h : #β ≤ #↑(f ⁻¹' {x})
⊢ #↑(f ⁻¹' {x}) ≤ #β

Tactic:
le_mk_iff_exists_set

Goal state after:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
x : α
h : #β ≤ #↑(f ⁻¹' {x})
⊢ ∃ p, #↑p = #↑(f ⁻¹' {x})
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫 {j | r j i}
⊢ ⨆ i, #↑(𝒫 {j | r j i}) ≤ #α

Tactic:
apply ciSup_le' _

Goal state after:
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫 {j | r j i}
⊢ ∀ (i : α), #↑(𝒫 {j | r j i}) ≤ #α