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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ X.degree + 0 < ↑p

pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ a₂.coeff 0 ^ p ^ (n + 1) ≠ 0

Tactic:
degree_X,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ 1 + 0 < ↑p

p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ a₂.coeff 0 ^ p ^ (n + 1) ≠ 0
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:
← add_sub_assoc,

Goal state after:
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)
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ let l' := ⋯ ▸ l;
  ofList l'.toList = l'

Tactic:
by
    induction l with
    | atom => cases h
    | nil => simp
    | cons' b a _ IH => simpa [cons] using IH rfl

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true) (l' : Lists α), l' ∈ l.toList → trans l'

Tactic:
apply inductionMut

Goal state after:
case C0
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : α), trans (atom a)

case C1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l : Lists' α true), (∀ (l' : Lists α), l' ∈ l.toList → trans l') → trans (of' l)

case D0
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l' : Lists α), l' ∈ Lists'.nil.toList → trans l'

case D1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : Lists α) (l : Lists' α true),
    trans a → (∀ (l' : Lists α), l' ∈ l.toList → trans l') → ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
⊢ e.NF

Tactic:
obtain - | ⟨h₁, h₂, h₃⟩ := h

Goal state after:
case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ e.NF
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
⊢ a.NFBelow e.repr

Tactic:
obtain - | ⟨h₁, h₂, h₃⟩ := h

Goal state after:
case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ a.NFBelow e.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
⊢ e.repr < b

Tactic:
obtain - | ⟨h₁, h₂, h₃⟩ := h

Goal state after:
case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ e.repr < b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
H : e.repr < b
b' : Ordinal.{0}
h : (e.oadd n a).NFBelow b'
⊢ (e.oadd n a).NFBelow b

Tactic:
obtain - | ⟨h₁, h₂, h₃⟩ := h

Goal state after:
case oadd'
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
H : e.repr < b
b' eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b'
⊢ (e.oadd n a).NFBelow b
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ IsNormal (veblenWith f o)

Tactic:
by
  obtain rfl | h := eq_or_ne o 0
  · rwa [veblenWith_zero]
  · exact isNormal_veblenWith' f h

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

Goal state before:
pp: case oadd.lt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.lt
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b

Tactic:
dsimp [addAux]

Goal state after:
case oadd.lt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.lt
⊢ (match e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')).NFBelow
    b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b

Tactic:
dsimp [addAux]

Goal state after:
case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
⊢ (match e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')).NFBelow
    b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.gt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b

Tactic:
dsimp [addAux]

Goal state after:
case oadd.gt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
⊢ (match e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')).NFBelow
    b
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, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)

Tactic:
let ⟨b, hb⟩ := αβ a

Goal state after:
α β : 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)
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: A : Class.{u_1}
hA : A.powerset ⊆ A
⊢ ∀ (x : ZFSet.{u_1}), A x

Tactic:
by_contra! hnA
      exact
        WellFounded.min_mem ZFSet.mem_wf _ hnA
          (hA fun x hx =>
            Classical.not_not.1 fun hB =>
              WellFounded.not_lt_min ZFSet.mem_wf _ hB <| coe_apply.1 hx)

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

Goal state before:
pp: o : Ordinal.{u}
x : ZFSet.{u}
⊢ x ∈ V_ o ↔ x.rank < o

Tactic:
by
  simp_rw [mem_vonNeumann', subset_vonNeumann]
  exact ⟨fun ⟨a, h₁, h₂⟩ ↦ h₂.trans_lt h₁, by aesop⟩

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

Goal state before:
pp: case neg.refine_2
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ω ^ e.repr = ω ^ 1 * ω ^ (e.repr - 1)
⊢ ω ^ e.repr * ↑↑n + (ω * a'.repr + ↑m') = ω * ((e - 1).oadd n a').repr + ↑m'

Tactic:
rw [this]
        simp [mul_add, mul_assoc, add_assoc]

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

Goal state before:
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
⊢ o'.NF ∧ ω ^ e.repr * ↑↑n + a.repr = ω * o'.repr + ↑m

Tactic:
· revert p
      rcases h' : split' a with ⟨a', m'⟩
      have := h.fst
      have := h.snd
      obtain ⟨IH₁, IH₂⟩ := nf_repr_split' h'
      simp only [IH₂, and_imp]
      intros
      subst o' m
      have : (ω : Ordinal.{0}) ^ repr e = ω ^ (1 : Ordinal.{0}) * ω ^ (repr e - 1) := by
        have := mt repr_inj.1 e0
        rw [← opow_add, Ordinal.add_sub_cancel_of_le (one_le_iff_ne_zero.2 this)]
      refine ⟨NF.oadd (by infer_instance) _ ?_, ?_⟩
      · simp only [opow_one, repr_sub, repr_one, Nat.cast_one] at this ⊢
        refine IH₁.below_of_lt' <| (mul_lt_mul_iff_right₀ omega0_pos).1 <|
          (le_self_add (α := Ordinal) (b := m')).trans_lt ?_
        rw [← this, ← IH₂]
        exact h.snd'.repr_lt
      · rw [this]
        simp [mul_add, mul_assoc, add_assoc]

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

Goal state before:
pp: f b : ℝ → ℝ
exp : ℝ
h_lt : exp < 0
h : Majorized f b exp
⊢ Tendsto f atTop (𝓝 0)

Tactic:
by
  simpa [Pi.pow_def, Majorized] using h 0 (by linarith)

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

Goal state before:
pp: case neg.h
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ∃ n, ↑m.succ = ↑n

Tactic:
exact ⟨_, rfl⟩

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

Goal state before:
pp: case cons
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
n : Fin (basis_hd :: basis_tl).length
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ (monomialRpow (basis_hd :: basis_tl) (↑n) r).Approximates

Tactic:
simp only [List.length_cons, monomialRpow, Fin.is_lt, getElem!_pos]
    cases n using Fin.cases with
    | zero =>
      simp only [Fin.coe_ofNat_eq_mod, Nat.zero_mod, Multiseries.monomialRpow,
        List.getElem_cons_zero]
      apply (one_approximates h_basis.tail).cons _ (by simp)
      exact Majorized.self <| h_basis.tendsto_atTop (by simp)
    | succ m =>
      simp only [Fin.val_succ, Multiseries.monomialRpow, List.getElem_cons_succ]
      apply (monomialRpow_approximates h_basis.tail).cons _ (by simp)
      apply h_basis.tail_pow_majorized_head (by simp)

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

Goal state before:
pp: ⊢ ¬FirstNonzeroIsPos []

Tactic:
simp [FirstNonzeroIsPos, sign]

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

Goal state before:
pp: case cons
m : UnitMonomial
right : Basis
left_hd : ℝ → ℝ
left_tl : List (ℝ → ℝ)
ih : (List.replicate left_tl.length 0 ++ m).toFun (left_tl ++ right) = m.toFun right
⊢ (List.replicate (left_hd :: left_tl).length 0 ++ m).toFun (left_hd :: left_tl ++ right) = m.toFun right

Tactic:
simp [List.replicate_succ, ih]

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

Goal state before:
pp: case cons.cons.cons.cons
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
h1 : (exp1 :: m1).length = (basis_hd :: basis_tl).length
m2 : List ℝ
h2 : (exp1 :: m2).length = (basis_hd :: basis_tl).length
h : List.Lex (fun x1 x2 ↦ x1 < x2) m1 m2
⊢ (basis_hd ^ exp1 * toFun m1 basis_tl) =o[atTop] (basis_hd ^ exp1 * toFun m2 basis_tl)

Tactic:
apply IsBigO.mul_isLittleO (isBigO_refl _ _)

Goal state after:
case cons.cons.cons.cons
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
h1 : (exp1 :: m1).length = (basis_hd :: basis_tl).length
m2 : List ℝ
h2 : (exp1 :: m2).length = (basis_hd :: basis_tl).length
h : List.Lex (fun x1 x2 ↦ x1 < x2) m1 m2
⊢ toFun m1 basis_tl =o[atTop] toFun m2 basis_tl
Module: Mathlib.Tactic.DeriveCountable

Goal state before:
pp: p : Prop
a b a' b' : ℕ
h : a = a' → b = b' → p
⊢ a = a' ∧ b = b' → p

Tactic:
and_imp

Goal state after:
p : Prop
a b a' b' : ℕ
h : a = a' → b = b' → p
⊢ a = a' → b = b' → p
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
h : y_den ≤ 0
⊢ False

Tactic:
simp only [nonpos_iff_eq_zero] at h

Goal state after:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
h : y_den = 0
⊢ False
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
h₃ : (x, val) ∈ xs.zip ys
⊢ val ∈ ys

Tactic:
apply (List.of_mem_zip h₃).2

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✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α)

Tactic:
rcases comp_comp_symm_mem_uniformity_sets hU with ⟨V, hV, Vsymm, hVU⟩

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
⊢ Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α)
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
⊢ Injective (List.applyId (xs.zip ys))

Tactic:
intro x y h

Goal state after:
α : 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
⊢ x = y
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module S E
inst✝⁴ : Module S E'
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : ContinuousAdd F
f : M → E
g g' : M → E'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f g'
⊢ f ⋆[L] (g + g') = f ⋆[L] g + f ⋆[L] g'

Tactic:
ext x; exact (hfg x).distrib_add L (hfg' x)

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 ∈ Vn n
h2 : x * x ∈ Vn n
⊢ x ∈ Vn (n + 1)

Tactic:
hVn

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)
⊢ |(↑x).arg| < π / 2 ^ (n + 1 + 1)
Module: Mathlib.Topology.Category.TopCat.Sphere

Goal state before:
pp: n : ℕ
t : Set (ULift.{?u.17, 0} ↑(Metric.closedBall 0 1))
x✝ : IsOpen t
s : Set ↑(Metric.closedBall 0 1)
r : Set (EuclideanSpace ℝ (Fin n))
hro : IsOpen r
hrs : Subtype.val ⁻¹' r = s
hst : ULift.down ⁻¹' s = t
⊢ IsOpen
    ((fun x ↦
        match x with
        | { down := ⟨p, hp⟩ } => { down := ⟨p, ⋯⟩ }) ⁻¹'
      t)

Tactic:
isOpen_induced_iff,

Goal state after:
n : ℕ
t : Set (ULift.{?u.17, 0} ↑(Metric.closedBall 0 1))
x✝ : IsOpen t
s : Set ↑(Metric.closedBall 0 1)
r : Set (EuclideanSpace ℝ (Fin n))
hro : IsOpen r
hrs : Subtype.val ⁻¹' r = s
hst : ULift.down ⁻¹' s = t
⊢ ∃ t_1,
    IsOpen t_1 ∧
      ULift.down ⁻¹' t_1 =
        (fun x ↦
            match x with
            | { down := ⟨p, hp⟩ } => { down := ⟨p, ⋯⟩ }) ⁻¹'
          t
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 : Finite C
x✝ : ∀ (n : ℕ), _root_.Finite (cell C n)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → IsEmpty (cell C b)
this : ∀ (m : ℕ) (j : cell C m), m < n
⊢ Function.LeftInverse
    (fun x ↦
      match x with
      | ⟨m, j⟩ => ⟨⟨m, ⋯⟩, j⟩)
    fun x ↦
    match x with
    | ⟨m, j⟩ => ⟨↑m, j⟩

Tactic:
by simp [Function.LeftInverse]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : RelCWComplex C ∅
⊢ ∀ (n : ℕ) (i : cell C n),
    ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)

Tactic:
simpa using mapsTo (C := C)

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
asubc : A ⊆ C
⊢ IsClosed[t] A → (∀ (n : ℕ) (j : cell C n), IsClosed[t] (A ∩ closedCell n j)) ∧ IsClosed[t] (A ∩ D)

Tactic:
exact fun closedA ↦ ⟨fun _ _ ↦ closedA.inter isClosed_closedCell, closedA.inter (isClosedBase C)⟩

Goal state after:
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
⊢ Injective (closedCell 0)

Tactic:
intro x y h

Goal state after:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x y : cell C 0
h : closedCell 0 x = closedCell 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) ![] = ↑(map 0 y) ![]
⊢ x = y

Tactic:
exact injective_map_zero C h

Goal state after:
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
⊢ Injective (openCell 0)

Tactic:
intro x y h

Goal state after:
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
Module: Mathlib.Topology.CWComplex.Classical.Basic

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

Tactic:
apply union_subset subset_union_left
    refine iUnion₂_subset fun m hm ↦ iUnion_subset fun j ↦ ?_
    rw [← cellFrontier_union_openCell_eq_closedCell]
    apply union_subset
    · 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
    · exact subset_union_of_subset_right (subset_iUnion₂_of_subset m hm (subset_iUnion _ j)) _

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
⊢ π (π C K) J = π C J

Tactic:
by
  ext x
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · obtain ⟨y, ⟨z, hz, rfl⟩, rfl⟩ := h
    refine ⟨z, hz, (?_ : _ = (Proj J ∘ Proj K) z)⟩
    rw [proj_comp_of_subset J K h]
  · obtain ⟨y, hy, rfl⟩ := h
    dsimp [π]
    rw [← Set.image_comp]
    refine ⟨y, hy, ?_⟩
    rw [proj_comp_of_subset J K h]

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

Goal state before:
pp: X Y : Compactum
f : X ⟶ Y
⊢ ∀ (x : X.A) (g : Ultrafilter X.A),
    ↑g ≤ 𝓝 x → Tendsto (⇑(ConcreteCategory.hom f)) (↑g) (𝓝 ((ConcreteCategory.hom f) x))

Tactic:
intro x g h

Goal state after:
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ Tendsto (⇑(ConcreteCategory.hom f)) (↑g) (𝓝 ((ConcreteCategory.hom f) x))
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
i : I
⊢ Continuous fun f ↦ if ↑f i = true then 1 else 0

Tactic:
exact (continuous_of_discreteTopology (f := fun (a : Bool) ↦ (if a then (1 : ℤ) else 0))).comp
      ((continuous_apply i).comp continuous_subtype_val)

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

Goal state before:
pp: case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne : ⟨a, ha⟩ ≠ ⟨b, hb⟩
h' : ⟨a, ha⟩ < ⟨b, hb⟩
⊢ False

Tactic:
apply hb; rw [← h]; exact Submodule.subset_span ⟨a, h', rfl⟩

Goal state after: