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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : x = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
;

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : x = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
;

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : x = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
;

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : x = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

case neg
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
hy : y = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
;

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
hy : y = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

case neg
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : x = 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

Tactic:
;

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : x = 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

case neg
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
hy : y = 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

Tactic:
;

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
hy : y = 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

case neg
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h.h.tail
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
s : Setoid α
inst✝ : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b✝ c✝ : α
a✝¹ : Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x b✝
a✝ : b✝ ≤ c✝ ∨ b✝ ≈ c✝
IH : Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b✝⟧
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦c✝⟧

Tactic:
;

Goal state after:
case h.h.tail
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
s : Setoid α
inst✝ : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b✝ c✝ : α
a✝¹ : Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x b✝
a✝ : b✝ ≤ c✝ ∨ b✝ ≈ c✝
IH : Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b✝⟧
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦c✝⟧
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: F : Type u_2
inst✝ : Field F
P : RingPreordering F
x✝ : F
⊢ x✝ ∈ P.supportAddSubgroup ↔ x✝ ∈ ⊥

Tactic:
;

Goal state after:
F : Type u_2
inst✝ : Field F
P : RingPreordering F
x✝ : F
⊢ x✝ ∈ P.supportAddSubgroup ↔ x✝ ∈ ⊥
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case zero
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
a : Γ
r : R
x✝ : Γ
⊢ ((single a) r ^ 0).coeff x✝ = ((single (0 • a)) (r ^ 0)).coeff x✝

Tactic:
;

Goal state after:
case zero
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
a : Γ
r : R
x✝ : Γ
⊢ ((single a) r ^ 0).coeff x✝ = ((single (0 • a)) (r ^ 0)).coeff x✝
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
⊢ Injective ⇑C

Tactic:
intro r

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
r : R
⊢ ∀ ⦃a₂ : R⦄, C r = C a₂ → r = a₂
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
a✝ : Γ
⊢ a✝ ∈ {a | y.coeff a ≠ z.coeff a} → a✝ ∈ y.support ∪ z.support

Tactic:
;

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
a✝ : Γ
⊢ a✝ ∈ {a | y.coeff a ≠ z.coeff a} → a✝ ∈ y.support ∪ z.support
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
a✝ : Γ
⊢ ¬y.coeff a✝ = z.coeff a✝ → ¬y.coeff a✝ = 0 ∨ ¬z.coeff a✝ = 0

Tactic:
;

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
a✝ : Γ
⊢ ¬y.coeff a✝ = z.coeff a✝ → ¬y.coeff a✝ = 0 ∨ ¬z.coeff a✝ = 0
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
x✝ : G
⊢ conjneg (conjneg f) x✝ = f x✝

Tactic:
;

Goal state after:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
x✝ : G
⊢ conjneg (conjneg f) x✝ = f x✝
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
x✝ : G
⊢ conjneg 0 x✝ = 0 x✝

Tactic:
;

Goal state after:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
x✝ : G
⊢ conjneg 0 x✝ = 0 x✝
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
x✝ : G
⊢ conjneg 1 x✝ = 1 x✝

Tactic:
;

Goal state after:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
x✝ : G
⊢ conjneg 1 x✝ = 1 x✝
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f g : G → R
x✝ : G
⊢ conjneg (f + g) x✝ = (conjneg f + conjneg g) x✝

Tactic:
;

Goal state after:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f g : G → R
x✝ : G
⊢ conjneg (f + g) x✝ = (conjneg f + conjneg g) x✝
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f g : G → R
x✝ : G
⊢ conjneg (f * g) x✝ = (conjneg f * conjneg g) x✝

Tactic:
;

Goal state after:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f g : G → R
x✝ : G
⊢ conjneg (f * g) x✝ = (conjneg f * conjneg g) x✝
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: ι : Type u_1
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
s : Finset ι
f : ι → G → R
x✝ : G
⊢ conjneg (∑ i ∈ s, f i) x✝ = (∑ i ∈ s, conjneg (f i)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
s : Finset ι
f : ι → G → R
x✝ : G
⊢ conjneg (∑ i ∈ s, f i) x✝ = (∑ i ∈ s, conjneg (f i)) x✝
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: ι : Type u_1
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
s : Finset ι
f : ι → G → R
x✝ : G
⊢ conjneg (∏ i ∈ s, f i) x✝ = (∏ i ∈ s, conjneg (f i)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
s : Finset ι
f : ι → G → R
x✝ : G
⊢ conjneg (∏ i ∈ s, f i) x✝ = (∏ i ∈ s, conjneg (f i)) x✝
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
x✝ : G
⊢ x✝ ∈ support (conjneg f) ↔ x✝ ∈ -support f

Tactic:
;

Goal state after:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
x✝ : G
⊢ x✝ ∈ support (conjneg f) ↔ x✝ ∈ -support f
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommRing R
inst✝ : StarRing R
f g : G → R
x✝ : G
⊢ conjneg (f - g) x✝ = (conjneg f - conjneg g) x✝

Tactic:
;

Goal state after:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommRing R
inst✝ : StarRing R
f g : G → R
x✝ : G
⊢ conjneg (f - g) x✝ = (conjneg f - conjneg g) x✝
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommRing R
inst✝ : StarRing R
f : G → R
x✝ : G
⊢ conjneg (-f) x✝ = (-conjneg f) x✝

Tactic:
;

Goal state after:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommRing R
inst✝ : StarRing R
f : G → R
x✝ : G
⊢ conjneg (-f) x✝ = (-conjneg f) x✝
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mk
K : Type u
inst✝ : Field K
y : ValuationSubring K
toSubring✝ : Subring K
mem_or_inv_mem'✝ : ∀ (x : K), x ∈ toSubring✝.carrier ∨ x⁻¹ ∈ toSubring✝.carrier
h : { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }.toSubring = y.toSubring
⊢ { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ } = y

Tactic:
;

Goal state after:
case mk
K : Type u
inst✝ : Field K
y : ValuationSubring K
toSubring✝ : Subring K
mem_or_inv_mem'✝ : ∀ (x : K), x ∈ toSubring✝.carrier ∨ x⁻¹ ∈ toSubring✝.carrier
h : { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }.toSubring = y.toSubring
⊢ { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ } = y
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mk.mk
K : Type u
inst✝ : Field K
toSubring✝¹ : Subring K
mem_or_inv_mem'✝¹ : ∀ (x : K), x ∈ toSubring✝¹.carrier ∨ x⁻¹ ∈ toSubring✝¹.carrier
toSubring✝ : Subring K
mem_or_inv_mem'✝ : ∀ (x : K), x ∈ toSubring✝.carrier ∨ x⁻¹ ∈ toSubring✝.carrier
h :
  { toSubring := toSubring✝¹, mem_or_inv_mem' := mem_or_inv_mem'✝¹ }.toSubring =
    { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }.toSubring
⊢ { toSubring := toSubring✝¹, mem_or_inv_mem' := mem_or_inv_mem'✝¹ } =
    { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }

Tactic:
;

Goal state after:
case mk.mk
K : Type u
inst✝ : Field K
toSubring✝¹ : Subring K
mem_or_inv_mem'✝¹ : ∀ (x : K), x ∈ toSubring✝¹.carrier ∨ x⁻¹ ∈ toSubring✝¹.carrier
toSubring✝ : Subring K
mem_or_inv_mem'✝ : ∀ (x : K), x ∈ toSubring✝.carrier ∨ x⁻¹ ∈ toSubring✝.carrier
h :
  { toSubring := toSubring✝¹, mem_or_inv_mem' := mem_or_inv_mem'✝¹ }.toSubring =
    { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }.toSubring
⊢ { toSubring := toSubring✝¹, mem_or_inv_mem' := mem_or_inv_mem'✝¹ } =
    { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ↑a = 0
⊢ a * 0 = b ∨ b * 0 = a

Tactic:
;

Goal state after:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ↑a = 0
⊢ a * 0 = b ∨ b * 0 = a
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
A : ValuationSubring K
z : K
h : z = 0
⊢ ∃ x, z * (algebraMap (↥A) K) ↑x.2 = (algebraMap (↥A) K) x.1

pp: case neg
K : Type u
inst✝ : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
⊢ ∃ x, z * (algebraMap (↥A) K) ↑x.2 = (algebraMap (↥A) K) x.1

Tactic:
;

Goal state after:
case pos
K : Type u
inst✝ : Field K
A : ValuationSubring K
z : K
h : z = 0
⊢ ∃ x, z * (algebraMap (↥A) K) ↑x.2 = (algebraMap (↥A) K) x.1

case neg
K : Type u
inst✝ : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
⊢ ∃ x, z * (algebraMap (↥A) K) ↑x.2 = (algebraMap (↥A) K) x.1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
z : K
h : z = 0
⊢ z * (algebraMap (↥A) K) ↑(0, 1).2 = (algebraMap (↥A) K) (0, 1).1

Tactic:
;

Goal state after:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
z : K
h : z = 0
⊢ z * (algebraMap (↥A) K) ↑(0, 1).2 = (algebraMap (↥A) K) (0, 1).1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
hh : z ∈ A
⊢ z * (algebraMap (↥A) K) ↑(⟨z, hh⟩, 1).2 = (algebraMap (↥A) K) (⟨z, hh⟩, 1).1

Tactic:
;

Goal state after:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
hh : z ∈ A
⊢ z * (algebraMap (↥A) K) ↑(⟨z, hh⟩, 1).2 = (algebraMap (↥A) K) (⟨z, hh⟩, 1).1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h : (algebraMap (↥A) K) a = (algebraMap (↥A) K) b
⊢ ↑(↑1 * a) = ↑(↑1 * b)

Tactic:
;

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h : (algebraMap (↥A) K) a = (algebraMap (↥A) K) b
⊢ ↑(↑1 * a) = ↑(↑1 * b)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h : (algebraMap (↥A) K) a = (algebraMap (↥A) K) b
⊢ ↑1 * a = ↑1 * b

Tactic:
ext; simpa using h

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ ∃ a_1, ↑↑a_1 * 1 = ↑↑a

Tactic:
;

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ ∃ a_1, ↑↑a_1 * 1 = ↑↑a
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ ↑↑a * 1 = ↑↑a

Tactic:
;

Goal state after:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ ↑↑a * 1 = ↑↑a
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
this : x - ↑y ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - ↑y) this
x✝ : ArchimedeanClass.mk (x - ↑y) ≠ ⊤
⊢ xy ≤ ⟨ArchimedeanClass.mk (x - ↑y), x✝⟩

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
this : x - ↑y ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - ↑y) this
x✝ : ArchimedeanClass.mk (x - ↑y) ≠ ⊤
⊢ xy ≤ ⟨ArchimedeanClass.mk (x - ↑y), x✝⟩
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
⊢ ¬IsUnit a ↔ A.valuation ↑a < 1

Tactic:
;

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
⊢ ¬IsUnit a ↔ A.valuation ↑a < 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mk.mk
K : Type u
inst✝ : Field K
A R S : ValuationSubring K
h : R ≤ S
x✝ : R.ValueGroup
a✝¹ : K
y✝ : R.ValueGroup
a✝ : K
⊢ Quotient.map' id ⋯ (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝¹ * Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝) =
    Quotient.map' id ⋯ (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝¹) *
      Quotient.map' id ⋯ (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝)

Tactic:
;

Goal state after:
case mk.mk
K : Type u
inst✝ : Field K
A R S : ValuationSubring K
h : R ≤ S
x✝ : R.ValueGroup
a✝¹ : K
y✝ : R.ValueGroup
a✝ : K
⊢ Quotient.map' id ⋯ (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝¹ * Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝) =
    Quotient.map' id ⋯ (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝¹) *
      Quotient.map' id ⋯ (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mk.mk
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a✝² : R.ValueGroup
a✝¹ : K
b✝ : R.ValueGroup
a✝ : K
a : ↥R
ha : a • a✝ = a✝¹
⊢ (R.mapOfLE S h) (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝¹) ≤
    (R.mapOfLE S h) (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝)

Tactic:
;

Goal state after:
case mk.mk
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a✝² : R.ValueGroup
a✝¹ : K
b✝ : R.ValueGroup
a✝ : K
a : ↥R
ha : a • a✝ = a✝¹
⊢ (R.mapOfLE S h) (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝¹) ≤
    (R.mapOfLE S h) (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x✝ : K
⊢ (⇑(R.mapOfLE S h) ∘ ⇑R.valuation) x✝ = S.valuation x✝

Tactic:
;

Goal state after:
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x✝ : K
⊢ (⇑(R.mapOfLE S h) ∘ ⇑R.valuation) x✝ = S.valuation x✝
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
⊢ (A.ofPrime P).valuation ↑x = 1 ↔ (A.ofPrime P).valuation ↑((algebraMap ↥A ↥(A.ofPrime P)) x) = 1

Tactic:
;

Goal state after:
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
⊢ (A.ofPrime P).valuation ↑x = 1 ↔ (A.ofPrime P).valuation ↑((algebraMap ↥A ↥(A.ofPrime P)) x) = 1