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
inst✝² : CharP R p
inst✝¹ : PerfectRing R p
S : Type u_2
inst✝ : CommRing S
f g : 𝕎 R →+* S
h : ∀ (x : R), f ((teichmuller p) x) = g ((teichmuller p) x)
n : ℕ
hn : ↑p ^ n = 0
x c : 𝕎 R
hc : x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i = ↑p ^ (n + 1) * c
⊢ ∑ i ≤ n, g ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i))) * ↑p ^ i =
    g (x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i) +
      g (∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i)

Tactic:
hc

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝³ : CommRing R
inst✝² : CharP R p
inst✝¹ : PerfectRing R p
S : Type u_2
inst✝ : CommRing S
f g : 𝕎 R →+* S
h : ∀ (x : R), f ((teichmuller p) x) = g ((teichmuller p) x)
n : ℕ
hn : ↑p ^ n = 0
x c : 𝕎 R
hc : x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i = ↑p ^ (n + 1) * c
⊢ ∑ i ≤ n, g ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i))) * ↑p ^ i =
    g (↑p ^ (n + 1) * c) + g (∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i)
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ x = y + y⁻¹ ∨ y = 0 ↔ y ^ 2 - x * y + 1 = 0 ∨ y = 0

Tactic:
apply or_congr _ Iff.rfl

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := ⋯
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ x = y + y⁻¹ ↔ y ^ 2 - x * y + 1 = 0
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) = (aeval x) (hermite n) * ((-1) ^ n) ^ 2

Tactic:
← pow_mul

Goal state after:
n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) = (aeval x) (hermite n) * (-1) ^ (n * 2)
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:
hermite_eq_deriv_gaussian,

Goal state after:
n : ℕ
x : ℝ
⊢ (-1) ^ n * deriv^[n] (fun y ↦ Real.exp (-(y ^ 2 / 2))) x / Real.exp (-(x ^ 2 / 2)) =
    (-1) ^ n * deriv^[n] (fun y ↦ Real.exp (-(y ^ 2 / 2))) x * Real.exp (x ^ 2 / 2)
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)
hc : 1 - a.coeff f.natDegree * b.coeff 0 = ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)
⊢ IsUnit (1 - a.coeff f.natDegree * b.coeff 0 - 1)

Tactic:
hc

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)
hc : 1 - a.coeff f.natDegree * b.coeff 0 = ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)
⊢ IsUnit (∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x) - 1)
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
a✝ : Nontrivial R
trinomial : R → R[X] := fun r ↦ a • X ^ 2 + r • X + C a
ht : ∀ (r : R), (X + C 1) * trinomial r = a • X ^ 3 + (a + r) • X ^ 2 + (a + r) • X + C a
⊢ (X + C 1) * trinomial b = (X + C 1) * trinomial c

Tactic:
ht,

Goal state after:
R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
a✝ : Nontrivial R
trinomial : R → R[X] := fun r ↦ a • X ^ 2 + r • X + C a
ht : ∀ (r : R), (X + C 1) * trinomial r = a • X ^ 3 + (a + r) • X ^ 2 + (a + r) • X + C a
⊢ a • X ^ 3 + (a + b) • X ^ 2 + (a + b) • X + C a = a • X ^ 3 + (a + c) • X ^ 2 + (a + c) • X + C a
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

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

Tactic:
mul_comm (n ! : ℤ[X]),

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

Goal state before:
pp: n : ℕ
⊢ ↑n ! * (-1) ^ n * (shiftedLegendre n).comp (1 - X) = ↑n ! * shiftedLegendre n

Tactic:
mul_comm (n ! : ℤ[X]),

Goal state after:
n : ℕ
⊢ (-1) ^ n * ↑n ! * (shiftedLegendre n).comp (1 - X) = ↑n ! * shiftedLegendre n
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: case h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
u : M ⊗[R] N
P : { P // P.FG }
t : ↥↑P ⊗[R] N
ht :
  (Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃P Q⦄ h ↦ rTensor N (inclusion h)) P) t =
    (FG.rTensor.directLimit R M N).symm u
⊢ (FG.rTensor.directLimit R M N)
      ((Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃x x_1⦄ h ↦ rTensor N (inclusion h)) P) t) =
    u

Tactic:
ht,

Goal state after:
case h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
u : M ⊗[R] N
P : { P // P.FG }
t : ↥↑P ⊗[R] N
ht :
  (Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃P Q⦄ h ↦ rTensor N (inclusion h)) P) t =
    (FG.rTensor.directLimit R M N).symm u
⊢ (FG.rTensor.directLimit R M N) ((FG.rTensor.directLimit R M N).symm u) = u
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
B : Subalgebra R S
hB : B.FG
ht : t ∈ (rTensor M B.val.toLinearMap).range
s : Finset S
hs : (φ R s).range = B
⊢ ∃ a, π R M S a = t

Tactic:
obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor B (le_of_eq hs.symm) ht

Goal state after:
R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
B : Subalgebra R S
hB : B.FG
ht : t ∈ (rTensor M B.val.toLinearMap).range
s : Finset S
hs : (φ R s).range = B
p : MvPolynomial (Fin s.card) R ⊗[R] M
hp : (rTensor M (φ R s).toLinearMap) p = t
⊢ ∃ a, π R M S a = t
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ (rTensor M A.val.toLinearMap).range
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (φ R gen).range
⊢ ∃ n ψ p q, (rTensor M ψ.toLinearMap) p = t ∧ ψ q = s

Tactic:
obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor _ hAB ht

Goal state after:
R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ (rTensor M A.val.toLinearMap).range
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (φ R gen).toLinearMap) p = t
⊢ ∃ n ψ p q, (rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
S : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup S
inst✝¹ : Module R M
inst✝ : Module R S
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ IsIsotypicOfType R (↥N) S ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule R ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)],
      Nonempty (↥↑((Submodule.MapSubtype.orderIso N).toEquiv a) ≃ₗ[R] S)

Tactic:
simp_rw [Submodule.MapSubtype.orderIso, Equiv.coe_fn_mk, ← (e _).isSimpleModule_iff]

Goal state after:
R : Type u_2
M : Type u
S : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup S
inst✝¹ : Module R M
inst✝ : Module R S
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ IsIsotypicOfType R (↥N) S ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule R ↥a], Nonempty (↥(Submodule.map N.subtype a) ≃ₗ[R] S)
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst✝⁹ : CommSemiring R₀
inst✝⁸ : Ring R
inst✝⁷ : Algebra R₀ R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R S
inst✝ : IsSemisimpleModule R M
m : ↥(fullyInvariantSubmodule R M)
x✝ : ↑(isotypicComponents R M)
⊢ x✝ ∈ (fun m ↦ {c | ↑c ≤ ↑m}) m → ⟨↑x✝, ⋯⟩ ≤ m

Tactic:
exact id

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

Goal state before:
pp: case refine_3
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
⊢ (∃ s ⊆ isotypicComponents R M, m = sSup s) → m.IsFullyInvariant

Tactic:
· rintro ⟨_, hs, rfl⟩
    exact (fullyInvariantSubmodule R M).sSupClosed fun _ h ↦ .of_mem_isotypicComponents (hs h)

Goal state after:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case h
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ f.ker ⊓ I • ⊤
y : TensorProduct R (↥I) M
hy : (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = x
inj : Function.Injective ⇑(↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I))
comm1 :
  (↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I)) ∘ₗ lTensor (↥I) f =
    f ∘ₗ ↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)
eq0 : (lTensor (↥I) f) y = 0
z : TensorProduct R ↥I ↥f.ker
hz : (lTensor (↥I) f.ker.subtype) z = y
comm2 :
  (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) ∘ₗ lTensor (↥I) f.ker.subtype =
    f.ker.subtype ∘ₗ ↑(TensorProduct.lid R ↥f.ker) ∘ₗ rTensor (↥f.ker) (Submodule.subtype I)
⊢ (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) ((lTensor (↥I) f.ker.subtype) z) = f.ker.subtype ⟨x, ⋯⟩

Tactic:
hz,

Goal state after:
case h
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ f.ker ⊓ I • ⊤
y : TensorProduct R (↥I) M
hy : (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = x
inj : Function.Injective ⇑(↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I))
comm1 :
  (↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I)) ∘ₗ lTensor (↥I) f =
    f ∘ₗ ↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)
eq0 : (lTensor (↥I) f) y = 0
z : TensorProduct R ↥I ↥f.ker
hz : (lTensor (↥I) f.ker.subtype) z = y
comm2 :
  (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) ∘ₗ lTensor (↥I) f.ker.subtype =
    f.ker.subtype ∘ₗ ↑(TensorProduct.lid R ↥f.ker) ∘ₗ rTensor (↥f.ker) (Submodule.subtype I)
⊢ (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = f.ker.subtype ⟨x, ⋯⟩
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case add
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy : f (J.toCotangent ⟨y, ⋯⟩) = 0
hz : f (J.toCotangent ⟨z, ⋯⟩) = 0
this : ⟨y + z, ⋯⟩ = ⟨y, ⋯⟩ + ⟨z, ⋯⟩
⊢ 0 + f (J.toCotangent ⟨z, ⋯⟩) = 0

Tactic:
hz,

Goal state after:
case add
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy : f (J.toCotangent ⟨y, ⋯⟩) = 0
hz : f (J.toCotangent ⟨z, ⋯⟩) = 0
this : ⟨y + z, ⋯⟩ = ⟨y, ⋯⟩ + ⟨z, ⋯⟩
⊢ 0 + 0 = 0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
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 [map_mul, bind₁_X_right]

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

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
ι : Type u_1
f : ι → Set α
inst✝ : OrderTop α
hs : ∀ (i : ι), IsClub (f i)
⊢ IsClub (⋂ i, f i)

Tactic:
by
  rw [← sInter_range]
  exact .sInter_of_orderTop (by simpa)

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

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
⊢ IsClub (Function.fixedPoints f)

Tactic:
by
  cases isEmpty_or_nonempty α; · simp
  refine ⟨fun s hs hs₀ _ a ha ↦ (hf.map_isLUB ha hs₀).unique ?_, fun a ↦ ?_⟩
  · rwa [image_congr hs, image_id']
  · cases topOrderOrNoTopOrder α with
    | inl => use ⊤; simpa using! hf.strictMono.id_le ⊤
    | inr h =>
      rw [noTopOrder_iff_noMaxOrder] at h
      suffices BddAbove (.range fun n ↦ f^[n] a) from
        ⟨_, hf.iSup_iterate_mem_fixedPoints a this, le_csSup this ⟨0, rfl⟩⟩
      refine .of_not_isCofinal fun h ↦ (cof_le h).not_gt
        ((aleph0_le_cof.lt_of_ne' hα).trans_le' ?_)
      simpa using mk_range_le_lift (f := fun n : ℕ ↦ f^[n] a)

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

Goal state before:
pp: case refine_1.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : lfpApprox f x o = x
ho : o ≠ 0
⊢ f x = x ∨ o = 0

Tactic:
have hpos : (0 : Ordinal) < o :=
        zero_lt_one.trans_le (one_le_iff_ne_zero.mpr ho)
      have hmem : lfpApprox f x 0 ∈ fixedPoints f :=
        lfpApprox_mem_fixedPoints_of_eq f hx hpos (le_refl _)
          ((lfpApprox_zero f).trans h.symm)
      have hfx : f x = x :=
        (mem_fixedPoints_iff.mp (by simpa [lfpApprox_zero] using hmem))
      exact Or.inl hfx

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

Goal state before:
pp: case pos
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
hf : lfpApprox f x a ∈ fixedPoints ⇑f
i : Ordinal.{u}
h : i ≤ a
⊢ lfpApprox f x i ≤ lfpApprox f x a

Tactic:
exact lfpApprox_mono_right f h

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✝ + ω ^ e✝.repr ≤ ω ^ b✝

Tactic:
← mul_succ,

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 * succ ↑↑n✝ ≤ ω ^ b✝
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : ↑n₁ < ↑n₂
⊢ ω ^ e.repr * ↑↑n₁ + ω ^ e.repr ≤ ω ^ e.repr * ↑↑n₂

Tactic:
← mul_succ,

Goal state after:
e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : ↑n₁ < ↑n₂
⊢ ω ^ e.repr * succ ↑↑n₁ ≤ ω ^ e.repr * ↑↑n₂
Module: Mathlib.SetTheory.ZFC.Basic

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

Tactic:
let := congr_arg sUnion H

Goal state after:
x y : ZFSet.{u_1}
H : {x} = {y}
this : ⋃₀ {x} = ⋃₀ {y} := congr_arg sUnion H
⊢ x = y
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: ⊢ invVeblen₂ 0 = 0

Tactic:
apply invVeblen₂_of_lt_opow

Goal state after:
⊢ 0 < ω ^ 0
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o a x : Ordinal.{u}
h : a < veblen o a
⊢ veblen o a = ω ^ x ↔ x.invVeblen₁ = o ∧ x.invVeblen₂ = a

Tactic:
refine ⟨?_, fun ⟨hx, ha⟩ ↦ ?_⟩
  · obtain rfl | ho := eq_zero_or_pos o
    · rw [veblen_zero] at h
      have := invVeblen₁_of_lt_opow h
      have := invVeblen₂_of_lt_opow h
      aesop
    · rw [← veblen_veblen_of_lt ho, veblen_zero_apply, opow_right_inj one_lt_omega0]
      rintro rfl
      simp [invVeblen₁_veblen h, invVeblen₂_veblen ho.ne' h]
  · convert! ← veblen_invVeblen₁_invVeblen₂ x

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ε_ (succ o) = nfp (fun a ↦ ω ^ a) (succ (ε_ o))

Tactic:
by
  rw [epsilon_eq_deriv, epsilon_eq_deriv, deriv_succ]

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

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∉ y ↔ y ⊆ x

Tactic:
by
  refine ⟨?_, fun hxy hyx ↦ mem_irrefl _ (hxy hyx)⟩
  revert hx hy
  refine Sym2.GameAdd.recursion mem_wf (fun x y IH hx hy hyx z hzy ↦ ?_) x y
  by_contra hzx
  exact hyx (mem_of_subset_of_mem hx hy (IH z x (Sym2.GameAdd.fst_snd hzy) (hy.mem hzy) hx hzx) hzy)

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

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ y ⊆ x → y ⊆ x

Tactic:
exact id

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

Goal state before:
pp: case gt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.gt
ee : Ordering.gt.Compares e₁ e₂
⊢ (match Ordering.gt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
exact
        (Ordinal.sub_eq_of_add_eq <|
            add_of_omega0_opow_le (h₂.below_of_lt ee).repr_lt <| omega0_le_oadd _ _ _).symm

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.toPSet.Type = o.ToType

Tactic:
rw [toPSet]
  rfl

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

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
⊢ a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁

Tactic:
apply add_of_omega0_opow_le h₁.snd'.repr_lt

Goal state after:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
⊢ ω ^ e₁.repr ≤ ω ^ e₁.repr * ↑↑n₁
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : e₂ = 0
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr

pp: case neg
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr

Tactic:
· obtain ⟨x, xe⟩ := Nat.exists_eq_succ_of_ne_zero n₂.ne_zero
      simp only [Mul.mul, mul, e0, ↓reduceIte, repr, repr_zero, PNat.mul_coe, natCast_mul,
        opow_zero, one_mul]
      simp only [xe, h₂.zero_of_zero e0, repr_zero, add_zero]
      rw [Nat.cast_add_one x, add_mul_add_one _ ao, mul_assoc]

Goal state after:
case neg
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
⊢ a.repr + ↑m < ω ^ e.repr

Tactic:
obtain ⟨h₁, h₂⟩ := nf_repr_split h
  obtain ⟨e0, d⟩ := h₁.of_dvd_omega0 (split_dvd h)
  apply isPrincipal_add_omega0_opow _ h₁.snd'.repr_lt (lt_of_lt_of_le (natCast_lt_omega0 _) _)
  simpa using opow_le_opow_right omega0_pos (one_le_iff_ne_zero.2 e0)

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

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
⊢ e.repr * succ b < e.repr * ω

Tactic:
by gcongr; exact isSuccLimit_omega0.succ_lt l

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'))
⊢ ∃ f,
    ∀ (b : β),
      match F b with
      | none => f b = nil
      | some (a, c, b') => f b = Seq.cons a (op c (f b'))

Tactic:
have hT : LipschitzWith 2⁻¹ T := by
    rw [lipschitzWith_iff_dist_le_mul]
    intro f g
    rw [UniformFun.dist_le (by positivity)]
    intro b
    simp only [UniformFun.toFun, UniformFun.ofFun, Equiv.coe_fn_symm_mk, NNReal.coe_inv,
      NNReal.coe_ofNat, T]
    cases F b with
    | none => simp
    | some v =>
      obtain ⟨a, c, b'⟩ := v
      simp
      calc
        _ ≤ dist (f b') (g b') := by
          have := h.friend c
          rw [FriendlyOperation, lipschitzWith_iff_dist_le_mul] at this
          specialize this (f b') (g b')
          simpa using this
        _ ≤ _ := by
          simp only [UniformFun.dist_def]
          apply le_ciSup (f := fun b ↦ dist (f b) (g b))
          have : ∃ C, ∀ (a b : Seq α), dist a b ≤ C := by
            rw [← Metric.boundedSpace_iff]
            infer_instance
          obtain ⟨C, hC⟩ := this
          use C
          simp [upperBounds]
          grind

Goal state after:
α : 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,
    ∀ (b : β),
      match F b with
      | none => f b = nil
      | some (a, c, b') => f b = Seq.cons a (op c (f b'))