mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0
h : (map (IsLocalRing.residue A)) g = 0
⊢ (map (IsLocalRing.residue A)) (a • g) = 0

Tactic:
simp [Algebra.smul_def, h]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
h : (IsLocalRing.residue A) a = 0
⊢ (map (IsLocalRing.residue A)) (a • g) = 0

Tactic:
simp [Algebra.smul_def, h]

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : IsSimpleRing R
tfae_1_to_2 : IsSemisimpleRing R → IsArtinianRing R
tfae_2_to_3 : IsArtinianRing R → ∃ I, IsAtom I
x✝ : ∃ I, IsAtom I
I : Ideal R
hI : IsAtom I
left✝ : Nontrivial R
h : ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
⊢ IsSemisimpleRing R

Tactic:
← isFullyInvariant_iff_isTwoSided

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : IsSimpleRing R
tfae_1_to_2 : IsSemisimpleRing R → IsArtinianRing R
tfae_2_to_3 : IsArtinianRing R → ∃ I, IsAtom I
x✝ : ∃ I, IsAtom I
I : Ideal R
hI : IsAtom I
left✝ : Nontrivial R
h : ∀ (I : Ideal R), Submodule.IsFullyInvariant I → I = ⊥ ∨ I = ⊤
⊢ IsSemisimpleRing R
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
S : Type u_2
inst✝¹⁰ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁹ : CommRing R'
inst✝⁸ : CommRing S'
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : Module.Flat R S
surj : Function.Surjective ⇑(algebraMap R R')
surjS : Function.Surjective ⇑(algebraMap S S')
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
sq0 : RingHom.ker (algebraMap R R') ^ 2 = ⊥
smoothq : FormallySmooth R' S'
P : Extension R S := (Generators.self R S).toExtension
this✝¹ : FormallySmooth R P.Ring := instFormallySmoothMvPolynomial S
IP : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) (RingHom.ker (algebraMap R R'))
Gen : Generators R' S' S :=
  { val := ⇑(algebraMap S S'), σ' := fun s' ↦ MvPolynomial.X (Classical.choose ⋯), aeval_val_σ' := ⋯,
    algebraMap_eq := ⋯ }
P' : Extension R' S' := Gen.toExtension
this✝ : FormallySmooth R' P'.Ring := instFormallySmoothMvPolynomial S
this : Algebra P.Ring P'.Ring := MvPolynomial.algebraMvPolynomial
⊢ FormallySmooth R S

Tactic:
let : IsScalarTower R P.Ring P'.Ring :=
    IsScalarTower.of_algebraMap_eq (fun x ↦ (MvPolynomial.map_C _ x).symm)

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
S : Type u_2
inst✝¹⁰ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁹ : CommRing R'
inst✝⁸ : CommRing S'
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : Module.Flat R S
surj : Function.Surjective ⇑(algebraMap R R')
surjS : Function.Surjective ⇑(algebraMap S S')
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
sq0 : RingHom.ker (algebraMap R R') ^ 2 = ⊥
smoothq : FormallySmooth R' S'
P : Extension R S := (Generators.self R S).toExtension
this✝² : FormallySmooth R P.Ring := instFormallySmoothMvPolynomial S
IP : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) (RingHom.ker (algebraMap R R'))
Gen : Generators R' S' S :=
  { val := ⇑(algebraMap S S'), σ' := fun s' ↦ MvPolynomial.X (Classical.choose ⋯), aeval_val_σ' := ⋯,
    algebraMap_eq := ⋯ }
P' : Extension R' S' := Gen.toExtension
this✝¹ : FormallySmooth R' P'.Ring := instFormallySmoothMvPolynomial S
this✝ : Algebra P.Ring P'.Ring := MvPolynomial.algebraMvPolynomial
this : IsScalarTower R P.Ring P'.Ring :=
  IsScalarTower.of_algebraMap_eq fun x ↦ Eq.symm (MvPolynomial.map_C (algebraMap R R') x)
⊢ FormallySmooth R S
Module: Mathlib.RingTheory.WittVector.Isocrystal

Goal state before:
pp: case h
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
⊢ Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)

Tactic:
refine ⟨⟨(LinearEquiv.smulOfNeZero K(p, k) _ _ hb).trans F, fun c ↦ ?_⟩⟩

Goal state after:
case h
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ Φ(p, k) ((LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb ≪≫ₗ F) c) =
    (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb ≪≫ₗ F) (Φ(p, k) c)
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: ⊢ UnivLE.{u, v} ∨ UnivLE.{v, u}

Tactic:
simp_rw [univLE_iff_cardinal_le]; apply le_total

Goal state after:
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case inl
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
h' : y.length ≤ x.length
⊢ y ∈ ↑T

Tactic:
rw [mem_pullSub_short h'] at h; exact mem_of_prefix h.1 (by simpa using h.2)

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

Goal state before:
pp: b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
⊢ (0, o / b ^ 0) :: CNF b (o % b ^ 0) = [(0, o)]

Tactic:
opow_zero,

Goal state after:
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
⊢ (0, o / 1) :: CNF b (o % 1) = [(0, o)]
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case refine_2
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : f x = x
o : Ordinal.{u}
⊢ lfpApprox f x o = x

Tactic:
have : lfpApprox f x 0 ∈ fixedPoints f := by
      rwa [mem_fixedPoints_iff, lfpApprox_zero]

Goal state after:
case refine_2
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : f x = x
o : Ordinal.{u}
this : lfpApprox f x 0 ∈ fixedPoints ⇑f
⊢ lfpApprox f x o = x
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
⊢ ∀ i_1 < i, f (lfpApprox f x i_1) ≤ f a

Tactic:
exact fun y hy ↦ f.mono (IH y hy)

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

Goal state before:
pp: case inr
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
x✝ : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := x✝
hne : (s ∩ Iic a).Nonempty
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
· refine ⟨hne, (isLUB_of_mem_closure ?_ h).csSup_eq hne⟩
      exact fun x hx => hx.2

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

Goal state before:
pp: case single_add.h.inl
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
e₂ : Ordinal.{u_1}
he₂✝ : e₂ ∈ (f₁ + f₂).support
he₂ : e₂ ∈ f₁.support
⊢ e₂ ≤ e₁

Tactic:
exact (hf₁ _ he₂).le

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

Goal state before:
pp: α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H✝ : (mk α A).Equiv (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : (mk γ C).Equiv ((mk β B).Func b)
a : (mk α A).Type
ha : ((mk α A).Func a).Equiv ((mk β B).Func b)
H : (A a).Equiv (mk γ C)
⊢ Acc (fun x1 x2 ↦ x1 ∈ x2) (mk γ C)

Tactic:
exact mem_wf_aux H

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

Goal state before:
pp: x : PSet.{u_1}
⊢ x.rank ≤ succ (⋃₀ x).rank

Tactic:
rw [← rank_powerset]

Goal state after:
x : PSet.{u_1}
⊢ x.rank ≤ (⋃₀ x).powerset.rank
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: ⊢ invVeblen₂ 0 = 0

Tactic:
by
  apply invVeblen₂_of_lt_opow
  simp

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

Goal state before:
pp: x : ZFSet.{u_1}
⊢ x.rank ≤ succ (⋃₀ x).rank

Tactic:
rw [← rank_powerset]

Goal state after:
x : ZFSet.{u_1}
⊢ x.rank ≤ (⋃₀ x).powerset.rank
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s : R
b : ℕ
h : r ^ b = s
⊢ (algebraMap R A) r ^ b = (algebraMap R A) s

Tactic:
rw [← map_pow, h]

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

Goal state before:
pp: x : ONote
inst✝¹ : x.NF
o : ONote
inst✝ : o.NF
⊢ (x.scale o).repr = ω ^ x.repr * o.repr

Tactic:
by
  simp only [scale_eq_mul, repr_mul, repr, PNat.one_coe, Nat.cast_one, mul_one, add_zero]

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

Goal state before:
pp: α : Type u_1
s t : Stream'.Seq α
h : s.head = t.head
⊢ dist s t = 2⁻¹ * dist s.tail t.tail

Tactic:
cases s

Goal state after:
case nil
α : Type u_1
t : Stream'.Seq α
h : nil.head = t.head
⊢ dist nil t = 2⁻¹ * dist nil.tail t.tail

case cons
α : Type u_1
t : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : (Seq.cons x✝ s✝).head = t.head
⊢ dist (Seq.cons x✝ s✝) t = 2⁻¹ * dist (Seq.cons x✝ s✝).tail t.tail
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
s t : Stream'.Seq α
h : dist s t ≤ 2⁻¹
⊢ s = nil ∧ t = nil ∨ ∃ hd s' t', s = Seq.cons hd s' ∧ t = Seq.cons hd t'

Tactic:
cases s

Goal state after:
case nil
α : Type u_1
t : Stream'.Seq α
h : dist nil t ≤ 2⁻¹
⊢ nil = nil ∧ t = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ t = Seq.cons hd t'

case cons
α : Type u_1
t : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝ s✝) t ≤ 2⁻¹
⊢ Seq.cons x✝ s✝ = nil ∧ t = nil ∨ ∃ hd s' t', Seq.cons x✝ s✝ = Seq.cons hd s' ∧ t = Seq.cons hd t'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s : Stream'.Seq α
⊢ (op s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      (h.unfold s.head)

Tactic:
by
  unfold unfold
  cases s with
  | nil =>
    generalize op nil = t
    cases t <;> simp
  | cons s_hd s_tl =>
    simp only [Seq.tail_cons, Seq.head_cons]
    generalize ht0 : op (.cons s_hd nil) = t0 at *
    generalize ht : op (.cons s_hd s_tl) = t at *
    have : t0.head = t.head := by
      rw [← ht0, ← ht, FriendlyOperation.op_cons_head_eq h]
    cases t0 with
    | nil =>
      cases t with
      | nil => simp
      | cons => simp at this
    | cons =>
      cases t with
      | nil => simp at this
      | cons => simp_all

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

Goal state before:
pp: hd : ℝ
tl : UnitMonomial
⊢ AllZero (hd :: tl) ↔ hd = 0 ∧ tl.AllZero

Tactic:
by
  grind [AllZero, sign]

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
⊢ s.leadingExp = ⊥ ↔ s = nil

Tactic:
cases s

Goal state after:
case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ nil.leadingExp = ⊥ ↔ nil = nil

case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
tl✝ : Multiseries basis_hd basis_tl
⊢ (cons exp✝ coef✝ tl✝).leadingExp = ⊥ ↔ cons exp✝ coef✝ tl✝ = nil
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : 0 < exps_hd
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
⊢ Tendsto (exps_hd • log ∘ basis_hd) atTop atTop

Tactic:
apply Filter.Tendsto.const_mul_atTop h_nonzero

Goal state after:
exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : 0 < exps_hd
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
⊢ Tendsto (log ∘ basis_hd) atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length m = List.length basis
h_firstIsPos : m.FirstNonzeroIsPos
⊢ Tendsto (m.toFun basis) atTop atTop

Tactic:
cases m with
  | nil => simp at h_firstIsPos
  | cons exps_hd exps_tl =>
    cases basis with
    | nil => simp at h_length
    | cons basis_hd basis_tl =>
      simp only [FirstNonzeroIsPos.cons_iff] at h_firstIsPos
      obtain h | h := h_firstIsPos
      · exact toFun_tendsto_top_of_head_pos h_basis h
      · have h_eq : UnitMonomial.toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) =
                    UnitMonomial.toFun exps_tl basis_tl := by
          ext x; simp [UnitMonomial.toFun, h.left]
        rw [h_eq]
        exact toFun_tendsto_top_of_firstNonzeroIsPos h_basis.tail (by simpa using h_length) h.right

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

Goal state before:
pp: case const
c✝ : MultiseriesExpansion []
hc : c✝.toReal = 0
h_approx : c✝.Approximates
⊢ c✝.toFun =ᶠ[atTop] 0

Tactic:
| const hc =>

Goal state after:
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (↑n - 1) a
pa : ↑a = a'
⊢ -b = a' * b

Tactic:
by
  rw [← pa, ← p.out, ← neg_one_mul]
  simp

Goal state after:
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat ((↑n - 1) * a) na
pa : ↑na = na'
⊢ -(a * b) = na' * b

Tactic:
by
  rw [← pa, ← p.out, ← neg_one_mul]
  simp

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: case pos.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ (U ∩ derivedSet a).Nonempty

pp: case pos.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ (U ∩ derivedSet b).Nonempty

Tactic:
· exact ha

Goal state after:
case pos.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ (U ∩ derivedSet b).Nonempty
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
A : Set X
hA : A ⊆ ↑E
h : (∀ (n : ℕ) (j : ↑(E.I n)), IsClosed[t] (A ∩ ↑(map n ↑j) '' closedBall 0 1)) ∧ IsClosed[t] (A ∩ D)
⊢ IsClosed[t] A

Tactic:
apply isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell
      (subset_trans hA (subset_complex (C := C) E)) h.2

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
A : Set X
hA : A ⊆ ↑E
h : (∀ (n : ℕ) (j : ↑(E.I n)), IsClosed[t] (A ∩ ↑(map n ↑j) '' closedBall 0 1)) ∧ IsClosed[t] (A ∩ D)
⊢ ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case cond
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := ⋯
ssu : Type u_1 := ⋯
ι : fsu → ssu := ⋯
T0 : ssu := ⋯
AA : Set (Ultrafilter X.A) := ⋯
T1 : ssu := ⋯
T2 : Set (Set (Ultrafilter X.A)) := ⋯
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
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ FiniteInter T0

pp: case H
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := ⋯
ssu : Type u_1 := ⋯
ι : fsu → ssu := ⋯
T0 : ssu := ⋯
AA : Set (Ultrafilter X.A) := ⋯
T1 : ssu := ⋯
T2 : Set (Set (Ultrafilter X.A)) := ⋯
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
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ S ∈ finiteInterClosure (insert AA T0)

Tactic:
· constructor
      · use Set.univ
        refine ⟨Filter.univ_sets _, ?_⟩
        ext
        refine ⟨?_, by tauto⟩
        · intro
          apply Filter.univ_sets
      · exact claim3

Goal state after:
case H
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := ⋯
ssu : Type u_1 := ⋯
ι : fsu → ssu := ⋯
T0 : ssu := ⋯
AA : Set (Ultrafilter X.A) := ⋯
T1 : ssu := ⋯
T2 : Set (Set (Ultrafilter X.A)) := ⋯
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
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ S ∈ finiteInterClosure (insert AA T0)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x y : cell C 0
h : openCell 0 x = openCell 0 y
⊢ x = y

Tactic:
openCell_zero_eq_singleton,

Goal state after:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x y : cell C 0
h : {↑(map 0 x) ![]} = openCell 0 y
⊢ x = y
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x y : cell C 0
h : {↑(map 0 x) ![]} = openCell 0 y
⊢ x = y

Tactic:
openCell_zero_eq_singleton,

Goal state after:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x y : cell C 0
h : {↑(map 0 x) ![]} = {↑(map 0 y) ![]}
⊢ x = y
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case e_s
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
e : cell C 1
f : Fin 1 → ℝ
⊢ f 0 = 1 ∨ f 0 = -1 ↔ f = -1 ∨ f = 1

Tactic:
rw [eq_const_of_unique (f := f), ← funext_iff_of_subsingleton (x := 0) (y := 0)]

Goal state after:
case e_s
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
e : cell C 1
f : Fin 1 → ℝ
⊢ const (Fin 1) (f default) 0 = 1 ∨ const (Fin 1) (f default) 0 = -1 ↔
    const (Fin 1) (f default) 0 = (-1) 0 ∨ const (Fin 1) (f default) = 1
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : ↑m < n
j : cell C m
⊢ openCell m j ⊆ ⋃ j, closedCell m j

Tactic:
apply subset_iUnion_of_subset j

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : ↑m < n
j : cell C m
⊢ openCell m j ⊆ closedCell m j
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
⊢ D ∪ ⋃ n, ⋃ j, openCell n j = C

Tactic:
suffices D ∪ ⋃ n, ⋃ (j : cell C n), openCell n j =
      D ∪ ⋃ (m : ℕ) (_ : m < (⊤ : ℕ∞)) (j : cell C m), closedCell m j by
    simpa [union] using this
  simp_rw [← RelCWComplex.iUnion_openCell_eq_iUnion_closedCell, ENat.natCast_lt_top, iUnion_true]

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

Goal state before:
pp: X : Compactum
⊢ ∀ {x y : X.A} (f : Ultrafilter X.A), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = y

Tactic:
intro _ _ F hx hy

Goal state after:
X : Compactum
x✝ y✝ : X.A
F : Ultrafilter X.A
hx : ↑F ≤ 𝓝 x✝
hy : ↑F ≤ 𝓝 y✝
⊢ x✝ = y✝
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X Y : Compactum
f : X.A → Y.A
cont : Continuous f
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
      rw [continuous_iff_ultrafilter] at cont
      ext (F : Ultrafilter X)
      specialize cont (X.str F) F (le_nhds_of_str_eq F (X.str F) rfl)
      simpa using! str_eq_of_le_nhds (Ultrafilter.map f F) _ cont

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : List I
hl : List.IsChain (fun x1 x2 ↦ x1 > x2) l
hll : Products.isGood {fun x ↦ false} ⟨l, hl⟩
a✝ : List.Lex (fun x1 x2 ↦ x1 < x2) [] l
he : {Products.nil} ⊆ {m | m < ⟨l, hl⟩}
⊢ Products.eval {fun x ↦ false} ⟨l, hl⟩ ∈ Submodule.span ℤ (Products.eval {fun x ↦ false} '' {m | m < ⟨l, hl⟩})

Tactic:
grw [← he]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : List I
hl : List.IsChain (fun x1 x2 ↦ x1 > x2) l
hll : Products.isGood {fun x ↦ false} ⟨l, hl⟩
a✝ : List.Lex (fun x1 x2 ↦ x1 < x2) [] l
he : {Products.nil} ⊆ {m | m < ⟨l, hl⟩}
⊢ Products.eval {fun x ↦ false} ⟨l, hl⟩ ∈ Submodule.span ℤ (Products.eval {fun x ↦ false} '' {Products.nil})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: 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.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
this : Products.eval C '' {m | m < l} ⊆ ↑(Submodule.span ℤ (Set.range (eval C)))
⊢ L l

Tactic:
rw [← span_le] at this
      exact this hl

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
hl : ∀ i ∈ ↑l, ord I i < o
f : LocallyConstant ↑C ℤ
⊢ (∃ x < l, eval C x = f) ↔ ∃ a < l, (πs C o) (eval (π C fun x ↦ ord I x < o) a) = f

Tactic:
apply exists_congr

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
hl : ∀ i ∈ ↑l, ord I i < o
f : LocallyConstant ↑C ℤ
⊢ ∀ (a : Products I), a < l ∧ eval C a = f ↔ a < l ∧ (πs C o) (eval (π C fun x ↦ ord I x < o) a) = f
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x ↦ ord I x < o₂) ℤ
⊢ (∃ x < l, eval (π C fun x ↦ ord I x < o₂) x = f) ↔ ∃ a < l, (πs' C h) (eval (π C fun x ↦ ord I x < o₁) a) = f

Tactic:
apply exists_congr

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x ↦ ord I x < o₂) ℤ
⊢ ∀ (a : Products I),
    a < l ∧ eval (π C fun x ↦ ord I x < o₂) a = f ↔ a < l ∧ (πs' C h) (eval (π C fun x ↦ ord I x < o₁) a) = f