mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R S
L : Type u_5
inst✝⁴ : Field L
inst✝³ : Algebra R L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R K L
inst✝ : IsPurelyInseparable K L
⊢ IsHomeomorph (comap (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S)).toRingHom)

Tactic:
let e : (L ⊗[R] S) ≃ₐ[K] L ⊗[K] (K ⊗[R] S) :=
    (Algebra.TensorProduct.cancelBaseChange R K K L S).symm
  let e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] (K ⊗[R] S) ⊗[K] L := Algebra.TensorProduct.comm ..
  have heq : Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) =
      (e.symm.toAlgHom.comp e2.symm.toAlgHom).comp
        (IsScalarTower.toAlgHom K (K ⊗[R] S) ((K ⊗[R] S) ⊗[K] L)) := by
    ext; simp [e, e2]
  rw [heq]
  simp only [AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom,
    AlgEquiv.toAlgHom_toRingHom, IsScalarTower.coe_toAlgHom, comap_comp]
  exact (isHomeomorph_comap_of_isPurelyInseparable K L (K ⊗[R] S)).comp <|
    (isHomeomorph_comap_of_bijective e2.symm.bijective).comp <|
    isHomeomorph_comap_of_bijective e.symm.bijective

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a ≤ b
⊢ lfpApprox f x a ≤ lfpApprox f x b

Tactic:
lfpApprox,

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a ≤ b
⊢ x ⊔ ⨆ b, ⨆ (_ : b < a), f (lfpApprox f x b) ≤ lfpApprox f x b
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ lfpApprox f x a ≤ ⨆ b, lfpApprox f x ↑b

Tactic:
lfpApprox,

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ x ⊔ ⨆ b, ⨆ (_ : b < a), f (lfpApprox f x b) ≤ ⨆ b, lfpApprox f x ↑b
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case ind
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ lfpApprox g x y
⊢ lfpApprox f x i ≤ lfpApprox g x i

Tactic:
lfpApprox,

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ lfpApprox g x y
⊢ x ⊔ ⨆ b, ⨆ (_ : b < i), f (lfpApprox f x b) ≤ lfpApprox g x i
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x₁ y ≤ lfpApprox f x₂ y
⊢ lfpApprox f x₁ i ≤ lfpApprox f x₂ i

Tactic:
lfpApprox,

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x₁ y ≤ lfpApprox f x₂ y
⊢ x₁ ⊔ ⨆ b, ⨆ (_ : b < i), f (lfpApprox f x₁ b) ≤ lfpApprox f x₂ i
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ (map Prod.toSigma (CNF b o)).NodupKeys

Tactic:
rw [NodupKeys, List.keys, map_map, Prod.fst_comp_toSigma]
  exact (CNF.sortedGT ..).nodup

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α false
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
cases l₁

Goal state after:
case atom
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst✝ : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ out f xs ≈ out f ys

Tactic:
rw [← Quotient.eq_iff_equiv, mk_eq, mk_eq, mk_out, mk_out]

Goal state after:
n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst✝ : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ (f fun x ↦ ZFSet.mk (xs x)) = f fun x ↦ ZFSet.mk (ys x)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x✝ y z x : ZFSet.{u}
a : PSet.{u}
f : a.Type → ↥(mk a) := fun i ↦ ⟨mk (a.Func i), ⋯⟩
this : Function.Surjective f
⊢ Small.{u, u + 1} ↥(⟦a⟧)

Tactic:
by exact small_of_surjective this

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

Goal state before:
pp: case refine_1
x y z : ZFSet.{u_1}
h : {x, y} = {z}
⊢ x ∈ {z} ∧ y = z

Tactic:
← mem_singleton

Goal state after:
case refine_1
x y z : ZFSet.{u_1}
h : {x, y} = {z}
⊢ x ∈ {z} ∧ y ∈ {z}
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: ⊢ ∅.rank = 0

Tactic:
by simp [empty_def, rank]

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

Goal state before:
pp: o x : Ordinal.{u}
h : x.invVeblen₁ < o
z : Ordinal.{u}
hz : veblen x.invVeblen₁ (veblen o z) = ω ^ x
hz' : veblen o z = ω ^ x
⊢ False

Tactic:
hz',

Goal state after:
o x : Ordinal.{u}
h : x.invVeblen₁ < o
z : Ordinal.{u}
hz : veblen x.invVeblen₁ (ω ^ x) = ω ^ x
hz' : veblen o z = ω ^ x
⊢ False
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case refine_1.inr
o a x : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ ω ^ veblen o a = ω ^ x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a

Tactic:
opow_right_inj one_lt_omega0

Goal state after:
case refine_1.inr
o a x : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ veblen o a = x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u}
x : ZFSet.{u}
⊢ x.rank < o → ∃ a < o, x.rank ≤ a

Tactic:
by aesop

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

Goal state before:
pp: case refine_2
o : Ordinal.{u_1}
z : ZFSet.{u_1}
a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
b : Ordinal.{u_1}
hb : b < a
hz : z ∈ b.toZFSet
hy : b.toZFSet ∈ a.toZFSet
⊢ z ∈ a.toZFSet

Tactic:
obtain ⟨c, hc, rfl⟩ := mem_toZFSet_iff.1 hz
    exact toZFSet_mem_toZFSet_iff.2 (hc.trans hb)

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

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (x y : Stream'.Seq α), dist (op x) (op y) ≤ ↑1 * dist x y
s t : Stream'.Seq α
⊢ dist (op s) (op t) ≤ dist s t

Tactic:
simpa using h s t

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

Goal state before:
pp: left right : Basis
h_left : WellFormedBasis left
h_right : WellFormedBasis right
h : ∀ f ∈ left, ∀ g ∈ right, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ WellFormedBasis (left ++ right)

Tactic:
simp only [WellFormedBasis] at *
  constructor
  · simpa [List.pairwise_append, h_left, h_right] using h
  · grind

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

Goal state before:
pp: case cons
hd : ℝ → ℝ
tl : List (ℝ → ℝ)
ih : WellFormedBasis tl → ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x
h :
  ((∀ a' ∈ tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ hd)) ∧
      List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) tl) ∧
    Tendsto hd atTop atTop ∧ ∀ a ∈ tl, Tendsto a atTop atTop
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < hd x ∧ ∀ a ∈ tl, 0 < a x

Tactic:
exact (h.right.left.eventually <| eventually_gt_atTop 0).and (ih (by tauto))

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

Goal state before:
pp: case succ
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, op') => (hd, ↑op' s.tail))
              (T s.head)
n : ℕ
ih :
  ∀ {op : Stream'.Seq α → Stream'.Seq α},
    motive op → ∀ (s t : Stream'.Seq α), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
op : Stream'.Seq α → Stream'.Seq α
h_base : motive op
s t : Stream'.Seq α
hn : dist s t ≤ 2⁻¹ ^ (n + 1)
⊢ dist (op s) (op t) ≤ 2⁻¹ ^ (n + 1)

Tactic:
obtain ⟨T, hT⟩ := h_step _ h_base
    have h_head : s.head = t.head := by
      replace hn : dist s t ≤ 2⁻¹ := by
        apply hn.trans
        simp only [pow_succ, inv_pos, Nat.ofNat_pos, mul_le_iff_le_one_left]
        apply pow_le_one₀ <;> norm_num
      rw [dist_le_half_iff] at hn
      obtain ⟨rfl, rfl⟩ | ⟨hd, s_tl, t_tl, rfl, rfl⟩ := hn <;> rfl
    have hs := hT s
    have ht := hT t
    cases hT_head : T s.head with
    | none =>
      simp only [hT_head, Option.map_none, ← h_head] at hs ht
      simp [hs, ht, destruct_eq_none]
    | some v =>
      obtain ⟨hd, op', h_next⟩ := v
      simp only [hT_head, Option.map_some, ← h_head] at hs ht
      simp only [destruct_eq_cons hs, destruct_eq_cons ht, dist_cons_cons, pow_succ', inv_pos,
        Nat.ofNat_pos, mul_le_mul_iff_right₀, ge_iff_le]
      apply ih h_next
      simpa [dist_eq_half_of_head h_head, pow_succ'] using hn

Goal state after:
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 : exps_hd ≠ 0
⊢ toLogFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd

Tactic:
simp only [toLogFun_cons]

Goal state after:
exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : exps_hd ≠ 0
⊢ exps_hd • log ∘ basis_hd + exps_tl.toLogFun basis_tl ~[atTop] exps_hd • log ∘ basis_hd
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case seq.h_Pairwise.cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
tl✝ : Multiseries basis_hd basis_tl
h_comp : (Multiseries.cons exp✝ coef✝ tl✝).leadingExp < ↑exp
h_tl_coef : ∀ x ∈ (mk (Multiseries.cons exp✝ coef✝ tl✝) 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp✝ coef✝ tl✝) 0).seq
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef (Multiseries.cons exp✝ coef✝ tl✝)) 0).seq

Tactic:
· exact h_tl_tl.cons_cons_of_trans (by simpa [lt_iff_lt] using h_comp)

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

Goal state before:
pp: ⊢ fastGrowingε₀ 0 = 1

Tactic:
by simp [fastGrowingε₀]

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

Goal state before:
pp: a : ℚ
n d : ℕ
hn : IsSquare n
hd : IsSquare d
ha : IsNNRat a n d
⊢ IsSquare a

Tactic:
rcases hn with ⟨n, rfl⟩

Goal state after:
a : ℚ
d : ℕ
hd : IsSquare d
n : ℕ
ha : IsNNRat a (n * n) d
⊢ IsSquare a
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
x' : ℤ := q.num
y : ℕ := q.den
h : ↑a / ↑b = (↑x' / ↑y) ^ d
⊢ False

Tactic:
obtain ⟨x, hx'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ x' by rwa [Rat.num_nonneg])

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
x' : ℤ := q.num
y : ℕ := q.den
h : ↑a / ↑b = (↑x' / ↑y) ^ d
x : ℕ
hx' : x' = ↑x
⊢ False
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq α
m : List ((_ : α) × β)
y : β
x : α
⊢ (withDefault m y).apply x = (List.dlookup x m).getD y

Tactic:
dsimp only [apply]
  congr 1
  induction m with
  | nil => simp
  | cons p m ih =>
    rcases p with ⟨fst, snd⟩
    by_cases heq : fst = x
    · simp [heq]
    · rw [List.dlookup_cons_ne]
      · simp [heq, ih]
      · symm
        simp [heq]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: case hc
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := ⋯
F : ℕ × ↑s → Set X := ⋯
this✝ : Nonempty X
this : Encodable ↑s
⊢ ∀ (i : ℕ × ↑s), IsClosed[inst✝⁸] (F i)

Tactic:
rintro ⟨n, ⟨g, hg⟩⟩

Goal state after:
case hc
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
this✝ : Nonempty X
this : Encodable ↑s
n : ℕ
g : G
hg : g ∈ s
⊢ IsClosed[inst✝⁸] (F (n, ⟨g, hg⟩))
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
⊢ IsOpenUnits R

Tactic:
by
  refine ⟨.of_continuous_injective_isOpenMap Units.continuous_val Units.val_injective ?_⟩
  refine (IsTopologicalGroup.isOpenMap_iff_nhds_one (f := Units.coeHom R)).mpr ?_
  rw [nhds_induced, nhds_prod_eq]
  simp only [Units.embedProduct_apply, Units.val_one, inv_one, MulOpposite.op_one]
  intro s hs
  have H := hR ▸ Ideal.hasBasis_nhds_adic I 1
  have := (H.prod (H.comap MulOpposite.opHomeomorph.symm))
  simp only [Homeomorph.comap_nhds_eq, Homeomorph.symm_symm, MulOpposite.opHomeomorph_apply,
    MulOpposite.op_one, and_self, Set.image_add_left] at this
  have : ∃ n₁ n₂, ∀ (u : Rˣ), (-1 + u : R) ∈ I ^ n₁ → (-1 + u⁻¹ : R) ∈ I ^ n₂ → ↑u ∈ s := by
    simpa [Set.subset_def, forall_comm (β := Rˣ), forall_comm (β := _ = _)] using
      (((this.comap (Units.embedProduct R)).map (Units.coeHom R)).1 _).mp hs
  obtain ⟨n, hn, hn'⟩ : ∃ n ≠ 0, ∀ (u : Rˣ), (-1 + u : R) ∈ I ^ n →
      (-1 + u⁻¹ : R) ∈ I ^ n → ↑u ∈ s := by
    obtain ⟨n₁, n₂, H⟩ := this
    exact ⟨n₁ ⊔ n₂ ⊔ 1, by simp, fun u h₁ h₂ ↦ H u
      (Ideal.pow_le_pow_right (by simp) h₁)
      (Ideal.pow_le_pow_right (by simp) h₂)⟩
  rw [H.1]
  refine ⟨n, trivial, ?_⟩
  rintro _ ⟨x, hx, rfl⟩
  have := Ideal.mem_jacobson_bot.mp (hI (Ideal.pow_le_self hn hx)) 1
  rw [mul_one, add_comm] at this
  refine hn' this.unit (by simpa using hx) ?_
  have : -1 + ↑this.unit⁻¹ = -this.unit⁻¹ * x := by
    trans this.unit⁻¹ * (-(1 + x) + 1)
    · rw [mul_add, mul_neg, IsUnit.val_inv_mul, mul_one]
    · simp
  rw [this]
  exact Ideal.mul_mem_left _ _ hx

Goal state after:
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : |(↑x).arg| < π / 2 ^ (n + 1)
h2 : |(↑x).arg + (↑x).arg| < π / 2 ^ (n + 1)
⊢ |(↑x).arg| < π / 2 ^ (n + 1 + 1)

pp: case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : |(↑x).arg| < π / 2 ^ (n + 1)
h2 : |(↑x * ↑x).arg| < π / 2 ^ (n + 1)
⊢ (↑x).arg + (↑x).arg ∈ Set.Ioc (-π) π

Tactic:
← two_mul,

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : |(↑x).arg| < π / 2 ^ (n + 1)
h2 : |2 * (↑x).arg| < π / 2 ^ (n + 1)
⊢ |(↑x).arg| < π / 2 ^ (n + 1 + 1)

case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : |(↑x).arg| < π / 2 ^ (n + 1)
h2 : |(↑x * ↑x).arg| < π / 2 ^ (n + 1)
⊢ (↑x).arg + (↑x).arg ∈ Set.Ioc (-π) π
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := ⋯
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : |(↑x).arg| < π / 2 ^ (n + 1)
h2 : |(↑x * ↑x).arg| < π / 2 ^ (n + 1)
⊢ (↑x).arg + (↑x).arg ∈ Set.Ioo (-π) π

Tactic:
← two_mul,

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : |(↑x).arg| < π / 2 ^ (n + 1)
h2 : |(↑x * ↑x).arg| < π / 2 ^ (n + 1)
⊢ 2 * (↑x).arg ∈ Set.Ioo (-π) π
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
V : Set (PontryaginDual A) := {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
⊢ IsOpen V

Tactic:
dsimp only [V]

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
V : Set (PontryaginDual A) := {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
⊢ IsOpen {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
Module: Mathlib.Topology.CWComplex.Classical.Graph

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
h : (cellFrontier 1 e).Subsingleton
x : cell C 0
hxy : cellFrontier 1 e = {↑(map 0 x) ![], ↑(map 0 x) ![]}
⊢ cellFrontier 1 e = closedCell 0 x

Tactic:
by simp [hxy, closedCell_zero_eq_singleton]

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

Goal state before:
pp: X Y : Compactum
x✝¹ x✝ : X ⟶ Y
h : (fun f ↦ ⇑(ConcreteCategory.hom f.f)) x✝¹ = (fun f ↦ ⇑(ConcreteCategory.hom f.f)) x✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by aesop

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

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
x✝² x✝¹ : ContinuousMapGeneratedBy X Y Z
x✝ : (fun f ↦ f.toFun) x✝² = (fun f ↦ f.toFun) x✝¹
⊢ x✝² = x✝¹

Tactic:
by aesop

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

Goal state before:
pp: case a.sr.hi
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' : ∀ m_1 ≤ m, ↑m_1 < n → ∀ (j : cell C m_1), cellFrontier m_1 j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j
hm : ↑(m + 1) < n
j : cell C (m + 1)
⊢ cellFrontier (m + 1) j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j

Tactic:
obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell (m + 1) j

Goal state after:
case a.sr.hi
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' : ∀ m_1 ≤ m, ↑m_1 < n → ∀ (j : cell C m_1), cellFrontier m_1 j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j
hm : ↑(m + 1) < n
j : cell C (m + 1)
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier (m + 1) j ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell m_1 j
⊢ cellFrontier (m + 1) j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : CWComplex C
inst✝ : T2Space X
A : Set X
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
⊢ IsClosed[t] (A ∩ ∅)

Tactic:
by simp only [inter_empty, isClosed_empty]

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

Goal state before:
pp: case hf
S : Profinite
a b : ↑S.toTop
h : (fun C ↦ decide (a ∈ ↑C)) = fun C ↦ decide (b ∈ ↑C)
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide (b ∈ C) = true

Tactic:
← congr_fun h ⟨C, hC⟩

Goal state after:
case hf
S : Profinite
a b : ↑S.toTop
h : (fun C ↦ decide (a ∈ ↑C)) = fun C ↦ decide (b ∈ ↑C)
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide (a ∈ ↑⟨C, hC⟩) = true
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
hEC : E ⊆ C
n : ℕ
x✝² : 0 < n
j : cell C n
h : j ∉ I n
x✝¹ : ℕ
x✝ : ↑(I x✝¹)
⊢ ⟨x✝¹, ↑x✝⟩ ≠ ⟨n, j⟩

Tactic:
by aesop

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
⊢ ⋃ n,
      ⋃ j,
        ↑(match n, j with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => PEmpty.elim i) ''
          closedBall 0 1 =
    D

Tactic:
by
    apply subset_antisymm (iUnion₂_subset_iff.mpr fun n ↦ by cases n <;> simp)
    intro x xD
    simp only [mem_iUnion, mem_image, mem_closedBall, dist_zero_right]
    refine ⟨0, ?_⟩
    simpa [-Matrix.zero_empty]

Goal state after: