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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ((minpoly R pb.gen).aroots F).prod = ∏ x, ↑x

pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ∀ (x : S →ₐ[R] F), x pb.gen = ↑(pb.liftEquiv' x)

Tactic:
·

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ((minpoly R pb.gen).aroots F).prod = ∏ x, ↑x
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ((minpoly R pb.gen).aroots F).Nodup

pp: case hfg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ∀ (x : { x // x ∈ (minpoly R pb.gen).aroots F }), ↑x = _root_.id ↑x

Tactic:
·

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ((minpoly R pb.gen).aroots F).Nodup
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case hfg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ∀ (x : { x // x ∈ (minpoly R pb.gen).aroots F }), ↑x = _root_.id ↑x

Tactic:
·

Goal state after:
case hfg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ∀ (x : { x // x ∈ (minpoly R pb.gen).aroots F }), ↑x = _root_.id ↑x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : a = 0
⊢ f (a * b) = f a * f b

pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
⊢ f (a * b) = f a * f b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : a = 0
⊢ f (a * b) = f a * f b
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ∀ (x : S →ₐ[R] F), x pb.gen = ↑(pb.liftEquiv' x)

Tactic:
·

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ∀ (x : S →ₐ[R] F), x pb.gen = ↑(pb.liftEquiv' x)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : b = 0
⊢ f (a * b) = f a * f b

pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
⊢ f (a * b) = f a * f b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : b = 0
⊢ f (a * b) = f a * f b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : f 1 = 0
⊢ f (a * b) = f a * f b

pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
⊢ f (a * b) = f a * f b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : f 1 = 0
⊢ f (a * b) = f a * f b
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: case pos
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : P.LiesOver p
⊢ p.inertiaDeg' (comap e P) = p.inertiaDeg' P

pp: case neg
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : ¬P.LiesOver p
⊢ p.inertiaDeg' (comap e P) = p.inertiaDeg' P

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : P.LiesOver p
⊢ p.inertiaDeg' (comap e P) = p.inertiaDeg' P
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: case neg
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : ¬P.LiesOver p
⊢ p.inertiaDeg' (comap e P) = p.inertiaDeg' P

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : ¬P.LiesOver p
⊢ p.inertiaDeg' (comap e P) = p.inertiaDeg' P
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
F : Type u_6
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field F
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K F
E : Type u_7
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra L F
inst✝³ : IsScalarTower K L F
inst✝² : IsAlgClosed E
inst✝¹ : Algebra.IsSeparable K F
inst✝ : FiniteDimensional K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∏ a, ∏ s, ⟨a, s⟩.fst pb.gen = ∏ x, x pb.gen ^ finrank L F

pp: K : Type u_4
L : Type u_5
F : Type u_6
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field F
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K F
E : Type u_7
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra L F
inst✝³ : IsScalarTower K L F
inst✝² : IsAlgClosed E
inst✝¹ : Algebra.IsSeparable K F
inst✝ : FiniteDimensional K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : F →ₐ[K] E), x ((algebraMap L F) pb.gen) = (algHomEquivSigma x).fst pb.gen

Tactic:
·

Goal state after:
K : Type u_4
L : Type u_5
F : Type u_6
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field F
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K F
E : Type u_7
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra L F
inst✝³ : IsScalarTower K L F
inst✝² : IsAlgClosed E
inst✝¹ : Algebra.IsSeparable K F
inst✝ : FiniteDimensional K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∏ a, ∏ s, ⟨a, s⟩.fst pb.gen = ∏ x, x pb.gen ^ finrank L F
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
F : Type u_6
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field F
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K F
E : Type u_7
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra L F
inst✝³ : IsScalarTower K L F
inst✝² : IsAlgClosed E
inst✝¹ : Algebra.IsSeparable K F
inst✝ : FiniteDimensional K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : F →ₐ[K] E), x ((algebraMap L F) pb.gen) = (algHomEquivSigma x).fst pb.gen

Tactic:
·

Goal state after:
K : Type u_4
L : Type u_5
F : Type u_6
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field F
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K F
E : Type u_7
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra L F
inst✝³ : IsScalarTower K L F
inst✝² : IsAlgClosed E
inst✝¹ : Algebra.IsSeparable K F
inst✝ : FiniteDimensional K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : F →ₐ[K] E), x ((algebraMap L F) pb.gen) = (algHomEquivSigma x).fst pb.gen
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case pos
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ∃ s, Nonempty (Basis (↥s) B C)
⊢ e ((norm A) x) = (norm B) x

pp: case neg
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ e ((norm A) x) = (norm B) x

Tactic:
·

Goal state after:
case pos
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ∃ s, Nonempty (Basis (↥s) B C)
⊢ e ((norm A) x) = (norm B) x
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case refine_2
A₁ : Type u_8
B₁ : Type u_9
A₂ : Type u_10
B₂ : Type u_11
inst✝⁵ : CommRing A₁
inst✝⁴ : Ring B₁
inst✝³ : CommRing A₂
inst✝² : Ring B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra' ?refine_1
⊢ (norm A₁) x = e₁.symm ((norm A₂) (e₂ x))

pp: case refine_1
A₁ : Type u_8
B₁ : Type u_9
A₂ : Type u_10
B₂ : Type u_11
inst✝⁵ : CommRing A₁
inst✝⁴ : Ring B₁
inst✝³ : CommRing A₂
inst✝² : Ring B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
⊢ ∀ (c : A₁) (x : B₂), ((↑e₂).comp (algebraMap A₁ B₁)) c * x = x * ((↑e₂).comp (algebraMap A₁ B₁)) c

Tactic:
·

Goal state after:
case refine_2
A₁ : Type u_8
B₁ : Type u_9
A₂ : Type u_10
B₂ : Type u_11
inst✝⁵ : CommRing A₁
inst✝⁴ : Ring B₁
inst✝³ : CommRing A₂
inst✝² : Ring B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra' ?refine_1
⊢ (norm A₁) x = e₁.symm ((norm A₂) (e₂ x))
Module: Mathlib.RingTheory.Artinian.Ring

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
r₂ : R
h : IsLocalization.mk' L 1 s = (algebraMap R L) r₂
⊢ ∃ a, (algebraMap R L) a = IsLocalization.mk' L r₁ s

pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
⊢ ∃ r, IsLocalization.mk' L 1 s = (algebraMap R L) r

Tactic:
·

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
r₂ : R
h : IsLocalization.mk' L 1 s = (algebraMap R L) r₂
⊢ ∃ a, (algebraMap R L) a = IsLocalization.mk' L r₁ s
Module: Mathlib.RingTheory.FiniteStability

Goal state before:
pp: case hf
R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(AlgHom.id R B)

pp: case hg
R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑f

Tactic:
·

Goal state after:
case hf
R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(AlgHom.id R B)
Module: Mathlib.RingTheory.FiniteStability

Goal state before:
pp: case hg
R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑f

Tactic:
·

Goal state after:
case hg
R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑f
Module: Mathlib.RingTheory.FiniteStability

Goal state before:
pp: case refine_1
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
hfgg : (RingHom.ker g).FG
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A := g.comp ↑(MvPolynomial.algebraTensorAlgEquiv R B).symm
⊢ Function.Surjective ⇑g'

pp: case refine_2
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
hfgg : (RingHom.ker g).FG
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A := g.comp ↑(MvPolynomial.algebraTensorAlgEquiv R B).symm
⊢ (RingHom.ker ↑↑(MvPolynomial.algebraTensorAlgEquiv R B).symm).FG

pp: case refine_3
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
hfgg : (RingHom.ker g).FG
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A := g.comp ↑(MvPolynomial.algebraTensorAlgEquiv R B).symm
⊢ Function.Surjective ⇑↑↑(MvPolynomial.algebraTensorAlgEquiv R B).symm

Tactic:
·

Goal state after:
case refine_1
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
hfgg : (RingHom.ker g).FG
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A := g.comp ↑(MvPolynomial.algebraTensorAlgEquiv R B).symm
⊢ Function.Surjective ⇑g'
Module: Mathlib.RingTheory.FiniteStability

Goal state before:
pp: case refine_2
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
hfgg : (RingHom.ker g).FG
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A := g.comp ↑(MvPolynomial.algebraTensorAlgEquiv R B).symm
⊢ (RingHom.ker ↑↑(MvPolynomial.algebraTensorAlgEquiv R B).symm).FG

pp: case refine_3
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
hfgg : (RingHom.ker g).FG
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A := g.comp ↑(MvPolynomial.algebraTensorAlgEquiv R B).symm
⊢ Function.Surjective ⇑↑↑(MvPolynomial.algebraTensorAlgEquiv R B).symm

Tactic:
·

Goal state after:
case refine_2
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
hfgg : (RingHom.ker g).FG
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A := g.comp ↑(MvPolynomial.algebraTensorAlgEquiv R B).symm
⊢ (RingHom.ker ↑↑(MvPolynomial.algebraTensorAlgEquiv R B).symm).FG
Module: Mathlib.RingTheory.FiniteStability

Goal state before:
pp: case refine_3
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
hfgg : (RingHom.ker g).FG
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A := g.comp ↑(MvPolynomial.algebraTensorAlgEquiv R B).symm
⊢ Function.Surjective ⇑↑↑(MvPolynomial.algebraTensorAlgEquiv R B).symm

Tactic:
·

Goal state after:
case refine_3
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
hfgg : (RingHom.ker g).FG
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A := g.comp ↑(MvPolynomial.algebraTensorAlgEquiv R B).symm
⊢ Function.Surjective ⇑↑↑(MvPolynomial.algebraTensorAlgEquiv R B).symm