mathlib-initiative/mathlib-tactics huggingface dataset:
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 ι
h : Disjoint I J
⊢ Disjoint (⨅ i ∈ Iᶜ, (proj i).ker) (⨅ i ∈ Jᶜ, (proj i).ker)

Tactic:
simp only [disjoint_iff_inf_le, SetLike.le_def, mem_iInf, mem_inf, mem_ker, mem_bot, proj_apply,
    funext_iff]

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ ∀ ⦃x : (i : ι) → φ i⦄, ((∀ i ∈ Iᶜ, x i = 0) ∧ ∀ i ∈ Jᶜ, x i = 0) → ∀ (x_1 : ι), x x_1 = 0 x_1
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
⊢ insert b (Icc a (pred b)) = Icc a b

Tactic:
by
  ext x; simp [or_and_left, ← le_iff_eq_or_le_pred]; simp_all

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case disjoint
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₂
⊢ ∀ x ∈ (inl R M M₂).range, x ∈ (inr R M M₂).range → x = 0

Tactic:
rintro ⟨_, _⟩ ⟨x, hx⟩ ⟨y, hy⟩

Goal state after:
case disjoint
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₂
fst✝ : M
snd✝ : M₂
x : M
hx : (inl R M M₂) x = (fst✝, snd✝)
y : M₂
hy : (inr R M M₂) y = (fst✝, snd✝)
⊢ (fst✝, snd✝) = 0
Module: Mathlib.LinearAlgebra.Pi

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
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ ↥(⨅ i ∈ J, (proj i).ker) ≃ₗ[R] (i : ↑I) → φ ↑i

Tactic:
refine
    LinearEquiv.ofLinearMap (pi fun i => (proj (i : ι)).comp (Submodule.subtype _))
      (codRestrict _ (pi fun i => if h : i ∈ I then proj (⟨i, h⟩ : I) else 0) ?_) ?_ ?_
  · intro b
    simp only [mem_iInf, mem_ker, proj_apply, pi_apply]
    intro j hjJ
    have : j ∉ I := fun hjI => hd.le_bot ⟨hjI, hjJ⟩
    rw [dif_neg this, zero_apply]
  · simp only [pi_comp, comp_assoc, subtype_comp_codRestrict, proj_pi, Subtype.coe_prop]
    ext b ⟨j, hj⟩
    simp only [dif_pos,
      LinearMap.coe_proj, LinearMap.pi_apply]
    rfl
  · ext1 ⟨b, hb⟩
    apply Subtype.ext
    ext j
    have hb : ∀ i ∈ J, b i = 0 := by
      simpa only [mem_iInf, mem_ker, proj_apply] using (mem_iInf _).1 hb
    simp only [comp_apply, pi_apply, id_apply, codRestrict_apply]
    split_ifs with h
    · rfl
    · exact (hb _ <| (hu trivial).resolve_left h).symm

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 : M
⊢ BijOn (fun x ↦ x + d) (Ici a) (Ici (a + d))

Tactic:
refine ⟨by simp [MapsTo], by simp, fun _ h => ?_⟩
  obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ici.mp h)
  rw [mem_Ici, add_right_comm, add_le_add_iff_right] at h
  exact ⟨a + c, h, by rw [add_right_comm]⟩

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Icc a b) = image (⇑(addLeftEmbedding c)) (Icc a b)

