mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: case e_f
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
u'FG : (φ R s').range.FG
huu' : (rTensor M (φ R s).range.val.toLinearMap) u = (rTensor M (φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (φ R s).range ≤ B
hA'B : (φ R s').range ≤ B
h : (rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = (rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (φ R t).range
hAB' : (φ R s).range ≤ (φ R t).range
hA'B' : (φ R s').range ≤ (φ R t).range
q : MvPolynomial (Fin t.card) R ⊗[R] M
hq :
  (rTensor M (φ R t).rangeRestrict.toLinearMap) q =
    (rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
⊢ rTensor M (Subalgebra.inclusion hAB').toLinearMap =
    rTensor M (Subalgebra.inclusion ⋯).toLinearMap ∘ₗ rTensor M (Subalgebra.inclusion hAB).toLinearMap

Tactic:
ext

Goal state after:
case e_f
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
u'FG : (φ R s').range.FG
huu' : (rTensor M (φ R s).range.val.toLinearMap) u = (rTensor M (φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (φ R s).range ≤ B
hA'B : (φ R s').range ≤ B
h : (rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = (rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (φ R t).range
hAB' : (φ R s).range ≤ (φ R t).range
hA'B' : (φ R s').range ≤ (φ R t).range
q : MvPolynomial (Fin t.card) R ⊗[R] M
hq :
  (rTensor M (φ R t).rangeRestrict.toLinearMap) q =
    (rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
x✝¹ : ↥(φ R s).range
x✝ : M
⊢ ((AlgebraTensorModule.curry (rTensor M (Subalgebra.inclusion hAB').toLinearMap)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry
          (rTensor M (Subalgebra.inclusion ⋯).toLinearMap ∘ₗ rTensor M (Subalgebra.inclusion hAB).toLinearMap))
        x✝¹)
      x✝
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
this :
  (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0 →
    ∃ B, B.FG ∧ ∃ (x : A ≤ B), (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
hu'✝ : (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' : (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
⊢ (LinearMap.baseChange (↥B) f) ((rTensor M (Subalgebra.inclusion hAB).toLinearMap) u) = 0 ∧
    (rTensor M B.val.toLinearMap) ((rTensor M (Subalgebra.inclusion hAB).toLinearMap) u) = t

Tactic:
constructor

Goal state after:
case h.left
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
this :
  (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0 →
    ∃ B, B.FG ∧ ∃ (x : A ≤ B), (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
hu'✝ : (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' : (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
⊢ (LinearMap.baseChange (↥B) f) ((rTensor M (Subalgebra.inclusion hAB).toLinearMap) u) = 0

case h.right
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
this :
  (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0 →
    ∃ B, B.FG ∧ ∃ (x : A ≤ B), (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
hu'✝ : (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' : (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
⊢ (rTensor M B.val.toLinearMap) ((rTensor M (Subalgebra.inclusion hAB).toLinearMap) u) = t
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case inr
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 ≠ ⊤
⊢ f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) I

Tactic:
constructor

Goal state after:
case inr.degree_lt
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 ≠ ⊤
⊢ (H.mod f).degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat

case eq_mul_add
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 ≠ ⊤
⊢ f = g * H.div f + ↑(H.mod f)
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
R' : Type u_2
inst✝ : CommRing R'
e : R ≃+* R'
⊢ IsRegularLocalRing R'

Tactic:
have := e.isLocalRing

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
R' : Type u_2
inst✝ : CommRing R'
e : R ≃+* R'
this : IsLocalRing R'
⊢ IsRegularLocalRing 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✝ f'✝ : A⟦X⟧
inst✝ : IsAdicComplete I A
f f' : A⟦X⟧ ⧸ Ideal.span {g}
⊢ Quotient.lift (fun f ↦ H.mod f) ⋯ (f + f') =
    Quotient.lift (fun f ↦ H.mod f) ⋯ f + Quotient.lift (fun f ↦ H.mod f) ⋯ f'

Tactic:
by
    obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f
    obtain ⟨f', rfl⟩ := Ideal.Quotient.mk_surjective f'
    exact H.mod_add f f'

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ (X ^ n).IsWeierstrassDivision g (↑⋯.unit⁻¹) (Polynomial.X ^ n - f)

Tactic:
constructor

Goal state after:
case degree_lt
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ⋯
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ (Polynomial.X ^ n - f).degree < ↑((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) g).order.toNat

case eq_mul_add
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ⋯
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ X ^ n = g * ↑⋯.unit⁻¹ + ↑(Polynomial.X ^ n - f)
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R S
L : Type u_5
inst✝⁴ : Field L
inst✝³ : Algebra R L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R K L
inst✝ : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := (Algebra.TensorProduct.cancelBaseChange R K K L S).symm
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
⊢ Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) =
    ((↑e.symm).comp ↑e2.symm).comp (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L))

Tactic:
ext

Goal state after:
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R S
L : Type u_5
inst✝⁴ : Field L
inst✝³ : Algebra R L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R K L
inst✝ : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := (Algebra.TensorProduct.cancelBaseChange R K K L S).symm
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
x✝ : S
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            (((↑e.symm).comp ↑e2.symm).comp (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L)))).comp
        Algebra.TensorProduct.includeRight)
      x✝
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: 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))
⊢ (↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I)) ∘ₗ lTensor (↥I) f =
    f ∘ₗ ↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)

Tactic:
ext

Goal state after:
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))
x✝¹ : ↥I
x✝ : M
⊢ ((TensorProduct.AlgebraTensorModule.curry
          ((↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I)) ∘ₗ lTensor (↥I) f))
        x✝¹)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (f ∘ₗ ↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I))) x✝¹)
      x✝
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: 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)
⊢ ((↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I)) ∘ₗ lTensor (↥I) f) y = 0

Tactic:
comm1,

Goal state after:
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)
⊢ (f ∘ₗ ↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = 0
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: 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
⊢ (↑(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)

Tactic:
ext

Goal state after:
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
x✝¹ : ↥I
x✝ : ↥f.ker
⊢ ((TensorProduct.AlgebraTensorModule.curry
          ((↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) ∘ₗ lTensor (↥I) f.ker.subtype))
        x✝¹)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
          (f.ker.subtype ∘ₗ ↑(TensorProduct.lid R ↥f.ker) ∘ₗ rTensor (↥f.ker) (Submodule.subtype I)))
        x✝¹)
      x✝
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
inst✝¹ : IsDomain R
inst✝ : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible 1
⊢ h = trivialRel

Tactic:
ext

Goal state after:
R Γ : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
inst✝¹ : IsDomain R
inst✝ : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible 1
x✝¹ x✝ : R
⊢ x✝¹ ≤ᵥ x✝ ↔ x✝¹ ≤ᵥ x✝
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
⊢ Subsingleton (ValueGroupWithZero R)ˣ

Tactic:
constructor

Goal state after:
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
⊢ ∀ (a b : (ValueGroupWithZero R)ˣ), a = b
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
⊢ (zmodEquivTrunc p n).symm.toRingHom.comp (truncate hm) =
    (ZMod.castHom ⋯ (ZMod (p ^ n))).comp (zmodEquivTrunc p m).symm.toRingHom

Tactic:
ext

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x✝ : TruncatedWittVector p m (ZMod p)
⊢ ((zmodEquivTrunc p n).symm.toRingHom.comp (truncate hm)) x✝ =
    ((ZMod.castHom ⋯ (ZMod (p ^ n))).comp (zmodEquivTrunc p m).symm.toRingHom) x✝
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
⊢ b.coeff 0 ≠ 0

Tactic:
contrapose hc

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
hc : b.coeff 0 = 0
⊢ b.coeff 0 ^ p ^ m = 0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((rename (Prod.mk 0)) (wittPolynomial p ℤ n)).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
refine Subset.trans (vars_rename _ _) ?_

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ image (Prod.mk 0) (wittPolynomial p ℤ n).vars ⊆ univ ×ˢ range (n + 1)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((rename (Prod.mk 1)) (wittPolynomial p ℤ n)).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
refine Subset.trans (vars_rename _ _) ?_

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ image (Prod.mk 1) (wittPolynomial p ℤ n).vars ⊆ univ ×ˢ range (n + 1)
Module: Mathlib.RingTheory.ZMod.Torsion

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ rootsOfUnity (p - 1) (ZMod p) = ⊤

Tactic:
ext

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ : (ZMod p)ˣ
⊢ x✝ ∈ rootsOfUnity (p - 1) (ZMod p) ↔ x✝ ∈ ⊤
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y : List A
⊢ subAt (subAt T x) y = subAt T (x ++ y)

Tactic:
ext

Goal state after:
A : Type u_1
T : ↥(tree A)
x y x✝ : List A
⊢ x✝ ∈ subAt (subAt T x) y ↔ x✝ ∈ subAt T (x ++ y)
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case neg
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)

Tactic:
constructor

Goal state after:
case neg.mp
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
⊢ z ∈ pullSub (pullSub T y) x → z ∈ pullSub T (x ++ y)

case neg.mpr
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
⊢ z ∈ pullSub T (x ++ y) → z ∈ pullSub (pullSub T y) x
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ x ≤ ⨆ b, lfpApprox f x ↑b ∧ ∀ (i : Ordinal.{u}), ⨆ (_ : i < a), f (lfpApprox f x i) ≤ ⨆ b, lfpApprox f x ↑b

Tactic:
constructor

Goal state after:
case left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ x ≤ ⨆ b, lfpApprox f x ↑b

case right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ ∀ (i : Ordinal.{u}), ⨆ (_ : i < a), f (lfpApprox f x i) ≤ ⨆ b, lfpApprox f x ↑b
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ l₁.toList → a ∈ l₂
⊢ l₁ ⊆ l₂

Tactic:
by
    induction l₁ using recOfList with | _ l₁
    induction l₁ with
    | nil => exact Subset.nil
    | cons h t t_ih =>
      simp only [to_ofList, ofList, toList_cons, List.mem_cons, forall_eq_or_imp] at *
      exact cons_subset.2 ⟨H.1, t_ih H.2⟩

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l : Lists' α true
x✝ : IsList ⟨true, l⟩
⊢ ofList (toList ⟨true, l⟩) = ⟨true, l⟩

Tactic:
simp_all [ofList, of']

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: 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₁

Tactic:
constructor

Goal state after:
case C1.antisymm.antisymm.left
α : 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₂✝

case C1.antisymm.antisymm.right
α : 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₁
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj : ¬Set.InjOn (lfpApprox f x) (Set.Iio (SuccOrder.succ #α).ord)
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

Tactic:
Set.injOn_iff_injective,

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj : ¬Injective ((Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x))
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) ((log b o, o / b ^ log b o).1 :: map Prod.fst (CNF b (o % b ^ log b o)))

Tactic:
pairwise_cons

Goal state after:
case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ (∀ a' ∈ map Prod.fst (CNF b (o % b ^ log b o)), (log b o, o / b ^ log b o).1 > a') ∧
    List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case atom
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ ⟨false, Lists'.atom a✝⟩ = ⟨false, l₂⟩ ↔ Lists'.atom a✝ = l₂

Tactic:
constructor

Goal state after:
case atom.mp
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ ⟨false, Lists'.atom a✝⟩ = ⟨false, l₂⟩ → Lists'.atom a✝ = l₂

case atom.mpr
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ Lists'.atom a✝ = l₂ → ⟨false, Lists'.atom a✝⟩ = ⟨false, l₂⟩