mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr : ¬g ∣ f
⊢ f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod

Tactic:
let r := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)

Goal state after:
case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr : ¬g ∣ f
r : K[X] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
⊢ f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case Splits.mem.inr
R✝ : Type u_1
inst✝² : CommRing R✝
R : Type u_1
inst✝¹ : Field R
f : R[X]
g : R[X]
r s : R
inst✝ : Nontrivial R
⊢ (X + C r + (taylor r) (C s)).resultant ((taylor r) g) = (X + C s).resultant g

Tactic:
taylor_C,

Goal state after:
case Splits.mem.inr
R✝ : Type u_1
inst✝² : CommRing R✝
R : Type u_1
inst✝¹ : Field R
f : R[X]
g : R[X]
r s : R
inst✝ : Nontrivial R
⊢ (X + C r + C s).resultant ((taylor r) g) = (X + C s).resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  ((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv
b₂ : Module.Basis (Fin (m + n)) R ↥R[X]_(m + n) := degreeLT.basis R (m + n)
this :
  (Matrix.toLin b₁ b₁)
      (((LinearMap.toMatrix b₁ b₂) (f.sylvesterMap g hf hg)).adjugate *
        (LinearMap.toMatrix b₁ b₂) (f.sylvesterMap g hf hg)) =
    (Matrix.toLin b₁ b₁) (((LinearMap.toMatrix b₁ b₂) (f.sylvesterMap g hf hg)).det • 1)
⊢ f.adjSylvester g ∘ₗ f.sylvesterMap g hf hg = f.resultant g m n • LinearMap.id

Tactic:
Matrix.toLin_mul b₁ b₂ b₁,

Goal state after:
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  ((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv
b₂ : Module.Basis (Fin (m + n)) R ↥R[X]_(m + n) := degreeLT.basis R (m + n)
this :
  (Matrix.toLin b₂ b₁) ((LinearMap.toMatrix b₁ b₂) (f.sylvesterMap g hf hg)).adjugate ∘ₗ
      (Matrix.toLin b₁ b₂) ((LinearMap.toMatrix b₁ b₂) (f.sylvesterMap g hf hg)) =
    (Matrix.toLin b₁ b₁) (((LinearMap.toMatrix b₁ b₂) (f.sylvesterMap g hf hg)).det • 1)
⊢ f.adjSylvester g ∘ₗ f.sylvesterMap g hf hg = f.resultant g m n • LinearMap.id
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : FiniteType R S
inst✝ : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : ↑s₂ ∉ q
hs₂ : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom s₂)
s₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  (Localization.awayMap (integralClosure R S).val.toRingHom s₂)
      (IsLocalization.mk' (Localization.Away s₂) s₃ ⟨(fun x ↦ s₂ ^ x) n, ⋯⟩) =
    (algebraMap S (Localization.Away ((integralClosure R S).val.toRingHom s₂))) s₁
m : ℕ
hm : ↑s₂ ^ m * ↑s₃ = ↑s₂ ^ m * (s₁ * ↑s₂ ^ n)
hm0 : 0 < m
hs₃q : ↑s₃ ∉ q
q' : Ideal ↥(integralClosure R S)
x✝¹ : q'.IsPrime
hq'q : q' ≠ Ideal.under (↥(integralClosure R S)) q
x✝ : q'.LiesOver p
this✝² : Algebra (↥(integralClosure R S)) (Localization.Away ↑s₂) := OreLocalization.instAlgebra
e : Localization.Away s₂ ≃ₐ[↥(integralClosure R S)] Localization.Away ↑s₂ :=
  AlgEquiv.ofBijective (Localization.awayMapₐ (ofId (↥(integralClosure R S)) S) s₂) hs₂
q's : Ideal (Localization.Away s₂) := Ideal.map (algebraMap (↥(integralClosure R S)) (Localization.Away s₂)) q'
H : ¬⟨↑s₂ ^ m * ↑s₃, ⋯⟩ ∈ q'
hq's : Disjoint ↑(Submonoid.powers s₂) ↑q'
this✝¹ : q's.IsPrime
this✝ : q's.LiesOver q'
this : q's.LiesOver p
⊢ Ideal.comap ((↑e.symm).comp (IsScalarTower.toAlgHom (↥(integralClosure R S)) S (Localization.Away ↑s₂))).toRingHom
      q's ≠
    q

Tactic:
by
      contrapose hq'q
      rw [← hq'q, Ideal.under, Ideal.comap_comap, AlgHom.toRingHom_eq_coe,
        AlgHom.comp_algebraMap, q's.over_def q']

Goal state after:
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: R S T : Type u_1
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : (algebraMap S (S ⊗[R] T)).FormallyUnramified
⊢ (algebraMap R T).FormallyUnramified

Tactic:
formallyUnramified_algebraMap

Goal state after:
R S T : Type u_1
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : Algebra.FormallyUnramified S (S ⊗[R] T)
⊢ Algebra.FormallyUnramified R T
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: ⊢ CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) fun {R S} [CommRing R] [CommRing S] ↦
    FaithfullyFlat

Tactic:
by
  refine .mk _ FormallyUnramified.respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_
  rw [formallyUnramified_algebraMap] at h' ⊢
  rw [faithfullyFlat_algebraMap_iff] at h
  exact .of_formallyUnramified_tensorProduct_of_faithfullyFlat S

Goal state after:
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: ⊢ CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Etale) fun {R S} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
refine .mk _ Etale.respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_

Goal state after:
R S T : Type u_1
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : (algebraMap S (S ⊗[R] T)).Etale
⊢ (algebraMap R T).Etale
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
t : T
x : P.Cotangent
⊢ (P.tensorCotangentOfFlat T) (t ⊗ₜ[R] x) = t • (Cotangent.map (toBaseChange T)) x

Tactic:
obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
t : T
x : ↥P.ker
⊢ (P.tensorCotangentOfFlat T) (t ⊗ₜ[R] Cotangent.mk x) = t • (Cotangent.map (toBaseChange T)) (Cotangent.mk x)
Module: Mathlib.AlgebraicGeometry.Group.Smooth

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
this✝ : JacobsonSpace ↥G
this : Nonempty ↥G
H : (↑(Scheme.Hom.smoothLocus f))ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f))ᶜ
hxc : x ∈ closedPoints ↥G
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : y ∈ closedPoints ↥G
x' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨x, hxc⟩) ⋯
y' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨y, hyc⟩) ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
⊢ (x' ≫ (GrpObj.mulRight x').inv) ≫ (GrpObj.mulRight y').hom = y'

Tactic:
← Iso.eq_comp_inv

Goal state after:
K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
this✝ : JacobsonSpace ↥G
this : Nonempty ↥G
H : (↑(Scheme.Hom.smoothLocus f))ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f))ᶜ
hxc : x ∈ closedPoints ↥G
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : y ∈ closedPoints ↥G
x' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨x, hxc⟩) ⋯
y' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨y, hyc⟩) ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
⊢ x' ≫ (GrpObj.mulRight x').inv = y' ≫ (GrpObj.mulRight y').inv
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ (g ◁ η ⊗≫ ε ▷ g) ⊗≫ g ◁ η ⊗≫ ε ▷ g = g ◁ η ⊗≫ (ε ▷ g ▷ 𝟙 a ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g

Tactic:
by
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) =
    𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom

Tactic:
by
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ (α_ r₁ g₁ g₂).inv ≫
      (𝟙 (r₁ ≫ g₁) ⊗≫ r₁ ◁ g₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h₁ ▷ r₂ ⊗≫ 𝟙 (h₁ ≫ r₂)) ▷ g₂ ≫
        (α_ h₁ r₂ g₂).hom ≫
          h₁ ◁ (𝟙 (r₂ ≫ g₂) ⊗≫ r₂ ◁ g₂ ◁ adj₃.unit ⊗≫ r₂ ◁ β ▷ r₃ ⊗≫ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 (h₂ ≫ r₃)) ≫
            (α_ h₁ h₂ r₃).inv =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ α ▷ r₂ ▷ g₂ ⊗≫
          (adj₁.counit ▷ (h₁ ≫ r₂ ≫ g₂ ≫ 𝟙 e) ≫ 𝟙 b ◁ h₁ ◁ r₂ ◁ g₂ ◁ adj₃.unit) ⊗≫
            h₁ ◁ r₂ ◁ β ▷ r₃ ⊗≫ h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)

Tactic:
by
      bicategory

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝³ : Flat f
inst✝² : QuasiCompact f
inst✝¹ : Surjective f
inst✝ : Mono f
⊢ IsIso f

Tactic:
apply MorphismProperty.of_pullback_fst_of_descendsAlong
    (P := isomorphisms Scheme.{u}) (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (f := f) (g := f)
  · tauto
  · exact inferInstanceAs <| IsIso (pullback.fst f f)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ IsIso φ

Tactic:
rw [ConcreteCategory.isIso_iff_bijective]

Goal state after:
R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ Function.Bijective ⇑(ConcreteCategory.hom φ)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      (r₃ ≫ r₁) ◁ g ◁ (adj₂.unit ⊗≫ l₂ ◁ adj₄.unit ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ l₄) ≫ r₄ ≫ r₂)) ⊗≫
        (r₃ ≫ r₁) ◁ ((α_ g l₂ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₃ k).inv) ▷ (r₄ ≫ r₂) ⊗≫
          (𝟙 ((r₃ ≫ r₁) ≫ l₁ ≫ l₃) ⊗≫ r₃ ◁ adj₁.counit ▷ l₃ ⊗≫ adj₃.counit) ▷ k ▷ (r₄ ≫ r₂) ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ ((g ≫ l₂) ◁ adj₄.unit ≫ α ▷ (l₄ ≫ r₄)) ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ β ≫ adj₁.counit ▷ (l₃ ≫ k)) ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂)

Tactic:
by
      bicategory

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
ha : a ∈ nonZeroDivisors R
⊢ ord R (b * a) = ord R a + ord R b

Tactic:
ord_mul R ha,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
ha : a ∈ nonZeroDivisors R
⊢ ord R b + ord R a = ord R a + ord R b
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬↑α * ϖ ^ m = 0
⊢ ord R ↑α + m • ord R ϖ = (IsDiscreteValuationRing.addVal R) (↑α * ϖ ^ m)

pp: case neg.hx
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬↑α * ϖ ^ m = 0
⊢ ϖ ∈ nonZeroDivisors R

pp: case neg.hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬↑α * ϖ ^ m = 0
⊢ ϖ ^ m ∈ nonZeroDivisors R

Tactic:
ord_of_irreducible hϖ

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬↑α * ϖ ^ m = 0
⊢ ord R ↑α + m • 1 = (IsDiscreteValuationRing.addVal R) (↑α * ϖ ^ m)

case neg.hx
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬↑α * ϖ ^ m = 0
⊢ ϖ ∈ nonZeroDivisors R

case neg.hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬↑α * ϖ ^ m = 0
⊢ ϖ ^ m ∈ nonZeroDivisors R
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ (α_ g₁ g₂ (l₅ ≫ l₆)).hom ≫
      g₁ ◁ ((α_ g₂ l₅ l₆).inv ≫ γ ▷ l₆ ≫ (α_ l₃ h₂ l₆).hom ≫ l₃ ◁ δ ≫ (α_ l₃ l₄ k₂).inv) ≫
        (α_ g₁ (l₃ ≫ l₄) k₂).inv ≫
          ((α_ g₁ l₃ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h₁ l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₂ k₁).inv) ▷ k₂ ≫
            (α_ (l₁ ≫ l₂) k₁ k₂).hom =
    𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂)

