mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) g ≠ 0
⊢ ∃ f h, g.IsWeierstrassFactorization f h

Tactic:
obtain ⟨q, r, H⟩ :=
    (X ^ (g.map (IsLocalRing.residue A)).order.toNat).exists_isWeierstrassDivision hg

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) g ≠ 0
q : A⟦X⟧
r : A[X]
H : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
⊢ ∃ f h, g.IsWeierstrassFactorization f h
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝⁴ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝³ : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this✝² : pS.IsPrime
this✝¹ : IsLocalization.AtPrime (Localization.AtPrime pS) p
this✝ : IsRegularLocalRing (Localization.AtPrime q)
eq : comap C pS = maximalIdeal (Localization.AtPrime q)
this : IsRegularLocalRing (Localization.AtPrime pS)
⊢ IsRegularLocalRing (Localization.AtPrime p)

Tactic:
exact IsRegularLocalRing.of_ringEquiv (IsLocalization.algEquiv p.primeCompl
    (Localization.AtPrime pS) (Localization.AtPrime p)).toRingEquiv

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : IsSimpleRing R
tfae_1_to_2 : IsSemisimpleRing R → IsArtinianRing R
tfae_2_to_3 : IsArtinianRing R → ∃ I, IsAtom I
⊢ [IsSemisimpleRing R, IsArtinianRing R, ∃ I, IsAtom I].TFAE

Tactic:
tfae_have 3 → 1 := fun ⟨I, hI⟩ ↦ by
    have ⟨_, h⟩ := isSimpleRing_iff_isTwoSided_imp.mp ‹IsSimpleRing R›
    simp_rw [← isFullyInvariant_iff_isTwoSided] at h
    have := isSimpleModule_iff_isAtom.mpr hI
    obtain eq | eq := h _ (.isotypicComponent R R I)
    · exact (hI.bot_lt.not_ge <| (le_sSup <| by exact ⟨.refl ..⟩).trans_eq eq).elim
    exact .congr (.symm <| .trans (.ofEq _ _ eq) Submodule.topEquiv)

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : IsSimpleRing R
tfae_1_to_2 : IsSemisimpleRing R → IsArtinianRing R
tfae_2_to_3 : IsArtinianRing R → ∃ I, IsAtom I
tfae_3_to_1 : (∃ I, IsAtom I) → IsSemisimpleRing R
⊢ [IsSemisimpleRing R, IsArtinianRing R, ∃ I, IsAtom I].TFAE
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ frobenius (frobeniusRotation p ha₁ ha₂) * a₁ = frobeniusRotation p ha₁ ha₂ * a₂

Tactic:
by
  ext n
  rcases n with - | n
  · simp only [WittVector.mul_coeff_zero, WittVector.coeff_frobenius_charP, frobeniusRotation,
      coeff_mk, frobeniusRotationCoeff]
    exact solution_spec' _ ha₁ _
  · simp only [nthRemainder_spec, WittVector.coeff_frobenius_charP,
      frobeniusRotation, coeff_mk, frobeniusRotationCoeff]
    have :=
      succNthVal_spec' p n a₁ a₂ (fun i : Fin (n + 1) => frobeniusRotationCoeff p ha₁ ha₂ i.val)
        ha₁ ha₂
    simp only [frobeniusRotationCoeff, Fin.val_zero] at this
    convert! this using 3; clear this
    apply TruncatedWittVector.ext
    intro i
    simp only [WittVector.coeff_truncateFun, WittVector.coeff_frobenius_charP]
    rfl

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

Goal state before:
pp: p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
⊢ ∃ a, a ≠ 0 ∧ Φ(p, k) x = a • x

Tactic:
by
    rw [finrank_eq_one_iff_of_nonzero' x hx] at h_dim
    obtain ⟨a, ha⟩ := h_dim (Φ(p, k) x)
    refine ⟨a, ?_, ha.symm⟩
    intro ha'
    apply this
    simp only [← ha, ha', zero_smul]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
⊢ peval (polyOfInterest p n) ![fun i ↦ x.coeff i, fun i ↦ y.coeff i] =
    (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)

Tactic:
rw [peval_polyOfInterest]
  have : (p : k) = 0 := CharP.cast_eq_zero k p
  simp only [this, ne_eq, add_eq_zero, and_false, zero_pow, zero_mul, add_zero,
    not_false_eq_true, reduceCtorEq]
  have sum_zero_pow_mul_pow_p (y : 𝕎 k) : ∑ x ∈ range (n + 1 + 1),
      (0 : k) ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1) := by
    rw [Finset.sum_eq_single_of_mem 0] <;> simp +contextual
  congr <;> apply sum_zero_pow_mul_pow_p

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

Goal state before:
pp: case inl
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : Fin 2 × ℕ
f₀ : (↑↑(univ ×ˢ range (a.2 + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p a.2)
x y : TruncatedWittVector p (a.2 + 1) k
ha : a ∈ ↑(univ ×ˢ range (a.2 + 1))
S : Set (Fin 2 × ℕ) := {a_1 | a_1.2 = a.2 ∨ a_1.2 < a.2}
⊢ a.2 < a.2 + 1

Tactic:
lia

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

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ ↑(univ ×ˢ range (n + 1))
S : Set (Fin 2 × ℕ) := {a | a.2 = n ∨ a.2 < n}
h✝ : a.2 < n
⊢ a.2 < n + 1

Tactic:
lia

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

Goal state before:
pp: case inr.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := ⋯
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
⊢ IsLUB (range fun n ↦ f ⟨t, ht⟩ (g n)) (sSup (range g))

Tactic:
refine ⟨?_, fun b hb ↦ csSup_le' ?_⟩ <;> rintro _ ⟨n, rfl⟩

Goal state after:
case inr.inr.refine_1
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := fun t ↦ Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) t
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
n : ℕ
⊢ (fun n ↦ f ⟨t, ht⟩ (g n)) n ≤ sSup (range g)

case inr.inr.refine_2
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := fun t ↦ Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) t
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
b : α
hb : b ∈ upperBounds (range fun n ↦ f ⟨t, ht⟩ (g n))
n : ℕ
⊢ g n ≤ b
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: ⊢ UnivLE.{u, v} ∨ UnivLE.{v, u}

Tactic:
simp_rw [univLE_iff_cardinal_le]

Goal state after:
⊢ univ.{u, v + 1} ≤ univ.{v, u + 1} ∨ univ.{v, u + 1} ≤ univ.{u, v + 1}
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
⊢ z.length ≤ x.length + y.length

Tactic:
lia

Goal state after:
Module: Mathlib.SetTheory.Lists

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

Tactic:
intro l₁ IH l₂ l₃ h₁ h₂
    obtain - | l₂ := id h₁
    · exact h₂
    obtain - | l₃ := id h₂
    · exact h₁
    obtain ⟨hl₁, hr₁⟩ := Equiv.antisymm_iff.1 h₁
    obtain ⟨hl₂, hr₂⟩ := Equiv.antisymm_iff.1 h₂
    apply Equiv.antisymm_iff.2; constructor <;> apply Lists'.subset_def.2
    · intro a₁ m₁
      rcases Lists'.mem_of_subset' hl₁ m₁ with ⟨a₂, m₂, e₁₂⟩
      rcases Lists'.mem_of_subset' hl₂ m₂ with ⟨a₃, m₃, e₂₃⟩
      exact ⟨a₃, m₃, IH _ m₁ e₁₂ e₂₃⟩
    · intro a₃ m₃
      rcases Lists'.mem_of_subset' hr₂ m₃ with ⟨a₂, m₂, e₃₂⟩
      rcases Lists'.mem_of_subset' hr₁ m₂ with ⟨a₁, m₁, e₂₁⟩
      exact ⟨a₁, m₁, (IH _ m₁ e₂₁.symm e₃₂.symm).symm⟩

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ 0 < sizeOf l

Tactic:
apply sizeof_pos

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

Goal state before:
pp: case pos
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : e' ∈ map Prod.fst (CNF b y)
⊢ (coeff b (b ^ e * x + y)) e' = (coeff b y) e'

Tactic:
rw [mem_map] at h
      obtain ⟨⟨f, c⟩, hf, rfl⟩ := h
      rw [coeff_of_mem_CNF hf]
      apply coeff_of_mem_CNF
      rw [CNF.opow_mul_add hb hx hxb hy]
      exact mem_cons_of_mem _ hf

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

Goal state before:
pp: s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} ↑t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1 ⊆ s, t_1.Nonempty ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
⊢ ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = sSup t

Tactic:
refine ⟨Shrink t, ?_, Subtype.val ∘ (equivShrink _).symm, ?_, ?_⟩

Goal state after:
case refine_1
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} ↑t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1 ⊆ s, t_1.Nonempty ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
⊢ Nonempty (Shrink.{u, u + 1} ↑t)

case refine_2
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} ↑t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1 ⊆ s, t_1.Nonempty ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
⊢ ∀ (i : Shrink.{u, u + 1} ↑t), (Subtype.val ∘ ⇑(equivShrink ↑t).symm) i ∈ s

case refine_3
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} ↑t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1 ⊆ s, t_1.Nonempty ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
⊢ ⨆ i, (Subtype.val ∘ ⇑(equivShrink ↑t).symm) i = sSup t
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case inr
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : ↑n₂ ≤ ↑n₁ ∧ (↑n₂ < ↑n₁ ∧ Ordering.gt = Ordering.lt ∨ ¬↑n₂ < ↑n₁ ∧ Ordering.eq = Ordering.lt)
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
rcases nh.right with nh | nh <;> cases nh

Goal state after:
case inr.inl.intro
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : ↑n₂ ≤ ↑n₁ ∧ (↑n₂ < ↑n₁ ∧ Ordering.gt = Ordering.lt ∨ ¬↑n₂ < ↑n₁ ∧ Ordering.eq = Ordering.lt)
left✝ : ↑n₂ < ↑n₁
right✝ : Ordering.gt = Ordering.lt
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

case inr.inr.intro
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : ↑n₂ ≤ ↑n₁ ∧ (↑n₂ < ↑n₁ ∧ Ordering.gt = Ordering.lt ∨ ¬↑n₂ < ↑n₁ ∧ Ordering.eq = Ordering.lt)
left✝ : ¬↑n₂ < ↑n₁
right✝ : Ordering.eq = Ordering.lt
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: x : PSet.{u}
⊢ (⋃₀ x).toSet = ⋃₀ (toSet '' x.toSet)

Tactic:
ext
  simp

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

Goal state before:
pp: x : ZFSet.{u_1}
⊢ {x, x} = {x}

Tactic:
ext
  simp

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

Goal state before:
pp: x y z : ZFSet.{u_1}
⊢ {x, y} = {z} ↔ x = z ∧ y = z

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · rw [← mem_singleton, ← mem_singleton]
    simp [← h]
  · rintro ⟨rfl, rfl⟩
    exact pair_eq_singleton y

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

Goal state before:
pp: a : ZFSet.{u_1}
p : ZFSet.{u_1} → Prop
⊢ ↑(ZFSet.sep p a) = {x | x ∈ a ∧ p x}

Tactic:
ext
  simp

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

Goal state before:
pp: e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
⊢ (e.oadd n a + o).repr = (e.oadd n a).repr + o.repr

Tactic:
have nf := ONote.add_nf a o

Goal state after:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
nf : (a + o).NF
⊢ (e.oadd n a + o).repr = (e.oadd n a).repr + o.repr
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: ⊢ ⋃₀ ∅ = ∅

Tactic:
ext
  simp

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

Goal state before:
pp: x : ZFSet.{u}
⊢ ↑(⋃₀ x) = ⋃₀ (SetLike.coe '' ↑x)

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ↑(⋃ (i : α), f i) = ⋃ i, ↑(f i)

Tactic:
ext
  simp

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

Goal state before:
pp: case a
x y : PSet.{u_1}
⊢ (insert x y).rank ≤ max (succ x.rank) y.rank

Tactic:
simp_rw [rank_le_iff, mem_insert_iff]
    rintro _ (h | h)
    · simp [rank_congr h]
    · simp [rank_lt_of_mem h]

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

Goal state before:
pp: case h₂
x y : PSet.{u_1}
⊢ y.rank ≤ (insert x y).rank

Tactic:
· exact rank_mono (subset_iff.2 fun z => mem_insert_of_mem x)

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

Goal state before:
pp: ⊢ ⋃₀ ∅ = ∅

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ∀ (i : α), succ (f i).rank ≤ (range f).rank

Tactic:
· simp [rank_lt_of_mem]

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

Goal state before:
pp: x : ZFSet.{u}
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) x

Tactic:
induction x using inductionOn with | _ x ih
   =>  _ 

Goal state after:
case h
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) x
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case limit.refine_1
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ ℵ₀ ≤ #↑(Set.Iio o)

pp: case limit.refine_2
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ lift.{u, u + 1} #↑(Set.Iio o) ≤ lift.{u + 1, u} (⨆ i, (V_ ↑i).card)

Tactic:
· rw [mk_Iio_ordinal, ← lift_aleph0.{u + 1, u}, lift_le, Ordinal.aleph0_le_card]
      exact Ordinal.omega0_le_of_isSuccLimit ho

Goal state after:
case limit.refine_2
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ lift.{u, u + 1} #↑(Set.Iio o) ≤ lift.{u + 1, u} (⨆ i, (V_ ↑i).card)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : ¬o₂ = 0
⊢ (o₁ ^ o₂).NF

Tactic:
· have h' : o₂ ≠ zero := fun he => h (he ▸ zero_def ▸ rfl)
        simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, OfNat.ofNat, Zero.zero, One.one,
          h', ite_false]
        exact NF.zero

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

Goal state before:
pp: case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
hzero : 0 = zero
h : ¬o₂ = 0
h' : ¬o₂.repr = repr 0
hne : o₂ ≠ zero
⊢ 0 = 0 ^ o₂.repr

Tactic:
exact (zero_opow h').symm

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

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
hs : ms.seq = Multiseries.nil
⊢ ms.Trimmed

Tactic:
convert Trimmed.nil (f := ms.toFun)
      simp [hs]

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: case isTrue
a b : ℕ
h : a ≠ 0
this✝ : a ≤ a * a
this : b ≤ b * b
h✝ : a < b
⊢ b < b * b + a

Tactic:
lia

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: case isFalse
a b : ℕ
h : a ≠ 0
this✝ : a ≤ a * a
this : b ≤ b * b
h✝ : ¬a < b
⊢ b < a * a + a + b

Tactic:
lia

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: n : ℕ
p : ℕ × ℕ := Nat.unpair n
h : ¬p.1 = 0
this : p.1 ≤ n
⊢ 1 ≤ n

Tactic:
lia

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: n' : ℕ
ih : ∀ m < n' + 1, (S.decode m).encode = m
h : ¬(Nat.unpair (n' + 1)).1 = 0
⊢ 1 ≤ n' + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: case a.succ
n' : ℕ
ih : ∀ m < n' + 1, (S.decode m).encode = m
h : ¬(Nat.unpair (n' + 1)).1 = 0
this : (Nat.unpair (n' + 1)).1 < n' + 1
⊢ (Nat.unpair (n' + 1)).1 - 1 < n' + 1

Tactic:
lia

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

Goal state before:
pp: i : ℕ
⊢ (fastGrowing 0)^[i] i = 2 * i

Tactic:
rw [two_mul, fastGrowing_zero]

Goal state after:
i : ℕ
⊢ Nat.succ^[i] i = i + i
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd
C : NONote → Sort u_1
H0 : C 0
H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C e → C a → C (e.oadd n a h)
e : ONote
n : ℕ+
a : ONote
IHe : (h : e.NF) → C ⟨e, h⟩
IHa : (h : a.NF) → C ⟨a, h⟩
h : (e.oadd n a).NF
⊢ C ⟨e.oadd n a, h⟩

Tactic:
| oadd e n a IHe IHa =>

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

Goal state before:
pp: C : NONote → Sort u_1
o : NONote
H0 : C 0
H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C e → C a → C (e.oadd n a h)
⊢ C o

Tactic:
by
  obtain ⟨o, h⟩ := o; induction o with
  | zero => exact H0
  | oadd e n a IHe IHa => exact H1 ⟨e, h.fst⟩ n ⟨a, h.snd⟩ h.snd' (IHe _) (IHa _)

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

Goal state before:
pp: b m n : ℕ
hb : 1 < b
h₁ : m < Nat.clog b n
h₂ : Nat.clog b n ≤ m + 1
⊢ Nat.clog b n = m + 1

Tactic:
lia

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

Goal state before:
pp: eb en : Q(ℕ)
b : ℕ := Expr.natLit! eb
n : ℕ := Expr.natLit! en
x✝¹ : ¬b ≤ 1
x✝ : ¬n ≤ 1
h : Nat.clog b n = 0
⊢ 1 < b

Tactic:
lia

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

Goal state before:
pp: eb en : Q(ℕ)
b : ℕ := Expr.natLit! eb
n : ℕ := Expr.natLit! en
x✝¹ : ¬b ≤ 1
x✝ : ¬n ≤ 1
h : Nat.clog b n = 0
⊢ 1 < n

Tactic:
lia

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

Goal state before:
pp: q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
x : ℚ
hx : ↑x = ↑q ^ (↑a / ↑b)
⊢ ¬b = 0

Tactic:
lia

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

Goal state before:
pp: n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
hf : n.factorization = q • f
hf0 : f 0 = 0
⊢ q ≠ 0

Tactic:
lia

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

Goal state before:
pp: n k d m : ℕ
h_right : m ^ d < (k + 1) ^ d
h_left : k ^ d < m ^ d
h : n = m ^ d
this✝ : k < m
this : m < k + 1
⊢ False

Tactic:
lia

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

Goal state before:
pp: a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
⊢ jacobiSymNat a b = r

Tactic:
rw [← hr, jacobiSymNat, jacobiSymNat, _root_.jacobiSym.mod_left a b, ← hab]

Goal state after:
a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
⊢ jacobiSym (↑a % ↑b) b = jacobiSym (↑(a % b)) b
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
⊢ jacobiSymNat a b = r

Tactic:
· have : NeZero c := ⟨hc'⟩
    -- for `jacobiSym.mul_right`
    rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right,
      ← jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]

Goal state after:
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
h : y_den = 0
hn1 : 1 < x_num
hn2 : x_num = 0
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.Tactic.PNatToNat

Goal state before:
pp: case pos
val✝¹ : ℕ
property✝¹ : 0 < val✝¹
val✝ : ℕ
property✝ : 0 < val✝
h✝ : val✝ < val✝¹
⊢ val✝¹ - val✝ = val✝¹ - 1 - val✝ + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Tactic.PNatToNat

Goal state before:
pp: case neg
val✝¹ : ℕ
property✝¹ : 0 < val✝¹
val✝ : ℕ
property✝ : 0 < val✝
h✝ : ¬val✝ < val✝¹
⊢ 1 = val✝¹ - 1 - val✝ + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Tactic.Simproc.Factors

Goal state before:
pp: en enl ea eal : Q(ℕ)
ehn : Q(IsNat «$en» «$enl»)
eha : Q(IsNat «$ea» «$eal»)
n : ℕ := Expr.natLit! enl
__x✝¹ : PLift (0 < n)
hn0 : 0 < n
a : ℕ := Expr.natLit! eal
b : ℕ := n.minFac
__x✝ : PLift (a ≤ b)
hab : a ≤ b
h_bn : ¬b < n
hbn_eq : b = n
hba : ¬b = a
⊢ a < n

Tactic:
lia

Goal state after:
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₃ : ∃ a b, (a, b) ∈ xs.zip ys ∧ ⟨a, b⟩ = ⟨x, val⟩
⊢ val ∈ ys

Tactic:
rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩

Goal state after:
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