mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝¹ : IsReflexive L M
this✝ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃✝ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃✝ ⋯
this : Fintype ↑v
v' : ↑v → ↥M' := fun i ↦ ⟨↑i, ⋯⟩
hv₃ : LinearIndependent K Subtype.val
x✝ : { x // x ∈ v }
⊢ ↑x✝ = (⇑M'.subtype ∘ v') x✝

Tactic:
;

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝¹ : IsReflexive L M
this✝ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃✝ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃✝ ⋯
this : Fintype ↑v
v' : ↑v → ↥M' := fun i ↦ ⟨↑i, ⋯⟩
hv₃ : LinearIndependent K Subtype.val
x✝ : { x // x ∈ v }
⊢ ↑x✝ = (⇑M'.subtype ∘ v') x✝
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h : eval 0 ((⇑derivative)^[k + 2] (U R n)) = -(((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n)))
⊢ eval 0 ((⇑derivative)^[k + 2] (U R n)) + -(((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n))) -
      (-((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n)) + eval 0 ((⇑derivative)^[k + 2] (U R n))) =
    0

Tactic:
;

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h : eval 0 ((⇑derivative)^[k + 2] (U R n)) = -(((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n)))
⊢ eval 0 ((⇑derivative)^[k + 2] (U R n)) + -(((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n))) -
      (-((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n)) + eval 0 ((⇑derivative)^[k + 2] (U R n))) =
    0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ 2 * T R m * X = 2 * X * T R m - T R (m - 1) + T R (m - 1)

Tactic:
;

Goal state after:
case one
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ 2 * T R m * X = 2 * X * T R m - T R (m - 1) + T R (m - 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ C R m * X = X * C R m - C R (m - 1) + C R (m - 1)

Tactic:
;

Goal state after:
case one
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ C R m * X = X * C R m - C R (m - 1) + C R (m - 1)
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c d e : ℕ
h : c = b + a
h' : e = d + c
x✝ : ↥(I ^ a • ⊤)
⊢ ((factorPow I M ⋯ ∘ₗ powSMulQuotInclusion I M ⋯ ⊤) ∘ₗ (I ^ (b + d) • ⊤).mkQ) x✝ =
    ((powSMulQuotInclusion I M h ⊤ ∘ₗ factorPow I ↥(I ^ a • ⊤) ⋯) ∘ₗ (I ^ (b + d) • ⊤).mkQ) x✝

Tactic:
;

Goal state after:
R : Type u_3
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c d e : ℕ
h : c = b + a
h' : e = d + c
x✝ : ↥(I ^ a • ⊤)
⊢ ((factorPow I M ⋯ ∘ₗ powSMulQuotInclusion I M ⋯ ⊤) ∘ₗ (I ^ (b + d) • ⊤).mkQ) x✝ =
    ((powSMulQuotInclusion I M h ⊤ ∘ₗ factorPow I ↥(I ^ a • ⊤) ⋯) ∘ₗ (I ^ (b + d) • ⊤).mkQ) x✝
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: case of_subsingleton
R : Type u_1
inst✝⁷ : Ring R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M✝ : Type u_2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : Subsingleton M✝
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M✝ ≃ₗ[R] N
this : Subsingleton N
⊢ IsFiniteLength R N

Tactic:
;

Goal state after:
case of_subsingleton
R : Type u_1
inst✝⁷ : Ring R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M✝ : Type u_2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : Subsingleton M✝
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M✝ ≃ₗ[R] N
this : Subsingleton N
⊢ IsFiniteLength R N
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
⊢ IsFiniteLength R ↥(RelSeries.head s)

Tactic:
;

Goal state after:
case zero
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
⊢ IsFiniteLength R ↥(RelSeries.head s)
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
⊢ IsFiniteLength R ↥⊥

Tactic:
;

Goal state after:
case zero
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
⊢ IsFiniteLength R ↥⊥
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
x : α
hx : 0 < ↑x
a b : α
h : a < b
⊢ x * a < x * b

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
x : α
hx : 0 < ↑x
a b : α
h : a < b
⊢ x * a < x * b
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightStrictMono α
x : α
hx : 0 < ↑x
a b : α
h : a < b
⊢ a * x < b * x

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightStrictMono α
x : α
hx : 0 < ↑x
a b : α
h : a < b
⊢ a * x < b * x
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
x : α
hx : 0 ≤ ↑x
a b : α
h : a ≤ b
⊢ x * a ≤ x * b

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
x : α
hx : 0 ≤ ↑x
a b : α
h : a ≤ b
⊢ x * a ≤ x * b
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightMono α
x : α
hx : 0 ≤ ↑x
a b : α
h : a ≤ b
⊢ a * x ≤ b * x

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightMono α
x : α
hx : 0 ≤ ↑x
a b : α
h : a ≤ b
⊢ a * x ≤ b * x
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: case mp
R : Type u
inst✝ : CommRing R
H : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {x, y})

Tactic:
;

Goal state after:
case mp
R : Type u
inst✝ : CommRing R
H : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {x, y})
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // J.FG } → R
hf : ∀ (I : { J // J.FG }), ↑I = Ideal.span {f I}
x y : { N // N.FG }
e : f x = f y
⊢ ↑x = ↑y

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // J.FG } → R
hf : ∀ (I : { J // J.FG }), ↑I = Ideal.span {f I}
x y : { N // N.FG }
e : f x = f y
⊢ ↑x = ↑y
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
⊢ (∃ c_1, c_1 • (fun m ↦ m • b) d = (fun m ↦ m • a) c) = ∃ c, c • b = a

Tactic:
;

Goal state after:
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
⊢ (∃ c_1, c_1 • (fun m ↦ m • b) d = (fun m ↦ m • a) c) = ∃ c, c • b = a
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mp
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : e • (fun m ↦ m • b) d = (fun m ↦ m • a) c
⊢ ∃ c, c • b = a

Tactic:
;

Goal state after:
case mp
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : e • (fun m ↦ m • b) d = (fun m ↦ m • a) c
⊢ ∃ c, c • b = a
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mpr
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : e • b = a
⊢ ∃ c_1, c_1 • (fun m ↦ m • b) d = (fun m ↦ m • a) c

Tactic:
;

Goal state after:
case mpr
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : e • b = a
⊢ ∃ c_1, c_1 • (fun m ↦ m • b) d = (fun m ↦ m • a) c
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b : ValueGroup A K
a : K
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≤ b ∨ b ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a

Tactic:
;

Goal state after:
case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b : ValueGroup A K
a : K
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≤ b ∨ b ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
hx : v x ≤ 1
⊢ -x ∈ {x | v x ≤ 1}

Tactic:
;

Goal state after:
R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
hx : v x ≤ 1
⊢ -x ∈ {x | v x ≤ 1}
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ (algebraMap A K) (c * xa * yb) = (algebraMap A K) (ya * xb)

Tactic:
;

Goal state after:
case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ (algebraMap A K) (c * xa * yb) = (algebraMap A K) (ya * xb)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h.e_6
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ c * xa * yb = ya * xb

Tactic:
;

Goal state after:
case h.e_6
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ c * xa * yb = ya * xb
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ (algebraMap A K) (c * xb * ya) = (algebraMap A K) (yb * xa)

Tactic:
;

Goal state after:
case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ (algebraMap A K) (c * xb * ya) = (algebraMap A K) (yb * xa)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h.e_6
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ c * xb * ya = yb * xa

Tactic:
;

Goal state after:
case h.e_6
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ c * xb * ya = yb * xa
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝¹ : ValueGroup A K
a✝ : K
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a✝ ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a✝

Tactic:
;

Goal state after:
case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝¹ : ValueGroup A K
a✝ : K
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a✝ ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a✝
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝¹ : ValueGroup A K
a✝ : K
⊢ 1 • a✝ = a✝

Tactic:
;

Goal state after:
case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝¹ : ValueGroup A K
a✝ : K
⊢ 1 • a✝ = a✝
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk.mk.mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b✝ c✝ : ValueGroup A K
c : K
e f : A
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) (e • f • c) ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c

Tactic:
;

Goal state after:
case mk.mk.mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b✝ c✝ : ValueGroup A K
c : K
e f : A
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) (e • f • c) ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b✝ c✝ : ValueGroup A K
c : K
e f : A
⊢ (e * f) • c = e • f • c

Tactic:
;

Goal state after:
case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b✝ c✝ : ValueGroup A K
c : K
e f : A
⊢ (e * f) • c = e • f • c
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case pos
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b✝ : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : b = 0
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) (e • b) = Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b

pp: case neg
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b✝ : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : ¬b = 0
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) (e • b) = Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b

Tactic:
;

Goal state after:
case pos
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b✝ : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : b = 0
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) (e • b) = Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b

case neg
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b✝ : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : ¬b = 0
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) (e • b) = Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b✝ : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : ¬b = 0
⊢ 1 = f * e

Tactic:
← mul_smul,

Goal state after:
case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b✝ : ValueGroup A K
b : K
e f : A
hf : (f * e) • b = b
hb : ¬b = 0
⊢ 1 = f * e
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk.mk.mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
b✝ : ValueGroup A K
b : K
c✝ : ValueGroup A K
c : K
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b *
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c =
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a *
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c)

Tactic:
;

Goal state after:
case mk.mk.mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
b✝ : ValueGroup A K
b : K
c✝ : ValueGroup A K
c : K
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b *
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c =
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a *
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk.mk.mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
b✝ : ValueGroup A K
b : K
c✝ : ValueGroup A K
c : K
⊢ (MulAction.orbitRel Aˣ K) (a * b * c) (a * (b * c))

Tactic:
;

Goal state after:
case mk.mk.mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
b✝ : ValueGroup A K
b : K
c✝ : ValueGroup A K
c : K
⊢ (MulAction.orbitRel Aˣ K) (a * b * c) (a * (b * c))
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
⊢ 1 * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a = Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a

Tactic:
;

Goal state after:
case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
⊢ 1 * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a = Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
⊢ (MulAction.orbitRel Aˣ K) (1 * a) a

Tactic:
;

Goal state after:
case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
⊢ (MulAction.orbitRel Aˣ K) (1 * a) a
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a * 1 = Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a

Tactic:
;

Goal state after:
case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a * 1 = Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
⊢ (MulAction.orbitRel Aˣ K) (a * 1) a

Tactic:
;

Goal state after:
case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
⊢ (MulAction.orbitRel Aˣ K) (a * 1) a
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk.mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
b✝ : ValueGroup A K
b : K
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b =
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a

Tactic:
;

Goal state after:
case mk.mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
b✝ : ValueGroup A K
b : K
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b =
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a