mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
x : ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V))
hx : x ∈ integralClosure ↑Γ(Y, Opposite.unop (Opposite.op V)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V))
i : Opposite.op V ⟶ Opposite.op U
algInst✝⁴ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst✝³ : Algebra ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ V) := (CommRingCat.Hom.hom (app f V)).toAlgebra
algInst✝² : Algebra ↑Γ(Y, V) ↑Γ(Y, U) := (CommRingCat.Hom.hom (Y.presheaf.map i)).toAlgebra
algInst✝¹ : Algebra ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
algInst✝ : Algebra ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯)).toAlgebra
⊢ algebraMap ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ U) = (algebraMap ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U)).comp (algebraMap ↑Γ(Y, V) ↑Γ(Y, U))

Tactic:
simp [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp]; rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m n : ℕ
⊢ resultant 0 0 m n = 0 ^ (m + n)

Tactic:
simp [pow_add]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case e'_3
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
e : ↑(fromNormalization f ⁻¹ᵁ ↑U) ≅ (normalizationOpenCover f).X U := ⋯
this : (CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op ↑U))).IsIntegral
e_1✝ : (normalizationOpenCover f).X U = Spec ((normalizationDiagram f).obj (Opposite.op ↑U))
⊢ (e.inv ≫ fromNormalization f ∣_ ↑U) ≫ (IsAffineOpen.isoSpec ⋯).hom =
    Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U))

Tactic:
← cancel_mono U.2.fromSpec

Goal state after:
case e'_3
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
e : ↑(fromNormalization f ⁻¹ᵁ ↑U) ≅ (normalizationOpenCover f).X U :=
  IsOpenImmersion.isoOfRangeEq (fromNormalization f ⁻¹ᵁ ↑U).ι ((normalizationOpenCover f).f U) ⋯
this : (CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op ↑U))).IsIntegral
e_1✝ : (normalizationOpenCover f).X U = Spec ((normalizationDiagram f).obj (Opposite.op ↑U))
⊢ ((e.inv ≫ fromNormalization f ∣_ ↑U) ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫ IsAffineOpen.fromSpec ⋯ =
    Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U)) ≫ IsAffineOpen.fromSpec ⋯
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (-1) ^ (2 * m + (n + 1)) = (-1) ^ (n + 1)

Tactic:
simp [pow_add]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n k✝ : ℕ
hf : f.natDegree ≤ m
k : ℕ
IH : f.resultant g (m + k) n = (-1) ^ (n * k) * g.coeff n ^ k * f.resultant g m n
⊢ f.resultant g (m + (k + 1)) n = (-1) ^ (n * (k + 1)) * g.coeff n ^ (k + 1) * f.resultant g m n

Tactic:
simp [← add_assoc, resultant_succ_left_deg, hf.trans, IH]

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n k✝ : ℕ
hf : f.natDegree ≤ m
k : ℕ
IH : f.resultant g (m + k) n = (-1) ^ (n * k) * g.coeff n ^ k * f.resultant g m n
⊢ (-1) ^ n * g.coeff n * ((-1) ^ (n * k) * g.coeff n ^ k * f.resultant g m n) =
    (-1) ^ (n * (k + 1)) * g.coeff n ^ (k + 1) * f.resultant g m n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
this :
  ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
    f.Monic →
      g.Monic →
        f.Splits →
          g.Splits →
            g.natDegree ≤ f.natDegree → f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
hfg : ¬g.natDegree ≤ f.natDegree
⊢ f.resultant g = (Multiset.map (fun ij ↦ -1 * (ij.2 - ij.1)) (f.roots ×ˢ g.roots)).prod

Tactic:
rw [resultant_comm, this g f hg hf hg' hf' (le_of_not_ge hfg), ← Multiset.map_swap_product,
        Multiset.map_map, Multiset.prod_map_mul]

Goal state after:
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
this :
  ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
    f.Monic →
      g.Monic →
        f.Splits →
          g.Splits →
            g.natDegree ≤ f.natDegree → f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
hfg : ¬g.natDegree ≤ f.natDegree
⊢ (-1) ^ (f.natDegree * g.natDegree) * (Multiset.map ((fun ij ↦ ij.1 - ij.2) ∘ Prod.swap) (f.roots ×ˢ g.roots)).prod =
    (Multiset.map (fun ij ↦ -1) (f.roots ×ˢ g.roots)).prod *
      (Multiset.map (fun ij ↦ ij.2 - ij.1) (f.roots ×ˢ g.roots)).prod
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case refine_1
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
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
⊢ t.Finite

Tactic:
simp only [t, Set.finite_insert]

Goal state after:
case refine_1
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
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
⊢ {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}.Finite
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
⊢ Spec.map
        (appLE f₂ (↑U) (f₂ ⁻¹ᵁ ↑U) ⋯ ≫
          CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
              (integralClosure ↑Γ(Y, toOpens U) ↑Γ(X, f ⁻¹ᵁ toOpens U)) ⋯)) ≫
      ⋯.fromSpec =
    (normalizationGlueData f).natTrans.app U ≫ (directedCover Y).f U

Tactic:
dsimp [normalizationGlueData, relativeGluingData, restrictIsoSpec]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
⊢ Spec.map
        (appLE f₂ (↑U) (f₂ ⁻¹ᵁ ↑U) ⋯ ≫
          CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
              (integralClosure ↑Γ(Y, toOpens U) ↑Γ(X, f ⁻¹ᵁ toOpens U)) ⋯)) ≫
      ⋯.fromSpec =
    (Spec.map ((normalizationDiagramMap f).app (Opposite.op (toOpens U))) ≫ ⋯.isoSpec.inv) ≫ (↑U).ι
Module: Mathlib.RingTheory.Ideal.Quotient.Over

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
f : S →ₐ[R] T
Hf : Function.Surjective ⇑f
P : Ideal R
P' : Ideal S
inst✝¹ : P'.IsPrime
inst✝ : P'.LiesOver P
hkP' : ¬RingHom.ker f.toRingHom ≤ P'
H : (P.primesOver S).Finite
⊢ P' ∉ comap f '' P.primesOver T

Tactic:
rintro ⟨q, ⟨_, _⟩, rfl⟩; exact hkP' (Ideal.ker_le_comap _)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H✝ : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
H : b.natDegree + g.natDegree < a.natDegree + f.natDegree
⊢ False

Tactic:
rw [← natDegree_mul ha hf, ← natDegree_mul hb hg] at H

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H✝ : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
H : (b * g).natDegree < (a * f).natDegree
⊢ False
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case tmul
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this : Algebra.IsIntegral R' (Localization.Away e₀)
a : R'
b : S
⊢ ∃ b_1 m,
    (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom b_1 =
      (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom (e₀ * 1 ⊗ₜ[R] g) ^ m * a ⊗ₜ[R] b

Tactic:
obtain ⟨b', m, e : _ = _⟩ := Localization.awayMap_surjective_iff.mp hg b
      refine ⟨e₀ ^ m * a ⊗ₜ b', m, ?_⟩
      simp [e, mul_pow, mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FaithfullyFlat R T
inst✝ : Module.Finite T (T ⊗[R] M)
n : ℕ
s : Fin n → T ⊗[R] M
hs : Submodule.span T (Set.range s) = ⊤
k : Fin n → ℕ
t : (i : Fin n) → Fin (k i) → T
m : (i : Fin n) → Fin (k i) → M
h : ∀ (i : Fin n), s i = ∑ j, t i j ⊗ₜ[R] m i j
f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M :=
  ((Pi.basisFun R ((i : Fin n) × Fin (k i))).constr R) fun x ↦
    match x with
    | ⟨i, j⟩ => m i j
⊢ ((AlgebraTensorModule.lTensor T T) f₀).range = ⊤

Tactic:
eq_top_iff,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FaithfullyFlat R T
inst✝ : Module.Finite T (T ⊗[R] M)
n : ℕ
s : Fin n → T ⊗[R] M
hs : Submodule.span T (Set.range s) = ⊤
k : Fin n → ℕ
t : (i : Fin n) → Fin (k i) → T
m : (i : Fin n) → Fin (k i) → M
h : ∀ (i : Fin n), s i = ∑ j, t i j ⊗ₜ[R] m i j
f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M :=
  ((Pi.basisFun R ((i : Fin n) × Fin (k i))).constr R) fun x ↦
    match x with
    | ⟨i, j⟩ => m i j
⊢ ⊤ ≤ ((AlgebraTensorModule.lTensor T T) f₀).range
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
⊢ IsOpen {x | QuasiFiniteAt f x}

Tactic:
by
  wlog H : IsAffineHom f
  · rw [isOpen_iff_forall_mem_open]
    intro x hx
    obtain ⟨_, ⟨U : Y.Opens, hU, rfl⟩, hxU, -⟩ := Y.isBasis_affineOpens.exists_subset_of_mem_open
      (Set.mem_univ (f x)) isOpen_univ
    obtain ⟨_, ⟨V : X.Opens, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open
      hxU (f ⁻¹ᵁ U).2
    have inst : IsAffineHom (f.resLE U V hVU) :=
      have : IsAffine _ := hU
      have : IsAffine _ := hV
      isAffineHom_of_isAffine _
    refine ⟨_, ?_, V.2.isOpenEmbedding_subtypeVal.isOpenMap _ (this (f.resLE U V hVU) inst), ?_⟩
    · rintro _ ⟨x : V, hx : (f.resLE U V hVU).QuasiFiniteAt _, rfl⟩
      rwa [← quasiFiniteAt_comp_iff (g := U.ι), resLE_comp_ι,
        quasiFiniteAt_comp_iff_of_isOpenImmersion] at hx
    · refine ⟨⟨x, hxV⟩, show (f.resLE _ _ _).QuasiFiniteAt _ from ?_, rfl⟩
      rwa [← quasiFiniteAt_comp_iff (g := U.ι), resLE_comp_ι,
        quasiFiniteAt_comp_iff_of_isOpenImmersion]
  obtain ⟨U, hU, e⟩ := Scheme.Hom.exists_isIso_morphismRestrict_toNormalization f
  exact e ▸ (f.toNormalization ⁻¹ᵁ U).2

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : FiniteType T (T ⊗[R] S)
s : Finset (T ⊗[R] S)
hs : adjoin T ↑s = ⊤
k : ↥s → ℕ
t : (x : ↥s) → Fin (k x) → T
m : (x : ↥s) → Fin (k x) → S
h : ∀ (x : ↥s), ↑x = ∑ j, t x j ⊗ₜ[R] m x j
f : MvPolynomial ((x : ↥s) × Fin (k x)) R →ₐ[R] S :=
  MvPolynomial.aeval fun x ↦
    match x with
    | ⟨x, i⟩ => m x i
x : T ⊗[R] S
hx : x ∈ ↑s
i : ↥s := ⟨x, hx⟩
⊢ x ∈ ↑(TensorProduct.map (AlgHom.id T T) f).range

Tactic:
use ∑ (j : Fin (k i)), t i j ⊗ₜ MvPolynomial.X ⟨i, j⟩

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : FiniteType T (T ⊗[R] S)
s : Finset (T ⊗[R] S)
hs : adjoin T ↑s = ⊤
k : ↥s → ℕ
t : (x : ↥s) → Fin (k x) → T
m : (x : ↥s) → Fin (k x) → S
h : ∀ (x : ↥s), ↑x = ∑ j, t x j ⊗ₜ[R] m x j
f : MvPolynomial ((x : ↥s) × Fin (k x)) R →ₐ[R] S := ⋯
x : T ⊗[R] S
hx : x ∈ ↑s
i : ↥s := ⋯
⊢ (TensorProduct.map (AlgHom.id T T) f).toRingHom (∑ j, t i j ⊗ₜ[R] MvPolynomial.X ⟨i, j⟩) = x
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case zero
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
t : T
⊢ (P.tensorCotangentSpace T) (t ⊗ₜ[R] 0) = t • (CotangentSpace.map (toBaseChange T)) 0

Tactic:
tmul_zero,

Goal state after:
case zero
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
t : T
⊢ (P.tensorCotangentSpace T) 0 = t • (CotangentSpace.map (toBaseChange T)) 0
Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f g : b ⟶ c
pf : a ⟶ c
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η.symm ≪≫ η_f = η_g

Tactic:
rw [← ih]
  apply Iso.ext (by simp)

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : Adj B
α β : a ⟶ b
x y : α ⟶ β
hl : x.τl = y.τl
⊢ x.τr = y.τr

Tactic:
simp only [← Hom₂.conjugateEquiv_τl, hl]

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₂) ⊗≫
      r₁ ◁ (g₁ ≫ g₂) ◁ adj₃.unit ⊗≫
        r₁ ◁ ((α_ g₁ g₂ l₃).hom ≫ g₁ ◁ β ≫ (α_ g₁ l₂ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ r₃ ⊗≫
          adj₁.counit ▷ (h₁ ≫ h₂) ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    (α_ 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

Tactic:
symm

Goal state after:
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₁ ≫ g₂) ◁ adj₃.unit ⊗≫
        r₁ ◁ ((α_ g₁ g₂ l₃).hom ≫ g₁ ◁ β ≫ (α_ g₁ l₂ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ r₃ ⊗≫
          adj₁.counit ▷ (h₁ ≫ h₂) ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
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₂) ⊗≫
      r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ 𝟙 e) ≫ (l₂ ≫ r₂) ◁ g₂ ◁ adj₃.unit) ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ l₃) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ β) ▷ r₃ ⊗≫
          (adj₁.counit ▷ h₁ ▷ (r₂ ≫ l₂) ≫ (𝟙 b ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ l₃) ≫ (l₂ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
          r₁ ◁ (α ▷ (r₂ ≫ l₂) ≫ (l₁ ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)

Tactic:
rw [← whisker_exchange, ← whisker_exchange, ← whisker_exchange]

Goal state after:
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₂) ⊗≫
      r₁ ◁ g₁ ◁ (𝟙 c ◁ g₂ ◁ adj₃.unit ≫ adj₂.unit ▷ (g₂ ≫ l₃ ≫ r₃)) ⊗≫
        r₁ ◁ ((g₁ ≫ l₂) ◁ r₂ ◁ β ≫ α ▷ (r₂ ≫ l₂ ≫ h₂)) ▷ r₃ ⊗≫
          (((r₁ ≫ l₁) ≫ h₁) ◁ adj₂.counit ≫ adj₁.counit ▷ h₁ ▷ 𝟙 d) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ l₃) ≫ (l₂ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
          r₁ ◁ (α ▷ (r₂ ≫ l₂) ≫ (l₁ ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], finrank f = 1 → (∃ R, Y = Spec R) → IsIso f
hY : ¬∃ R, Y = Spec R
⊢ IsIso f

Tactic:
rw [← MorphismProperty.isomorphisms.iff,
      IsZariskiLocalAtTarget.iff_of_openCover (P := .isomorphisms Scheme) Y.affineCover]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], finrank f = 1 → (∃ R, Y = Spec R) → IsIso f
hY : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    MorphismProperty.isomorphisms Scheme (Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsNoetherianRing R
inst✝³ : KrullDimLE 1 R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : IsUnit x
⊢ (ordFrac R) ((algebraMap R K) x) = 1

Tactic:
by
  simp [ordFrac_eq_ord R (IsUnit.ne_zero hx), IsUnit.mem_nonZeroDivisors hx,
      ordMonoidWithZeroHom_eq_ord, ord_of_isUnit hx]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
⊢ (mateEquiv adj₁ adj₃) (leftAdjointSquareConjugate.vcomp α β) =
    rightAdjointSquareConjugate.vcomp ((mateEquiv adj₁ adj₂) α) ((conjugateEquiv adj₂ adj₃) β)

Tactic:
symm

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
⊢ rightAdjointSquareConjugate.vcomp ((mateEquiv adj₁ adj₂) α) ((conjugateEquiv adj₂ adj₃) β) =
    (mateEquiv adj₁ adj₃) (leftAdjointSquareConjugate.vcomp α β)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
⊢ (mateEquiv adj₁ adj₃) (leftAdjointConjugateSquare.vcomp α β) =
    rightAdjointConjugateSquare.vcomp ((conjugateEquiv adj₁ adj₂) α) ((mateEquiv adj₂ adj₃) β)

Tactic:
symm

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
⊢ rightAdjointConjugateSquare.vcomp ((conjugateEquiv adj₁ adj₂) α) ((mateEquiv adj₂ adj₃) β) =
    (mateEquiv adj₁ adj₃) (leftAdjointConjugateSquare.vcomp α β)
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: case inl
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
ha : antidiag = {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂)) (x * y) =
    (proj 𝒜 max₁) x * (proj 𝒜 max₂) y + ∑ ij ∈ antidiag.erase (max₁, max₂), (proj 𝒜 ij.1) x * (proj 𝒜 ij.2) y
i j : ι
H₁ : ¬(i = max₁ ∧ j = max₂)
H₄ : i + j = max₁ + max₂
H₂ : i ∈ DFinsupp.support ((decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support ((decompose 𝒜) y)
max_lt : max₁ < i
notMem : i ∈ DFinsupp.support ((decompose 𝒜) x) → (proj 𝒜 i) x ∈ I
⊢ (proj 𝒜 (i, j).1) x * (proj 𝒜 (i, j).2) y ∈ I

Tactic:
exact Ideal.mul_mem_right _ I (notMem H₂)

Goal state after: