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

Goal state before:
pp: case pos
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
n : ℕ
hn : P n
⊢ 0 = y.coeff n

Tactic:
exact hn.symm

Goal state after:
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
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ insert a S' ∧ (x r).coeff n ≠ 0}
n : ℕ
this : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ S' ∧ (x r).coeff n ≠ 0}
hind : ∀ (n : ℕ), (∑ s ∈ S', x s).coeff n = ∑ s ∈ S', (x s).coeff n
⊢ ∀ (n : ℕ), (x a).coeff n = 0 ∨ (∑ s ∈ S', x s).coeff n = 0

Tactic:
simp only [hind]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝ : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ insert a S' ∧ (x r).coeff n ≠ 0}
n : ℕ
this : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ S' ∧ (x r).coeff n ≠ 0}
hind : ∀ (n : ℕ), (∑ s ∈ S', x s).coeff n = ∑ s ∈ S', (x s).coeff n
⊢ ∀ (n : ℕ), (x a).coeff n = 0 ∨ ∑ s ∈ S', (x s).coeff n = 0
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
I : Ideal R
distinguish : f.IsDistinguishedAt I
⊢ map (Ideal.Quotient.mk I) f = X ^ f.natDegree

Tactic:
by
  ext i
  by_cases ne : i = f.natDegree
  · simp [ne, distinguish.monic]
  · rcases lt_or_gt_of_ne ne with lt | gt
    · simpa [ne, eq_zero_iff_mem] using (distinguish.mem lt)
    · simp [ne, Polynomial.coeff_eq_zero_of_natDegree_lt gt]

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

Goal state before:
pp: case succ.refine_1
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
s : ℕ
hs : s ∈ p.support
⊢ s ∈ Finset.range n.succ

pp: case succ.refine_2
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ Finset.range n.succ \ p.support
⊢ p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) = 0

pp: case succ.refine_3
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ p.support
⊢ p.coeff x * ↑((n + d - x).choose d) = p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1))

Tactic:
· rw [Finset.mem_range_succ_iff]
        exact h_le ⟨s, hs⟩

Goal state after:
case succ.refine_2
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ Finset.range n.succ \ p.support
⊢ p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) = 0

case succ.refine_3
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ p.support
⊢ p.coeff x * ↑((n + d - x).choose d) = p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1))
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: case e'_3
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
hroots : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
p : R[X] := C a * X ^ 2 + C b * X + C c
⊢ 2 = p.roots.card

Tactic:
hroots,

Goal state after:
case e'_3
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
hroots : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
p : R[X] := C a * X ^ 2 + C b * X + C c
⊢ 2 = {x1, x2}.card
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
hroots : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
p : R[X] := C a * X ^ 2 + C b * X + C c
hp_natDegree : p.natDegree = 2
⊢ p.roots.card = 2

Tactic:
hroots,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
hroots : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
p : R[X] := C a * X ^ 2 + C b * X + C c
hp_natDegree : p.natDegree = 2
⊢ {x1, x2}.card = 2
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
haroots : (C a * X ^ 2 + C b * X + C c).aroots S = {x1, x2}
⊢ (algebraMap T S) b = -(algebraMap T S) a * (x1 + x2)

Tactic:
aroots_def,

Goal state after:
T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
haroots : (map (algebraMap T S) (C a * X ^ 2 + C b * X + C c)).roots = {x1, x2}
⊢ (algebraMap T S) b = -(algebraMap T S) a * (x1 + x2)
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
haroots : (C a * X ^ 2 + C b * X + C c).aroots S = {x1, x2}
⊢ (algebraMap T S) c = (algebraMap T S) a * x1 * x2

Tactic:
aroots_def,

Goal state after:
T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
haroots : (map (algebraMap T S) (C a * X ^ 2 + C b * X + C c)).roots = {x1, x2}
⊢ (algebraMap T S) c = (algebraMap T S) a * x1 * x2
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
ha : (algebraMap T S) a ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).aroots S = {x1, x2} ↔
    (algebraMap T S) b = -(algebraMap T S) a * (x1 + x2) ∧ (algebraMap T S) c = (algebraMap T S) a * x1 * x2

Tactic:
aroots_def,

Goal state after:
T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
ha : (algebraMap T S) a ≠ 0
⊢ (map (algebraMap T S) (C a * X ^ 2 + C b * X + C c)).roots = {x1, x2} ↔
    (algebraMap T S) b = -(algebraMap T S) a * (x1 + x2) ∧ (algebraMap T S) c = (algebraMap T S) a * x1 * x2
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: T : Type u_2
S : Type u_3
inst✝² : CommRing T
inst✝¹ : Field S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
ha : (algebraMap T S) a ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).aroots S = {x1, x2} ↔
    x1 + x2 = -(algebraMap T S) b / (algebraMap T S) a ∧ x1 * x2 = (algebraMap T S) c / (algebraMap T S) a

Tactic:
aroots_def,

Goal state after:
T : Type u_2
S : Type u_3
inst✝² : CommRing T
inst✝¹ : Field S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
ha : (algebraMap T S) a ≠ 0
⊢ (map (algebraMap T S) (C a * X ^ 2 + C b * X + C c)).roots = {x1, x2} ↔
    x1 + x2 = -(algebraMap T S) b / (algebraMap T S) a ∧ x1 * x2 = (algebraMap T S) c / (algebraMap T S) a
Module: Mathlib.RingTheory.Polynomial.Morse

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
hp : (f.rootSet S).ncard ≤ (↑(f.aroots (S ⧸ p)).toFinset).ncard + 1
g : G
hg : g ∈ Ideal.inertia G p
hfp : map (algebraMap R (S ⧸ p)) f = 0
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap

Tactic:
aroots_def,

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
hp : (f.rootSet S).ncard ≤ (↑(map (algebraMap R (S ⧸ p)) f).roots.toFinset).ncard + 1
g : G
hg : g ∈ Ideal.inertia G p
hfp : map (algebraMap R (S ⧸ p)) f = 0
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
q : ℕ
hq : q ≠ 0
i : R⟦X⟧
⊢ (expand (p * q) ⋯) i = ((expand p hp).comp (expand q hq)) i

Tactic:
simp [expand, MvPowerSeries.expand_mul_eq_comp p hp q hq]

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
inst✝ : IsHausdorff I A
q q' : A⟦X⟧
r r' : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hr' : r'.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = g * q' + ↑r' - ↑r
⊢ g * (q - q') = ↑r' - ↑r

Tactic:
mul_sub,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q q' : A⟦X⟧
r r' : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hr' : r'.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = g * q' + ↑r' - ↑r
⊢ g * q - g * q' = ↑r' - ↑r
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
a : A
f : A⟦X⟧
inst✝ : IsAdicComplete I A
⊢ H.mod (a • f) = a • H.mod f

Tactic:
by
  have H1 := (H.isWeierstrassDivisionAt_div_mod f).smul a
  have H2 := H.isWeierstrassDivisionAt_div_mod (a • f)
  exact (H.eq_of_mul_add_eq_mul_add H2.degree_lt H1.degree_lt
    (H2.eq_mul_add.symm.trans H1.eq_mul_add)).2

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

Goal state before:
pp: case inl
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
x✝ : ∃ I, IsAtom I
I : Ideal R
hI : IsAtom I
left✝ : Nontrivial R
h : ∀ (I : Ideal R), Submodule.IsFullyInvariant I → I = ⊥ ∨ I = ⊤
this : IsSimpleModule R ↥I
eq : isotypicComponent R R ↥I = ⊥
⊢ IsSemisimpleRing R

pp: case inr
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
x✝ : ∃ I, IsAtom I
I : Ideal R
hI : IsAtom I
left✝ : Nontrivial R
h : ∀ (I : Ideal R), Submodule.IsFullyInvariant I → I = ⊥ ∨ I = ⊤
this : IsSimpleModule R ↥I
eq : isotypicComponent R R ↥I = ⊤
⊢ IsSemisimpleRing R

Tactic:
· exact (hI.bot_lt.not_ge <| (le_sSup <| by exact ⟨.refl ..⟩).trans_eq eq).elim

Goal state after:
case inr
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
x✝ : ∃ I, IsAtom I
I : Ideal R
hI : IsAtom I
left✝ : Nontrivial R
h : ∀ (I : Ideal R), Submodule.IsFullyInvariant I → I = ⊥ ∨ I = ⊤
this : IsSimpleModule R ↥I
eq : isotypicComponent R R ↥I = ⊤
⊢ IsSemisimpleRing R
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : Associated a b
⊢ (if Squarefree b then (-1) ^ (factors a).card else 0) = if Squarefree b then (-1) ^ (factors b).card else 0

Tactic:
h.card_factors_eq

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : Associated a b
⊢ (if Squarefree b then (-1) ^ (factors b).card else 0) = if Squarefree b then (-1) ^ (factors b).card else 0
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 : 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
⊢ StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V

Tactic:
refine LinearEquiv.ofBijective F₀ ⟨?_, ?_⟩

Goal state after:
case refine_1
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
⊢ Function.Injective ⇑F₀

case refine_2
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
⊢ Function.Surjective ⇑F₀
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inr.refine_2.inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
a : α
val✝ : OrderTop α
⊢ ∃ y ∈ Function.fixedPoints f, a ≤ y

Tactic:
use ⊤

Goal state after:
case h
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
a : α
val✝ : OrderTop α
⊢ ⊤ ∈ Function.fixedPoints f ∧ a ≤ ⊤
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
s : Set α
inst✝ : LinearOrder α
hs : IsStationary s
⊢ s.Nonempty

Tactic:
by
  simpa using hs .univ

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
this :
  {b : Bool} →
    (l : Lists' α b) →
      C ⟨b, l⟩ ×'
        match b, l with
        | true, l => D l
        | false, x => PUnit
⊢ ((l : Lists α) → C l) ×' ((l : Lists' α true) → D l)

Tactic:
by exact ⟨fun ⟨b, l⟩ => (this _).1, fun l => (this l).2⟩

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case refl
α : Type u_1
l₁ : Lists' α true
⊢ l₁ ⊆ l₁ ∧ l₁ ⊆ l₁

Tactic:
simp [Lists'.Subset.refl]

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

Goal state after:
case inr.inl
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)
nh : ↑n₂ < ↑n₁ ∧ 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
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)
nh : ¬↑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✝)
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]

Goal state after:
case a
x y : PSet.{u_1}
⊢ ∀ ⦃y_1 : PSet.{u_1}⦄, y_1.Equiv x ∨ y_1 ∈ y → y_1.rank < max (succ x.rank) y.rank
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: a x : Ordinal.{u}
⊢ x.invVeblen₂ ≤ a ↔ ω ^ x ≤ veblen x.invVeblen₁ a

Tactic:
by
  rw [← veblen_le_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]

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

Goal state before:
pp: a x : Ordinal.{u}
⊢ a ≤ x.invVeblen₂ ↔ veblen x.invVeblen₁ a ≤ ω ^ x

Tactic:
by
  rw [← veblen_le_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]

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

Goal state before:
pp: p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ Hereditarily p x → p ∅

Tactic:
apply @ZFSet.inductionOn _ x
  intro y IH h
  rcases ZFSet.eq_empty_or_nonempty y with (rfl | ⟨a, ha⟩)
  · exact h.self
  · exact IH a ha (h.mem ha)

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

Goal state before:
pp: case mpr.inr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x ∈ y
⊢ x ⊆ y

Tactic:
exact hy.subset_of_mem h

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

Goal state before:
pp: o' : ONote
m : ℕ
x✝ : NF 0
fst_eq✝ : 0 = o'
snd_eq✝ : 0 = m
⊢ split 0 = (scale 1 o', m)

Tactic:
subst o' m

Goal state after:
x✝ : NF 0
⊢ split 0 = (scale 1 0, 0)
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
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
this : 1 + (e - 1) = e
a✝¹ : (e - 1).oadd n a' = o'
a✝ : m' = m
⊢ e.oadd n (scale 1 a') = scale 1 o' ∧ m' = m

Tactic:
subst o' m

Goal state after:
case neg
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
this : 1 + (e - 1) = e
⊢ e.oadd n (scale 1 a') = scale 1 ((e - 1).oadd n a') ∧ m' = m'
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o' : ONote
m : ℕ
x✝ : NF 0
fst_eq✝ : 0 = o'
snd_eq✝ : 0 = m
⊢ o'.NF ∧ repr 0 = ω * o'.repr + ↑m

Tactic:
subst o' m

Goal state after:
x✝ : NF 0
⊢ NF 0 ∧ repr 0 = ω * repr 0 + ↑0
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
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
a✝¹ : (e - 1).oadd n a' = o'
a✝ : m' = m
⊢ o'.NF ∧ ω ^ e.repr * ↑↑n + (ω * a'.repr + ↑m') = ω * o'.repr + ↑m

Tactic:
subst o' m

Goal state after:
case neg
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'
⊢ ((e - 1).oadd n a').NF ∧ ω ^ e.repr * ↑↑n + (ω * a'.repr + ↑m') = ω * ((e - 1).oadd n a').repr + ↑m'
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
⊢ (e.opowAux a0 a k m).NF

Tactic:
unfold opowAux

Goal state after:
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
⊢ (match k, m with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m).NF
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
k0 : k = 0
⊢ (opowAux 0 a0 (a0.oadd n a' * ↑m) 0 m).repr < ω ^ a0.repr

Tactic:
refine lt_of_lt_of_le ?_ (opow_le_opow_right omega0_pos (one_le_iff_ne_zero.2 e0))

Goal state after:
case pos
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
k0 : k = 0
⊢ (opowAux 0 a0 (a0.oadd n a' * ↑m) 0 m).repr < ω ^ 1
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
αd : ω ∣ α'
⊢ ¬IsMin α'

Tactic:
rw [isMin_iff_eq_bot]

Goal state after:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
αd : ω ∣ α'
⊢ ¬α' = ⊥