Tactic:
addLeftEmbedding,

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Icc a b) = image (⇑{ toFun := fun h ↦ c + h, inj' := ⋯ }) (Icc a b)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ico a b) = image (⇑(addLeftEmbedding c)) (Ico a b)

Tactic:
addLeftEmbedding,

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ico a b) = image (⇑{ toFun := fun h ↦ c + h, inj' := ⋯ }) (Ico a b)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ioc a b) = image (⇑(addLeftEmbedding c)) (Ioc a b)

Tactic:
addLeftEmbedding,

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ioc a b) = image (⇑{ toFun := fun h ↦ c + h, inj' := ⋯ }) (Ioc a b)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ioo a b) = image (⇑(addLeftEmbedding c)) (Ioo a b)

Tactic:
addLeftEmbedding,

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ioo a b) = image (⇑{ toFun := fun h ↦ c + h, inj' := ⋯ }) (Ioo a b)
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
h : i0 ≤ pred^[n] i0
h_eq : pred^[n] i0 = i0
⊢ -↑n ≤ toZ i0 (pred^[n] i0)

Tactic:
rw [h_eq, toZ_of_eq]

Goal state after:
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
h : i0 ≤ pred^[n] i0
h_eq : pred^[n] i0 = i0
⊢ -↑n ≤ 0
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
⊢ (univ.sup fun x ↦ (Iic x).sup (disjointed f)) = univ.sup fun x ↦ (Iic x).sup f

Tactic:
sup_congr rfl (fun i _ ↦ ?_)

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
⊢ univ.sup ?m.83 = univ.sup fun x ↦ (Iic x).sup f

α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
⊢ ι → α

α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
i : ι
x✝ : i ∈ univ
⊢ (Iic i).sup (disjointed f) = ?m.83 i
Module: Mathlib.Order.Disjointed

Goal state before:
pp: ι : Type u_2
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
α : Type u_3
f : ι → Set α
n : ι
⊢ ⋃ i ∈ Iic n, disjointed f i = (partialSups f) n

Tactic:
rw [← partialSups_disjointed, partialSups_eq_biSup]
  simp

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

Goal state before:
pp: n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ a.1 ≤ k) = (fun a ↦ a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ b a, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j

Tactic:
exact exists₂_congr (fun a b ↦ by rw [add_comm])

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

Goal state before:
pp: n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ k ≤ a.2) = (fun a ↦ k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ b a, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j

Tactic:
exact exists₂_congr (fun a b ↦ by rw [add_comm])

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

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

Tactic:
rw [mul_comm, span_pair_add_right_mul]

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

Goal state before:
pp: case h
R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
x : R
⊢ (lift I f H) ((mk I) x) = f x

Tactic:
simp only [Ideal.Quotient.lift_mk]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ x.powerset
⊢ #y < #x + 1

Tactic:
Nat.lt_succ_iff

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ x.powerset
⊢ #y ≤ #x
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: case isUnit_or_isUnit.refine_2
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ a * (c * d) * (a * (c * d)) = a * (c * d)

Tactic:
refine Eq.trans ?_ (congrArg (· * (c * d)) ha.symm)

Goal state after:
case isUnit_or_isUnit.refine_2
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ a * (c * d) * (a * (c * d)) = a * c * (a * d) * (c * d)
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝³ : CommSemiring α
inst✝² : IsPrincipalIdealRing α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
P : Ideal α
⊢ P.IsPrime ↔ P ≠ ⊥ → P.IsPrime

Tactic:
← or_iff_not_imp_left,

Goal state after:
α : Type u
inst✝³ : CommSemiring α
inst✝² : IsPrincipalIdealRing α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
P : Ideal α
⊢ P.IsPrime ↔ P = ⊥ ∨ P.IsPrime
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
x : ℕ →₀ P
⊢ (f.prodOfFinsuppNat x).2 = f (f.prodOfFinsuppNat ((comapDomain.addMonoidHom ⋯) x))

Tactic:
simp_rw [prodOfFinsuppNat, coe_lsum, sum, Prod.snd_sum]

Goal state after:
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
x : ℕ →₀ P
⊢ ∑ c ∈ x.support, ((((inr R P M ∘ₗ f) ^ c) ∘ₗ inl R P M) (x c)).2 =
    f
      (∑ x_1 ∈ ((comapDomain.addMonoidHom ⋯) x).support,
        (((inr R P M ∘ₗ f) ^ x_1) ∘ₗ inl R P M) (((comapDomain.addMonoidHom ⋯) x) x_1))
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t✝ : Set β
m : α → β
f : Filter α
t : Set β
s : Set α
hs : s ∈ f.sets
hst : kernImage m s ⊆ t
⊢ kernImage m (s ∪ m ⁻¹' t) = t

Tactic:
kernImage_union_preimage,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t✝ : Set β
m : α → β
f : Filter α
t : Set β
s : Set α
hs : s ∈ f.sets
hst : kernImage m s ⊆ t
⊢ kernImage m s ∪ t = t
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
s : Set α
hsf : s ∈ f
hsg : s ∈ g
hm : InjOn m s
⊢ map m f = map m g ↔ f = g

Tactic:
by
  simp only [le_antisymm_iff, map_le_map_iff_of_injOn hsf hsg hm,
    map_le_map_iff_of_injOn hsg hsf hm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g : α → β
f : Filter α
⊢ (pure g).seq f = map g f

Tactic:
refine le_antisymm (le_map fun s hs => ?_) (le_seq fun s hs t ht => ?_)

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

case refine_2
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
⊢ s.seq t ∈ map g f
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
⊢ f.seq (pure a) = map (fun g ↦ g a) f

Tactic:
refine le_antisymm (le_map fun s hs => ?_) (le_seq fun s hs t ht => ?_)

Goal state after:
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)

case refine_2
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
⊢ s.seq t ∈ map (fun g ↦ g a) f
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
inst✝ : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : n ≤ m
⊢ (f ^ m).ker ⊓ (f ^ m).range = ⊥

Tactic:
rw [← hn _ hm, Submodule.eq_bot_iff]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : n ≤ m
⊢ ∀ x ∈ LinearMap.ker (f ^ n) ⊓ (f ^ m).range, x = 0
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case a
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ cof α ≠ 0

Tactic:
cof_ne_zero_iff

Goal state after:
case a
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ Nonempty α
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
⊢ DirSupInaccOn D sᶜ ↔ DirSupClosedOn D s

Tactic:
← dirSupClosedOn_compl,

Goal state after:
α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
⊢ DirSupClosedOn D sᶜᶜ ↔ DirSupClosedOn D s
Module: Mathlib.Order.DirSupClosed

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

Tactic:
← dirSupClosedOn_compl,

Goal state after:
α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInaccOn D x
⊢ DirSupClosedOn D (⋃₀ s)ᶜ
Module: Mathlib.Order.DirSupClosed

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

Tactic:
← dirSupClosedOn_compl,

Goal state after:
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupClosedOn D (s ∪ t)ᶜ
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_6
M : ι → Type u_7
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), Module.Finite R (M i)
⊢ ⊤.FG

Tactic:
rw [← pi_top]

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_6
M : ι → Type u_7
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), Module.Finite R (M i)
⊢ (Submodule.pi ?m.29 fun i ↦ ⊤).FG

R : Type u_1
A : Type u_2
B : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_6
M : ι → Type u_7
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), Module.Finite R (M i)
⊢ Set ι
Module: Mathlib.Order.DirSupClosed

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

Tactic:
← dirSupClosedOn_compl,

Goal state after:
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupClosedOn D (s ∩ t)ᶜ
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
simpa using Ordinal.add_sub_cancel_of_le le_self_add

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

Goal state before:
pp: case mp
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs))
⊢ StrictMono (Subtype.val ∘ ⇑(enum s hs)) ∧ range (Subtype.val ∘ ⇑(enum s hs)) = s

Tactic:
use (Subtype.strictMono_coe _).comp (enum s hs).strictMono

Goal state after:
case right
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs))
⊢ range (Subtype.val ∘ ⇑(enum s hs)) = s
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
⊢ enum (range f) ⋯ = StrictMono.orderIso f hf

Tactic:
ext x
  apply congrFun (enum_eq_iff.2 ⟨?_, ?_⟩)
  · exact (Subtype.strictMono_coe _).comp (OrderIso.strictMono _)
  · simp

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

Goal state before:
pp: α : Type u_2
inst✝² : ConditionallyCompleteLinearOrderBot α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ ↑((enum s hs) ⊥) = sInf s

Tactic:
let : Bot s := ⟨⟨sInf s, csInf_mem hs.nonempty⟩⟩
  let : OrderBot s := .mk fun a ↦ csInf_le' a.2
  rw [OrderIso.map_bot]
  rfl

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
g : Ordinal.{v} → Ordinal.{max v w}
⊢ BddAbove (range (g ∘ f))

Tactic:
rw [range_comp]
  exact bddAbove_image hf g

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

Goal state before:
pp: b n : ℕ
⊢ 0 < log b n ↔ b ≤ n ∧ 1 < b

Tactic:
Nat.pos_iff_ne_zero,

Goal state after:
b n : ℕ
⊢ log b n ≠ 0 ↔ b ≤ n ∧ 1 < b
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
⊢ 0 < log b n ↔ b ≤ n ∧ 1 < b

Tactic:
by
  rw [Nat.pos_iff_ne_zero, Ne, log_eq_zero_iff, not_or, not_lt, not_le]

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ (o.blsub fun x x_1 ↦ f x) = f o

Tactic:
← IsNormal.bsup_eq.{u, v} H h,

Goal state after:
f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ (o.blsub fun x x_1 ↦ f x) = o.bsup fun x x_1 ↦ f x
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case add_one
o✝ : Ordinal.{u_1}
IH : 1 ^ o✝ = 1
⊢ 1 ^ (o✝ + 1) = 1

Tactic:
simp [IH, mul_one]

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

Goal state before:
pp: b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b n ≤ log c n

Tactic:
by
  rcases eq_or_ne n 0 with (rfl | hn); · rw [log_zero_right, log_zero_right]
  apply le_log_of_pow_le hc
  calc
    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.Family

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ⨆ n, o * ↑n = o * ω

Tactic:
by
  rw [← iSup_natCast, Ordinal.mul_iSup]

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

Goal state before:
pp: case inl.inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1✝ : a ≤ 1
a1 : a = 1
⊢ a ^ 1 ≤ a ^ b

Tactic:
rw [a1, one_opow, one_opow]

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

Goal state before:
pp: m n : ℕ
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  · have hn' : (n : Ordinal) ≠ 0 := Nat.cast_ne_zero.2 hn
    apply le_antisymm
    · rw [← mul_le_iff_le_div hn', ← natCast_mul, Nat.cast_le, mul_comm]
      apply Nat.div_mul_le_self
    · rw [div_le hn', succ_eq_add_one, ← Nat.cast_succ, ← natCast_mul, Nat.cast_lt, mul_comm,
        ← Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero hn)]
      apply Nat.lt_succ_self

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

Goal state before:
pp: case case1
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y

Tactic:
| case1 h =>

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} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
⊢ f i (nfpFamily f a) = nfpFamily f a

Tactic:
by
  rw [nfpFamily, H.map_iSup bddAbove_of_small]
  apply le_antisymm <;> refine Ordinal.iSup_le fun l => ?_
  · exact Ordinal.le_iSup _ (i::l)
  · exact H.strictMono.le_apply.trans (Ordinal.le_iSup _ _)

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ ∃ o, deriv f o = a

Tactic:
unfold deriv
  rw [← le_iff_derivFamily fun _ : Unit => H]
  exact ⟨fun h _ => h, fun h => h Unit.unit⟩

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

Goal state before:
pp: ⊢ ω.card.ord = ω

Tactic:
card_omega0,

Goal state after:
⊢ ℵ₀.ord = ω
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case ind
c : Cardinal.{u_1}
IH : ∀ y < c, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ c
⊢ c * c = c

Tactic:
| ind c IH
   => 

Goal state after:
case ind
c : Cardinal.{u_1}
IH : ∀ y < c, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ c
⊢ c * c = c
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ ≤ ℵ_ o

Tactic:
rw [aleph_eq_preAleph, aleph0_le_preAleph]

Goal state after:
o : Ordinal.{u_1}
⊢ ω ≤ ω + o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case isSuccPrelimit.mpr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi✝ : Ordinal.lift.{v, u_1} i ∈ Iio (Ordinal.lift.{v, u_1} o)
hi : Ordinal.lift.{v, u_1} i < Ordinal.lift.{v, u_1} o
⊢ (fun a ↦ preBeth ↑a) ⟨Ordinal.lift.{v, u_1} i, hi✝⟩ ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)

Tactic:
Ordinal.lift_lt

Goal state after:
case isSuccPrelimit.mpr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi✝ : Ordinal.lift.{v, u_1} i ∈ Iio (Ordinal.lift.{v, u_1} o)
hi : i < o
⊢ (fun a ↦ preBeth ↑a) ⟨Ordinal.lift.{v, u_1} i, hi✝⟩ ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
⊢ a * b ≤ b ^ succ (log b a)

Tactic:
(isNormal_mul_right (pos_iff_ne_zero.2 ha)).apply_of_isSuccLimit hbl,

Goal state after:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
⊢ ⨆ b_1, a * ↑b_1 ≤ b ^ succ (log b a)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℶ_ ↑n ≤ lift.{v, u} c ↔ ℶ_ ↑n ≤ c

Tactic:
simpa using lift_le (a := ℶ_ n)

Goal state after: