mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a → ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a) → ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a
⊢ [a ∈ closure s, a ∈ closure (s ∩ Iic a), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a,
      ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a, ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a].TFAE

Tactic:
tfae_have 5 → 1 := by
    rintro ⟨ι, hne, f, hfs, rfl⟩
    exact closure_mono (range_subset_iff.2 hfs) <| csSup_mem_closure (range_nonempty f)
      bddAbove_of_small

Goal state after:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a → ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a) → ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a
tfae_5_to_1 : (∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a) → a ∈ closure s
⊢ [a ∈ closure s, a ∈ closure (s ∩ Iic a), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a,
      ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a, ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a].TFAE
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
⊢ IsClosed s ↔ ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s

Tactic:
use fun hs ι hι f hf => (mem_iff_iSup_of_isClosed hs).2 ⟨ι, hι, f, hf, rfl⟩

Goal state after:
case mpr
s : Set Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s) → IsClosed s
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u_1}
h : x.Nonempty
⊢ (∀ z ∈ x, y ∈ z) → y ∈ ⋃₀ x

Tactic:
intro mem

Goal state after:
x y : ZFSet.{u_1}
h : x.Nonempty
mem : ∀ z ∈ x, y ∈ z
⊢ y ∈ ⋃₀ x
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u}
⊢ y ∈ ⋃₀ {x} ↔ y ∈ x

Tactic:
simp_rw [mem_sUnion, mem_singleton, exists_eq_left]

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

Goal state before:
pp: o : ONote
b : Ordinal.{0}
x✝ : NFBelow 0 b
h₂ : o.NF
⊢ (0 - o).NFBelow b

Tactic:
by cases o <;> exact NFBelow.zero

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

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

Tactic:
cases s <;> cases t <;> simp at h

Goal state after:
case nil.nil
α : Type u_1
h : True
⊢ dist nil nil = 2⁻¹ * dist nil.tail nil.tail

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α
h : LipschitzWith 2⁻¹ F
hF : ContractingWith 2⁻¹ F
f : β →ᵤ Stream'.Seq α := ContractingWith.fixedPoint F hF
⊢ ∃ f, Function.IsFixedPt F f

Tactic:
use f

Goal state after:
case h
α : Type u_1
β : Type u_2
F : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α
h : LipschitzWith 2⁻¹ F
hF : ContractingWith 2⁻¹ F
f : β →ᵤ Stream'.Seq α := ⋯
⊢ Function.IsFixedPt F f
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
F : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α
h : LipschitzWith 2⁻¹ F
⊢ ∃ f, Function.IsFixedPt F f

Tactic:
have hF : ContractingWith 2⁻¹ F := by
    constructor
    · norm_num
    · exact h
  let f := hF.fixedPoint _
  use f
  exact hF.fixedPoint_isFixedPt

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
⊢ ∃ f,
    ∀ (b : β),
      match F b with
      | none => f b = nil
      | some (a, c, b') => f b = Seq.cons a (op c (f b'))

Tactic:
use f

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α := ⋯
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
⊢ ∀ (b : β),
    match F b with
    | none => f b = nil
    | some (a, c, b') => f b = Seq.cons a (op c (f b'))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case hf_tendsto
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ Tendsto (Real.log ∘ (basis_hd :: basis_tl).getLast ⋯) atTop atTop

pp: case hf_comp
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ ∀ (g : ℝ → ℝ),
    (basis_hd :: basis_tl).getLast? = some g →
      (Real.log ∘ Real.log ∘ (basis_hd :: basis_tl).getLast ⋯) =o[atTop] (Real.log ∘ g)

Tactic:
· simp [Real.tendsto_log_atTop.comp, h_basis.right]

Goal state after:
case hf_comp
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ ∀ (g : ℝ → ℝ),
    (basis_hd :: basis_tl).getLast? = some g →
      (Real.log ∘ Real.log ∘ (basis_hd :: basis_tl).getLast ⋯) =o[atTop] (Real.log ∘ g)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates

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

Tactic:
grind [AllZero, sign]

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

Goal state before:
pp: case zero
⊢ AllZero (List.replicate 0 0)

Tactic:
grind [AllZero, sign]

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

Goal state before:
pp: case succ
n✝ : ℕ
a✝ : AllZero (List.replicate n✝ 0)
⊢ AllZero (List.replicate (n✝ + 1) 0)

Tactic:
grind [AllZero, sign]

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

Goal state before:
pp: case oadd.inl.none
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
e : b.fundamentalSequence = Sum.inl none
⊢ match
    match a.fundamentalSequence, m.natPred with
    | Sum.inl none, 0 => Sum.inl (some zero)
    | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
    | Sum.inl (some a'), 0 => Sum.inr fun i ↦ a'.oadd i.succPNat zero
    | Sum.inl (some a'), m.succ => Sum.inr fun i ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
    | Sum.inr f, 0 => Sum.inr fun i ↦ (f i).oadd 1 zero
    | Sum.inr f, m.succ => Sum.inr fun i ↦ a.oadd m.succPNat ((f i).oadd 1 zero) with
  | Sum.inl none => a.oadd m b = 0
  | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF)
  | Sum.inr f =>
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (f i).repr

Tactic:
rw [e, FundamentalSequenceProp] at ihb

Goal state after:
case oadd.inl.none
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e : b.fundamentalSequence = Sum.inl none
⊢ match
    match a.fundamentalSequence, m.natPred with
    | Sum.inl none, 0 => Sum.inl (some zero)
    | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
    | Sum.inl (some a'), 0 => Sum.inr fun i ↦ a'.oadd i.succPNat zero
    | Sum.inl (some a'), m.succ => Sum.inr fun i ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
    | Sum.inr f, 0 => Sum.inr fun i ↦ (f i).oadd 1 zero
    | Sum.inr f, m.succ => Sum.inr fun i ↦ a.oadd m.succPNat ((f i).oadd 1 zero) with
  | Sum.inl none => a.oadd m b = 0
  | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF)
  | Sum.inr f =>
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (f i).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.some
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
b' : ONote
e : b.fundamentalSequence = Sum.inl (some b')
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr ∧ ((a.oadd m b).NF → (a.oadd m b').NF)

Tactic:
rw [e, FundamentalSequenceProp] at ihb

Goal state after:
case oadd.inl.some
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr ∧ ((a.oadd m b).NF → (a.oadd m b').NF)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inr
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
f : ℕ → ONote
e : b.fundamentalSequence = Sum.inr f
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m (f i) < a.oadd m (f (i + 1)) ∧ a.oadd m (f i) < a.oadd m b ∧ ((a.oadd m b).NF → (a.oadd m (f i)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m (f i)).repr

Tactic:
rw [e, FundamentalSequenceProp] at ihb

Goal state after:
case oadd.inr
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
f : ℕ → ONote
ihb :
  IsSuccLimit b.repr ∧ (∀ (i : ℕ), f i < f (i + 1) ∧ f i < b ∧ (b.NF → (f i).NF)) ∧ ∀ a < b.repr, ∃ i, a < (f i).repr
e : b.fundamentalSequence = Sum.inr f
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m (f i) < a.oadd m (f (i + 1)) ∧ a.oadd m (f i) < a.oadd m b ∧ ((a.oadd m b).NF → (a.oadd m (f i)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m (f i)).repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case h_step
α : 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, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
⊢ ∃ T,
    ∀ (s : Stream'.Seq α),
      ((op ∘ opf) s).destruct =
        Option.map
          (fun x ↦
            match x with
            | (hd, op') => (hd, ↑op' s.tail))
          (T s.head)

Tactic:
use fun hd? ↦
    match (h_opf.unfold hd?) with
    | none => (T none).map fun (hd, opf', op') =>
      (hd, ⟨_, fun _ ↦ opf'.val nil, op', rfl, FriendlyOperation.const, op'.prop⟩)
    | some (hd, opf') => (T (some hd)).map fun (hd', opf'', op') =>
      (hd', ⟨_, opf''.val ∘ opf'.val, op'.val, rfl,
        FriendlyOperation.comp opf''.prop opf'.prop, op'.prop⟩)

Goal state after:
case h
α : 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, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop := ⋯
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
⊢ ∀ (s : Stream'.Seq α),
    ((op ∘ opf) s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, op') => (hd, ↑op' s.tail))
        ((fun hd? ↦
            match h_opf.unfold hd? with
            | none =>
              Option.map
                (fun x ↦
                  match x with
                  | (hd, opf', op') => (hd, ⟨↑op' ∘ fun x ↦ ↑opf' nil, ⋯⟩))
                (T none)
            | some (hd, opf') =>
              Option.map
                (fun x ↦
                  match x with
                  | (hd', opf'', op') => (hd', ⟨↑op' ∘ ↑opf'' ∘ ↑opf', ⋯⟩))
                (T (some hd)))
          s.head)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case h_coef
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
⊢ ∀ x ∈ (mk s 0).seq, x.2.Sorted

Tactic:
apply Seq.all_coind
    · exact h_base
    · intro (exp, coef) tl h
      grind [h_step exp coef tl h]

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

Goal state before:
pp: case oadd.inl.none.inr.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
i : ℕ
⊢ (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)

Tactic:
obtain ⟨h4, h5, h6⟩ := h2 i

Goal state after:
case oadd.inl.none.inr.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
⊢ (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
i : ℕ
⊢ (f i).repr < (f (i + 1)).repr ∧
    (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)

Tactic:
obtain ⟨h4, h5, h6⟩ := h2 i

Goal state after:
case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
⊢ (f i).repr < (f (i + 1)).repr ∧
    (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
⊢ Irrational ((↑q).rpow ↑(↑a / ↑b))

Tactic:
simp only [Irrational, Rat.cast_div, Rat.cast_natCast, Real.rpow_eq_pow, Set.mem_range,
    not_exists]

Goal state after:
q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
⊢ ∀ (x : ℚ), ¬↑x = ↑q ^ (↑a / ↑b)
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 4 = 1
hr : jacobiSymNat b a = r
⊢ jacobiSymNat a b = r

Tactic:
by
  rwa [jacobiSymNat, ← jacobiSym.quadratic_reciprocity_one_mod_four hb (Nat.odd_iff.mpr ha)]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs.length = ys.length
x y : α
i : ℕ
h₂ : xs[i]? = some x
⊢ applyId (xs.zip ys) x = y ↔ ys[i]? = some y

Tactic:
induction xs generalizing ys i with

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 ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
this : IsInducing ((⋃₀ 𝔖).domRestrict ∘ F)
Q : X → Set α
Q_compact : ∀ x ∈ ⋃₀ 𝔖, IsCompact (Q x)
F_in_Q : ∀ x ∈ ⋃₀ 𝔖, ∀ (i : ι), F i x ∈ Q x
⊢ IsCompact (range ((⋃₀ 𝔖).domRestrict ∘ F))

Tactic:
refine IsCompact.of_isClosed_subset (isCompact_univ_pi fun x ↦ Q_compact x x.2)
    (EquicontinuousOn.isClosed_range_pi_of_uniformOnFun' 𝔖_compact F_eqcont F_cl)
    (range_subset_iff.mpr fun i x _ ↦ F_in_Q x x.2 i)

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

Goal state before:
pp: G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous[inst✝⁸, inst✝³] ⇑f
A : MulAction G H := MulAction.compHom H f
⊢ IsOpenMap ⇑f

Tactic:
have : ContinuousSMul G H := continuousSMul_compHom h'f

Goal state after:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous[inst✝⁸, inst✝³] ⇑f
A : MulAction G H := MulAction.compHom H f
this : ContinuousSMul G H
⊢ IsOpenMap ⇑f
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
⊢ IsClosed[inst✝] A

Tactic:
rw [isClosed_iff_clusterPt]
    intro a ha
    by_contra! nh
    have : A = A \ {a} := by simp [nh]
    rw [this, ← accPt_principal_iff_clusterPt] at ha
    exact nh (h ha)

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
⊢ IsGeneratedBy X PUnit.{v + 1}

Tactic:
rw [iff_le_generatedBy]
  exact Eq.le (by subsingleton)

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

Goal state before:
pp: case refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h : x ∈ C
⊢ Proj J x = x

Tactic:
rw [proj_eq_self]; exact (hh · x h)

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

Goal state before:
pp: ⊢ CreatesLimits (forget CompHaus)

Tactic:
by
  let e : forget CompHaus ≅ compactumToCompHaus.inv ⋙ Compactum.forget :=
    (((forget CompHaus).leftUnitor.symm ≪≫
    Functor.isoWhiskerRight compactumToCompHaus.asEquivalence.symm.unitIso (forget CompHaus)) ≪≫
    compactumToCompHaus.inv.associator compactumToCompHaus (forget CompHaus)) ≪≫
    Functor.isoWhiskerLeft _ compactumToCompHausCompForget
  exact createsLimitsOfNatIso e.symm

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

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Continuous (SwapTrue o)

Tactic:
dsimp +unfoldPartialApp [SwapTrue]
  apply continuous_pi
  intro i
  apply Continuous.comp'
  · apply continuous_bot
  · apply continuous_apply

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

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
m : Products I
hm : m ∈ {m | m < l}
⊢ Products.eval C m ∈ ↑(Submodule.span ℤ (Set.range (eval C)))

Tactic:
exact h m hm

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

Goal state before:
pp: S : Profinite
⊢ Free ℤ (LocallyConstant ↑S.toTop ℤ)

Tactic:
obtain ⟨_, _⟩ := exists_wellFoundedLT {C : Set S // IsClopen C}
  exact @Nobeling_aux {C : Set S // IsClopen C} _ _ S (Nobeling.ι S) (Nobeling.isClosedEmbedding S)

Goal state after:
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}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x✝¹ : ↑(GoodProducts (π C fun x ↦ ord I x < o))
x✝ : ↑(MaxProducts C ho)
a : Products I
ha : a ∈ GoodProducts (π C fun x ↦ ord I x < o)
b : Products I
hb : b ∈ MaxProducts C ho
hab : a = b
⊢ False

Tactic:
rw [← hab] at hb

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x✝¹ : ↑(GoodProducts (π C fun x ↦ ord I x < o))
x✝ : ↑(MaxProducts C ho)
a : Products I
ha : a ∈ GoodProducts (π C fun x ↦ ord I x < o)
b : Products I
hb : a ∈ MaxProducts C ho
hab : a = b
⊢ 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
⊢ (((e C (term I ho)) ⟨SwapTrue o ↑x, ⋯⟩ * if ∀ i ∈ ↑l.Tail, ↑⟨SwapTrue o ↑x, ⋯⟩ i = true then 1 else 0) -
      (e C (term I ho)) ⟨↑x, ⋯⟩ * if ∀ i ∈ ↑l.Tail, ↑⟨↑x, ⋯⟩ i = true then 1 else 0) =
    if ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true then 1 else 0

Tactic:
simp only [mul_ite, mul_one, mul_zero]

Goal state after:
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
⊢ ((if ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true then (e C (term I ho)) ⟨SwapTrue o ↑x, ⋯⟩ else 0) -
      if ∀ i ∈ ↑l.Tail, ↑x i = true then (e C (term I ho)) ⟨↑x, ⋯⟩ else 0) =
    if ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true then 1 else 0
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, ↑(skeleton C ↑n) = C

Tactic:
apply subset_antisymm (iUnion_subset_iff.2 fun _ ↦ (skeleton C _).subset_complex)

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ C ⊆ ⋃ i, ↑(skeleton C ↑i)