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

Goal state before:
pp: n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Nontrivial R
this✝³ : Nontrivial S
U : Type u
w✝¹ : CommRing U
w✝ : Algebra S U
e : S ⊗[R] S ≃ₐ[S] S × U
algInst✝ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝² : IsScalarTower S (S × U) U
this✝¹ : Etale S U
this✝ : Module.Finite S U
this : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n + 1
⊢ Module.rankAtStalk U = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale R S
inst✝ : WeaklyEtale S T
⊢ WeaklyEtale R T

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R✝ : Type u
S✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
inst✝³ : Algebra R✝ S✝
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (IsScalarTower.toAlgHom R P.extendScalars.Ring S).comp (IsScalarTower.toAlgHom R P.Ring P.extendScalars.Ring) =
    (IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R P.Ring S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Finite

Goal state before:
pp: R : Type u
inst✝⁷ : CommRing R
k : Type u
inst✝⁶ : Field k
Ω : Type w
inst✝⁵ : Field Ω
inst✝⁴ : Algebra R Ω
S : Type w
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra S Ω
inst✝ : IsScalarTower R S Ω
A B : FiniteEtale R
f : A ⟶ B
⊢ (baseChange R R).map f ≫ (isoMk (Algebra.TensorProduct.lid R ↑B.obj)).hom =
    (isoMk (Algebra.TensorProduct.lid R ↑A.obj)).hom ≫ (𝟭 (FiniteEtale R)).map f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ ↑P.cotangentExtendScalarsEquiv.symm = Cotangent.map P.toExtendScalars

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Finite

Goal state before:
pp: R✝ : Type u
inst✝⁹ : CommRing R✝
k : Type u
inst✝⁸ : Field k
Ω✝ : Type w
inst✝⁷ : Field Ω✝
inst✝⁶ : Algebra R✝ Ω✝
S✝ : Type w
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
inst✝³ : Algebra S✝ Ω✝
inst✝² : IsScalarTower R✝ S✝ Ω✝
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
R S : (FiniteEtale Ω)ᵒᵖ
f : R ⟶ S
⊢ (finiteSpec Ω ⋙
            { obj := fun X ↦ Opposite.op (of Ω (X.obj → Ω)),
              map := fun {X Y} f ↦
                (ofHom (AlgHom.pi fun i ↦ Pi.evalAlgHom Ω (fun a ↦ Ω) ((ConcreteCategory.hom f) i))).op,
              map_id := ⋯, map_comp := ⋯ }).map
        f ≫
      (isoMk (Algebra.FormallyEtale.equivPiOfIsSepClosed Ω ↑(Opposite.unop S).obj)).op.hom =
    (isoMk (Algebra.FormallyEtale.equivPiOfIsSepClosed Ω ↑(Opposite.unop R).obj)).op.hom ≫ (𝟭 (FiniteEtale Ω)ᵒᵖ).map f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Function.Injective ⇑(map P.toExtendScalars)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: n✝ : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n✝ →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n✝ + 1)
h✝ : Nontrivial R
this✝⁴ : Nontrivial S
U : Type u
w✝⁶ : CommRing U
w✝⁵ : Algebra S U
e✝ : S ⊗[R] S ≃ₐ[S] S × U
algInst✝¹ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝³ : IsScalarTower S (S × U) U
this✝² : Etale S U
this✝¹ : Module.Finite S U
this✝ : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n✝ + 1
this : Module.rankAtStalk U = ↑n✝
V : Type u
w✝⁴ : CommRing V
w✝³ : Algebra S V
w✝² : Module.FaithfullyFlat S V
w✝¹ : Module.Finite S V
w✝ : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst✝ : Algebra R V := ((algebraMap S V).comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S V := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R V))
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  (TensorProduct.cancelBaseChange R S V V S).symm.trans
    ((TensorProduct.congr AlgEquiv.refl e✝).trans
      ((TensorProduct.prodRight S V V S U).trans
        (((TensorProduct.rid S V V).prodCongr f).trans
          (((AlgEquiv.funUnique V Unit V).symm.prodCongr AlgEquiv.refl).trans
            (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V).symm))))
⊢ Module.FaithfullyFlat R S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R✝ : Type u
S✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
inst✝³ : Algebra R✝ S✝
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (IsScalarTower.toAlgHom P.Ring (Generators.self P.Ring S).toExtension.Ring S).comp
      (ofId P.Ring (Generators.self P.Ring S).toExtension.Ring) =
    (IsScalarTower.toAlgHom P.Ring S S).comp (IsScalarTower.toAlgHom P.Ring P.extendScalars.Ring S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R✝ : Type u
S✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
inst✝³ : Algebra R✝ S✝
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
h : Function.Surjective ⇑(algebraMap R P.Ring)
x : P.Cotangent
⊢ x ∈ P.cotangentComplex.ker

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Finite

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
k : Type u
inst✝⁸ : Field k
Ω✝ : Type w
inst✝⁷ : Field Ω✝
inst✝⁶ : Algebra R Ω✝
S : Type w
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Ω✝
inst✝² : IsScalarTower R S Ω✝
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
X : FintypeCat
⊢ { obj := fun X ↦ Opposite.op (of Ω (X.obj → Ω)),
            map := fun {X Y} f ↦
              (ofHom (AlgHom.pi fun i ↦ Pi.evalAlgHom Ω (fun a ↦ Ω) ((ConcreteCategory.hom f) i))).op,
            map_id := ⋯, map_comp := ⋯ }.map
        ((NatIso.ofComponents
                (fun X ↦
                  FintypeCat.equivEquivIso
                    ((Equiv.sigmaUnique ((𝟭 FintypeCat).obj X).obj fun a ↦ PrimeSpectrum Ω).symm.trans
                      (PrimeSpectrum.sigmaToPiHomeo fun a ↦ Ω).toEquiv))
                ⋯).hom.app
          X) ≫
      (NatIso.ofComponents (fun R ↦ (isoMk (Algebra.FormallyEtale.equivPiOfIsSepClosed Ω ↑(Opposite.unop R).obj)).op)
              ⋯).hom.app
        ({ obj := fun X ↦ Opposite.op (of Ω (X.obj → Ω)),
              map := fun {X Y} f ↦
                (ofHom (AlgHom.pi fun i ↦ Pi.evalAlgHom Ω (fun a ↦ Ω) ((ConcreteCategory.hom f) i))).op,
              map_id := ⋯, map_comp := ⋯ }.obj
          X) =
    𝟙
      ({ obj := fun X ↦ Opposite.op (of Ω (X.obj → Ω)),
            map := fun {X Y} f ↦
              (ofHom (AlgHom.pi fun i ↦ Pi.evalAlgHom Ω (fun a ↦ Ω) ((ConcreteCategory.hom f) i))).op,
            map_id := ⋯, map_comp := ⋯ }.obj
        X)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Ring
x_in : x ∈ P.ker
property✝ : Cotangent.mk ⟨x, x_in⟩ ∈ P.extendScalars.cotangentComplex.ker
⊢ (algebraMap P.Ring (Generators.self P.Ring S).toExtension.Ring) x ∈ (Generators.self P.Ring S).toExtension.ker

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.LocallyFree

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Flat R M
p : Ideal R
inst✝ : p.IsPrime
h :
  ∀ (m : Ideal R) [inst : m.IsMaximal],
    rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }
h✝ : Nontrivial R
Rₚ : Type u_1 := Localization.AtPrime p
n : ℕ := rankAtStalk M { asIdeal := p, isPrime := ⋯ }
f : (Fin n →₀ R) →ₗ[R] Fin n →₀ Rₚ := Finsupp.mapRange.linearMap (Algebra.linearMap R Rₚ)
g : M →ₗ[R] LocalizedModule.AtPrime p M := mkLinearMap p.primeCompl M
φ : (Fin n →₀ R) →ₗ[R] M
hφps : Function.Surjective ⇑((IsLocalizedModule.map p.primeCompl f g) φ)
⊢ ?m.274

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ P.cotangentComplex ∘ₗ ↑P.h1CotangentEquivCotangent = H1Cotangent.δ R P.Ring S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.LocallyFree

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Flat R M
p : Ideal R
inst✝ : p.IsPrime
h :
  ∀ (m : Ideal R) [inst : m.IsMaximal],
    rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }
⊢ ∃ a ∉ p, Free (Localization.Away a) (LocalizedModule.Away a M)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
n : ℕ
hn : Module.rankAtStalk S = ↑n
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
⊢ ∀ (n : ℕ), n ≠ 0 → hI.dpow n z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
⊢ hI.dpow k z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal :=
  { carrier := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}, isSubideal := ⋯, dpow_mem := ⋯ }
x : A
hx : x ∈ S
⊢ x = hI.dpow 1 x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ ↑P.h1CotangentEquivCotangent ∘ₗ Algebra.H1Cotangent.map R P.Ring S S =
    h1Cotangentι ∘ₗ H1Cotangent.map (defaultHom R S P)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Function.Surjective ⇑(map (defaultHom R S P))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal :=
  { carrier := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}, isSubideal := ⋯, dpow_mem := ⋯ }
K : hI.SubDPIdeal
hK : K ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
⊢ S ⊆ ↑K

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ (SubDPIdeal.span hI S).carrier = span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
⊢ hI.IsSubDPIdeal (RingHom.ker f ⊓ I)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : hI.DPMorphism hJ
x✝ : ℕ
hn : x✝ ≠ 0
a : A
⊢ a ∈ RingHom.ker f.toRingHom ⊓ I → hI.dpow x✝ a ∈ RingHom.ker f.toRingHom ⊓ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a b : A
ha : a ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
hb : b ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
n : ℕ
k : ℕ × ℕ
x✝ : k ∈ Finset.antidiagonal n
⊢ hI.dpow k.1 a * hI.dpow k.2 b = hI'.dpow k.1 a * hI'.dpow k.2 b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a b : A
ha : a ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
hb : b ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
⊢ a + b ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
⊢ 0 ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a x : A
hx : x ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
n : ℕ
⊢ hI.dpow n (a * x) = hI'.dpow n (a * x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a x : A
hx : x ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
⊢ a • x ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x : A
⊢ x ∈ hI.dpEqualizer hI' ↔ x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x✝ : ℕ
hn : x✝ ≠ 0
x : A
hx : x ∈ hI.dpEqualizer hI'
m : ℕ
⊢ hI.dpow m (hI.dpow x✝ x) = hI'.dpow m (hI.dpow x✝ x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x✝ : ℕ
hn : x✝ ≠ 0
x : A
hx : x ∈ hI.dpEqualizer hI'
m : ℕ
⊢ hI.dpow m (hI'.dpow x✝ x) = hI'.dpow m (hI'.dpow x✝ x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
a : A
ha : a ∈ ↑I
n : ℕ
⊢ hK.dpow n (f a) = hK'.dpow n (f a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
⊢ Ideal.map f I ≤ hK.dpEqualizer hK'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A✝ : Type u_1
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ hI' : DividedPowers I✝
A : Type u_2
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
⊢ J ⊓ I ≤ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A✝ : Type u_1
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ hI' : DividedPowers I✝
A : Type u_2
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
x✝¹ : ℕ
hn : x✝¹ ≠ 0
a : A
x✝ : a ∈ J ⊓ I
haJ : a ∈ ↑J
haI : a ∈ ↑I
ha0 : φ.toRingHom a = 0
⊢ hJ.dpow x✝¹ (φ.toRingHom a) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A✝ : Type u_1
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ hI' : DividedPowers I✝
A : Type u_2
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
x✝¹ : ℕ
hn : x✝¹ ≠ 0
a : A
x✝ : a ∈ J ⊓ I
haJ : a ∈ ↑J
haI : a ∈ ↑I
⊢ hI.dpow x✝¹ a ∈ J ⊓ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ ∃ a_1, f ↑a_1 = f a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ dpow hI f n (f a) = f (hI.dpow n a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hx' : x ∉ J
⊢ dpow hI f n x = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
x : B
hx : x ∈ J
⊢ dpow hI f 0 x = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
x : B
hx : x ∈ J
⊢ dpow hI f 1 x = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S
⊢ (Ideal.Quotient.mk Q) (φ x) = (Ideal.Quotient.mk Q) x ^ Nat.card (R ⧸ Ideal.under R Q)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
h : Infinite (R ⧸ Ideal.under R Q)
⊢ Q = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
⊢ dpow hI f n x ∈ J

Tactic:
rw [hIJ] at hx ⊢
    obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp hx
    rw [dpow_apply' hI hIf ha]
    exact mem_map_of_mem _ (hI.dpow_mem hn ha)

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
⊢ dpow hI f n x ∈ J

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
⊢ _root_.Finite (R ⧸ Ideal.under R Q)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
⊢ Q ≤ Ideal.comap φ Q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : R ⧸ Ideal.under R Q
⊢ (↑↑(Ideal.quotientMap Q ↑φ ⋯)).toFun ((algebraMap (R ⧸ Ideal.under R Q) (S ⧸ Q)) x) =
    (algebraMap (R ⧸ Ideal.under R Q) (S ⧸ Q)) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S ⧸ Q
⊢ H.restrict x = x ^ Nat.card (R ⧸ Ideal.under R Q)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n✝ : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
b : A
hb : b ∈ I
hy : f b ∈ J
k : ℕ × ℕ
x✝ : k ∈ Finset.antidiagonal n✝
⊢ f (hI.dpow k.1 a * hI.dpow k.2 b) = dpow hI f k.1 (f a) * dpow hI f k.2 (f b)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n✝ : ℕ
x✝ y✝ : B
hx : x✝ ∈ J
hy : y✝ ∈ J
⊢ dpow hI f n✝ (x✝ + y✝) = ∑ k ∈ Finset.antidiagonal n✝, dpow hI f k.1 x✝ * dpow hI f k.2 y✝

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ Function.Injective ⇑H.restrict

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x y : B
hy : y ∈ J
⊢ dpow hI f n (x * y) = x ^ n * dpow hI f n y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ Ideal.comap φ Q = Q

Tactic:
by

Goal state after: