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

Goal state before:
pp: K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
⊢ x ∈ R.ofPrime (R.idealOfLE S h) ↔ x ∈ S

Tactic:
;

Goal state after:
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
⊢ x ∈ R.ofPrime (R.idealOfLE S h) ↔ x ∈ S
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mp
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ (algebraMap (↥R) K) a * ((algebraMap (↥R) K) r)⁻¹ ∈ S

Tactic:
;

Goal state after:
case mp
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ (algebraMap (↥R) K) a * ((algebraMap (↥R) K) r)⁻¹ ∈ S
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mp.a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ (algebraMap (↥R) K) a ∈ S

pp: case a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ ((algebraMap (↥R) K) r)⁻¹ ∈ S

Tactic:
;

Goal state after:
case mp.a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ (algebraMap (↥R) K) a ∈ S

case a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ ((algebraMap (↥R) K) r)⁻¹ ∈ S
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
;

Goal state after:
case mpr
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
⊢ x ∈ R.ofPrime (R.idealOfLE S h)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∈ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

pp: case neg
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
;

Goal state after:
case pos
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∈ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

case neg
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
R S : ValuationSubring K
h✝ : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
h : x = 0
⊢ 0 ∈ R

Tactic:
;

Goal state after:
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h✝ : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
h : x = 0
⊢ 0 ∈ R
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : 1 ≤ R.valuation ↑((A.inclusion R hR) x)
⊢ False

Tactic:
;

Goal state after:
K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : 1 ≤ R.valuation ↑((A.inclusion R hR) x)
⊢ False
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
P : PrimeSpectrum ↥A
⊢ ((fun S ↦ { asIdeal := A.idealOfLE ↑S ⋯, isPrime := ⋯ }) ((fun P ↦ ⟨A.ofPrime P.asIdeal, ⋯⟩) P)).asIdeal = P.asIdeal

Tactic:
;

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
P : PrimeSpectrum ↥A
⊢ ((fun S ↦ { asIdeal := A.idealOfLE ↑S ⋯, isPrime := ⋯ }) ((fun P ↦ ⟨A.ofPrime P.asIdeal, ⋯⟩) P)).asIdeal = P.asIdeal
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
S : { S // A ≤ S }
⊢ ↑((fun P ↦ ⟨A.ofPrime P.asIdeal, ⋯⟩) ((fun S ↦ { asIdeal := A.idealOfLE ↑S ⋯, isPrime := ⋯ }) S)) = ↑S

Tactic:
;

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
S : { S // A ≤ S }
⊢ ↑((fun P ↦ ⟨A.ofPrime P.asIdeal, ⋯⟩) ((fun S ↦ { asIdeal := A.idealOfLE ↑S ⋯, isPrime := ⋯ }) S)) = ↑S
Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹² : PartialOrder α
inst✝¹¹ : AddCommSemigroup α
inst✝¹⁰ : ExistsAddOfLE α
inst✝⁹ : AddLeftMono α
inst✝⁸ : Sub α
inst✝⁷ : OrderedSub α
inst✝⁶ : PartialOrder β
inst✝⁵ : AddCommSemigroup β
inst✝⁴ : Sub β
inst✝³ : OrderedSub β
inst✝² : AddLeftReflectLE β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : α
h : b ≤ a
| f a - f b

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹² : PartialOrder α
inst✝¹¹ : AddCommSemigroup α
inst✝¹⁰ : ExistsAddOfLE α
inst✝⁹ : AddLeftMono α
inst✝⁸ : Sub α
inst✝⁷ : OrderedSub α
inst✝⁶ : PartialOrder β
inst✝⁵ : AddCommSemigroup β
inst✝⁴ : Sub β
inst✝³ : OrderedSub β
inst✝² : AddLeftReflectLE β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : α
h : b ≤ a
| f a - f b
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : (PrimeSpectrum ↥A)ᵒᵈ
h : a ≤ b
⊢ (OrderDual.ofDual b).asIdeal ≤ (OrderDual.ofDual a).asIdeal

Tactic:
;

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : (PrimeSpectrum ↥A)ᵒᵈ
h : a ≤ b
⊢ (OrderDual.ofDual b).asIdeal ≤ (OrderDual.ofDual a).asIdeal
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mp
K : Type u
inst✝² : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
inst✝ : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.IsEquiv v₂
⊢ v₁.valuationSubring = v₂.valuationSubring

Tactic:
;

Goal state after:
case mp
K : Type u
inst✝² : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
inst✝ : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.IsEquiv v₂
⊢ v₁.valuationSubring = v₂.valuationSubring
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mp
K : Type u
inst✝² : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
inst✝ : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.IsEquiv v₂
x : K
⊢ x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring

Tactic:
;

Goal state after:
case mp
K : Type u
inst✝² : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
inst✝ : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.IsEquiv v₂
x : K
⊢ x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mp
K : Type u
inst✝² : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
inst✝ : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
x : K
h : v₁ x ≤ v₁ 1 ↔ v₂ x ≤ v₂ 1
⊢ x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring

Tactic:
;

Goal state after:
case mp
K : Type u
inst✝² : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
inst✝ : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
x : K
h : v₁ x ≤ v₁ 1 ↔ v₂ x ≤ v₂ 1
⊢ x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mpr
K : Type u
inst✝² : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
inst✝ : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.valuationSubring = v₂.valuationSubring
⊢ v₁.IsEquiv v₂

Tactic:
;

Goal state after:
case mpr
K : Type u
inst✝² : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
inst✝ : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.valuationSubring = v₂.valuationSubring
⊢ v₁.IsEquiv v₂
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : K
⊢ x✝ ∈ A.valuation.valuationSubring ↔ x✝ ∈ A

Tactic:
;

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : K
⊢ x✝ ∈ A.valuation.valuationSubring ↔ x✝ ∈ A
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : K
⊢ x✝ ∈ A.valuation.valuationSubring ↔ A.valuation x✝ ≤ 1

Tactic:
;

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : K
⊢ x✝ ∈ A.valuation.valuationSubring ↔ A.valuation x✝ ≤ 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A.unitGroup
⊢ ↑↑{ val := ⟨↑↑(a * b), ⋯⟩, inv := ⟨↑↑(a * b)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ } =
    ↑↑({ val := ⟨↑↑a, ⋯⟩, inv := ⟨↑↑a⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ } *
          { val := ⟨↑↑b, ⋯⟩, inv := ⟨↑↑b⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ })

Tactic:
;

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A.unitGroup
⊢ ↑↑{ val := ⟨↑↑(a * b), ⋯⟩, inv := ⟨↑↑(a * b)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ } =
    ↑↑({ val := ⟨↑↑a, ⋯⟩, inv := ⟨↑↑a⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ } *
          { val := ⟨↑↑b, ⋯⟩, inv := ⟨↑↑b⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ })
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : x = 0
⊢ x ∈ B

pp: case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : ¬x = 0
⊢ x ∈ B

Tactic:
;

Goal state after:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : x = 0
⊢ x ∈ B

case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : ¬x = 0
⊢ x ∈ B
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
c : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (↑y - x) ⋯
hc : ArchimedeanClass.mk (↑y - x) = ↑c
this : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
⊢ False

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
c : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (↑y - x) ⋯
hc : ArchimedeanClass.mk (↑y - x) = ↑c
this : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
⊢ False
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
h_1 : x = 0
⊢ x ∈ B

pp: case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
h_1 : ¬x = 0
⊢ x ∈ B

Tactic:
;

Goal state after:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
h_1 : x = 0
⊢ x ∈ B

case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
h_1 : ¬x = 0
⊢ x ∈ B
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : ¬A.valuation x⁻¹ < 1
h_1 : ¬x = 0
h_2 : B.valuation x⁻¹ < 1
⊢ False

Tactic:
;

Goal state after:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : ¬A.valuation x⁻¹ < 1
h_1 : ¬x = 0
h_2 : B.valuation x⁻¹ < 1
⊢ False
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : K
hx : x ∈ B.nonunits
h_1 : x ∉ A.nonunits
⊢ False

Tactic:
;

Goal state after:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : K
hx : x ∈ B.nonunits
h_1 : x ∉ A.nonunits
⊢ False
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
y z : ↥(↑f).domain
hx : ↑z ∉ (↑f).domain
h : ↑z < ↑y
hxy0 : ↑y - ↑z ≠ 0
hz : ↑z - ↑z ∈ ball K (FiniteArchimedeanClass.mk (↑y - ↑z) ⋯)
⊢ False

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
y z : ↥(↑f).domain
hx : ↑z ∉ (↑f).domain
h : ↑z < ↑y
hxy0 : ↑y - ↑z ≠ 0
hz : ↑z - ↑z ∈ ball K (FiniteArchimedeanClass.mk (↑y - ↑z) ⋯)
⊢ False
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : x = 0
⊢ x ∈ B

pp: case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
⊢ x ∈ B

Tactic:
;

Goal state after:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : x = 0
⊢ x ∈ B

case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
⊢ x ∈ B
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : x ∈ B.principalUnitGroup
h_1 : x ∉ A.principalUnitGroup
⊢ False

Tactic:
;

Goal state after:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : x ∈ B.principalUnitGroup
h_1 : x ∉ A.principalUnitGroup
⊢ False
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥(Units.map ↑(IsLocalRing.residue ↥A)).ker
⊢ A.unitGroupMulEquiv (A.unitGroupMulEquiv.symm ↑x) ∈ (Units.map ↑(IsLocalRing.residue ↥A)).ker

Tactic:
;

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥(Units.map ↑(IsLocalRing.residue ↥A)).ker
⊢ A.unitGroupMulEquiv (A.unitGroupMulEquiv.symm ↑x) ∈ (Units.map ↑(IsLocalRing.residue ↥A)).ker
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : FiniteElement K
⊢ mk x = mk y ↔ 0 < ArchimedeanClass.mk (↑x - ↑y)

Tactic:
apply Quotient.eq.trans

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : FiniteElement K
⊢ (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))) x y ↔ 0 < ArchimedeanClass.mk (↑x - ↑y)
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
b : α
x✝ : G
⊢ x✝ ∈ stabilizer G {b} ↔ x✝ ∈ stabilizer G b

Tactic:
;

Goal state after:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
b : α
x✝ : G
⊢ x✝ ∈ stabilizer G {b} ↔ x✝ ∈ stabilizer G b
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : stabilizer G s ≤ stabilizer G t
hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t
⊢ s ∩ t ⊆ ∅

Tactic:
;

Goal state after:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : stabilizer G s ≤ stabilizer G t
hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t
⊢ s ∩ t ⊆ ∅
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ b <• a ∈ b •> s

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ b <• a ∈ b •> s
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
s : Finset α
x✝ : G
⊢ x✝ ∈ stabilizer G ↑s ↔ x✝ ∈ stabilizer G s

Tactic:
;

Goal state after:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
s : Finset α
x✝ : G
⊢ x✝ ∈ stabilizer G ↑s ↔ x✝ ∈ stabilizer G s
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
b : α
x✝ : G
⊢ x✝ ∈ stabilizer G {b} ↔ x✝ ∈ stabilizer G b

Tactic:
;

Goal state after:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
b : α
x✝ : G
⊢ x✝ ∈ stabilizer G {b} ↔ x✝ ∈ stabilizer G b
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : R →+*o K
⊢ ∀ (a : R), (ofArchimedean f) a = 0 → a = 0

Tactic:
intro r

Goal state after:
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : R →+*o K
r : R
⊢ (ofArchimedean f) r = 0 → r = 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
⊢ stdPart (-x) = -stdPart x

Tactic:
simp_rw [stdPart, ArchimedeanClass.mk_neg]
  split_ifs
  · rw [← FiniteElement.neg_mk, map_neg]
  · simp

Goal state after:
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb : x < ↑b
hn : {r | x < f r}.Nonempty
⊢ BddBelow {r | x < f r}

Tactic:
refine ⟨a, fun r hr ↦ ?_⟩

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb : x < ↑b
hn : {r | x < f r}.Nonempty
r : ℝ
hr : r ∈ {r | x < f r}
⊢ ↑a ≤ r
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inl.hl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb✝ : x < ↑b
hn : {r | x < f r}.Nonempty
hb : BddBelow {r | x < f r}
⊢ ∀ s < sInf {r | x < f r}, f s ≤ x

Tactic:
intro r

Goal state after:
case inl.hl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb✝ : x < ↑b
hn : {r | x < f r}.Nonempty
hb : BddBelow {r | x < f r}
r : ℝ
⊢ r < sInf {r | x < f r} → f r ≤ x
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inl.hr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb✝ : x < ↑b
hn : {r | x < f r}.Nonempty
hb : BddBelow {r | x < f r}
⊢ ∀ s > sInf {r | x < f r}, x ≤ f s

Tactic:
intro r

Goal state after:
case inl.hr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb✝ : x < ↑b
hn : {r | x < f r}.Nonempty
hb : BddBelow {r | x < f r}
r : ℝ
⊢ r > sInf {r | x < f r} → x ≤ f r
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
hn2 : n = P.natDegree - P.eraseLead.degree.succ
⊢ P.coeffList = P.leadingCoeff :: (List.replicate n 0 ++ P.eraseLead.coeffList)

Tactic:
;

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
hn2 : n = P.natDegree - P.eraseLead.degree.succ
⊢ P.coeffList = P.leadingCoeff :: (List.replicate n 0 ++ P.eraseLead.coeffList)
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
| P.coeff (P.degree.succ - 1 - (k + 1))

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
| P.coeff (P.degree.succ - 1 - (k + 1))
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case monomial.monomial
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
n : ℕ
a : A
m : ℕ
b : A
a✝ : ℕ
⊢ ((PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a * (monomial m) b))).coeff a✝ =
    ((monomial n) a • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial m) b)) +
          (monomial m) b • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a))).coeff
      a✝

Tactic:
;

Goal state after:
case monomial.monomial
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
n : ℕ
a : A
m : ℕ
b : A
a✝ : ℕ
⊢ ((PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a * (monomial m) b))).coeff a✝ =
    ((monomial n) a • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial m) b)) +
          (monomial m) b • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a))).coeff
      a✝