mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this : (E.sigmaOfIsColimit hc).HasPullbacks
i : E.I₀
⊢ HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)

Tactic:
dsimp [sigmaOfIsColimit_f]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this : (E.sigmaOfIsColimit hc).HasPullbacks
i : E.I₀
⊢ HasPullback (E.f i) (Cofan.IsColimit.desc hc E.f)
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝ : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
⊢ (piComparison F fun x ↦ op (X x)) =
    F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫ Pi.lift fun i ↦ F.map (c.inj i).op

Tactic:
have h : Pi.lift (fun i ↦ F.map (c.inj i).op) =
      F.map (Pi.lift (fun i ↦ (c.inj i).op)) ≫ piComparison F _ := by simp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝ : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
h : (Pi.lift fun i ↦ F.map (c.inj i).op) = F.map (Pi.lift fun i ↦ (c.inj i).op) ≫ piComparison F fun i ↦ op (X i)
⊢ (piComparison F fun x ↦ op (X x)) =
    F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫ Pi.lift fun i ↦ F.map (c.inj i).op
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W ![0, 1, 0] = -toAffine W P

Tactic:
toAffine_zero,

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ 0 = -toAffine W P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ ⇑f ∘ P ≈ ⇑f ∘ Q ↔ P ≈ Q

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Goal state after:
case refine_1
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
⊢ P ≈ Q

case refine_2
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
⊢ ⇑f ∘ P ≈ ⇑f ∘ Q
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
⊢ Equalizer.Presieve.Arrows.firstMap F X c.inj = Equalizer.Presieve.Arrows.secondMap F X c.inj

Tactic:
ext ⟨i, j⟩ a
  simp only [Equalizer.Presieve.Arrows.firstMap, limit.lift_π, Fan.mk_π_app,
    TypeCat.Fun.toFun_apply, comp_apply, Equalizer.Presieve.Arrows.secondMap]
  by_cases hi : i = j
  · rw [hi, Mono.right_cancellation _ _ pullback.condition]
  · have := preservesTerminal_of_isSheaf_for_empty F hF hI
    apply_fun (F.mapIso ((hd hi).isoPullback).op ≪≫ F.mapIso (terminalIsoIsTerminal
      (terminalOpOfInitial initialIsInitial)).symm ≪≫ (PreservesTerminal.iso F)).hom using
      injective_of_mono _
    ext ⟨i⟩
    exact i.elim

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ toAffine W ![0, 1, 0] = toAffine W Q

Tactic:
toAffine_zero,

Goal state after:
case pos
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ 0 = toAffine W Q
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: X : TopCat
⊢ ∀ ⦃X_1 : TopCat⦄ (E : precoverage.ZeroHypercover X_1), Presieve.IsSheafFor (yoneda.obj X) E.presieve₀

Tactic:
intro Y

Goal state after:
X Y : TopCat
⊢ ∀ (E : precoverage.ZeroHypercover Y), Presieve.IsSheafFor (yoneda.obj X) E.presieve₀
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: X Y : Scheme
S : Presieve Y
hS : S ∈ (precoverage IsOpenImmersion).coverings Y
x : Presieve.FamilyOfElements (yoneda.obj X) S
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t

Tactic:
obtain ⟨(𝓤 : OpenCover Y), rfl⟩ := exists_cover_of_mem_pretopology hS

Goal state after:
X Y : Scheme
𝓤 : Y.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y
x : Presieve.FamilyOfElements (yoneda.obj X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{u_2, u_1} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
⊢ Sieve.generate (Presieve.ofArrows F.obj (colimit.ι F)) ≤ Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app)

Tactic:
Sieve.generate_le_iff

Goal state after:
J : Type u_1
inst✝⁴ : Category.{u_2, u_1} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
⊢ Presieve.ofArrows F.obj (colimit.ι F) ≤ (Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app)).arrows
Module: Mathlib.AlgebraicGeometry.GluingOneHypercover

Goal state before:
pp: D : GlueData
⊢ Sieve.ofArrows D.openCover.X D.openCover.f ≤ { I₀ := D.J, X := D.U, f := D.ι }.sieve₀

Tactic:
Sieve.generate_le_iff

Goal state after:
D : GlueData
⊢ Presieve.ofArrows D.openCover.X D.openCover.f ≤ { I₀ := D.J, X := D.U, f := D.ι }.sieve₀.arrows
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝¹ : FormallyUnramified K L
this✝ : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := ⋯
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
this : IsUnit ((Ideal.Quotient.mk I) ((aeval x) (derivative (minpoly K pb.gen))))
u : B
hu : (Ideal.Quotient.mk I) u = -↑this.unit⁻¹
⊢ (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I

Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, map_add, map_mul, map_one, hu, mul_neg,
      IsUnit.mul_val_inv, neg_add_cancel]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
⊢ IsScalarTower R A (S ⊗[R] Ω[A⁄R])

Tactic:
by
  apply IsScalarTower.of_algebraMap_smul
  intro r x
  induction x
  · simp only [smul_zero]
  · rw [mulActionBaseChange_smul_tmul, algebraMap_smul, tmul_smul]
  · simp only [smul_add, *]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
⊢ Function.Surjective ⇑(ofTensorProduct I M)

Tactic:
obtain ⟨n, p, hp⟩ := Module.Finite.exists_fin' R M

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
⊢ Function.Surjective ⇑(ofTensorProduct I M)
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
p q : Submodule R M
hpq : IsCompl p q
hmap : map g q = ⊤
x : ↥p
triv : x ∈ ⊤
⊢ x ∈ map (p.projectionOnto q hpq) g.ker

Tactic:
obtain ⟨a, haq, ha⟩ : g x.val ∈ q.map g := by rwa [hmap]

Goal state after:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
p q : Submodule R M
hpq : IsCompl p q
hmap : map g q = ⊤
x : ↥p
triv : x ∈ ⊤
a : M
haq : a ∈ ↑q
ha : g a = g ↑x
⊢ x ∈ map (p.projectionOnto q hpq) g.ker
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ W.dblXYZ P =
    W.dblZ P •
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]

Tactic:
have hZ : IsUnit <| W.dblZ P := isUnit_dblZ_of_Y_ne' hP hQ hPz hQz hx hy

Goal state after:
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
hZ : IsUnit (W.dblZ P)
⊢ W.dblXYZ P =
    W.dblZ P •
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case hQa
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n

Tactic:
exact isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway n

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : (aeval a) q₁ = 0
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : q₂.totalDegree ≤ 0
⊢ IsUnit q₁ ∨ IsUnit q₂

Tactic:
nonpos_iff_eq_zero

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : (aeval a) q₁ = 0
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : q₂.totalDegree = 0
⊢ IsUnit q₁ ∨ IsUnit q₂
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
X Y : Scheme
inst✝ : P.RespectsIso
f : X ⟶ Y
x✝ : sourceLocalClosure IsOpenImmersion P f
x : ↥X
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ ∃ U, x ∈ U ∧ P (U.ι ≫ f)

pp: case refine_2
P : MorphismProperty Scheme
X Y : Scheme
inst✝ : P.RespectsIso
f : X ⟶ Y
H : ∀ (x : ↥X), ∃ U, x ∈ U ∧ P (U.ι ≫ f)
⊢ sourceLocalClosure IsOpenImmersion P f

Tactic:
· refine ⟨(𝒰.f (𝒰.idx x)).opensRange, 𝒰.covers x, ?_⟩
    rw [← Scheme.Hom.isoOpensRange_inv_comp, Category.assoc, P.cancel_left_of_respectsIso]
    apply hf

Goal state after:
case refine_2
P : MorphismProperty Scheme
X Y : Scheme
inst✝ : P.RespectsIso
f : X ⟶ Y
H : ∀ (x : ↥X), ∃ U, x ∈ U ∧ P (U.ι ≫ f)
⊢ sourceLocalClosure IsOpenImmersion P f
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis k fun x ↦ a ↑x
⊢ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)

Tactic:
let k' := adjoin k (a '' {i}ᶜ)

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis k fun x ↦ a ↑x
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
⊢ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this : IsDominant i
x✝ : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f (g₁ x✝) ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : g₁ x✝ ∈ ↑V
hVU : V ≤ f ⁻¹ᵁ U
x : ↥Z'
⊢ g₁ (i x) = g₂ (i x)

Tactic:
exact congr($hig x)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P Q : Fin 3 → R
⊢ (W'.map f).addX (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addX P Q)

Tactic:
simp only [addX]

Goal state after:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P Q : Fin 3 → R
⊢ -(⇑f ∘ P) x * (⇑f ∘ Q) y ^ 2 * (⇑f ∘ P) z + (⇑f ∘ Q) x * (⇑f ∘ P) y ^ 2 * (⇑f ∘ Q) z -
                                2 * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) y * (⇑f ∘ Q) z +
                              2 * (⇑f ∘ Q) x * (⇑f ∘ P) y * (⇑f ∘ Q) y * (⇑f ∘ P) z -
                            (W'.map f).a₁ * (⇑f ∘ P) x ^ 2 * (⇑f ∘ Q) y * (⇑f ∘ Q) z +
                          (W'.map f).a₁ * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) y * (⇑f ∘ P) z +
                        (W'.map f).a₂ * (⇑f ∘ P) x ^ 2 * (⇑f ∘ Q) x * (⇑f ∘ Q) z -
                      (W'.map f).a₂ * (⇑f ∘ P) x * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) z -
                    (W'.map f).a₃ * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) z ^ 2 +
                  (W'.map f).a₃ * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 2 -
                2 * (W'.map f).a₃ * (⇑f ∘ P) x * (⇑f ∘ Q) y * (⇑f ∘ P) z * (⇑f ∘ Q) z +
              2 * (W'.map f).a₃ * (⇑f ∘ Q) x * (⇑f ∘ P) y * (⇑f ∘ P) z * (⇑f ∘ Q) z +
            (W'.map f).a₄ * (⇑f ∘ P) x ^ 2 * (⇑f ∘ Q) z ^ 2 -
          (W'.map f).a₄ * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) z ^ 2 +
        3 * (W'.map f).a₆ * (⇑f ∘ P) x * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 2 -
      3 * (W'.map f).a₆ * (⇑f ∘ Q) x * (⇑f ∘ P) z ^ 2 * (⇑f ∘ Q) z =
    f
      (-P x * Q y ^ 2 * P z + Q x * P y ^ 2 * Q z - 2 * P x * P y * Q y * Q z + 2 * Q x * P y * Q y * P z -
                              W'.a₁ * P x ^ 2 * Q y * Q z +
                            W'.a₁ * Q x ^ 2 * P y * P z +
                          W'.a₂ * P x ^ 2 * Q x * Q z -
                        W'.a₂ * P x * Q x ^ 2 * P z -
                      W'.a₃ * P x * P y * Q z ^ 2 +
                    W'.a₃ * Q x * Q y * P z ^ 2 -
                  2 * W'.a₃ * P x * Q y * P z * Q z +
                2 * W'.a₃ * Q x * P y * P z * Q z +
              W'.a₄ * P x ^ 2 * Q z ^ 2 -
            W'.a₄ * Q x ^ 2 * P z ^ 2 +
          3 * W'.a₆ * P x * P z * Q z ^ 2 -
        3 * W'.a₆ * Q x * P z ^ 2 * Q z)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦
    RingHom.FaithfullyFlat
⊢ P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
refine HasRingHomProperty.descendsAlong _ _ _ _ ?_ ?_ h
  · rw [inf_comm]
    gcongr
    exact IsLocalIso.le_of_isZariskiLocalAtSource @Flat
  · intro R S f ⟨hf₁, hf₂⟩
    rw [RingHom.FaithfullyFlat.iff_flat_and_comap_surjective]
    refine ⟨?_, (Spec.map f).surjective⟩
    rwa [HasRingHomProperty.Spec_iff (P := @Flat)] at hf₂

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
M : Submonoid S
inst✝¹ : IsLocalization M T
inst✝ : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
p : R[X]
u : S
s : ↥M
hp : (aeval ((algebraMap S T) x)) p * IsLocalization.mk' T u s = 0
a : S
haM : a ∈ M
e : a * ((aeval x) p * u) = 0
this : map (algebraMap R T) p * C (a • (algebraMap S T) u) = 0
⊢ map (algebraMap R T) p * C (IsLocalization.mk' T u s) * C ((algebraMap S T) ↑(⟨a, haM⟩ * s)) =
    0 * C ((algebraMap S T) ↑(⟨a, haM⟩ * s))

Tactic:
simpa [mul_assoc, ← map_mul, mul_comm _ (algebraMap _ _ _), ← Algebra.smul_def, mul_smul]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
hx : IsIntegral (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) (C x * X)
h✝ : Subsingleton R
⊢ ∃ p, p.Monic ∧ (aeval x) p = 0 ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)

Tactic:
use 0; simp [Monic, Subsingleton.elim (α := R) 0 1]

Goal state after:
Module: Mathlib.RingTheory.RingHom.QuasiFinite

Goal state before:
pp: R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite) ((algebraMap S (Localization.Away ↑r)).comp f✝)
algInst✝ : Algebra R S := f✝.toAlgebra
P : Ideal R
x✝ : P.IsPrime
this✝¹ : ∀ (r : ↥s), Module.Finite P.ResidueField (P.Fiber (Localization.Away ↑r))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away ↑r) :=
  fun r ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away ↑r))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away ↑r) := AlgHom.pi φ
this✝ : IsNoetherian P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away ↑r))
a : P.Fiber S
ha : f a = 0
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
I : ↑(P.primesOver S) := (PrimeSpectrum.primesOverOrderIsoFiber R S P).symm { asIdeal := J, isPrime := ⋯ }
this : ¬↑s ⊆ ↑↑I
r : S
hrs : r ∈ ↑s
hrI : r ∉ ↑↑I
ψ : P.Fiber (Localization.Away r) →ₐ[P.ResidueField] Localization.AtPrime J :=
  Algebra.TensorProduct.lift (Algebra.ofId P.ResidueField (Localization.AtPrime J))
    { toRingHom := IsLocalization.map (Localization.AtPrime J) Algebra.TensorProduct.includeRight.toRingHom ⋯,
      commutes' := ⋯ }
    ⋯
hψ : ψ.comp (φ ⟨r, hrs⟩) = IsScalarTower.toAlgHom P.ResidueField (P.Fiber S) (Localization.AtPrime J)
⊢ (algebraMap (P.Fiber S) (Localization.AtPrime J)) a = 0

Tactic:
refine congr($hψ a).symm.trans
    (show ψ (f a ⟨r, hrs⟩) = 0 by simp only [ha, Pi.zero_apply, map_zero])

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)

Tactic:
div_mul_div_comm,

Goal state after:
case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num /
      (Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom)
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : CommRing T
inst✝² : Algebra R T
p : Ideal R
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : QuasiFiniteAt R q
⊢ WeaklyQuasiFiniteAt R q

Tactic:
weaklyQuasiFiniteAt_iff

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : CommRing T
inst✝² : Algebra R T
p : Ideal R
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : QuasiFiniteAt R q
⊢ QuasiFinite R (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))