mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: 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 = ⊥
⊢ I ∈ {m | Nonempty (↥m ≃ₗ[R] ↥I)}

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 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
⊢ IsSemisimpleRing R

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : IsSimpleRing R
⊢ [IsSemisimpleRing R, IsArtinianRing R, ∃ I, IsAtom I].TFAE

Tactic:
by

Goal state after:
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
m : Submodule R M
ne : m ≠ ⊥
⊢ m = isotypicComponent R M S → IsIsotypicOfType R (↥m) S ∧ m.IsFullyInvariant

Tactic:
by

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

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
⊢ m ∈ isotypicComponents R M → IsIsotypic R ↥m ∧ m.IsFullyInvariant ∧ m ≠ ⊥

Tactic:
by

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

Goal state after:
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)
S : Submodule R M
x✝ : S ∈ {m_1 | IsSimpleModule R ↥m_1 ∧ m_1 ≤ ↑m}
simple : IsSimpleModule R ↥S
le : S ≤ ↑m
⊢ isotypicComponent R M ↥S ≤ ↑(⨆ i ∈ (fun m ↦ {c | ↑c ≤ ↑m}) m, ⟨↑i, ⋯⟩)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
right✝ : IsArtinianRing R
this : IsSemisimpleRing R
x✝ : (Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤) ∧ IsArtinianRing R
left✝ : Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
⊢ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R

Tactic:
by

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : Ring R
right✝ : IsArtinianRing R
this : IsSemisimpleRing R
x✝ : (Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤) ∧ IsArtinianRing R
left✝ : Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
⊢ IsSemisimpleRing R ∧ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R

Tactic:
exact ⟨this, by rwa [and_comm]⟩

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ IsSimpleRing R ∧ IsArtinianRing R ↔ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R

Tactic:
by

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

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
⊢ m.IsFullyInvariant ↔ ∃ s ⊆ isotypicComponents R M, m = sSup s

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
⊢ ∃ n, ∃ (_ : NeZero n), ∃ I, ∃ (_ : IsSimpleModule R ↥I), Nonempty (R ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
⊢ ∃ n, ∃ (_ : NeZero n), ∃ D x, Nonempty (R ≃+* Matrix (Fin n) (Fin n) D)

Tactic:
by

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

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
⊢ ∃ n,
    ∃ (_ : NeZero n), ∃ I, ∃ (_ : IsSimpleModule R ↥I), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)

Tactic:
have ⟨n, hn, S, hS, ⟨e⟩⟩ := (isIsotypic R R).linearEquiv_fun
  refine ⟨n, hn, S, hS, ⟨.trans (.opOp R₀ R) <| .trans (.op ?_) (.symm .mopMatrix)⟩⟩
  exact .trans (.moduleEndSelf R₀) <| .trans (e.conjAlgEquiv R₀) (endVecAlgEquivMatrixEnd ..)

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

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
⊢ ∃ n,
    ∃ (_ : NeZero n), ∃ I, ∃ (_ : IsSimpleModule R ↥I), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)

Tactic:
by

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

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
⊢ ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

Tactic:
by

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

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁵ : CommSemiring R₀
inst✝⁴ : Ring R
inst✝³ : Algebra R₀ R
inst✝² : IsSimpleRing R
inst✝¹ : IsArtinianRing R
inst✝ : Module.Finite R₀ R
⊢ ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, ∃ (_ : Module.Finite R₀ D), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

Tactic:
by

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

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁸ : CommSemiring R₀
inst✝⁷ : Ring R
inst✝⁶ : Algebra R₀ R
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite R M
⊢ ∃ n S d,
    (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧
      (∀ (i : Fin n), NeZero (d i)) ∧
        Nonempty (End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (End R ↥(S i)))

Tactic:
by

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

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁸ : CommSemiring R₀
inst✝⁷ : Ring R
inst✝⁶ : Algebra R₀ R
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite R M
⊢ ∃ n D d x x_1,
    (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))

Tactic:
by

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

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝³ : CommSemiring R₀
inst✝² : Ring R
inst✝¹ : Algebra R₀ R
inst✝ : IsSemisimpleRing R
⊢ ∃ n D d x x_1, (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))

Tactic:
by

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

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSemisimpleRing R
inst✝ : Module.Finite R₀ R
n : ℕ
D : Fin n → Type u
d : Fin n → ℕ
w✝¹ : (i : Fin n) → DivisionRing (D i)
w✝ : (i : Fin n) → Algebra R₀ (D i)
hd : ∀ (i : Fin n), NeZero (d i)
e : R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)
this : Module.Finite R₀ ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
i : Fin n
l : ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)) →ₗ[R₀] D i :=
  Matrix.entryLinearMap R₀ (D i) 0 0 ∘ₗ LinearMap.proj i
x : D i
⊢ (l fun j x_1 x_2 ↦ Function.update (fun x ↦ 0) i x j) = x

Tactic:
by

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

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSemisimpleRing R
inst✝ : Module.Finite R₀ R
⊢ ∃ n D d x x_1,
    ∃ (_ : ∀ (i : Fin n), Module.Finite R₀ (D i)),
      (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Topology

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ range toPrimeSpectrum = {x | IsClosed {x}}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Topology

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : MaximalSpectrum R
⊢ toPrimeSpectrum ⁻¹' {x.toPrimeSpectrum} = {x}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (imageOfDf f)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ imageOfDf f = PrimeSpectrum.comap C '' (zeroLocus {f})ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ IsOpenMap (PrimeSpectrum.comap C)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ (List.map f l).sum ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ (Multiset.map f s).sum ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ s.sum f ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∃ x ∈ l, f x ∈ I
⊢ (List.map f l).prod ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∃ x ∈ s, f x ∈ I
⊢ (Multiset.map f s).prod ∈ I

Tactic:
rcases s
  simpa using listProd_mem (hl := hs)

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∃ x ∈ s, f x ∈ I
⊢ (Multiset.map f s).prod ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∃ x ∈ s, f x ∈ I
⊢ s.prod f ∈ I

Tactic:
by

Goal state after:
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
⊢ Function.Injective (comap f)

Tactic:
by

Goal state after:
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 s) = comap f ⁻¹' ↑(basicOpen r)

Tactic:
by

Goal state after:
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
⊢ IsHomeomorph (comap f)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
⊢ IsHomeomorph (comap (algebraMap R (R ⊗[k] K)))

Tactic:
by

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

Goal state after:
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
⊢ IsHomeomorph (comap (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S)).toRingHom)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact

Goal state before:
pp: R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : IsBaseChange S h₁
isb₂ : IsBaseChange S h₂
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
⊢ IsBaseChange S h₃

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: n : ℕ
⊢ moebius n = ArithmeticFunction.moebius n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
⊢ moebius 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ moebius 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : Associated a b
⊢ moebius a = moebius b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : IsUnit a
⊢ moebius a = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
⊢ moebius a = -1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.AlgebraInstances

Goal state before:
pp: K : Type u_1
inst✝² : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : ↥(integralClosure (↥v.valuationSubring) L)
⊢ IsIntegral (↥v.valuationSubring) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.AlgebraInstances

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
E : Type ?u.16
inst✝³ : Field E
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
⊢ ↑⟨(algebraMap L E) ↑1, ⋯⟩ = ↑1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.AlgebraInstances

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
E : Type ?u.16
inst✝³ : Field E
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
x y : ↥(integralClosure (↥v.valuationSubring) L)
⊢ ↑⟨(algebraMap L E) ↑(x * y), ⋯⟩ = ↑(⟨(algebraMap L E) ↑x, ⋯⟩ * ⟨(algebraMap L E) ↑y, ⋯⟩)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.AlgebraInstances

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
E : Type ?u.16
inst✝³ : Field E
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
⊢ ↑⟨(algebraMap L E) ↑0, ⋯⟩ = ↑0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.AlgebraInstances

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
E : Type ?u.16
inst✝³ : Field E
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
x y : ↥(integralClosure (↥v.valuationSubring) L)
⊢ ↑⟨(algebraMap L E) ↑(x + y), ⋯⟩ = ↑(⟨(algebraMap L E) ↑x, ⋯⟩ + ⟨(algebraMap L E) ↑y, ⋯⟩)

Tactic:
by

Goal state after:
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
⊢ Function.Injective ⇑(↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.Minpoly

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : K
⊢ v ((minpoly K ((algebraMap K L) x)).coeff 0) = v x

Tactic:
by

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

Goal state after:
Module: Mathlib.RingTheory.Valuation.Minpoly

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
hx : IsUnit x
⊢ v ((minpoly K x).coeff 0) ^ (finrank K L / (minpoly K x).natDegree) ≠ 0

Tactic:
by

Goal state after:
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)
⊢ (lTensor (↥I) f) y = 0

Tactic:
by

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

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

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
q : R ⧸ J
a b : R
h : (Submodule.quotientRel J) a b
⊢ v a = v (b + -(-a + b))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
⊢ J ≤ (comap (Ideal.Quotient.mk J) v).supp

Tactic:
by

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

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
⊢ ∀ (r : R ⧸ J), ((comap (Ideal.Quotient.mk J) v).onQuot ⋯) r = v r

Tactic:
by

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

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ (v.onQuot hJ).supp = Ideal.map (Ideal.Quotient.mk J) v.supp

Tactic:
by

Goal state after: