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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsFiniteLength R M
⊢ length R M ≠ ⊤

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsFiniteLength R M
⊢ length R M ≠ ⊤
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
⊢ length R M = length R N + length R P

pp: case neg
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : ¬IsFiniteLength R P
⊢ length R M = length R N + length R P

Tactic:
·

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
⊢ length R M = length R N + length R P
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : IsFiniteLength R N
⊢ length R M = length R N + length R P

pp: case neg
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : ¬IsFiniteLength R N
⊢ length R M = length R N + length R P

Tactic:
·

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : IsFiniteLength R N
⊢ length R M = length R N + length R P
Module: Mathlib.RingTheory.Bezout

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

pp: case mpr
R : Type u
inst✝ : CommRing R
⊢ (∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})) → IsBezout R

Tactic:
·

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

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

Tactic:
·

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

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

pp: case mpr.sup
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (N₁ N₂ : Submodule R R), N₁.FG → N₂.FG → N₁.IsPrincipal → N₂.IsPrincipal → (N₁ ⊔ N₂).IsPrincipal

Tactic:
·

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

Goal state before:
pp: case mpr.sup
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (N₁ N₂ : Submodule R R), N₁.FG → N₂.FG → N₁.IsPrincipal → N₂.IsPrincipal → (N₁ ⊔ N₂).IsPrincipal

Tactic:
·

Goal state after:
case mpr.sup
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (N₁ N₂ : Submodule R R), N₁.FG → N₂.FG → N₁.IsPrincipal → N₂.IsPrincipal → (N₁ ⊔ N₂).IsPrincipal
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : ¬IsFiniteLength R N
⊢ length R M = length R N + length R P

Tactic:
·

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : ¬IsFiniteLength R N
⊢ length R M = length R N + length R P
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {f x, f y} = Ideal.map f (Ideal.span {gcd x y})

pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.map f (Ideal.span {gcd x y}) = S ∙ f (gcd x y)

Tactic:
·

Goal state after:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {f x, f y} = Ideal.map f (Ideal.span {gcd x y})
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : length R N = ⊤
this : length R M = ⊤
⊢ length R M = length R N + length R P

Tactic:
hN,

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : length R N = ⊤
this : length R M = ⊤
⊢ length R M = ⊤ + length R P
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.map f (Ideal.span {gcd x y}) = S ∙ f (gcd x y)

Tactic:
·

Goal state after:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.map f (Ideal.span {gcd x y}) = S ∙ f (gcd x y)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : ¬IsFiniteLength R P
⊢ length R M = length R N + length R P

Tactic:
·

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : ¬IsFiniteLength R P
⊢ length R M = length R N + length R P
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:
ext1; rw [hf, hf, e]

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case of_equiv
R : Type u_1
inst✝ : Ring R
⊢ ∀ (α β : Type u_5) [inst : Fintype β] (e : α ≃ β),
    (∀ (M : α → Type u_6) [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)],
        length R ((i : α) → M i) = ∑ i, length R (M i)) →
      ∀ (M : β → Type u_6) [inst_1 : (i : β) → AddCommGroup (M i)] [inst_2 : (i : β) → Module R (M i)],
        length R ((i : β) → M i) = ∑ i, length R (M i)

pp: case h_empty
R : Type u_1
inst✝ : Ring R
⊢ ∀ (M : PEmpty.{u_5 + 1} → Type u_6) [inst : (i : PEmpty.{u_5 + 1}) → AddCommGroup (M i)]
    [inst_1 : (i : PEmpty.{u_5 + 1}) → Module R (M i)], length R ((i : PEmpty.{u_5 + 1}) → M i) = ∑ i, length R (M i)

pp: case h_option
R : Type u_1
inst✝ : Ring R
⊢ ∀ (α : Type u_5) [inst : Fintype α],
    (∀ (M : α → Type u_6) [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)],
        length R ((i : α) → M i) = ∑ i, length R (M i)) →
      ∀ (M : Option α → Type u_6) [inst_1 : (i : Option α) → AddCommGroup (M i)]
        [inst_2 : (i : Option α) → Module R (M i)], length R ((i : Option α) → M i) = ∑ i, length R (M i)

Tactic:
·

Goal state after:
case of_equiv
R : Type u_1
inst✝ : Ring R
⊢ ∀ (α β : Type u_5) [inst : Fintype β] (e : α ≃ β),
    (∀ (M : α → Type u_6) [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)],
        length R ((i : α) → M i) = ∑ i, length R (M i)) →
      ∀ (M : β → Type u_6) [inst_1 : (i : β) → AddCommGroup (M i)] [inst_2 : (i : β) → Module R (M i)],
        length R ((i : β) → M i) = ∑ i, length R (M i)
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
tfae_4_to_1 : WfDvdMonoid R → IsNoetherianRing R
⊢ [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE

Tactic:
tfae_finish

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case h_empty
R : Type u_1
inst✝ : Ring R
⊢ ∀ (M : PEmpty.{u_5 + 1} → Type u_6) [inst : (i : PEmpty.{u_5 + 1}) → AddCommGroup (M i)]
    [inst_1 : (i : PEmpty.{u_5 + 1}) → Module R (M i)], length R ((i : PEmpty.{u_5 + 1}) → M i) = ∑ i, length R (M i)

pp: case h_option
R : Type u_1
inst✝ : Ring R
⊢ ∀ (α : Type u_5) [inst : Fintype α],
    (∀ (M : α → Type u_6) [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)],
        length R ((i : α) → M i) = ∑ i, length R (M i)) →
      ∀ (M : Option α → Type u_6) [inst_1 : (i : Option α) → AddCommGroup (M i)]
        [inst_2 : (i : Option α) → Module R (M i)], length R ((i : Option α) → M i) = ∑ i, length R (M i)

Tactic:
·

Goal state after:
case h_empty
R : Type u_1
inst✝ : Ring R
⊢ ∀ (M : PEmpty.{u_5 + 1} → Type u_6) [inst : (i : PEmpty.{u_5 + 1}) → AddCommGroup (M i)]
    [inst_1 : (i : PEmpty.{u_5 + 1}) → Module R (M i)], length R ((i : PEmpty.{u_5 + 1}) → M i) = ∑ i, length R (M i)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case h_option
R : Type u_1
inst✝ : Ring R
⊢ ∀ (α : Type u_5) [inst : Fintype α],
    (∀ (M : α → Type u_6) [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)],
        length R ((i : α) → M i) = ∑ i, length R (M i)) →
      ∀ (M : Option α → Type u_6) [inst_1 : (i : Option α) → AddCommGroup (M i)]
        [inst_2 : (i : Option α) → Module R (M i)], length R ((i : Option α) → M i) = ∑ i, length R (M i)

Tactic:
·

Goal state after:
case h_option
R : Type u_1
inst✝ : Ring R
⊢ ∀ (α : Type u_5) [inst : Fintype α],
    (∀ (M : α → Type u_6) [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)],
        length R ((i : α) → M i) = ∑ i, length R (M i)) →
      ∀ (M : Option α → Type u_6) [inst_1 : (i : Option α) → AddCommGroup (M i)]
        [inst_2 : (i : Option α) → Module R (M i)], length R ((i : Option α) → M i) = ∑ i, length R (M i)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case inl
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_5
h✝ : Finite ι
⊢ length R (ι →₀ M) = ENat.card ι * length R M

pp: case inr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_5
h✝ : Infinite ι
⊢ length R (ι →₀ M) = ENat.card ι * length R M

Tactic:
·

Goal state after:
case inl
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_5
h✝ : Finite ι
⊢ length R (ι →₀ M) = ENat.card ι * length R M
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case inl
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_5
h✝ : Finite ι
⊢ length R (ι → M) = ENat.card ι * length R M

pp: case inr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_5
h✝ : Infinite ι
⊢ length R (ι → M) = ENat.card ι * length R M

Tactic:
·

Goal state after:
case inl
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_5
h✝ : Finite ι
⊢ length R (ι → M) = ENat.card ι * length R M
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
a✝¹ : Nontrivial R
a✝ : Nontrivial M
H : length R R = ⊤
⊢ length R M = Cardinal.toENat (Module.rank R M) * length R R

pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
a✝¹ : Nontrivial R
a✝ : Nontrivial M
H : ¬length R R = ⊤
⊢ length R M = Cardinal.toENat (Module.rank R M) * length R R

Tactic:
·

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
a✝¹ : Nontrivial R
a✝ : Nontrivial M
H : length R R = ⊤
⊢ length R M = Cardinal.toENat (Module.rank R M) * length R R
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ˣ
⊢ (∃ c_1, c_1 • (fun m ↦ m • b) d = (fun m ↦ m • a) c) → ∃ c, c • b = a

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ˣ
⊢ (∃ c, c • b = a) → ∃ c_1, c_1 • (fun m ↦ m • b) d = (fun m ↦ m • a) c

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ˣ
⊢ (∃ 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 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ˣ
⊢ (∃ c, c • 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ˣ
⊢ (∃ c, c • 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.mk.inl
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
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xa / (algebraMap A K) ya) ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xb / (algebraMap A K) yb) ∨
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xb / (algebraMap A K) yb) ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xa / (algebraMap A K) ya)

pp: case mk.mk.inr
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
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xa / (algebraMap A K) ya) ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xb / (algebraMap A K) yb) ∨
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xb / (algebraMap A K) yb) ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xa / (algebraMap A K) ya)

Tactic:
·

Goal state after:
case mk.mk.inl
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
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xa / (algebraMap A K) ya) ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xb / (algebraMap A K) yb) ∨
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xb / (algebraMap A K) yb) ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xa / (algebraMap A K) ya)
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
x : O
hx : IsUnit x
H : ∀ (x : O), v ((algebraMap O R) x) ≤ 1
u : Oˣ
hu : ↑u = x
⊢ 1 ≤ v ((algebraMap O R) x)

Tactic:
by
    grw [← v.map_one, ← (algebraMap O R).map_one, ← u.mul_inv, ← mul_one (v (algebraMap O R x)), hu,
      (algebraMap O R).map_mul, v.map_mul, H (u⁻¹ : Units O)]

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

Goal state before:
pp: case mk.mk.inr
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
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xa / (algebraMap A K) ya) ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xb / (algebraMap A K) yb) ∨
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xb / (algebraMap A K) yb) ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xa / (algebraMap A K) ya)

Tactic:
·

Goal state after:
case mk.mk.inr
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
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xa / (algebraMap A K) ya) ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xb / (algebraMap A K) yb) ∨
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xb / (algebraMap A K) yb) ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xa / (algebraMap A K) ya)
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mp
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
h : Nontrivial O
⊢ Nontrivial R

pp: case mpr
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
h : Nontrivial R
⊢ Nontrivial O

Tactic:
·

Goal state after:
case mp
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
h : Nontrivial O
⊢ Nontrivial R
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mpr
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
h : Nontrivial R
⊢ Nontrivial O

Tactic:
·

Goal state after:
case mpr
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
h : Nontrivial R
⊢ Nontrivial O
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
⊢ DvdNotUnit x y ↔ v ((algebraMap O F) y) ≤ v ((algebraMap O F) x) ∧ ¬v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)

Tactic:
hv.le_iff_dvd,

Goal state after:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
⊢ DvdNotUnit x y ↔ x ∣ y ∧ ¬v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)
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