Tactic:
by
      bicategory

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
⊢ ord (f * g) x = ord f x + ord g x

Tactic:
by
  by_cases! hx : coheight x ≠ 1
  · simp [hx]
  rw [ord_eq_iff hx <| (mul_ne_zero_iff_right hg).mpr hf]
  simp [hf, hg, ord_eq_ordHom_of_coheight_eq_one hx, unzeroD_eq_unzero]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
⊢ (α_ (r₂ ≫ r₁) g₁ g₂).inv ≫
      ((α_ r₂ r₁ g₁).hom ≫ r₂ ◁ α ≫ (α_ r₂ h₁ r₃).inv ≫ β ▷ r₃ ≫ (α_ k₁ r₄ r₃).hom) ▷ g₂ ≫
        (α_ k₁ (r₄ ≫ r₃) g₂).hom ≫
          k₁ ◁ ((α_ r₄ r₃ g₂).hom ≫ r₄ ◁ γ ≫ (α_ r₄ h₂ r₅).inv ≫ δ ▷ r₅ ≫ (α_ k₂ r₆ r₅).hom) ≫
            (α_ k₁ k₂ (r₆ ≫ r₅)).inv =
    𝟙 ((r₂ ≫ r₁) ≫ g₁ ≫ g₂) ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 ((k₁ ≫ k₂) ≫ r₆ ≫ r₅)

Tactic:
by
      bicategory

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
hs' : ∀ (i : ι), ∃ c, (c.sum fun i_1 a ↦ a * (⇑(Pi.evalRingHom (fun x ↦ R x) i) ∘ Subtype.val) i_1) = 1
⊢ ∃ c, (c.sum fun i a ↦ a * ↑i) = 1

Tactic:
choose f hf using hs'

Goal state after:
ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x // x ∈ s } →₀ R i
hf : ∀ (i : ι), ((f i).sum fun i_1 a ↦ a * (⇑(Pi.evalRingHom (fun x ↦ R x) i) ∘ Subtype.val) i_1) = 1
⊢ ∃ c, (c.sum fun i a ↦ a * ↑i) = 1
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ⟶ l₁
⊢ (conjugateEquiv adj₁ adj₂) α =
    (ρ_ r₁).inv ≫ r₁ ◁ adj₂.unit ≫ r₁ ◁ α ▷ r₂ ≫ (α_ r₁ l₁ r₂).inv ≫ adj₁.counit ▷ r₂ ≫ (λ_ r₂).hom

Tactic:
conjugateEquiv_apply,

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ⟶ l₁
⊢ (ρ_ r₁).inv ≫ (mateEquiv adj₁ adj₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫ (λ_ r₂).hom =
    (ρ_ r₁).inv ≫ r₁ ◁ adj₂.unit ≫ r₁ ◁ α ▷ r₂ ≫ (α_ r₁ l₁ r₂).inv ≫ adj₁.counit ▷ r₂ ≫ (λ_ r₂).hom
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ (conjugateEquiv adj₁ adj₁) (𝟙 l₁) = 𝟙 r₁

Tactic:
conjugateEquiv_apply,

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ (ρ_ r₁).inv ≫ (mateEquiv adj₁ adj₁) ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ≫ (λ_ r₁).hom = 𝟙 r₁
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ (ρ_ r₁).inv ≫
      (𝟙 (r₁ ≫ 𝟙 c) ⊗≫
          r₁ ◁ 𝟙 c ◁ adj₁.unit ⊗≫
            r₁ ◁ ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ▷ r₁ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₁ ⊗≫ 𝟙 (𝟙 d ≫ r₁)) ≫
        (λ_ r₁).hom =
    𝟙 r₁ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 r₁

Tactic:
by
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : 𝟙 c ⟶ l
⊢ (conjugateEquiv adj (Adjunction.id c)) α = (ρ_ r).inv ≫ r ◁ α ≫ adj.counit

Tactic:
conjugateEquiv_apply,

Goal state after:
B : Type u
inst✝ : Bicategory B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : 𝟙 c ⟶ l
⊢ (ρ_ r).inv ≫ (mateEquiv adj (Adjunction.id c)) ((λ_ (𝟙 c)).hom ≫ α ≫ (ρ_ l).inv) ≫ (λ_ (𝟙 c)).hom =
    (ρ_ r).inv ≫ r ◁ α ≫ adj.counit
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
⊢ ∀ A_1 ⊆ Set.range (zeroLocus 𝒜), ⋂₀ A_1 ∈ Set.range (zeroLocus 𝒜)

Tactic:
by
      intro Zs h
      rw [Set.sInter_eq_iInter]
      let f : Zs → Set _ := fun i => Classical.choose (h i.2)
      have H : (Set.iInter fun i ↦ zeroLocus 𝒜 (f i)) ∈ Set.range (zeroLocus 𝒜) :=
        ⟨_, zeroLocus_iUnion 𝒜 _⟩
      convert! H using 2
      funext i
      exact (Classical.choose_spec (h i.2)).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : Set (ProjectiveSpectrum 𝒜)
⊢ IsOpen U ↔ ∃ s, Uᶜ = zeroLocus 𝒜 s

Tactic:
simp only [@eq_comm _ Uᶜ]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
M : Y.Modules
U : X.Opens
r : ↑Γ(Y, f ''ᵁ U)
⊢ smul r ≫ (restrictAppIso f M U).inv =
    (restrictAppIso f M U).inv ≫ smul ((ConcreteCategory.hom (Hom.appIso f U).hom) r)

Tactic:
simp [← cancel_mono (M.restrictAppIso f U).hom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_2
X✝ Y Z T : Scheme
M N K : X✝.Modules
φ : M ⟶ N
U✝ V✝ : X✝.Opens
X : Scheme
U V : X.Opens
f : V ⟶ U
this✝⁴ :
  (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥↑V) (Opens.grothendieckTopology ↑U.carrier)
this✝³ :
  Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology ↥X).over U)
    (Opens.overEquivalence U).inverse
this✝² : (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology ↥↑U)
this✝¹ :
  ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
this✝ :
  (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology ↥↑U)
    ((Opens.grothendieckTopology ↥X).over U)
this :
  (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
W : (TopologicalSpace.Opens ↥V)ᵒᵖ
x : ↑(((Opens.sheafRestrict V).obj X.ringCatSheaf).obj.obj W)
⊢ (ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯))) x =
    (ConcreteCategory.hom (Hom.appIso (X.homOfLE ⋯) (Opposite.unop W)).inv) x

Tactic:
Scheme.Hom.appIso_homOfLE_inv

Goal state after:
case refine_2
X✝ Y Z T : Scheme
M N K : X✝.Modules
φ : M ⟶ N
U✝ V✝ : X✝.Opens
X : Scheme
U V : X.Opens
f : V ⟶ U
this✝⁴ :
  (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥↑V) (Opens.grothendieckTopology ↑U.carrier)
this✝³ :
  Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology ↥X).over U)
    (Opens.overEquivalence U).inverse
this✝² : (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology ↥↑U)
this✝¹ :
  ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
this✝ :
  (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology ↥↑U)
    ((Opens.grothendieckTopology ↥X).over U)
this :
  (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
W : (TopologicalSpace.Opens ↥V)ᵒᵖ
x : ↑(((Opens.sheafRestrict V).obj X.ringCatSheaf).obj.obj W)
⊢ (ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯))) x = (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ (algebraMap A (Localization.Away x)) f * Localization.mk g ⟨f * g, ⋯⟩ = 1

Tactic:
rw [← Algebra.smul_def, Localization.smul_mk]

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ Localization.mk (f • g) ⟨f * g, ⋯⟩ = 1