awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
p : PrimeSpectrum A
this : LocalizedModule p.asIdeal.primeCompl Ω[A⁄R] ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (unramifiedLocus R A) p ↔
    Subsingleton.{u_2 + 1} (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])

Tactic:
(Algebra.formallyUnramified_iff _ _).trans this.subsingleton_congr.symm

Premises used: Algebra.formallyUnramified_iff, Set.Mem, Equiv.subsingleton_congr, setOf, LinearEquiv.toAddEquiv, Algebra.unramifiedLocus, Iff.trans, AddEquiv.toEquiv, Iff.symm
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
p : PrimeSpectrum A
this : LocalizedModule p.asIdeal.primeCompl Ω[A⁄R] ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (unramifiedLocus R A) p ↔
    Subsingleton.{u_2 + 1} (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])

Tactic:
exact (Algebra.formallyUnramified_iff _ _).trans this.subsingleton_congr.symm

Premises used: Algebra.formallyUnramified_iff, Equiv.subsingleton_congr, LinearEquiv.toAddEquiv, Iff.trans, AddEquiv.toEquiv, Iff.symm
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
rw : Subsingleton.{u_2 + 1} (LocalizedModule.Away f Ω[A⁄R]) ↔ Subsingleton.{u_2 + 1} Ω[Localization.Away f⁄R]
⊢ (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum A)) ⊆ unramifiedLocus R A ↔
    FormallyUnramified.{u_2, u_1} R (Localization.Away f)

Tactic:
rw [unramifiedLocus_eq_compl_support, Set.subset_compl_comm,
    PrimeSpectrum.basicOpen_eq_zeroLocus_compl, compl_compl,
    ← LocalizedModule.subsingleton_iff_support_subset, Algebra.formallyUnramified_iff]

Premises used: compl_compl, Algebra.formallyUnramified_iff, Set.subset_compl_comm, Algebra.unramifiedLocus_eq_compl_support, LocalizedModule.subsingleton_iff_support_subset, PrimeSpectrum.basicOpen_eq_zeroLocus_compl
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
⊢ Subsingleton.{u_2 + 1} (LocalizedModule.Away f Ω[A⁄R]) ↔ Subsingleton.{u_2 + 1} Ω[Localization.Away f⁄R]

Tactic:
(IsLocalizedModule.iso (.powers f)
    (KaehlerDifferential.map R R A (Localization.Away f))).subsingleton_congr

Premises used: IsLocalizedModule.iso, Equiv.subsingleton_congr, Localization.Away, LinearEquiv.toAddEquiv, Submonoid.powers, AddEquiv.toEquiv, KaehlerDifferential.map
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
⊢ Subsingleton.{u_2 + 1} (LocalizedModule.Away f Ω[A⁄R]) ↔ Subsingleton.{u_2 + 1} Ω[Localization.Away f⁄R]

Tactic:
exact (IsLocalizedModule.iso (.powers f)
    (KaehlerDifferential.map R R A (Localization.Away f))).subsingleton_congr

Premises used: IsLocalizedModule.iso, Equiv.subsingleton_congr, Localization.Away, LinearEquiv.toAddEquiv, Submonoid.powers, AddEquiv.toEquiv, KaehlerDifferential.map
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
rw : Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R])ᶜ Set.univ ↔ FormallyUnramified R A
rw₁ : Eq (α := Set (PrimeSpectrum A)) Set.univᶜ (Module.support A Ω[A⁄R]) ↔ FormallyUnramified R A
rw₂ : Eq (α := Set (PrimeSpectrum A)) ∅ (Module.support A Ω[A⁄R]) ↔ FormallyUnramified R A
rw₃ : Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R]) ∅ ↔ FormallyUnramified R A
rw₄ : Subsingleton.{u_2 + 1} Ω[A⁄R] ↔ FormallyUnramified R A
rw₅ rw₆ : Subsingleton.{u_2 + 1} Ω[A⁄R] ↔ Subsingleton.{u_2 + 1} Ω[A⁄R]
⊢ Eq (α := Set (PrimeSpectrum A)) (unramifiedLocus R A) Set.univ ↔ FormallyUnramified R A

Tactic:
rw [unramifiedLocus_eq_compl_support, compl_eq_comm, Set.compl_univ, eq_comm,
    Module.support_eq_empty_iff, Algebra.formallyUnramified_iff]

Premises used: Algebra.formallyUnramified_iff, Algebra.unramifiedLocus_eq_compl_support, Set.compl_univ, eq_comm, Module.support_eq_empty_iff, compl_eq_comm
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ FormallyUnramified R A ↔ ∀ (q : PrimeSpectrum A), IsUnramifiedAt R q.asIdeal

Tactic:
unramifiedLocus_eq_univ_iff.symm.trans Set.eq_univ_iff_forall

Premises used: Set.eq_univ_iff_forall, Algebra.unramifiedLocus_eq_univ_iff, Iff.trans, Iff.symm
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FiniteType R A
⊢ Unramified R A ↔ ∀ (q : PrimeSpectrum A), IsUnramifiedAt R q.asIdeal

Tactic:
.trans ⟨fun h ↦ h.formallyUnramified, fun h ↦ ⟨h, inferInstance⟩⟩ formallyUnramified_iff_forall

Premises used: Algebra.formallyUnramified_iff_forall, inferInstance, Algebra.Unramified.mk, Iff.intro, Iff.trans, Algebra.Unramified.formallyUnramified
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
rw : IsOpen (X := PrimeSpectrum A) (PrimeSpectrum.zeroLocus (↑(Module.annihilator A Ω[A⁄R]) : Set A))ᶜ
⊢ IsOpen (X := PrimeSpectrum A) (unramifiedLocus R A)

Tactic:
rw [unramifiedLocus_eq_compl_support, Module.support_eq_zeroLocus]

Premises used: Algebra.unramifiedLocus_eq_compl_support, Module.support_eq_zeroLocus
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
⊢ IsOpen (X := PrimeSpectrum A) (PrimeSpectrum.zeroLocus (↑(Module.annihilator A Ω[A⁄R]) : Set A))ᶜ

Tactic:
(PrimeSpectrum.isClosed_zeroLocus _).isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
⊢ IsOpen (X := PrimeSpectrum A) (PrimeSpectrum.zeroLocus (↑(Module.annihilator A Ω[A⁄R]) : Set A))ᶜ

Tactic:
exact (PrimeSpectrum.isClosed_zeroLocus _).isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : Ideal A
inst_4 : p.IsPrime
inst_5 : IsUnramifiedAt R p
obtain :
  ∀ (r : A)
    (hpr :
      { asIdeal := p, isPrime := inst_4 : PrimeSpectrum A } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum A)))
    (hr : (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum A)) ⊆ unramifiedLocus R A),
    ∃ f ∉ p, FormallyUnramified.{u_2, u_1} R (Localization.Away f)
⊢ ∃ f ∉ p, FormallyUnramified.{u_2, u_1} R (Localization.Away f)

Tactic:
obtain ⟨_, ⟨_, ⟨r, rfl⟩, rfl⟩, hpr, hr⟩ :=
    PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open
      (show ⟨p, ‹_›⟩ ∈ unramifiedLocus R A from ‹_›) isOpen_unramifiedLocus

Premises used: Algebra.isOpen_unramifiedLocus, PrimeSpectrum.isBasis_basic_opens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : Ideal A
inst_4 : p.IsPrime
inst_5 : IsUnramifiedAt R p
r : A
hpr : { asIdeal := p, isPrime := inst_4 : PrimeSpectrum A } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum A))
hr : (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum A)) ⊆ unramifiedLocus R A
⊢ ∃ f ∉ p, FormallyUnramified.{u_2, u_1} R (Localization.Away f)

Tactic:
⟨r, hpr, basicOpen_subset_unramifiedLocus_iff.mp hr⟩

Premises used: Algebra.basicOpen_subset_unramifiedLocus_iff, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : Ideal A
inst_4 : p.IsPrime
inst_5 : IsUnramifiedAt R p
r : A
hpr : { asIdeal := p, isPrime := inst_4 : PrimeSpectrum A } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum A))
hr : (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum A)) ⊆ unramifiedLocus R A
⊢ ∃ f ∉ p, FormallyUnramified.{u_2, u_1} R (Localization.Away f)

Tactic:
exact ⟨r, hpr, basicOpen_subset_unramifiedLocus_iff.mp hr⟩
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FiniteType R A
p : Ideal A
inst_4 : p.IsPrime
inst_5 : IsUnramifiedAt R p
obtain :
  ∀ (f : A) (hfp : f ∉ p) (H : FormallyUnramified.{u_2, u_1} R (Localization.Away f)),
    ∃ f ∉ p, Unramified.{u_1, u_2} R (Localization.Away f)
⊢ ∃ f ∉ p, Unramified.{u_1, u_2} R (Localization.Away f)

Tactic:
obtain ⟨f, hfp, H⟩ := exists_formallyUnramified_of_isUnramifiedAt (R := R) p

Premises used: Algebra.exists_formallyUnramified_of_isUnramifiedAt
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FiniteType R A
p : Ideal A
inst_4 : p.IsPrime
inst_5 : IsUnramifiedAt R p
f : A
hfp : f ∉ p
H : FormallyUnramified.{u_2, u_1} R (Localization.Away f)
⊢ ∃ f ∉ p, Unramified.{u_1, u_2} R (Localization.Away f)

Tactic:
⟨f, hfp, ⟨H, .trans ‹_› (IsLocalization.finiteType_of_monoid_fg (.powers f) _)⟩⟩

Premises used: IsLocalization.finiteType_of_monoid_fg, Algebra.Unramified.mk, And.intro, Submonoid.powers, Exists.intro, Algebra.FiniteType.trans
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FiniteType R A
p : Ideal A
inst_4 : p.IsPrime
inst_5 : IsUnramifiedAt R p
f : A
hfp : f ∉ p
H : FormallyUnramified.{u_2, u_1} R (Localization.Away f)
⊢ ∃ f ∉ p, Unramified.{u_1, u_2} R (Localization.Away f)

Tactic:
exact ⟨f, hfp, ⟨H, .trans ‹_› (IsLocalization.finiteType_of_monoid_fg (.powers f) _)⟩⟩
-- Module: Mathlib.RingTheory.Unramified.Pi
Goal:
R : Type u_1
I : Type u_2
inst : Finite I
f : I → Type u_3
inst_1 : CommRing R
inst_2 : (i : I) → CommRing (f i)
inst_3 : (i : I) → Algebra.{u_1, u_3} R (f i)
inst_4 : ∀ (i : I), FormallyUnramified.{u_3, u_1} R (f i)
⊢ FormallyUnramified R ((i : I) → f i)

Tactic:
(pi_iff _).mpr ‹_›

Premises used: Iff.mpr, Algebra.FormallyUnramified.pi_iff
-- Module: Mathlib.RingTheory.Valuation.AlgebraInstances
Goal:
K : Type u_1
inst : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
⊢ Injective.{u_1 + 1, u_2 + 1} (α := ↥v.valuationSubring) (β := L)
    (⇑(algebraMap (↥v.valuationSubring) L) : (a : ↥v.valuationSubring) → L)

Tactic:
(FaithfulSMul.algebraMap_injective K L).comp (IsFractionRing.injective _ _)

Premises used: IsFractionRing.injective, Function.Injective.comp, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.Valuation.AlgebraInstances
Goal:
K : Type u_1
inst : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : Membership.mem (γ := Subalgebra.{u_1, u_2} (↥v.valuationSubring) L) (integralClosure (↥v.valuationSubring) L) x
⊢ IsIntegral.{u_1, u_2} (↥v.valuationSubring)
    (Subtype.mk (p := fun (x : L) ↦
      Membership.mem (γ := Subalgebra.{u_1, u_2} (↥v.valuationSubring) L) (integralClosure (↥v.valuationSubring) L) x) x
      hx)

Tactic:
integralClosure.isIntegral ⟨x, hx⟩

Premises used: Subtype.mk, integralClosure.isIntegral
-- Module: Mathlib.RingTheory.Valuation.AlgebraInstances
Goal:
K : Type u_1
inst : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
x : ↥(integralClosure (↥v.valuationSubring) L)
⊢ IsIntegral.{u_1, u_2} (↥v.valuationSubring) x

Tactic:
apply isIntegral_of_mem_ringOfIntegers

Premises used: ValuationSubring.isIntegral_of_mem_ringOfIntegers
-- Module: Mathlib.RingTheory.Valuation.AlgebraInstances
Goal:
K : Type u_1
inst : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_3
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
⊢ IsScalarTower.{u_1, u_2, u_3} (↥v.valuationSubring) L E

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Valuation.AlgebraInstances
Goal:
K : Type u_1
inst : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_3
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
⊢ Eq.{u_3 + 1} (α := E)
    ((↑(Subtype.mk (p := fun (x : E) ↦
            Membership.mem (γ := Subalgebra.{u_1, u_3} (↥v.valuationSubring) E)
              (integralClosure (↥v.valuationSubring) E) x)
            ((algebraMap L E : (a : L) → E) (↑1 : L)) ⋯) :
        E) :
      E)
    ((↑1 : E) : E)

Tactic:
simp only [Subalgebra.coe_one, map_one]

