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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝ : CommRing R
α : Type u_2
S : Finset α
x : α → 𝕎 R
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ S ∧ (x r).coeff n ≠ 0}
n : ℕ
⊢ (∑ s ∈ S, x s).coeff n = ∑ s ∈ S, (x s).coeff n

Tactic:
induction S using Finset.induction generalizing n with
  | empty =>
    simp
  | insert a S' ha hind =>
    have : (∀ (n : ℕ), Subsingleton {r | r ∈ S' ∧ (x r).coeff n ≠ 0}) := by
      refine fun n ↦ ⟨fun b c ↦ ?_⟩
      ext
      exact congrArg (fun x ↦ x.1) <|
          (h n).allEq ⟨b.1, S'.subset_insert a b.2.1, b.2.2⟩ ⟨c.1, S'.subset_insert a c.2.1, c.2.2⟩
    replace hind := hind this
    simp only [ha, not_false_eq_true, Finset.sum_insert]
    have : ∀ (n : ℕ), (x a).coeff n = 0 ∨ (∑ s ∈ S', x s).coeff n = 0 := by
      simp only [hind]
      by_contra! ⟨m, hma, hmS'⟩
      have := Finset.sum_eq_zero.mt hmS'
      push Not at this
      choose b hb hb' using this
      have : a = b :=
        congrArg (fun x ↦ x.1) <|
          (h m).allEq ⟨a, S'.mem_insert_self a, hma⟩ ⟨b, S'.mem_insert_of_mem hb, hb'⟩
      exact ha (this ▸ hb)
    rw [coeff_add_of_disjoint n _ _ this, hind n]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) = (-1) ^ n * deriv^[n] (fun y ↦ Real.exp (-(y ^ 2 / 2))) x * Real.exp (x ^ 2 / 2)

Tactic:
by
  rw [hermite_eq_deriv_gaussian, Real.exp_neg]
  field

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case succ
F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i
⊢ ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i = a • ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i

Tactic:
rw [← sum_def _ fun _ r => r • _, ← sum_def _ fun _ r => r • _, Polynomial.smul_sum,
        sum_smul_index' _ _ _ fun i => zero_smul F (preHilbertPoly F d i)]

Goal state after:
case succ
F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i
⊢ (p.sum fun n a_1 ↦ (a • a_1) • preHilbertPoly F d n) = p.sum fun n a_1 ↦ a • a_1 • preHilbertPoly F d n
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
⊢ (a • p).hilbertPoly d = a • p.hilbertPoly d

Tactic:
by
  delta hilbertPoly
  induction d with
  | zero => simp only [smul_zero]
  | succ d _ =>
      simp only
      rw [← sum_def _ fun _ r => r • _, ← sum_def _ fun _ r => r • _, Polynomial.smul_sum,
        sum_smul_index' _ _ _ fun i => zero_smul F (preHilbertPoly F d i)]
      simp only [smul_assoc]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ (q * (-1) ^ (rootMultiplicity 1 p - d + d) * (1 - X) ^ (rootMultiplicity 1 p - d) * (1 - X) ^ d).hilbertPoly (0 + d) =
    0

Tactic:
hilbertPoly_mul_one_sub_pow_add,

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ (q * (-1) ^ (rootMultiplicity 1 p - d + d) * (1 - X) ^ (rootMultiplicity 1 p - d)).hilbertPoly 0 = 0
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ ((q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p).hilbertPoly
        (d - rootMultiplicity 1 p + rootMultiplicity 1 p)).natDegree =
    d - rootMultiplicity 1 p - 1

Tactic:
hilbertPoly_mul_one_sub_pow_add,

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ ((q * (-1) ^ rootMultiplicity 1 p).hilbertPoly (d - rootMultiplicity 1 p)).natDegree = d - rootMultiplicity 1 p - 1
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : (algebraMap ℤ ℂ) (-1) * z ^ 0 + (algebraMap ℤ ℂ) (-1) * z ^ 1 + (algebraMap ℤ ℂ) 1 * z ^ n = 0
h2 : (algebraMap ℤ ℂ) 1 * z ^ 0 + (algebraMap ℤ ℂ) (-1) * z ^ (n - 1 + 0) + (algebraMap ℤ ℂ) (-1) * z ^ n = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Tactic:
map_neg,

Goal state after:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : -(algebraMap ℤ ℂ) 1 * z ^ 0 + -(algebraMap ℤ ℂ) 1 * z ^ 1 + (algebraMap ℤ ℂ) 1 * z ^ n = 0
h2 : (algebraMap ℤ ℂ) 1 * z ^ 0 + -(algebraMap ℤ ℂ) 1 * z ^ (n - 1 + 0) + -(algebraMap ℤ ℂ) 1 * z ^ n = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: case a.e_a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ ↑((n + x)! / x !) = C ↑((n + x).choose n) * ↑n !

Tactic:
rw [add_comm, add_choose]

Goal state after:
case a.e_a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ ↑((x + n)! / x !) = C ↑((x + n)! / (x ! * n !)) * ↑n !
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
⊢ (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}

Tactic:
by
    suffices C a * X ^ 2 + C b * X + C c = C a * (X - C x1) * (X - C x2) by
      have h1 : C a * (X - C x1) ≠ 0 := mul_ne_zero (by simpa) (Polynomial.X_sub_C_ne_zero _)
      have h2 : C a * (X - C x1) * (X - C x2) ≠ 0 := mul_ne_zero h1 (Polynomial.X_sub_C_ne_zero _)
      simp [this, Polynomial.roots_mul h2, Polynomial.roots_mul h1]
    simp [hvieta.1, hvieta.2]
    ring

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
⊢ (coeff i) (H.seq f (k + 1) - H.seq f k) ∈ I ^ k

Tactic:
rw [seq, add_sub_cancel_left]
  refine coeff_mul_mem_ideal_of_coeff_left_mem_ideal' (fun i ↦ ?_) i
  rw [coeff_mk]
  exact H.coeff_seq_mem f k (by simp)

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
inst✝ : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
hi : ¬i < ((map (Ideal.Quotient.mk I)) g).order.toNat
k : ℕ
⊢ (coeff i) (f - g * H.div f) ∈ I ^ k

Tactic:
show f - g * H.div f =
      f - g * (H.seq f k) - g * (H.div f - (H.seq f k)) by ring,

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
inst✝ : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
hi : ¬i < ((map (Ideal.Quotient.mk I)) g).order.toNat
k : ℕ
⊢ (coeff i) (f - g * H.seq f k - g * (H.div f - H.seq f k)) ∈ I ^ k
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)

Tactic:
let q := (maximalIdeal R).map C

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f g : A⟦X⟧
inst✝ : IsPrecomplete (IsLocalRing.maximalIdeal A) A
⊢ (f %ʷ g).degree < ↑((map (IsLocalRing.residue A)) g).order.toNat

Tactic:
by
  rw [weierstrassMod]
  split_ifs with hg
  · exact degree_trunc_lt _ _
  · nontriviality A
    rw [Polynomial.degree_zero]
    exact WithBot.bot_lt_coe _

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
H1 : r.degree < ↑n
f : A[X] := Polynomial.X ^ n - r
⊢ r.degree < (Polynomial.X ^ n).degree

Tactic:
Polynomial.degree_X_pow

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
H1 : r.degree < ↑n
f : A[X] := Polynomial.X ^ n - r
⊢ r.degree < ↑n
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
⊢ (Polynomial.X ^ n).degree = ↑n

Tactic:
Polynomial.degree_X_pow

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
⊢ ↑n = ↑n
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
x✝¹ : IsSimpleModule R ↥S
S' : Submodule R M
x✝ : S' ∈ {m | Nonempty (↥m ≃ₗ[R] ↥S)}
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ ↑e.symm
⊢ S' ≤ (S'.subtype ∘ₗ ↑e.symm).range

Tactic:
e.symm.range_comp,

Goal state after:
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
x✝¹ : IsSimpleModule R ↥S
S' : Submodule R M
x✝ : S' ∈ {m | Nonempty (↥m ≃ₗ[R] ↥S)}
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ ↑e.symm
⊢ S' ≤ S'.subtype.range
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case e'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ i ∈ range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i) =
    (bind₁ (wittStructureInt p (X 0 * X 1))) (wittPolynomial p ℤ n)

pp: case e'_3
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (rename (Prod.mk 0)) (wittPolynomial p ℤ n) * (rename (Prod.mk 1)) (wittPolynomial p ℤ n) =
    (bind₁ fun i ↦ (rename (Prod.mk i)) (wittPolynomial p ℤ n)) (X 0 * X 1)

Tactic:
· simp only [wittPolynomial, wittMul]
    rw [map_sum]
    congr 1 with i
    congr 1
    have hsupp : (Finsupp.single i (p ^ (n - i))).support = {i} := by
      rw [Finsupp.support_eq_singleton]
      simp only [and_true, Finsupp.single_eq_same, Ne]
      exact pow_ne_zero _ hp.out.ne_zero
    simp only [bind₁_monomial, hsupp, Int.cast_natCast, prod_singleton, eq_intCast,
      Finsupp.single_eq_same, Int.cast_pow]

Goal state after:
case e'_3
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (rename (Prod.mk 0)) (wittPolynomial p ℤ n) * (rename (Prod.mk 1)) (wittPolynomial p ℤ n) =
    (bind₁ fun i ↦ (rename (Prod.mk i)) (wittPolynomial p ℤ n)) (X 0 * X 1)
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

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

Tactic:
intro h
  have := solution_spec p a₁ a₂
  rw [h, zero_pow] at this
  · simpa [ha₁, ha₂] using _root_.div_eq_zero_iff.mp this.symm
  · exact Nat.sub_ne_zero_of_lt hp.out.one_lt

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

Goal state before:
pp: case succ
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
n : ℕ
⊢ (frobenius (frobeniusRotation p ha₁ ha₂) * a₁).coeff (n + 1) = (frobeniusRotation p ha₁ ha₂ * a₂).coeff (n + 1)

Tactic:
· 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: case h
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 : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ φ(p, k) b • φ(p, k) c • a • x = b • (↑p ^ m * φ(p, k) c) • x

Tactic:
simp only [← mul_smul]

Goal state after:
case h
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 : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ (φ(p, k) b * (φ(p, k) c * a)) • x = (b * (↑p ^ m * φ(p, k) c)) • x
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
h : [] ∉ T
⊢ T = ⊥

Tactic:
ext x; simpa using fun h' ↦ h <| mem_of_prefix x.nil_prefix h'

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case nil.mk
α : Type u_1
l₁ l₂ : Lists' α true
fst✝ : Bool
snd✝ : Lists' α fst✝
h' : cons ⟨fst✝, snd✝⟩ l₁ = nil
⊢ ⟨fst✝, snd✝⟩ ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
cases h'

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case cons.mk.mk
α : Type u_1
l₁ l₂ : Lists' α true
a'✝ : Lists α
l✝ : Lists' α true
m : a'✝ ∈ l₂.toList
s : l✝.Subset l₂
fst✝¹ : Bool
snd✝¹ : Lists' α fst✝¹
fst✝ : Bool
snd✝ : Lists' α fst✝
e : ⟨fst✝, snd✝⟩ ~ a'✝
h' : cons ⟨fst✝¹, snd✝¹⟩ l₁ = cons ⟨fst✝, snd✝⟩ l✝
⊢ ⟨fst✝¹, snd✝¹⟩ ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
cases h'

Goal state after:
case cons.mk.mk.refl
α : Type u_1
l₁ l₂ : Lists' α true
a'✝ : Lists α
m : a'✝ ∈ l₂.toList
fst✝ : Bool
snd✝ : Lists' α fst✝
e : ⟨fst✝, snd✝⟩ ~ a'✝
s : l₁.Subset l₂
⊢ ⟨fst✝, snd✝⟩ ∈ l₂ ∧ l₁ ⊆ l₂
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case cons
α : Type u_1
l : Lists' α true
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : ofList tail✝ ⊆ nil → ofList tail✝ = nil
h : ofList (head✝ :: tail✝) ⊆ nil
⊢ ofList (head✝ :: tail✝) = nil

Tactic:
· rcases cons_subset.1 h with ⟨⟨_, ⟨⟩, _⟩, _⟩

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.antisymm
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
⊢ of' l₁ ~ ⟨true, l₂✝⟩

Tactic:
obtain ⟨hl₂, hr₂⟩ := Equiv.antisymm_iff.1 h₂

Goal state after:
case C1.antisymm.antisymm
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
⊢ of' l₁ ~ ⟨true, l₂✝⟩
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.antisymm
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
⊢ of' l₁ ~ ⟨true, l₂✝⟩

Tactic:
apply Equiv.antisymm_iff.2

Goal state after:
case C1.antisymm.antisymm
α : Type u_1
trans : Lists α → Prop := ⋯
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
⊢ l₁ ⊆ l₂✝ ∧ l₂✝ ⊆ l₁
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
⊢ foldr (fun p r ↦ b ^ p * (single e x + f) p + r) 0 (e :: f.support.sort fun x1 x2 ↦ x1 ≥ x2) = b ^ e * x + eval b f

Tactic:
simp only [add_apply, foldr_cons, single_eq_same, hf, add_zero, add_right_inj]
    apply foldr_ext
    intro e' he' _
    congr
    rw [single_eq_of_ne, zero_add]
    aesop

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

Goal state before:
pp: b x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
a : Ordinal.{u_1}
ha : a ∈ (single e' y + f).support
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ a
a✝ : single e' y + f = f → eval b (single a x + (single e' y + f)) = b ^ a * x + eval b (single e' y + f)
he' : e' < a
⊢ a ∈ f.support

Tactic:
simpa [he'.ne'] using ha

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

Goal state before:
pp: case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ e✝.repr * ↑↑n✝ + a✝².repr < ω ^ b✝

Tactic:
apply (add_lt_add_right IH _).trans_le

Goal state after:
case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ e✝.repr * ↑↑n✝ + ω ^ e✝.repr ≤ ω ^ b✝
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x y : ZFSet.{u}
h : x ⊆ y
⊢ x.card ≤ y.card

Tactic:
by
  simpa [cardinalMk_coe_sort] using mk_le_mk_of_subset (coe_subset_coe.2 h)

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List ↑(Iio o)
this : ∃ b < o, List.foldr (?m.63 b) 0 l ≤ veblenWith f b 0
⊢ List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ a

Tactic:
obtain ⟨b, hb, hb'⟩ := this

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List ↑(Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (?m.63 b) 0 l ≤ veblenWith f b 0
⊢ List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ a
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case nil
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ ∃ b < o, List.foldr (fun x ↦ veblenWith f ↑x) 0 [] ≤ veblenWith f b 0

Tactic:
use 0; simpa using ho.bot_lt

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

Goal state before:
pp: case mpr
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsWellOrder (↥x) (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
⊢ x.IsOrdinal

Tactic:
refine isOrdinal_iff_isTrans.2 ⟨h₁, ?_⟩

Goal state after:
case mpr
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsWellOrder (↥x) (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
⊢ IsTrans (↥x) (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : e₂ = 0
⊢ e₁.repr < e₁.repr + b₂

Tactic:
grw [← h₂.lt.pos, add_zero]

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

Goal state before:
pp: b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c exp : ℝ
h_exp : exp > 0
⊢ Tendsto (norm ∘ (b ^ exp)) atTop atTop

Tactic:
apply tendsto_norm_atTop_atTop.comp

Goal state after:
b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c exp : ℝ
h_exp : exp > 0
⊢ Tendsto (b ^ exp) atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
s t : Stream'.Seq α
h : s ≠ t
⊢ ∃ n, dist ↑s ↑t = 2⁻¹ ^ n

Tactic:
PiNat.dist_eq_of_ne (Subtype.coe_ne_coe.mpr h)

Goal state after:
α : Type u_1
s t : Stream'.Seq α
h : s ≠ t
⊢ ∃ n, (1 / 2) ^ PiNat.firstDiff ↑s ↑t = 2⁻¹ ^ n