mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: case zero
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung)^[n] b ≠ 0
ha0 : (⇑verschiebung)^[0] a ≠ 0
hab : ↑p = (⇑verschiebung)^[0] a * (⇑verschiebung)^[n] b
⊢ IsUnit ((⇑verschiebung)^[0] a) ∨ IsUnit ((⇑verschiebung)^[n] b)

Tactic:
exact Or.inl (isUnit_of_coeff_zero_ne_zero a ha)

Goal state after:
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ (n + 1) * wittMul p (n + 1) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
            ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
          ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
        remainder p n -
      wittPolyProdRemainder p (n + 1)

Tactic:
eq_sub_iff_add_eq,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ (n + 1) * wittMul p (n + 1) + wittPolyProdRemainder p (n + 1) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
      remainder p n
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ (n + 1) * wittMul p (n + 1) + ↑p ^ (n + 1) * (↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    ↑p ^ (n + 1) * (X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) +
      (↑p ^ (n + 1) * (X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))

Tactic:
mul_polyOfInterest_aux4 p n

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
            ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
          ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
        (remainder p n - wittPolyProdRemainder p (n + 1)) +
      ↑p ^ (n + 1) * (↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    ↑p ^ (n + 1) * (X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) +
      (↑p ^ (n + 1) * (X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

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

Tactic:
induction a using WellFoundedLT.induction with | ind i IH

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
⊢ lfpApprox f x i ≤ lfpApprox g x i
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

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

Tactic:
induction a using WellFoundedLT.induction with | ind i IH

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
⊢ lfpApprox f x₁ i ≤ lfpApprox f x₂ i
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
⊢ sizeOf ⟨b, a⟩ < 1 + 1 + sizeOf a + sizeOf l₁

Tactic:
by simp [sizeof_pos]

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
⊢ sizeOf ⟨b✝, b⟩ < 1 + 1 + sizeOf b + sizeOf l₂

Tactic:
by simp [sizeof_pos]

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

Goal state before:
pp: b : Ordinal.{u_1}
⊢ coeff b 0 = 0

Tactic:
ext e

Goal state after:
b e : Ordinal.{u_1}
⊢ (coeff b 0) e = 0 e
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: u : ZFSet.{u_1}
⊢ u = ∅ ∨ u.Nonempty

Tactic:
eq_empty,

Goal state after:
u : ZFSet.{u_1}
⊢ (∀ (y : ZFSet.{u_1}), y ∉ u) ∨ u.Nonempty
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{u, v} (⋃ (i : α), f i).card ≤ sum fun i ↦ (f i).card

Tactic:
rw [← lift_le.{max u (v + 1)}, lift_umax.{max u v, v + 1}]
  simpa [cardinalMk_coe_sort, ← coe_iUnion, -mem_iUnion] using
    mk_iUnion_le_sum_mk_lift (f := SetLike.coe ∘ f)

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

Goal state before:
pp: n✝ : ZFSet.{u}
x : PSet.{u}
x✝ : ⟦x⟧ ∈ omega
n : ℕ
h : x.Equiv (PSet.omega.Func { down := n })
⊢ insert (mk x) (mk x) = insert (mk (ofNat n)) (mk (ofNat n))

Tactic:
ZFSet.sound h

Goal state after:
n✝ : ZFSet.{u}
x : PSet.{u}
x✝ : ⟦x⟧ ∈ omega
n : ℕ
h : x.Equiv (PSet.omega.Func { down := n })
⊢ insert (mk (PSet.omega.Func { down := n })) (mk (PSet.omega.Func { down := n })) =
    insert (mk (ofNat n)) (mk (ofNat n))
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: ⊢ ∀ (a : Class.{u}), Acc (fun x1 x2 ↦ x1 ∈ x2) a

Tactic:
by
    have H : ∀ x : ZFSet.{u}, @Acc Class.{u} (· ∈ ·) ↑x := by
      refine fun a => ZFSet.inductionOn a fun x IH => ⟨_, ?_⟩
      rintro A ⟨z, rfl, hz⟩
      exact IH z hz
    refine fun A => ⟨A, ?_⟩
    rintro B ⟨x, rfl, _⟩
    exact H x

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

Goal state before:
pp: x : ZFSet.{u}
h : x.IsOrdinal
⊢ ∀ {a b : ↥x},
    Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) a b ∨ a = b ∨ Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) b a

Tactic:
intro ⟨a, ha⟩

Goal state after:
x : ZFSet.{u}
h : x.IsOrdinal
a : ZFSet.{u}
ha : a ∈ x
⊢ ∀ {b : ↥x},
    Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) ⟨a, ha⟩ b ∨
      ⟨a, ha⟩ = b ∨ Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) b ⟨a, ha⟩
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u}
⊢ (V_ o).card = preBeth o

Tactic:
induction o using Ordinal.limitRecOn with
  | zero => simp
  | add_one o ih => simp [ih]
  | limit o ho ih =>
    simp_rw [preBeth_limit ho.isSuccPrelimit, ← fun i : Set.Iio o => ih i i.2,
      vonNeumann_of_isSuccPrelimit ho.isSuccPrelimit]
    apply iSup_card_le_card_iUnion.antisymm'
    rw [← lift_le.{u + 1}]
    apply lift_card_iUnion_le_sum_card.trans
    refine (sum_eq_lift_iSup_of_lift_mk_le_lift_iSup ?_ ?_).le
    · rw [mk_Iio_ordinal, ← lift_aleph0.{u + 1, u}, lift_le, Ordinal.aleph0_le_card]
      exact Ordinal.omega0_le_of_isSuccLimit ho
    · rw [mk_Iio_ordinal, lift_lift, lift_le]
      by_contra! h
      refine (⨆ i : Set.Iio o, (V_ ↑i).card).card_ord.not_lt <|
        (Ordinal.card_le_card_vonNeumann _).trans_lt <| (cantor _).trans_le ?_
      rw [← card_powerset, ← vonNeumann_add_one]
      refine le_ciSup bddAbove_of_small (⟨_, ho.succ_lt ?_⟩ : Set.Iio o)
      exact (ord_card_le _).trans_lt' (ord_strictMono h)

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

Goal state before:
pp: case neg
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr

Tactic:
simp only [repr]
      have := h₁.fst
      have := h₂.fst
      simp only [Mul.mul, mul, e0, ite_false, repr.eq_2, repr_add, opow_add, IH, repr, mul_add]
      rw [← mul_assoc]
      congr 2
      have := mt repr_inj.1 e0
      rw [add_mul_of_isSuccLimit ao (isSuccLimit_opow_left isSuccLimit_omega0 this), mul_assoc,
        mul_omega0_dvd (Nat.cast_pos'.2 n₁.pos) (natCast_lt_omega0 _)]
      simpa using! opow_dvd_opow ω (one_le_iff_ne_zero.2 this)

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

Goal state before:
pp: case pos
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : e = 0
p : 0 = o' ∧ ↑n = m
⊢ 0 = scale 1 o' ∧ ↑n = m

pp: case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m
⊢ e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Tactic:
· rcases p with ⟨rfl, rfl⟩
      exact ⟨rfl, rfl⟩

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

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

pp: 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)

Tactic:
· simp_rw [scale_eq_mul]
      simp [Mul.mul, mul, e0, h.zero_of_zero,
        show x + 0 = x from repr_inj.1 (by simp)]

Goal state after:
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.SetTheory.Ordinal.Notation

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

Tactic:
obtain ⟨s₁, s₂⟩ := nf_repr_split' e

Goal state after:
o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + ↑n
⊢ o'.NF ∧ o.repr = o'.repr + ↑m
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
⊢ (f * g) =o[atTop] (b ^ exp)

Tactic:
specialize hg (g_exp + ε) (by dsimp [ε]; linarith)

Goal state after:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hg : g =o[atTop] (b ^ (g_exp + ε))
hf : f =o[atTop] (b ^ (f_exp + ε))
⊢ (f * g) =o[atTop] (b ^ exp)
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 : ℕ
t : Stream' (Option α)
hn : t n = none
hts : dist t s < (1 / 2) ^ (n + 1)
ht : t ∈ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
⊢ t (n + 1) = none

Tactic:
exact ht hn

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

Goal state before:
pp: case neg
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
⊢ dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t

Tactic:
have h' : cons x s ≠ cons x t := by
    simpa

Goal state after:
case neg
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
⊢ dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t
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_eq : g =ᶠ[atTop] f
h_approx : g =ᶠ[atTop] 0
⊢ f =ᶠ[atTop] 0

Tactic:
← 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
⊢ g =ᶠ[atTop] 0
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inl.some.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
e' : m.natPred = 0
this : 0 < ω ^ a'.repr
i : ℕ
⊢ ω ^ a'.repr * (↑i + 1) < ω ^ a'.repr * ω

Tactic:
← Nat.cast_add_one

Goal state after:
case oadd.inl.none.inl.some.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
e' : m.natPred = 0
this : 0 < ω ^ a'.repr
i : ℕ
⊢ ω ^ a'.repr * ↑(i + 1) < ω ^ a'.repr * ω
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inl.some.succ.refine_1
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
⊢ ω ^ a'.repr * (↑i + 1) < ω ^ a'.repr * ω

Tactic:
← Nat.cast_add_one

Goal state after:
case oadd.inl.none.inl.some.succ.refine_1
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
⊢ ω ^ a'.repr * ↑(i + 1) < ω ^ a'.repr * ω
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
h : o.fundamentalSequence = Sum.inl none
⊢ o.fastGrowing = Nat.succ

Tactic:
by
  rw [fastGrowing_def h]

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

Goal state before:
pp: o a : ONote
h : o.fundamentalSequence = Sum.inl (some a)
⊢ o.fastGrowing = fun i ↦ a.fastGrowing^[i] i

Tactic:
by
  rw [fastGrowing_def h]

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

Goal state before:
pp: o : ONote
f : ℕ → ONote
h : o.fundamentalSequence = Sum.inr f
⊢ o.fastGrowing = fun i ↦ (f i).fastGrowing i

Tactic:
by
  rw [fastGrowing_def h]

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
x' : ℤ := q.num
h : ↑a / ↑b = (↑x' / ↑q.den) ^ d
⊢ False

Tactic:
set y := q.den

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
⊢ False
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ ∀ (x_1 : α), (x, x_1) ∉ xs.zip ys

Tactic:
intro y hy

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
y : α
hy : (x, y) ∈ xs.zip ys
⊢ False
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 : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ some x = some y

Tactic:
← hx,

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ xs[i]? = some y
Module: Mathlib.Topology.Algebra.MvPolynomial

Goal state before:
pp: X : Type u_1
σ : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CommSemiring X
inst✝ : IsTopologicalSemiring X
p : MvPolynomial σ X
⊢ Continuous fun x ↦ (eval x) p

Tactic:
by
  continuity

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Sphere

Goal state before:
pp: n : ℕ
⊢ Function.Injective ⇑(ConcreteCategory.hom (diskBoundaryInclusion n))

Tactic:
intro ⟨x, hx⟩ ⟨y, hy⟩ h

Goal state after:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : x ∈ Metric.sphere 0 1
y : EuclideanSpace ℝ (Fin n)
hy : y ∈ Metric.sphere 0 1
h :
  (ConcreteCategory.hom (diskBoundaryInclusion n)) { down := ⟨x, hx⟩ } =
    (ConcreteCategory.hom (diskBoundaryInclusion n)) { down := ⟨y, hy⟩ }
⊢ { down := ⟨x, hx⟩ } = { down := ⟨y, hy⟩ }
Module: Mathlib.Topology.Category.TopCat.Sphere

Goal state before:
pp: n : ℕ
⊢ Function.Injective ⇑(ConcreteCategory.hom (ballInclusion n))

Tactic:
intro ⟨x, hx⟩ ⟨y, hy⟩ h

Goal state after:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : x ∈ Metric.ball 0 1
y : EuclideanSpace ℝ (Fin n)
hy : y ∈ Metric.ball 0 1
h :
  (ConcreteCategory.hom (ballInclusion n)) { down := ⟨x, hx⟩ } =
    (ConcreteCategory.hom (ballInclusion n)) { down := ⟨y, hy⟩ }
⊢ { down := ⟨x, hx⟩ } = { down := ⟨y, hy⟩ }
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
⊢ AccPt (f x) (Filter.map f F)

Tactic:
apply map_neBot (m := f) (hf := h) |>.mono
  rw [Filter.map_inf hf2]
  gcongr
  apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hf1.continuousWithinAt
  simpa [hf2.eq_iff] using! eventually_mem_nhdsWithin

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
inst✝ : IsGeneratedBy X Y
U : Set Y
⊢ IsOpen[tY] U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen[inst✝¹ i] (⇑f ⁻¹' U)

Tactic:
by
  simp [← (homeomorph (X := X)).isQuotientMap.isOpen_preimage,
    WithGeneratedByTopology.isOpen_iff]

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
g : Y → Z
hg : Continuous[tY, inst✝¹] g
⊢ Continuous[tY, _] (⇑WithGeneratedByTopology.equiv.symm ∘ g)

Tactic:
rw [continuous_iff (X := X)]

Goal state after:
ι : 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
g : Y → Z
hg : Continuous[tY, inst✝¹] g
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f)
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 : Continuous[inst✝¹, inst✝] g
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, inst✝] (g ∘ ⇑f)

Tactic:
exact fun _ f ↦ hg.comp f.continuous

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

Goal state before:
pp: case tr
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
l : ℕ
hl : l < m + 1
i : cell C l
x✝ : i ∈ I l
⊢ openCell l i ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j

Tactic:
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.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
⊢ Function.Injective (eval C)

Tactic:
intro ⟨a, ha⟩

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
⊢ ∀ ⦃a₂ : { l // Products.isGood C l }⦄, eval C ⟨a, ha⟩ = eval C a₂ → ⟨a, ha⟩ = 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}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ IsClosed (C0 C ho)

Tactic:
refine hC.inter ?_

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ IsClosed {f | f (term I ho) = false}
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}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ IsClosed (C1 C ho)

Tactic:
refine hC.inter ?_

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ IsClosed {f | f (term I ho) = true}
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
g : LocallyConstant ↑(π C fun x ↦ ord I x < o₁) ℤ
hg : g ∈ range (π C fun x ↦ ord I x < o₁)
⊢ (πs C o₁) g ∈ smaller C o₂

Tactic:
simp only [smaller, Set.mem_image]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
g : LocallyConstant ↑(π C fun x ↦ ord I x < o₁) ℤ
hg : g ∈ range (π C fun x ↦ ord I x < o₁)
⊢ ∃ x ∈ range (π C fun x ↦ ord I x < o₂), (πs C o₂) x = (πs C o₁) g
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
⊢ ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o ∧
    isGood (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l

Tactic:
refine ⟨hslt, fun he ↦ h ?_⟩

Goal state after:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
⊢ eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (eval (π C fun x ↦ ord I x < o) '' {m | m < l})
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : (completionFunctor.obj X').α
⊢ ↑(ConcreteCategory.hom
          ({ toFun := fun f ↦ X'.completionHom ≫ f.hom, invFun := fun f ↦ extensionHom f, left_inv := ⋯,
                right_inv := ⋯ }.symm
            (f ≫ g)))
      x =
    ↑(ConcreteCategory.hom
          (completionFunctor.map f ≫
            { toFun := fun f ↦ X.completionHom ≫ f.hom, invFun := fun f ↦ extensionHom f, left_inv := ⋯,
                  right_inv := ⋯ }.symm
              g))
      x

Tactic:
dsimp [-Function.comp_apply]

Goal state after:
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : (completionFunctor.obj X').α
⊢ ↑(ConcreteCategory.hom (extensionHom (f ≫ g))) x =
    (⇑(ConcreteCategory.hom (extensionHom g)) ∘ ⇑(ConcreteCategory.hom (completionFunctor.map f))) x
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 : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ ∀ (i : ℕ), ↑i < n → ∀ (i_2 : cell C i), Disjoint (openCell i i_2) (openCell m j)

Tactic:
intro l hln i

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
l : ℕ
hln : ↑l < n
i : cell C l
⊢ Disjoint (openCell l i) (openCell m j)