Premises used: Subalgebra.coe_one, map_one
-- Module: Mathlib.RingTheory.Valuation.AlgebraInstances
Goal:
K : Type u_1
inst : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_3
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
x y : ↥(integralClosure (↥v.valuationSubring) L)
⊢ (↑(Subtype.mk (p := fun (x : E) ↦
          Membership.mem (γ := Subalgebra.{u_1, u_3} (↥v.valuationSubring) E) (integralClosure (↥v.valuationSubring) E)
            x)
          ((algebraMap L E : (a : L) → E) (↑(x * y) : L)) ⋯) :
      E) =
    (↑(HMul.hMul (α := ↥(integralClosure (↥v.valuationSubring) E)) (β := ↥(integralClosure (↥v.valuationSubring) E))
          (Subtype.mk (p := fun (x : E) ↦
              Membership.mem (γ := Subalgebra.{u_1, u_3} (↥v.valuationSubring) E)
                (integralClosure (↥v.valuationSubring) E) x)
              ((algebraMap L E : (a : L) → E) (↑x : L)) ⋯ :
            ↥(integralClosure (↥v.valuationSubring) E))
          (Subtype.mk (p := fun (x : E) ↦
              Membership.mem (γ := Subalgebra.{u_1, u_3} (↥v.valuationSubring) E)
                (integralClosure (↥v.valuationSubring) E) x)
              ((algebraMap L E : (a : L) → E) (↑y : L)) ⋯ :
            ↥(integralClosure (↥v.valuationSubring) E))) :
      E)

Tactic:
simp only [Subalgebra.coe_mul, map_mul]

Premises used: Subalgebra.coe_mul, map_mul
-- Module: Mathlib.RingTheory.Valuation.AlgebraInstances
Goal:
K : Type u_1
inst : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_3
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
⊢ Eq.{u_3 + 1} (α := E)
    ((↑(Subtype.mk (p := fun (x : E) ↦
            Membership.mem (γ := Subalgebra.{u_1, u_3} (↥v.valuationSubring) E)
              (integralClosure (↥v.valuationSubring) E) x)
            ((algebraMap L E : (a : L) → E) (↑0 : L)) ⋯) :
        E) :
      E)
    ((↑0 : E) : E)

Tactic:
simp only [Subalgebra.coe_zero, map_zero]

Premises used: map_zero, Subalgebra.coe_zero
-- Module: Mathlib.RingTheory.Valuation.AlgebraInstances
Goal:
K : Type u_1
inst : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_3
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
x y : ↥(integralClosure (↥v.valuationSubring) L)
⊢ (↑(Subtype.mk (p := fun (x : E) ↦
          Membership.mem (γ := Subalgebra.{u_1, u_3} (↥v.valuationSubring) E) (integralClosure (↥v.valuationSubring) E)
            x)
          ((algebraMap L E : (a : L) → E) (↑(x + y) : L)) ⋯) :
      E) =
    (↑(HAdd.hAdd (α := ↥(integralClosure (↥v.valuationSubring) E)) (β := ↥(integralClosure (↥v.valuationSubring) E))
          (Subtype.mk (p := fun (x : E) ↦
              Membership.mem (γ := Subalgebra.{u_1, u_3} (↥v.valuationSubring) E)
                (integralClosure (↥v.valuationSubring) E) x)
              ((algebraMap L E : (a : L) → E) (↑x : L)) ⋯ :
            ↥(integralClosure (↥v.valuationSubring) E))
          (Subtype.mk (p := fun (x : E) ↦
              Membership.mem (γ := Subalgebra.{u_1, u_3} (↥v.valuationSubring) E)
                (integralClosure (↥v.valuationSubring) E) x)
              ((algebraMap L E : (a : L) → E) (↑y : L)) ⋯ :
            ↥(integralClosure (↥v.valuationSubring) E))) :
      E)

Tactic:
simp only [map_add, Subalgebra.coe_add]

Premises used: map_add, Subalgebra.coe_add
-- Module: Mathlib.RingTheory.Valuation.AlgebraInstances
Goal:
K : Type u_1
inst : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
⊢ Injective.{u_1 + 1, u_2 + 1} (α := ↥v.valuationSubring) (β := ↥(integralClosure (↥v.valuationSubring) L))
    (⇑(algebraMap ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L)) :
      (a : ↥v.valuationSubring) → ↥(integralClosure (↥v.valuationSubring) L))

Tactic:
FaithfulSMul.algebraMap_injective ..

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v_1 : Valuation F Γ₀
v : F →*₀ Γ₀
simp :
  ∀ (a : F) (ha : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : F) → Γ₀) a : Γ₀)) (a_1 a_2 : F)
    (hbc : LT.lt.{u_2} (α := Γ₀) ((v : (a : F) → Γ₀) a_1 : Γ₀) ((v : (a : F) → Γ₀) a_2 : Γ₀)),
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) a : Γ₀) ((v : (a : F) → Γ₀) a_1 : Γ₀) <
      HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) a : Γ₀) ((v : (a : F) → Γ₀) a_2 : Γ₀)
⊢ ∀ ⦃a : ↥(MonoidHom.mrange v)⦄ (ha : 0 < a) ⦃b c : ↥(MonoidHom.mrange v)⦄ (hbc : b < c), a * b < a * c

Tactic:
simp only [← Subtype.coe_lt_coe, val_mrange_zero, Submonoid.coe_mul, Subtype.forall,
      MonoidHom.mem_mrange, forall_exists_index, forall_apply_eq_imp_iff]

Premises used: Subtype.coe_lt_coe, forall_exists_index, Subtype.forall, MonoidWithZeroHom.val_mrange_zero, forall_apply_eq_imp_iff, Submonoid.coe_mul, MonoidHom.mem_mrange
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v_1 : Valuation F Γ₀
v : F →*₀ Γ₀
a : F
ha : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : F) → Γ₀) a : Γ₀)
b c : F
hbc : LT.lt.{u_2} (α := Γ₀) ((v : (a : F) → Γ₀) b : Γ₀) ((v : (a : F) → Γ₀) c : Γ₀)
ha₁ : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : F) → Γ₀) a : Γ₀)
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) a : Γ₀) ((v : (a : F) → Γ₀) b : Γ₀) <
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) a : Γ₀) ((v : (a : F) → Γ₀) c : Γ₀)

Tactic:
gcongr
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v_1 : Valuation F Γ₀
v : F →*₀ Γ₀
⊢ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) ⊥

Tactic:
simp [bot_eq_zero]

Premises used: bot_eq_zero
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v_1 : Valuation F Γ₀
v : F →*₀ Γ₀
a : ↥(MonoidHom.mrange v)
⊢ Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x) ⊥ ⋯ ≤ a

Tactic:
simp [bot_eq_zero, ← Subtype.coe_le_coe]

Premises used: Subtype.coe_le_coe, bot_eq_zero
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v_1 : Valuation F Γ₀
v : F →*₀ Γ₀
a : ↥(MonoidHom.mrange v)
⊢ 0 ≤ a

Tactic:
simp [← Subtype.coe_le_coe]

Premises used: Subtype.coe_le_coe
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
hv : v.Integers O
⊢ WfDvdMonoid O ↔
    WellFounded.{u_3 + 1} (α := O)
      ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
        Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F))

Tactic:
⟨fun _ ↦ wellFounded_dvdNotUnit.mono ?_, fun h ↦ ⟨h.mono ?_⟩⟩

Premises used: IsWellFounded.mk, wellFounded_dvdNotUnit, Iff.intro, WellFounded.mono
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
hv : v.Integers O
refine_1 :
  WfDvdMonoid O →
    ∀ (a b : O),
      ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
            Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F))
          a b →
        DvdNotUnit a b
refine_2 :
  ∀
    (h :
      WellFounded.{u_3 + 1} (α := O)
        ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
          Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
    (a b : O),
    DvdNotUnit a b →
      ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
          Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F))
        a b
⊢ WfDvdMonoid O ↔
    WellFounded.{u_3 + 1} (α := O)
      ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
        Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F))

Tactic:
refine ⟨fun _ ↦ wellFounded_dvdNotUnit.mono ?_, fun h ↦ ⟨h.mono ?_⟩⟩
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
hv : v.Integers O
h : WfDvdMonoid O
⊢ ∀ (a b : O),
    ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
          Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F))
        a b →
      DvdNotUnit a b

Tactic:
simp [Function.onFun, hv.dvdNotUnit_iff_lt]

Premises used: Function.onFun, Valuation.Integers.dvdNotUnit_iff_lt
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
hv : v.Integers O
h :
  WellFounded.{u_3 + 1} (α := O)
    ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
      Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F))
⊢ ∀ (a b : O),
    DvdNotUnit a b →
      ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
          Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F))
        a b

Tactic:
simp [Function.onFun, hv.dvdNotUnit_iff_lt]

Premises used: Function.onFun, Valuation.Integers.dvdNotUnit_iff_lt
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
rw :
  (Set.WellFoundedOn
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      fun (x1 x2 : Γ₀) ↦ x1 > x2) ↔
    Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2
⊢ WellFounded.{u_3 + 1} (α := O)
      ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
        Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)) ↔
    Nonempty.{max 1 (u_2 + 1)} (↥(MonoidHom.mrange v) ≃*o WithZero (Multiplicative ℤ))

Tactic:
rw [← LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero
    one_ne_zero, ← Set.wellFoundedOn_range]

Premises used: Set.wellFoundedOn_range, LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero, one_ne_zero