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

Goal state before:
pp: case inr
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
x : S
hx : R[x] = ⊤
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (x : S), R[x] = ⊤ → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
⊢ ZariskisMainProperty R p

Tactic:
let inst : Algebra (integralClosure R S) (Localization.AtPrime p) :=
      OreLocalization.instAlgebra

Goal state after:
case inr
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
x : S
hx : R[x] = ⊤
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (x : S), R[x] = ⊤ → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
inst : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
⊢ ZariskisMainProperty R p
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S), f.Finite → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
⊢ ZariskisMainProperty R p

Tactic:
let inst : Algebra (integralClosure R S) (Localization.AtPrime p) :=
      OreLocalization.instAlgebra

Goal state after:
case inr
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S), f.Finite → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
inst : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
⊢ ZariskisMainProperty R p
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
⊢ (-1) ^ (m * n) * g.resultant 0 n m = 0 ^ n * g.coeff 0 ^ m

Tactic:
resultant_zero_right

Goal state after:
R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
⊢ (-1) ^ (m * n) * (0 ^ n * g.coeff 0 ^ m) = 0 ^ n * g.coeff 0 ^ m
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R✝ S✝ : Type u
inst✝⁹ : CommRing R✝
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ S✝
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := (conductor R (f X)).radical
hp : J ≤ p
inst✝¹ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst✝ : IsReduced (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)
⊢ False

Tactic:
refine not_isStronglyTranscendental_of_weaklyQuasiFiniteAt ?_ (p.map (Ideal.Quotient.mk J))
      (isStronglyTranscendental_mk_radical_conductor H (f X) (by convert! hf; ext; simp))

Goal state after:
R✝ S✝ : Type u
inst✝⁹ : CommRing R✝
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ S✝
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := (conductor R (f X)).radical
hp : J ≤ p
inst✝¹ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst✝ : IsReduced (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)
⊢ (aeval ((Ideal.Quotient.mk (conductor R (f X)).radical) (f X))).Finite
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this : IsIso (app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U))
⊢ app (fromNormalization f) U =
    CommRingCat.ofHom (algebraMap ↑(Y.presheaf.1 (Opposite.op U)) ↥(integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U))) ≫
      (normalizationObjIso f hU).inv

Tactic:
have H : ⊤ = ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) ⁻¹ᵁ U := by
    rw [f.ι_fromNormalization]; simp

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this : IsIso (app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U))
H : ⊤ = ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) ⁻¹ᵁ U
⊢ app (fromNormalization f) U =
    CommRingCat.ofHom (algebraMap ↑(Y.presheaf.1 (Opposite.op U)) ↥(integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U))) ≫
      (normalizationObjIso f hU).inv
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : f.Finite
⊢ ZariskisMainProperty R p

Tactic:
induction n generalizing R S with

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FiniteType R S
p : Ideal S
inst✝ : p.IsPrime
H✝ : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : (Subalgebra.toSubmodule S').FG
r : ↥S'
hrp : ↑r ∉ p
H : Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)
this✝¹ : Module.Finite R ↥S'
this✝ : QuasiFinite R (Localization.Away r)
this : QuasiFinite R (Localization.Away ↑r)
f : Localization.Away ↑r →ₐ[S] Localization.AtPrime p := IsLocalization.Away.liftAlgHom ↑r ⋯
x s : S
hs : s ∈ p.primeCompl
⊢ IsUnit ((AlgHom.restrictScalars R f) ((algebraMap S (Localization.Away ↑r)) s))

Tactic:
by simpa using IsLocalization.map_units _ ⟨s, hs⟩

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case a.convert_2.mul_X
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom (↑(universalFactorizationMap R n m k hn)) (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)
H : ∀ (i : Fin m ⊕ Fin k), (tensorEquivSum R (Fin m) (Fin k) R) (f (X i)) = X i
p : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)
i : Fin m ⊕ Fin k
a✝ :
  p - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f p)) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))
⊢ p * X i - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f (p * X i))) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))

Tactic:
| mul_X p i _ =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hf0 : ¬f = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R →
          ¬f = 0 →
            f.Monic → f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod
hfm : ¬f.Monic
inst : Field R := hR.toField
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod

Tactic:
have H : (C f.leadingCoeff⁻¹ * f).Monic := by
      rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simp [hf0]), coeff_C_mul]; simp [hf0]

Goal state after:
case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hf0 : ¬f = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R →
          ¬f = 0 →
            f.Monic → f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod
hfm : ¬f.Monic
inst : Field R := hR.toField
H : (C f.leadingCoeff⁻¹ * f).Monic
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
f g₁ g₂ : R[X]
m : ℕ
hm : f.natDegree ≤ m
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g₁ g₂ : R[X]) (m : ℕ),
    f.natDegree ≤ m →
      m = f.natDegree → f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
hgn : ¬m = f.natDegree
⊢ f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m

Tactic:
obtain ⟨c, rfl⟩ := le_iff_exists_add.mp hm

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
f g₁ g₂ : R[X]
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g₁ g₂ : R[X]) (m : ℕ),
    f.natDegree ≤ m →
      m = f.natDegree → f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
c : ℕ
hm : f.natDegree ≤ f.natDegree + c
hgn : ¬f.natDegree + c = f.natDegree
⊢ f.resultant (g₁ * g₂) (f.natDegree + c) (g₁.natDegree + g₂.natDegree) =
    f.resultant g₁ (f.natDegree + c) * f.resultant g₂ (f.natDegree + c)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
M G✝ H✝ X Y : C
inst✝² : MonObj M
inst✝¹ : GrpObj G✝
inst✝ : GrpObj H✝
G H : Grp C
α : yonedaGrp.obj G ⟶ yonedaGrp.obj H
⊢ yonedaGrp.map (Grp.homMk' (yonedaMonFullyFaithful.preimage (Functor.whiskerRight α (forget₂ GrpCat MonCat)))) = α

Tactic:
by
    ext X : 3
    exact congr(($(yonedaMonFullyFaithful.map_preimage (X := G.toMon) (Y := H.toMon)
      (Functor.whiskerRight α (forget₂ GrpCat MonCat))).app X).hom)

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this : IsIso (toNormalization f ∣_ ⨆ x, V x)
⊢ ∃ U, IsIso (toNormalization f ∣_ U) ∧ (toNormalization f ⁻¹ᵁ U).carrier = {x | QuasiFiniteAt f x}

Tactic:
refine ⟨⨆ x : { x | f.QuasiFiniteAt x }, V x, this, ?_⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this : IsIso (toNormalization f ∣_ ⨆ x, V x)
⊢ (toNormalization f ⁻¹ᵁ ⨆ x, V x).carrier = {x | QuasiFiniteAt f x}
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : (⇑f '' ⇑(f ≫ g) ⁻¹' {s}).Finite
inst✝² : IsProper (f ≫ g)
inst✝¹ : IsSeparated g
inst✝ : LocallyOfFiniteType g
this✝ : IsProper f
this : IsProper (Scheme.Hom.imageι f ≫ g)
x : ↥X
hx : (Scheme.Hom.toImage f) x ∈ ⇑(Scheme.Hom.imageι f ≫ g) ⁻¹' {s}
⊢ x ∈ ⇑(f ≫ g) ⁻¹' {s}

Tactic:
simpa [← Scheme.Hom.comp_apply, -Scheme.Hom.comp_base] using hx

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

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
x' y' : ℕ∞
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (x' + y') =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) x' * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) y'

Tactic:
cases x' <;> cases y'

Goal state after:
case pos.top.top
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (⊤ + ⊤) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤

case pos.top.coe
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
a✝ : ℕ
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (⊤ + ↑a✝) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝

case pos.coe.top
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
a✝ : ℕ
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (↑a✝ + ⊤) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤

case pos.coe.coe
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
a✝¹ a✝ : ℕ
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (↑a✝¹ + ↑a✝) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝¹ *
      ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
⊢ min (ord R x) (ord R y) ≤ ord R (x + y)

Tactic:
grw [ord_eq_addVal x, ord_eq_addVal y, ord_eq_addVal (x + y), IsDiscreteValuationRing.addVal_add]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx' : x ∈ U
⊢ ord ((ConcreteCategory.hom (X.germToFunctionField U)) f) x = 0

Tactic:
by_cases! hx : coheight x ≠ 1
  · simp [hx]
  simp [map_ne_zero_iff, germToFunctionField_injective, IsUnit.ne_zero hf,
    ord_eq_iff hx, ordHom_of_isUnit hf hx hx']

Goal state after:
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₂
α : r₁ ⟶ r₂
β : r₂ ⟶ r₁
αβ : α ≫ β = 𝟙 r₁
⊢ (conjugateEquiv adj₂ adj₁).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = 𝟙 l₁

Tactic:
conjugateEquiv_symm_comp,

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₂
α : r₁ ⟶ r₂
β : r₂ ⟶ r₁
αβ : α ≫ β = 𝟙 r₁
⊢ (conjugateEquiv adj₁ adj₁).symm (α ≫ β) = 𝟙 l₁
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₂
β : r₁ ≅ r₂
⊢ (conjugateEquiv adj₁ adj₂).symm β.hom ≫ (conjugateEquiv adj₂ adj₁).symm β.inv = 𝟙 l₂

Tactic:
conjugateEquiv_symm_comp,

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₂
β : r₁ ≅ r₂
⊢ (conjugateEquiv adj₂ adj₂).symm (β.inv ≫ β.hom) = 𝟙 l₂
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₂
β : r₁ ≅ r₂
⊢ (conjugateEquiv adj₂ adj₁).symm β.inv ≫ (conjugateEquiv adj₁ adj₂).symm β.hom = 𝟙 l₁

Tactic:
conjugateEquiv_symm_comp,

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₂
β : r₁ ≅ r₂
⊢ (conjugateEquiv adj₁ adj₁).symm (β.hom ≫ β.inv) = 𝟙 l₁
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
g : (j₀ : 𝒰.I₀) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.X j₀
hg :
  ∀ (j₀ : 𝒰.I₀) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.f j₀) (f ↑x) ⋯
R' : 𝒰.I₀ → CommRingCat := fun j₀ ↦ CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.I₀) → ↑(R' j₀)) :=
  { toFun := fun f x i ↦ f ↑i, invFun := fun f i ↦ f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
i : ι
this :
  (Pi.evalRingHom (fun x ↦ ↑(R x)) i).comp e.symm.toRingHom =
    (Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩).comp (Pi.evalRingHom (fun x ↦ ↑(R' x)) (j i))
⊢ pointsPi R X (Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫ inv (sigmaSpec R') ≫ Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.f j₀)
      i =
    f i

Tactic:
rw [pointsPi, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp, this, CommRingCat.ofHom_comp,
    Spec.map_comp_assoc, ← ι_sigmaSpec R', Category.assoc, IsIso.hom_inv_id_assoc,
    Sigma.ι_desc, ← Category.assoc, hg, IsOpenImmersion.lift_fac]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f₁ : a ⟶ c
u₁ : c ⟶ a
f₂ : b ⟶ d
u₂ : d ⟶ b
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : f₁ ⊣ u₁
adj₄ : f₂ ⊣ u₂
α : u₂ ≫ r₁ ⟶ r₂ ≫ u₁
⊢ (conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) ((mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α)) = α

Tactic:
← iterated_mateEquiv_conjugateEquiv

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
f₁ : a ⟶ c
u₁ : c ⟶ a
f₂ : b ⟶ d
u₂ : d ⟶ b
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : f₁ ⊣ u₁
adj₄ : f₂ ⊣ u₂
α : u₂ ≫ r₁ ⟶ r₂ ≫ u₁
⊢ (mateEquiv adj₄ adj₃) ((mateEquiv adj₁ adj₂) ((mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α))) = α
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f₁ : a ⟶ c
u₁ : c ⟶ a
f₂ : b ⟶ d
u₂ : d ⟶ b
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : f₁ ⊣ u₁
adj₄ : f₂ ⊣ u₂
α : u₂ ≫ r₁ ⟶ r₂ ≫ u₁
⊢ (mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α) = (conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm α

Tactic:
rw [Equiv.eq_symm_apply, ← iterated_mateEquiv_conjugateEquiv]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
f₁ : a ⟶ c
u₁ : c ⟶ a
f₂ : b ⟶ d
u₂ : d ⟶ b
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : f₁ ⊣ u₁
adj₄ : f₂ ⊣ u₂
α : u₂ ≫ r₁ ⟶ r₂ ≫ u₁
⊢ (mateEquiv adj₄ adj₃) ((mateEquiv adj₁ adj₂) ((mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α))) = α
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ a ∈ carrier f_deg q ↔
    HomogeneousLocalization.mk { deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal

Tactic:
trans (HomogeneousLocalization.mk ⟨m * n, ⟨proj 𝒜 n a ^ m, by rw [← smul_eq_mul]; mem_tac⟩,
    ⟨f ^ n, by rw [mul_comm]; mem_tac⟩, ⟨_, rfl⟩⟩ : A⁰_ f) ∈ q.asIdeal

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ a ∈ carrier f_deg q ↔
    HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal

A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal ↔
    HomogeneousLocalization.mk { deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
⊢ TopologicalSpace.IsOpenCover fun ir ↦ X.basicOpen (f ir.snd.fst)

Tactic:
by
    classical
    have H : Ideal.span (Set.range fun x : Σ' i r, 0 < i ∧ r ∈ 𝒜 i ↦ x.2.1) =
        (HomogeneousIdeal.irrelevant 𝒜).toIdeal := by
      apply le_antisymm
      · rw [Ideal.span_le, Set.range_subset_iff]
        rintro ⟨i, r, hi0, hri⟩
        simp [-ZeroMemClass.coe_eq_zero,
          DirectSum.decompose_of_mem_ne 𝒜 hri hi0.ne']
      · intro x hx
        rw [← DirectSum.sum_support_decompose 𝒜 x]
        refine Ideal.sum_mem _ fun c hc ↦ ?_
        have : c ≠ 0 := by contrapose hc; simpa [hc] using hx
        exact Ideal.subset_span ⟨⟨c, _, this.bot_lt, by simp⟩, rfl⟩
    ext1
    apply compl_injective
    simp only [TopologicalSpace.Opens.coe_iSup, Set.compl_iUnion, ← Scheme.zeroLocus_singleton,
      ← Scheme.zeroLocus_iUnion, Set.iUnion_singleton_eq_range, TopologicalSpace.Opens.coe_top,
      Set.compl_univ]
    rw [← Scheme.zeroLocus_span, Set.range_comp', ← Ideal.map_span, H, hf]
    simp

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

Goal state before:
pp: case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx : ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ ↑(fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r)
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ X.basicOpen (f r)

Tactic:
simp only [TopologicalSpace.Opens.map_coe, Set.mem_preimage, SetLike.mem_coe,
      ← Scheme.Hom.comp_apply, fromOfGlobalSections, Scheme.Cover.ι_glueMorphisms] at hx

Goal state after:
case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx : (toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫ (basicOpen 𝒜 i.snd.fst).ι) x ∈ basicOpen 𝒜 r
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ X.basicOpen (f r)