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

Goal state before:
pp: case hh'
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
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
s' : Finset T := ⋯
h' : ↥(φ R s).range →ₐ[R] ↥(φ R s').range := ⋯
j : Fin s.card → Fin s'.card := ⋯
eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M := ⋯
ha' : π R M T ⟨s', p'⟩ = (rTensor M h.toLinearMap) t
⊢ (φ R s').range.val.comp h' = h.comp (φ R s).range.val

pp: case hpq
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
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
s' : Finset T := ⋯
h' : ↥(φ R s).range →ₐ[R] ↥(φ R s').range := ⋯
j : Fin s.card → Fin s'.card := ⋯
eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M := ⋯
ha' : π R M T ⟨s', p'⟩ = (rTensor M h.toLinearMap) t
⊢ (rTensor M (h'.comp (φ R s).rangeRestrict).toLinearMap) p = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'

Tactic:
· simp only [val_comp_codRestrict, h']

Goal state after:
case hpq
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
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
s' : Finset T := ⋯
h' : ↥(φ R s).range →ₐ[R] ↥(φ R s').range := ⋯
j : Fin s.card → Fin s'.card := ⋯
eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M := ⋯
ha' : π R M T ⟨s', p'⟩ = (rTensor M h.toLinearMap) t
⊢ (rTensor M (h'.comp (φ R s).rangeRestrict).toLinearMap) p = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
h✝ : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
f : A[X]
⊢ f /ₘ g * g = f - (f - g * (f /ₘ g))

Tactic:
;

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
h✝ : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
f : A[X]
⊢ f /ₘ g * g = f - (f - g * (f /ₘ g))
Module: Mathlib.RingTheory.RingInvo

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : EquivLike F R Rᵐᵒᵖ
f : RingInvo R
tE : R ≃ Rᵐᵒᵖ
map_mul'✝ : ∀ (x y : R), tE.toFun (x * y) = tE.toFun x * tE.toFun y
map_add'✝ : ∀ (x y : R), tE.toFun (x + y) = tE.toFun x + tE.toFun y
involution'✝ :
  ∀ (x : R),
    MulOpposite.unop
        ({ toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toFun
          (MulOpposite.unop ({ toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toFun x))) =
      x
h₁ : { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝, involution' := involution'✝ }.toFun = f.toFun
h₂ : { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝, involution' := involution'✝ }.invFun = f.invFun
⊢ { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝, involution' := involution'✝ } = f

Tactic:
;

Goal state after:
F : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : EquivLike F R Rᵐᵒᵖ
f : RingInvo R
tE : R ≃ Rᵐᵒᵖ
map_mul'✝ : ∀ (x y : R), tE.toFun (x * y) = tE.toFun x * tE.toFun y
map_add'✝ : ∀ (x y : R), tE.toFun (x + y) = tE.toFun x + tE.toFun y
involution'✝ :
  ∀ (x : R),
    MulOpposite.unop
        ({ toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toFun
          (MulOpposite.unop ({ toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toFun x))) =
      x
h₁ : { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝, involution' := involution'✝ }.toFun = f.toFun
h₂ : { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝, involution' := involution'✝ }.invFun = f.invFun
⊢ { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝, involution' := involution'✝ } = f
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
g' : A⟦X⟧
f' : A[X]
h' : A⟦X⟧
H' : g'.IsWeierstrassFactorizationAt f' h' I
⊢ ↑f * h * (↑f' * h') = ↑f * ↑f' * (h * h')

Tactic:
;

Goal state after:
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
g' : A⟦X⟧
f' : A[X]
h' : A⟦X⟧
H' : g'.IsWeierstrassFactorizationAt f' h' I
⊢ ↑f * h * (↑f' * h') = ↑f * ↑f' * (h * h')
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
this : f.degree = ↑n
⊢ WithBot.unbotD 0 ↑n = n

Tactic:
;

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
this : f.degree = ↑n
⊢ WithBot.unbotD 0 ↑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
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule R ↥S
e : Nonempty (M ≃ₗ[R] Fin 0 → ↥S)
⊢ False

Tactic:
;

Goal state after:
R : Type u_2
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsSemisimpleModule R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule R ↥S
e : Nonempty (M ≃ₗ[R] Fin 0 → ↥S)
⊢ False
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
w✝ : Submodule R M
left✝ : IsSimpleModule R ↥w✝
⊢ ⊥ < isotypicComponent R M ↥w✝

Tactic:
;

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
w✝ : Submodule R M
left✝ : IsSimpleModule R ↥w✝
⊢ ⊥ < isotypicComponent R M ↥w✝
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✝
S : Submodule R M
left✝ : IsSimpleModule R ↥S
⊢ IsSemisimpleModule R ↥↑⟨isotypicComponent R M ↥S, ⋯⟩

Tactic:
;

Goal state after:
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✝
S : Submodule R M
left✝ : IsSimpleModule R ↥S
⊢ IsSemisimpleModule R ↥↑⟨isotypicComponent R M ↥S, ⋯⟩
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
w✝ : Submodule R M
left✝ : IsSimpleModule R ↥w✝
⊢ IsIsotypic R ↥(isotypicComponent R M ↥w✝)

Tactic:
;

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
w✝ : Submodule R M
left✝ : IsSimpleModule R ↥w✝
⊢ IsIsotypic R ↥(isotypicComponent R M ↥w✝)
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
S : Submodule R M
left✝ : IsSimpleModule R ↥S
s : Set (Submodule R M) := isotypicComponents R M \ {isotypicComponent R M ↥S}
ne : ¬isotypicComponent R M ↥S ⊓ sSup s = ⊥
⊢ IsSemisimpleModule R ↥(isotypicComponent R M ↥S)

Tactic:
;

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
left✝ : IsSimpleModule R ↥S
s : Set (Submodule R M) := isotypicComponents R M \ {isotypicComponent R M ↥S}
ne : ¬isotypicComponent R M ↥S ⊓ sSup s = ⊥
⊢ IsSemisimpleModule R ↥(isotypicComponent R M ↥S)
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
c : Submodule R M
hc : c ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this✝ : IsSemisimpleModule R ↥c
this : IsSemisimpleModule R ↥(c ⊓ sSup s)
w✝ : Submodule R M
left✝ : IsSimpleModule R ↥w✝
right✝ : isotypicComponent R M ↥w✝ ∉ {c}
⊢ IsSemisimpleModule R ↥↑⟨isotypicComponent R M ↥w✝, ⋯⟩

Tactic:
;

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
c : Submodule R M
hc : c ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this✝ : IsSemisimpleModule R ↥c
this : IsSemisimpleModule R ↥(c ⊓ sSup s)
w✝ : Submodule R M
left✝ : IsSimpleModule R ↥w✝
right✝ : isotypicComponent R M ↥w✝ ∉ {c}
⊢ IsSemisimpleModule R ↥↑⟨isotypicComponent R M ↥w✝, ⋯⟩
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✝¹ : IsSimpleModule R S
ι : Type u_5
inst✝ : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : ⨆ i, N i = ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : (i : ι) → Module.End R ↥(N i)
i : ι
x : ↥(N i)
⊢ ↑(((fun f i ↦ LinearMap.restrict f ⋯)
          ((fun f ↦ ↑(ind.linearEquiv iSup_top) ∘ₗ DFinsupp.mapRange.linearMap f ∘ₗ ↑(ind.linearEquiv iSup_top).symm) f)
          i)
        x) =
    ↑((f i) x)

Tactic:
;

Goal state after:
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✝¹ : IsSimpleModule R S
ι : Type u_5
inst✝ : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : ⨆ i, N i = ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : (i : ι) → Module.End R ↥(N i)
i : ι
x : ↥(N i)
⊢ ↑(((fun f i ↦ LinearMap.restrict f ⋯)
          ((fun f ↦ ↑(ind.linearEquiv iSup_top) ∘ₗ DFinsupp.mapRange.linearMap f ∘ₗ ↑(ind.linearEquiv iSup_top).symm) f)
          i)
        x) =
    ↑((f i) x)
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
w✝ : Submodule R M
left✝ : IsSimpleModule R ↥w✝
⊢ (isotypicComponent R M ↥w✝).IsFullyInvariant

Tactic:
;

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
w✝ : Submodule R M
left✝ : IsSimpleModule R ↥w✝
⊢ (isotypicComponent R M ↥w✝).IsFullyInvariant
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
inst✝¹ : IsSimpleModule R S
inst✝ : IsSemisimpleModule R M
ne : isotypicComponent R M S ≠ ⊥
⊢ IsIsotypicOfType R (↥(isotypicComponent R M S)) S ∧ (isotypicComponent R M S).IsFullyInvariant

Tactic:
;

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
inst✝¹ : IsSimpleModule R S
inst✝ : IsSemisimpleModule R M
ne : isotypicComponent R M S ≠ ⊥
⊢ IsIsotypicOfType R (↥(isotypicComponent R M S)) S ∧ (isotypicComponent R M S).IsFullyInvariant
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
S : Submodule R M
left✝ : IsSimpleModule R ↥S
⊢ IsIsotypic R ↥(isotypicComponent R M ↥S) ∧ (isotypicComponent R M ↥S).IsFullyInvariant ∧ isotypicComponent R M ↥S ≠ ⊥

Tactic:
;

Goal state after:
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
S : Submodule R M
left✝ : IsSimpleModule R ↥S
⊢ IsIsotypic R ↥(isotypicComponent R M ↥S) ∧ (isotypicComponent R M ↥S).IsFullyInvariant ∧ isotypicComponent R M ↥S ≠ ⊥
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: case refine_1
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
c : { x // x ∈ isotypicComponents R M }
left✝ : c ∈ OrderIso.setIsotypicComponents.symm ⟨m, h⟩
⊢ ↑c ∈ isotypicComponents R M

Tactic:
;

Goal state after:
case refine_1
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
c : { x // x ∈ isotypicComponents R M }
left✝ : c ∈ OrderIso.setIsotypicComponents.symm ⟨m, h⟩
⊢ ↑c ∈ isotypicComponents R M
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
s : S
n : ℕ
hn : n > 0
r : R
hr : f r = s ^ n
⊢ ↑(basicOpen (f r)) = comap f ⁻¹' ↑(basicOpen r)

Tactic:
;

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
s : S
n : ℕ
hn : n > 0
r : R
hr : f r = s ^ n
⊢ ↑(basicOpen (f r)) = comap f ⁻¹' ↑(basicOpen r)
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)
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✝

Tactic:
;

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.UniqueFactorizationDomain.Moebius

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
⊢ moebius (a * b) = moebius a * moebius b

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : ¬Squarefree a
⊢ moebius (a * b) = moebius a * moebius b

Tactic:
;

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
⊢ moebius (a * b) = moebius a * moebius b

case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : ¬Squarefree a
⊢ moebius (a * b) = moebius a * moebius b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
hb : Squarefree b
⊢ moebius (a * b) = moebius a * moebius b

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
hb : ¬Squarefree b
⊢ moebius (a * b) = moebius a * moebius b

Tactic:
;

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
hb : Squarefree b
⊢ moebius (a * b) = moebius a * moebius b

case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
hb : ¬Squarefree b
⊢ moebius (a * b) = moebius a * moebius b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
hb : Squarefree b
hab : Squarefree (a * b)
⊢ (-1) ^ (factors a + factors b).card = moebius a * moebius b

Tactic:
Multiset.card_add,

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
hb : Squarefree b
hab : Squarefree (a * b)
⊢ (-1) ^ ((factors a).card + (factors b).card) = moebius a * moebius b
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: case pos
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
z✝ y✝ x✝² : R
x✝¹ : if y✝ = 0 then x✝² = 0 else True
x✝ : if z✝ = 0 then y✝ = 0 else True
h✝ : z✝ = 0
⊢ x✝² = 0

Tactic:
;

Goal state after:
case pos
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
z✝ y✝ x✝² : R
x✝¹ : if y✝ = 0 then x✝² = 0 else True
x✝ : if z✝ = 0 then y✝ = 0 else True
h✝ : z✝ = 0
⊢ x✝² = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: case pos
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝² y✝ z✝ : R
x✝¹ : if z✝ = 0 then x✝² = 0 else True
x✝ : if z✝ = 0 then y✝ = 0 else True
h✝ : z✝ = 0
⊢ x✝² + y✝ = 0

Tactic:
;

Goal state after:
case pos
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝² y✝ z✝ : R
x✝¹ : if z✝ = 0 then x✝² = 0 else True
x✝ : if z✝ = 0 then y✝ = 0 else True
h✝ : z✝ = 0
⊢ x✝² + y✝ = 0
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hpi : i ≠ n
hin : i < n
⊢ ↑p ^ i ≠ 0

Tactic:
;

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hpi : i ≠ n
hin : i < n
⊢ ↑p ^ i ≠ 0
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : ↑p ^ i = (WittVector.truncate n) (↑p ^ i)
⊢ ∃ x, ¬coeff x ((WittVector.truncate n) (↑p ^ i)) = coeff x 0

Tactic:
;

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : ↑p ^ i = (WittVector.truncate n) (↑p ^ i)
⊢ ∃ x, ¬coeff x ((WittVector.truncate n) (↑p ^ i)) = coeff x 0
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Fintype.card (TruncatedWittVector p n (ZMod p)) = p ^ n

Tactic:
by
  rw [card, ZMod.card]

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

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

Tactic:
;

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

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

Tactic:
;

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: p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
⊢ a * b ≠ 0

Tactic:
;

Goal state after:
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
⊢ a * b ≠ 0
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
h : a * b = 0
⊢ False

Tactic:
;

Goal state after:
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
h : a * b = 0
⊢ False
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = 0
h : a * b = 0
⊢ False

Tactic:
;

Goal state after:
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = 0
h : a * b = 0
⊢ False