mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
have : Nonempty α := ⟨a⟩
      have : Nonempty β := ⟨b⟩
      rw [hf.preimage_Iic h (ha ▸ bddAbove_Iio)]
      exact isClosed_Iic

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : a ∈ closure[inst✝³] s ∩ closure[inst✝³] sᶜ
⊢ ¬IsOpen[inst✝³] {a}

Tactic:
grind [mem_closure_iff, Set.Nonempty]

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

Goal state before:
pp: x : ZFSet.{u}
⊢ {x}.card = 1

Tactic:
simpa [notMem_singleton] using card_insert (notMem_empty x)

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
a : Ordinal.{u}
⊢ veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a

Tactic:
by
  apply (mem_range_veblenWith hf h.ne_bot).1 _ _ h
  simp

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

Goal state before:
pp: x : ZFSet.{u}
h : x.Nonempty
x✝ : ZFSet.{u}
⊢ x✝ ∈ ↑(⋂₀ x) ↔ x✝ ∈ ⋂₀ (SetLike.coe '' ↑x)

Tactic:
simp [mem_sInter h]

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

Goal state before:
pp: case mp
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y → x = y ∨ x ∈ y

Tactic:
hxy

Goal state after:
case mp
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
⊢ x = y ∨ x ∈ y
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u}
a : ↑(Set.Iio o)
⊢ ↑a < o

Tactic:
exact a.2

Goal state after:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u}
x : ZFSet.{u}
⊢ x ∈ V_ o ↔ ∃ a < o, x ⊆ V_ a

Tactic:
rw [vonNeumann]; simp

Goal state after:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case limit
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ lift.{u + 1, u} (⋃ (i : ↑(Set.Iio o)), V_ ↑i).card ≤ lift.{u + 1, u} (⨆ i, (V_ ↑i).card)

Tactic:
apply lift_card_iUnion_le_sum_card.trans

Goal state after:
case limit
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ (sum fun i ↦ (V_ ↑i).card) ≤ lift.{u + 1, u} (⨆ i, (V_ ↑i).card)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
⊢ (e.oadd n a).split = (scale 1 o', m)

Tactic:
by_cases e0 : e = 0

Goal state after:
case pos
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : e = 0
⊢ (e.oadd n a).split = (scale 1 o', m)

case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : ¬e = 0
⊢ (e.oadd n a).split = (scale 1 o', m)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + ↑m

Tactic:
by_cases e0 : e = 0

Goal state after:
case pos
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : e = 0
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + ↑m

case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : ¬e = 0
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + ↑m
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Tactic:
by_cases e0 : e = 0

Goal state after:
case pos
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : e = 0
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

case neg
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : ¬e = 0
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
this : IsClosed {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
⊢ CompleteSpace (Stream'.Seq α)

Tactic:
by
    exact this.completeSpace_coe

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}).Nonempty
n : ℕ
hn : s n = none
⊢ s (n + 1) = none

Tactic:
obtain ⟨t, hts, ht⟩ := hs (Metric.ball s ((1 / 2 : ℝ) ^ (n + 1)))
    (Metric.ball_mem_nhds _ (by positivity))

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}).Nonempty
n : ℕ
hn : s n = none
t : Stream' (Option α)
hts : t ∈ Metric.ball s ((1 / 2) ^ (n + 1))
ht : t ∈ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
⊢ s (n + 1) = none
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹ * dist x y
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head

Tactic:
dist_le_one x y,

Goal state after:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹ * 1
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
basis_hd' : ℝ → ℝ
basis_tl' : Basis
f : ℝ → ℝ
g : MultiseriesExpansion basis_tl → MultiseriesExpansion basis_tl'
⊢ map f g nil = nil

Tactic:
by
  simp [map, nil]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.nil
exps_hd : ℝ
basis_hd : ℝ → ℝ
h_nonzero : exps_hd ≠ 0
e : ℝ
es : List ℝ
ih :
  ∀ {basis_tl : Basis},
    (∀ b ∈ basis_tl, (log ∘ b) =o[atTop] (log ∘ basis_hd)) → toLogFun es basis_tl =o[atTop] (log ∘ basis_hd)
hlo : ∀ b ∈ [], (log ∘ b) =o[atTop] (log ∘ basis_hd)
⊢ toLogFun (e :: es) [] =o[atTop] (log ∘ basis_hd)

Tactic:
simp only [toLogFun_nil_basis]

Goal state after:
case cons.nil
exps_hd : ℝ
basis_hd : ℝ → ℝ
h_nonzero : exps_hd ≠ 0
e : ℝ
es : List ℝ
ih :
  ∀ {basis_tl : Basis},
    (∀ b ∈ basis_tl, (log ∘ b) =o[atTop] (log ∘ basis_hd)) → toLogFun es basis_tl =o[atTop] (log ∘ basis_hd)
hlo : ∀ b ∈ [], (log ∘ b) =o[atTop] (log ∘ basis_hd)
⊢ 0 =o[atTop] (log ∘ basis_hd)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case hyp
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ∀ {basis : Basis} (ms : MultiseriesExpansion basis),
    (ms.Approximates ∨ ∃ (h_basis : basis = basis_hd :: basis_tl), motive (h_basis ▸ ms)) →
      basis = [] ∨
        (∃ basis_hd basis_tl f, f =ᶠ[atTop] 0 ∧ basis = basis_hd :: basis_tl ∧ ms ≍ mk Multiseries.nil f) ∨
          ∃ basis_hd_1 f basis_tl_1 exp coef tl,
            (coef.Approximates ∨ ∃ (h_basis : basis_tl_1 = basis_hd :: basis_tl), motive (h_basis ▸ coef)) ∧
              Majorized f basis_hd_1 exp ∧
                ((mk tl (f - basis_hd_1 ^ exp * coef.toFun)).Approximates ∨
                    ∃ (h_basis : basis_hd_1 :: basis_tl_1 = basis_hd :: basis_tl),
                      motive (h_basis ▸ mk tl (f - basis_hd_1 ^ exp * coef.toFun))) ∧
                  basis = basis_hd_1 :: basis_tl_1 ∧ ms ≍ mk (Multiseries.cons exp coef tl) f

pp: case x
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ms.Approximates ∨ ∃ (h_basis : basis_hd :: basis_tl = basis_hd :: basis_tl), motive (h_basis ▸ ms)

Tactic:
· rintro basis ms (h_ms | ⟨rfl, h_ms⟩)
    · cases h_ms <;> grind
    simp only [reduceCtorEq, List.cons.injEq, ↓existsAndEq, and_true, heq_eq_eq, ms_eq_mk_iff,
      true_and, exists_eq_right_right', exists_and_left, false_or] at h_ms ⊢
    rcases h_step _ h_ms with h_step | ⟨exp, coef, tl, h_seq, h_coef, h_maj, h_tl⟩
    · grind
    · refine .inr ⟨basis_hd, ms.toFun, basis_tl, exp, coef, by simpa, ‹_›, tl, ?_⟩
      simp
      grind

Goal state after:
case x
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ms.Approximates ∨ ∃ (h_basis : basis_hd :: basis_tl = basis_hd :: basis_tl), motive (h_basis ▸ ms)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f✝ : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f✝
h_approx✝ : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
f g : ℝ → ℝ
h_approx : (mk Multiseries.nil g).Approximates
h_eq : (mk Multiseries.nil g).toFun =ᶠ[atTop] f
⊢ ((mk Multiseries.nil g).replaceFun f).seq = Multiseries.nil ∧
      ((mk Multiseries.nil g).replaceFun f).toFun =ᶠ[atTop] 0 ∨
    ∃ exp coef tl,
      ((mk Multiseries.nil g).replaceFun f).seq = Multiseries.cons exp coef tl ∧
        coef.Approximates ∧
          Majorized ((mk Multiseries.nil g).replaceFun f).toFun basis_hd exp ∧
            motive (mk tl (((mk Multiseries.nil g).replaceFun f).toFun - basis_hd ^ exp * coef.toFun))

Tactic:
simp only [nil_iff, mk_toFun, mk_replaceFun, mk_seq, true_and,
      Multiseries.nil_ne_cons, false_and, exists_const, or_false] at h_approx h_eq ⊢

Goal state after:
case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f✝ : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f✝
h_approx✝ : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
f g : ℝ → ℝ
h_eq : g =ᶠ[atTop] f
h_approx : g =ᶠ[atTop] 0
⊢ f =ᶠ[atTop] 0
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: ⊢ fastGrowing 1 = fun n ↦ 2 * n

Tactic:
by
  rw [@fastGrowing_succ 1 0 rfl]; funext i; rw [two_mul, fastGrowing_zero]
  exact Nat.succ_iterate _ _

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

Goal state before:
pp: a : ONote
ha : a.NF
b : ONote
hb : b.NF
⊢ (a.cmp b).Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
have := ONote.cmp_compares a b

Goal state after:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
⊢ (a.cmp b).Compares ⟨a, ha⟩ ⟨b, hb⟩
Module: Mathlib.Tactic.NormNum.NatLog

Goal state before:
pp: b m n : ℕ
hb : Nat.blt 1 b = true
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1

Tactic:
rw [Nat.blt_eq] at hb

Goal state after:
b m n : ℕ
hb : 1 < b
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
n : ℕ
h : IsNat a n
⊢ IsSquare n ↔ IsSquare a

Tactic:
simp [h.1]

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case neg
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
h : ↑a / ↑b = q ^ d
⊢ False

Tactic:
← Rat.num_div_den q

Goal state after:
case neg
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
h : ↑a / ↑b = (↑q.num / ↑q.den) ^ d
⊢ False
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: case hb0
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ 0 < ↑d

pp: case h
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ (↑n).natAbs.Coprime (↑d).natAbs

Tactic:
· contrapose! hnd
    have : n ≠ 1 := by rintro rfl; simp at hn
    simp_all

Goal state after:
case h
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ (↑n).natAbs.Coprime (↑d).natAbs
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case neg.inr
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_odd : Odd d
⊢ ↑a / ↑b ≠ q ^ d

Tactic:
contrapose hq

Goal state after:
case neg.inr
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
h_odd : Odd d
hq : ↑a / ↑b = q ^ d
⊢ 0 ≤ q
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: e' r : ℤ
α : Type u_1
inst✝ : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % ↑n') r
⊢ e = ↑r

Tactic:
by rw [he.out, CharP.intCast_eq_intCast_mod α n, show n = n' from hn.out, h₂.out, Int.cast_id]

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case nil
α : Type u
inst✝ : DecidableEq α
x y : α
ys : List α
h₀ : [].Nodup
h₁ : [].length = ys.length
i : ℕ
h₂ : [][i]? = some x
⊢ applyId ([].zip ys) x = y ↔ ys[i]? = some y

Tactic:
cases h₂

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.succ.cons.cons.hnc
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ x ∈ xs

Tactic:
apply List.mem_of_getElem? h₂

Goal state after:
Module: Mathlib.Topology.Algebra.Ring.Compact

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
⊢ IsOpen ↑I

Tactic:
by
  rw [← Ideal.finprod_heightOneSpectrum_factorization hI,
    finprod_eq_finsetProd_of_mulSupport_subset _
      (s := (Ideal.hasFiniteMulSupport hI).toFinset) (by simp)]
  refine @AddSubgroup.isOpen_of_isClosed_of_finiteIndex _ _ _ _ (Submodule.toAddSubgroup _)
    ?_ (IsNoetherianRing.isClosed_ideal _)
  refine @AddSubgroup.finiteIndex_of_finite_quotient _ _ _ ?_
  refine Ideal.finite_quotient_prod _ _ (fun _ _ ↦ IsNoetherian.noetherian _) fun _ _ ↦ ?_
  exact Ideal.finite_quotient_pow (IsNoetherian.noetherian _) _

Goal state after:
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
⊢ Continuous[_, tY] WithGeneratedByTopology.equiv.toFun

Tactic:
dsimp; fun_prop

Goal state after:
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
⊢ Continuous[tY, _] WithGeneratedByTopology.equiv.invFun

Tactic:
dsimp; fun_prop

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case inl
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
this : ∀ S ∈ T2, S ∈ T0 ∨ ∃ Q ∈ T0, S = AA ∩ Q
S : Set (Ultrafilter X.A)
hS : S ∈ T2
h : S ∈ T0
⊢ S.Nonempty

pp: case inr
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
this : ∀ S ∈ T2, S ∈ T0 ∨ ∃ Q ∈ T0, S = AA ∩ Q
S : Set (Ultrafilter X.A)
hS : S ∈ T2
h : ∃ Q ∈ T0, S = AA ∩ Q
⊢ S.Nonempty

Tactic:
· exact claim5 S h

Goal state after:
case inr
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
this : ∀ S ∈ T2, S ∈ T0 ∨ ∃ Q ∈ T0, S = AA ∩ Q
S : Set (Ultrafilter X.A)
hS : S ∈ T2
h : ∃ Q ∈ T0, S = AA ∩ Q
⊢ S.Nonempty
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ 1 - e (π C fun x ↦ x ∈ s) a ∈ factors C s x

Tactic:
by
  simp only [factors, List.mem_map, Finset.mem_sort]
  use a
  simp only [hx]
  rcases y with ⟨_, z, hz, rfl⟩
  aesop (add simp Proj)

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝³ : (i : I) → Decidable (J i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
x✝ : (Finset I)ᵒᵖ
s : Finset I
⊢ (indexCone hC).π.app (op s) =
    (Iso.refl (indexCone hC).pt).hom ≫
      ((Cone.postcompose (spanFunctorIsoIndexFunctor hC).hom).obj (spanCone hC)).π.app (op s)

Tactic:
by
      ext
      have : iso_map C (· ∈ s) ∘ ProjRestrict C (· ∈ s) = IndexFunctor.π_app C (· ∈ s) := by
        ext _ i; exact dif_pos i.prop
      exact congr_fun this.symm _

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.isGood C l
⊢ L l

Tactic:
apply subset_span
    exact ⟨⟨l, hl⟩, rfl⟩

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x✝ : ↑(smaller C o)
a : LocallyConstant ↑C ℤ
b : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
hb : b ∈ range (π C fun x ↦ ord I x < o) ∧ (πs C o) b = a
⊢ ∃ a_1, (fun x ↦ ⟨(πs C o) ↑x, ⋯⟩) a_1 = ⟨a, ⋯⟩

Tactic:
use ⟨b, hb.1⟩

Goal state after:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x✝ : ↑(smaller C o)
a : LocallyConstant ↑C ℤ
b : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
hb : b ∈ range (π C fun x ↦ ord I x < o) ∧ (πs C o) b = a
⊢ (fun x ↦ ⟨(πs C o) ↑x, ⋯⟩) ⟨b, ⋯⟩ = ⟨a, ⋯⟩
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ ∀ x ∈ C' C ho, x (term I ho) = false

Tactic:
rintro x ⟨_, y, _, rfl⟩

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
y : I → Bool
left✝¹ : y ∈ C1 C ho
left✝ : Proj (fun x ↦ ord I x < o) y ∈ C0 C ho
⊢ Proj (fun x ↦ ord I x < o) y (term I ho) = false
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
⊢ ↑(skeletonLT C m) ⊆ ↑(skeletonLT C n)

Tactic:
simp_rw [coe_skeletonLT]
  apply union_subset_union_right
  intro x xmem
  simp_rw [mem_iUnion, exists_prop] at xmem ⊢
  obtain ⟨l, lltm, xmeml⟩ := xmem
  exact ⟨l, lt_of_lt_of_le lltm h, xmeml⟩

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
x : X
⊢ x ∈ skeletonLT C n ↔ x ∈ D ∨ ∃ m, ∃ (_ : ↑m < n), ∃ j, x ∈ openCell m j

Tactic:
simp [← SetLike.mem_coe, ← iUnion_openCell_eq_skeletonLT]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : T2Space X
inst✝ : CWComplex C
n : ℕ∞
x : X
⊢ x ∈ skeletonLT C n ↔ ∃ m, ∃ (_ : ↑m < n), ∃ j, x ∈ openCell m j

Tactic:
simp [← SetLike.mem_coe, ← iUnion_openCell_eq_skeletonLT]

Goal state after: