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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ imageOfDf f ↔ x ∈ PrimeSpectrum.comap C '' (zeroLocus {f})ᶜ

Tactic:
refine ⟨fun hx => ⟨⟨map C x.asIdeal, isPrime_map_C_of_isPrime⟩, ⟨?_, ?_⟩⟩, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ { asIdeal := Ideal.map C x.asIdeal, isPrime := ⋯ } ∈ (zeroLocus {f})ᶜ

case refine_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ PrimeSpectrum.comap C { asIdeal := Ideal.map C x.asIdeal, isPrime := ⋯ } = x

case refine_3
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ PrimeSpectrum.comap C '' (zeroLocus {f})ᶜ → x ∈ imageOfDf f
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
⊢ a = b

Tactic:
have : (valuation R).IsEquiv (1 : Valuation R Γ) := isEquiv _ _

Goal state after:
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
⊢ a = b
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'
surjRS : Function.Surjective ⇑(algebraMap R S)
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
⊢ RingHom.ker ((algebraMap R' S').comp (algebraMap R R')) = RingHom.ker (algebraMap R R') ⊔ RingHom.ker (algebraMap R S)

Tactic:
← IsScalarTower.algebraMap_eq,

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'
surjRS : Function.Surjective ⇑(algebraMap R S)
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
⊢ RingHom.ker (algebraMap R S') = RingHom.ker (algebraMap R R') ⊔ RingHom.ker (algebraMap R S)
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : ZMod (p ^ m)
⊢ ((truncate hm).comp (zmodEquivTrunc p m).toRingHom) x = (zmodEquivTrunc p n) ((ZMod.castHom ⋯ (ZMod (p ^ n))) x)

Tactic:
rw [commutes _ _ hm]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : ZMod (p ^ m)
⊢ ((zmodEquivTrunc p n).toRingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ n)))) x =
    (zmodEquivTrunc p n) ((ZMod.castHom ⋯ (ZMod (p ^ n))) x)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
s : Set α
inst✝ : LinearOrder α
hs : ¬IsCofinal sᶜ
⊢ IsStationary s

Tactic:
intro t ht
  obtain ⟨a, ha⟩ := not_isCofinal_iff.1 hs
  obtain ⟨b, hb, hb'⟩ := ht.isCofinal a
  refine ⟨b, ?_, hb⟩
  contrapose! ha
  exact ⟨b, ha, hb'⟩

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

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
ι : Sort u_1
f : ι → Set α
hα : cof α ≤ 1
⊢ IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i)

Tactic:
rw [← sUnion_range, isStationary_sUnion_iff_of_cof_le_one hα]
  simp

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

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Tactic:
by
  refine CNF.rec b ?_ ?_ o
  · rw [zero_right, foldr_nil]
  · intro o ho IH
    rw [CNF.ne_zero ho, foldr_cons, IH, div_add_mod]

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
⊢ cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
by
  refine ⟨fun h => ?_, fun ⟨⟨a', m, e⟩, s⟩ => Subset.cons e m s⟩
  generalize h' : Lists'.cons a l₁ = l₁' at h
  obtain - | @⟨a', _, _, _, e, m, s⟩ := h
  · cases a
    cases h'
  cases a; cases a'; cases h'; exact ⟨⟨_, m, e⟩, s⟩

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

Goal state before:
pp: case refine_1
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : lfpApprox f x (0 + 1) = x
⊢ f x = x

Tactic:
lfpApprox_add_one f hx,

Goal state after:
case refine_1
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : f (lfpApprox f x 0) = x
⊢ f x = x
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
⊢ lfpApprox f x (succ #α).ord ∈ fixedPoints ⇑f

Tactic:
let ⟨a, ha, b, hb, hne, hf⟩ := exists_lfpApprox_eq_lfpApprox f x
  cases le_total a b with
  | inl hab => exact lfpApprox_mem_fixedPoints_of_eq f hx (hne.lt_of_le hab) ha.le hf
  | inr hba => exact lfpApprox_mem_fixedPoints_of_eq f hx (hne.symm.lt_of_le hba) hb.le hf.symm

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

Goal state before:
pp: case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ e✝.NFBelow ?oadd'.eb

pp: case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ a✝.NFBelow e✝.repr

pp: case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ e✝.repr < b₂

pp: case oadd'.eb
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ Ordinal.{0}

Tactic:
exacts [h₁, h₂, lt_of_lt_of_le h₃ bb]

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

Goal state before:
pp: case pos
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
e' : Ordinal.{u_1}
he' : e' ∈ f.support
⊢ f e' < b

Tactic:
apply (hf e').trans_eq'
        rw [add_apply, single_eq_of_ne, zero_add]
        exact (hf' _ he').ne

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

Goal state before:
pp: α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : (A a).Equiv (B b)
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)

Tactic:
induction ea : A a with | _ γ Γ
     =>  _ 

Goal state after:
case mk
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : (A a).Equiv (B b)
γ : Type u
Γ : γ → PSet.{u}
A_ih✝ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
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
⊢ x.scale (e.oadd n a) = x.oadd 1 0 * e.oadd n a

Tactic:
simp only [HMul.hMul]; simp only [scale]
    have := h.snd
    by_cases e0 : e = 0
    · simp_rw [scale_eq_mul]
      simp [Mul.mul, mul, e0, h.zero_of_zero,
        show x + 0 = x from repr_inj.1 (by simp)]
    · simp [e0, Mul.mul, mul, scale_eq_mul, (· * ·)]

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

Goal state before:
pp: hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ (f ^ r) =o[atTop] (hd ^ exp)

Tactic:
apply pow_isLittleO_pow_of_log

Goal state after:
case hf
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < f x

case hg
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ Tendsto hd atTop atTop

case h
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)

case hb
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ 0 < exp
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_coef : 0 < coef
h_exps : exps.FirstNonzeroIsPos
⊢ let t := { coef := coef, unit := exps };
  Tendsto (t.toFun basis) atTop atTop

Tactic:
by
  intro t
  eta_expand
  simp only [toFun, Pi.smul_apply, smul_eq_mul]
  convert Filter.Tendsto.const_mul_atTop h_coef
    (UnitMonomial.toFun_tendsto_top_of_firstNonzeroIsPos h_basis h_length h_exps)

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

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

Tactic:
by
  by_cases hb_zero : b = 0
  · subst hb_zero
    contrapose! ha
    simp only [Nat.coprime_zero_right] at h_coprime
    subst h_coprime
    use 1
    simp
  by_contra! h
  rw [← Rat.num_div_den q] at h
  set x' := q.num
  set y := q.den
  obtain ⟨x, hx'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ x' by rwa [Rat.num_nonneg])
  rw [hx'] at h
  specialize ha x
  simp only [Int.cast_natCast, div_pow] at h
  rw [div_eq_div_iff] at h
  rotate_left
  · simpa
  · simp [y]
  replace h : a * y ^ d = x ^ d * b := by
    qify
    assumption
  apply ha
  conv at h => rhs; rw [mul_comm]
  apply eq_of_mul_eq_mul_of_coprime h_coprime _ h
  apply Nat.Coprime.pow_left
  apply Nat.Coprime.pow_right
  apply Nat.Coprime.symm
  simpa [hx'] using (show x'.natAbs.Coprime y from Rat.reduced q)

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

Goal state before:
pp: case e_opt
α : Type u
β : Type v
inst✝ : DecidableEq α
m : List ((_ : α) × β)
y : β
x : α
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m

Tactic:
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.Testing.Plausible.Functions

Goal state before:
pp: case cons.zero
α : Type u
inst✝ : DecidableEq α
y x' : α
xs ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
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)
⊢ applyId ((x' :: xs).zip ys) x' = y ↔ ys[0]? = some y

Tactic:
cases ys

Goal state after:
case cons.zero.nil
α : Type u
inst✝ : DecidableEq α
y x' : α
xs : List α
h₀ : (x' :: xs).Nodup
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)
h₁ : (x' :: xs).length = [].length
⊢ applyId ((x' :: xs).zip []) x' = y ↔ [][0]? = some y

case cons.zero.cons
α : Type u
inst✝ : DecidableEq α
y x' : α
xs : List α
h₀ : (x' :: xs).Nodup
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)
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x' = y ↔ (head✝ :: tail✝)[0]? = some y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.succ
α : 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)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[n✝ + 1]? = some y

Tactic:
cases ys

Goal state after:
case cons.succ.nil
α : 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)
h₀ : (x' :: xs).Nodup
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
h₁ : (x' :: xs).length = [].length
⊢ applyId ((x' :: xs).zip []) x = y ↔ [][n✝ + 1]? = some y

case cons.succ.cons
α : 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)
h₀ : (x' :: xs).Nodup
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x = y ↔ (head✝ :: tail✝)[n✝ + 1]? = some y
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : UniformSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ IsUniformInducing (⇑UniformFun.ofFun ∘ F) ↔ IsUniformInducing F

Tactic:
rw [isUniformInducing_iff_uniformSpace, isUniformInducing_iff_uniformSpace,
      ← F_eqcont.comap_uniformFun_eq]
  rfl

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ IsInducing (⇑UniformFun.ofFun ∘ F) ↔ IsInducing F

Tactic:
rw [isInducing_iff, isInducing_iff]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ inst✝¹ = TopologicalSpace.induced (⇑UniformFun.ofFun ∘ F) (UniformFun.topologicalSpace X α) ↔
    inst✝¹ = TopologicalSpace.induced F Pi.topologicalSpace
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : List.applyId (xs.zip ys) x ∈ ys
hy : List.applyId (xs.zip ys) y ∉ ys
⊢ x = y

Tactic:
rw [h] at hx

Goal state after:
case neg
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : List.applyId (xs.zip ys) y ∈ ys
hy : List.applyId (xs.zip ys) y ∉ ys
⊢ x = y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : List.applyId (xs.zip ys) x ∉ ys
hy : List.applyId (xs.zip ys) y ∈ ys
⊢ x = y

Tactic:
rw [h] at hx

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : List.applyId (xs.zip ys) y ∉ ys
hy : List.applyId (xs.zip ys) y ∈ ys
⊢ x = y
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsInducing ((⋃₀ 𝔖).domRestrict ∘ F)

Tactic:
rw [isInducing_iff, isInducing_iff]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ inst✝ = TopologicalSpace.induced (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (UniformOnFun.topologicalSpace X α 𝔖) ↔
    inst✝ = TopologicalSpace.induced ((⋃₀ 𝔖).domRestrict ∘ F) Pi.topologicalSpace
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
⊢ [MapClusterPt x atTop fun x ↦ y ^ x, MapClusterPt x atTop fun x ↦ y ^ x, x ∈ closure[inst✝²] (range fun x ↦ y ^ x),
      x ∈ closure[inst✝²] (range fun x ↦ y ^ x)].TFAE

Tactic:
tfae_have 2 ↔ 1 := mapClusterPt_atTop_zpow_iff_pow

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x ↦ y ^ x) ↔ MapClusterPt x atTop fun x ↦ y ^ x
⊢ [MapClusterPt x atTop fun x ↦ y ^ x, MapClusterPt x atTop fun x ↦ y ^ x, x ∈ closure[inst✝²] (range fun x ↦ y ^ x),
      x ∈ closure[inst✝²] (range fun x ↦ y ^ x)].TFAE
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous[inst✝¹, inst✝] f
ho : IsOpenMap f
⊢ {t | IsOpen[inst✝] t ∧ Dense t} ⊆ (map f (residual α)).sets

Tactic:
rintro t ⟨ht, htd⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous[inst✝¹, inst✝] f
ho : IsOpenMap f
t : Set β
ht : IsOpen[inst✝] t
htd : Dense t
⊢ t ∈ (map f (residual α)).sets
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: case h
X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : _root_.Finite ((n : ℕ) × cell C n)
h✝ : Nonempty ((n : ℕ) × cell C n)
x✝ : Fintype ((n : ℕ) × cell C n)
A : Finset ℕ := Finset.image Sigma.fst Finset.univ
m : ℕ
a✝ : A.max' ⋯ + 1 ≤ m
h' : Nonempty (cell C m)
⊢ False

Tactic:
have hmA : m ∈ A := by
      simp only [Finset.mem_image, Finset.mem_univ, true_and, A]
      simp only [← exists_true_iff_nonempty] at h'
      obtain ⟨j, _⟩ := h'
      use ⟨m, j⟩

Goal state after:
case h
X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : _root_.Finite ((n : ℕ) × cell C n)
h✝ : Nonempty ((n : ℕ) × cell C n)
x✝ : Fintype ((n : ℕ) × cell C n)
A : Finset ℕ := Finset.image Sigma.fst Finset.univ
m : ℕ
a✝ : A.max' ⋯ + 1 ≤ m
h' : Nonempty (cell C m)
hmA : m ∈ A
⊢ False
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : _root_.Finite ((n : ℕ) × cell C n)
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell C n)

Tactic:
simp only [Filter.eventually_atTop]
    cases isEmpty_or_nonempty (Σ n, cell C n)
    · exact ⟨0, by simp_all⟩
    -- We take the greatest `n` such that there is a `j : cell C n` and show that this fulfills
    -- the necessary conditions.
    have _ := Fintype.ofFinite (Σ n, cell C n)
    let A := (Finset.univ : Finset (Σ n, cell C n)).image Sigma.fst
    use A.max' (Finset.image_nonempty.2 Finset.univ_nonempty) + 1
    intro m _
    by_contra! h'
    have hmA : m ∈ A := by
      simp only [Finset.mem_image, Finset.mem_univ, true_and, A]
      simp only [← exists_true_iff_nonempty] at h'
      obtain ⟨j, _⟩ := h'
      use ⟨m, j⟩
    linarith [A.le_max' m hmA]

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

Goal state before:
pp: X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
⊢ X.str F ∈ cl A

Tactic:
let ssu := Set (Set (Ultrafilter X))

Goal state after:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
⊢ X.str F ∈ cl A
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
g : Y → Z
hg : ContinuousGeneratedBy X g
⊢ Continuous (⇑WithGeneratedByTopology.equiv.symm ∘ g ∘ ⇑WithGeneratedByTopology.equiv)

Tactic:
by
    rwa [← continuousGeneratedBy_iff]

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

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
⊢ ↑F ≤ 𝓝 x → X.str F = x

Tactic:
let ssu := Set (Set (Ultrafilter X))

Goal state after:
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))
⊢ ↑F ≤ 𝓝 x → X.str F = x
Module: Mathlib.Topology.CWComplex.Classical.Basic

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

Tactic:
induction m using Nat.case_strong_induction_on with
      | hz => simp [cellFrontier_zero_eq_empty]
      | hi m hm' =>
        obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell (m + 1) j
        apply hI.trans
        apply union_subset subset_union_left
        apply iUnion₂_subset fun l hl ↦ iUnion₂_subset fun i _ ↦ ?_
        rw [← cellFrontier_union_openCell_eq_closedCell]
        apply union_subset
        · exact (hm' l (Nat.le_of_lt_succ hl) ((ENat.natCast_lt_natCast.2 hl).trans hm) i)
        · apply subset_union_of_subset_right
          exact subset_iUnion₂_of_subset l ((ENat.natCast_lt_natCast.2 hl).trans hm) <|
            subset_iUnion _ i

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

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
⊢ Proj (fun x ↦ ord I x < o) g i = g i

Tactic:
simp only [Proj, ite_eq_left_iff, not_lt, @eq_comm _ false, ← Bool.not_eq_true]

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
⊢ o ≤ ord I i → ¬g i = true
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case hi
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
hn : ∀ m ≤ n, ∀ (i : cell C m), ∃ I, cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ I m_1, openCell m_1 j
i : cell C (n + 1)
⊢ ∃ I, cellFrontier (n + 1) i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell m j

Tactic:
obtain ⟨J, hJ⟩ := cellFrontier_subset_base_union_finite_closedCell n.succ i

Goal state after:
case hi
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
hn : ∀ m ≤ n, ∀ (i : cell C m), ∃ I, cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ I m_1, openCell m_1 j
i : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
hJ : cellFrontier n.succ i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell m j
⊢ ∃ I, cellFrontier (n + 1) i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell m j
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: S : Profinite
C : { C // IsClopen C }
x : ↑S.toTop
⊢ x ∈ (fun a ↦ decide (a ∈ ↑C)) ⁻¹' {true} ↔ x ∈ ↑C

Tactic:
simp only [Set.mem_preimage, Set.mem_singleton_iff, decide_eq_true_eq]

Goal state after: