mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case neg
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ¬P ≈ Q
⊢ (W.map f).addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Tactic:
add_of_not_equiv h,

Goal state after:
case neg
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ¬P ≈ Q
⊢ (W.map f).addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.addXYZ P Q
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul.add
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
h : Algebra.IsPushout R S A B
a : A
x✝ y✝ : S ⊗[R] Ω[A⁄R]
a✝¹ :
  (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • x✝) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) x✝
a✝ :
  (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • y✝) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) y✝
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • (x✝ + y✝)) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) (x✝ + y✝)

Tactic:
· simp only [map_add, smul_add, *]

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

Goal state before:
pp: case tmul.add
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
h : Algebra.IsPushout R S A B
x n₁✝ n₂✝ : B
a✝¹ : x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) n₁✝) = x • (D S B) n₁✝
a✝ : x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) n₂✝) = x • (D S B) n₂✝
⊢ x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) (n₁✝ + n₂✝)) =
    x • (D S B) (n₁✝ + n₂✝)

Tactic:
· simp only [map_add, smul_add, *]

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
⊢ IsUnit (LinearMap.det P.aevalDifferential) ↔ Function.Bijective ⇑P.aevalDifferential

Tactic:
← LinearMap.isUnit_iff_isUnit_det

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
⊢ IsUnit P.aevalDifferential ↔ Function.Bijective ⇑P.aevalDifferential
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: case refine_2
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
y : AdicCompletion I N
⊢ y ∈ (map I g).ker → y ∈ (map I f).range

Tactic:
· apply AdicCompletion.induction_on I N y (fun b ↦ ?_)
    intro hz
    obtain ⟨k, hk⟩ := Ideal.exists_pow_inf_eq_pow_smul I (LinearMap.range f)
    have hb (n : ℕ) : g (b n) ∈ (I ^ n • ⊤ : Submodule R P) := by
      simpa using congrArg (fun x ↦ x.val n) hz
    let a := mapExactAux hf hfg hg hk b hb
    refine ⟨AdicCompletion.mk I M (AdicCauchySequence.mk I M (fun n ↦ (a n : M)) ?_), ?_⟩
    · refine fun n ↦ SModEq.symm ?_
      simp [a, mapExactAux, SModEq]
    · ext n
      suffices h : Submodule.Quotient.mk (p := (I ^ n • ⊤ : Submodule R N)) (f (a n)) =
            Submodule.Quotient.mk (p := (I ^ n • ⊤ : Submodule R N)) (b (k + n)) by
        simp [h, AdicCauchySequence.mk_eq_mk (show n ≤ k + n by lia)]
      rw [Submodule.Quotient.eq]
      have hle : (I ^ (k + n) • ⊤ : Submodule R N) ≤ (I ^ n • ⊤ : Submodule R N) :=
        Submodule.smul_mono_left (Ideal.pow_le_pow_right (by lia))
      exact hle (a n).property

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm : Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤
hk : Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
inst✝ : Subsingleton (H1Cotangent R S)
⊢ Function.Bijective ⇑(P.cotangentRestrict hu)

Tactic:
cotangentRestrict,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm : Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤
hk : Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
inst✝ : Subsingleton (H1Cotangent R S)
⊢ Function.Bijective ⇑(Finsupp.lcomapDomain u hu ∘ₗ ↑P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex)
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
⊢ IsStableUnderBaseChange (@IsStandardSmoothOfRelativeDimension n)

Tactic:
by
  apply IsStableUnderBaseChange.mk
  · exact isStandardSmoothOfRelativeDimension_respectsIso
  · introv h
    replace h : Algebra.IsStandardSmoothOfRelativeDimension n R T := by
      rw [RingHom.IsStandardSmoothOfRelativeDimension] at h
      convert! h; ext; simp_rw [Algebra.smul_def]; rfl
    suffices Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T) by
      rw [RingHom.IsStandardSmoothOfRelativeDimension]
      convert! this; ext; simp_rw [Algebra.smul_def]; rfl
    infer_instance

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ W'.negAddY (u • P) (v • Q) = (u * v) ^ 2 * W'.negAddY P Q

Tactic:
simp only [negAddY, smul_fin3_ext]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ -3 * (u * P x) ^ 2 * (v * Q x) * (v * Q y) + 3 * (u * P x) * (v * Q x) ^ 2 * (u * P y) -
                                    (u * P y) ^ 2 * (v * Q y) * (v * Q z) +
                                  u * P y * (v * Q y) ^ 2 * (u * P z) +
                                W'.a₁ * (u * P x) * (v * Q y) ^ 2 * (u * P z) -
                              W'.a₁ * (v * Q x) * (u * P y) ^ 2 * (v * Q z) -
                            W'.a₂ * (u * P x) ^ 2 * (v * Q y) * (v * Q z) +
                          W'.a₂ * (v * Q x) ^ 2 * (u * P y) * (u * P z) +
                        2 * W'.a₂ * (u * P x) * (v * Q x) * (u * P y) * (v * Q z) -
                      2 * W'.a₂ * (u * P x) * (v * Q x) * (v * Q y) * (u * P z) -
                    W'.a₃ * (u * P y) ^ 2 * (v * Q z) ^ 2 +
                  W'.a₃ * (v * Q y) ^ 2 * (u * P z) ^ 2 +
                W'.a₄ * (u * P x) * (u * P y) * (v * Q z) ^ 2 -
              2 * W'.a₄ * (u * P x) * (v * Q y) * (u * P z) * (v * Q z) +
            2 * W'.a₄ * (v * Q x) * (u * P y) * (u * P z) * (v * Q z) -
          W'.a₄ * (v * Q x) * (v * Q y) * (u * P z) ^ 2 +
        3 * W'.a₆ * (u * P y) * (u * P z) * (v * Q z) ^ 2 -
      3 * W'.a₆ * (v * Q y) * (u * P z) ^ 2 * (v * Q z) =
    (u * v) ^ 2 *
      (-3 * P x ^ 2 * Q x * Q y + 3 * P x * Q x ^ 2 * P y - P y ^ 2 * Q y * Q z + P y * Q y ^ 2 * P z +
                                  W'.a₁ * P x * Q y ^ 2 * P z -
                                W'.a₁ * Q x * P y ^ 2 * Q z -
                              W'.a₂ * P x ^ 2 * Q y * Q z +
                            W'.a₂ * Q x ^ 2 * P y * P z +
                          2 * W'.a₂ * P x * Q x * P y * Q z -
                        2 * W'.a₂ * P x * Q x * Q y * P z -
                      W'.a₃ * P y ^ 2 * Q z ^ 2 +
                    W'.a₃ * Q y ^ 2 * P z ^ 2 +
                  W'.a₄ * P x * P y * Q 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₄ * Q x * Q y * P z ^ 2 +
          3 * W'.a₆ * P y * P z * Q z ^ 2 -
        3 * W'.a₆ * Q y * P z ^ 2 * Q z)
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ @LocallyOfFiniteType ⊓ @FormallyUnramified ≤ diagonal @Etale

Tactic:
intro X Y f ⟨hft, hfu⟩

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hft : LocallyOfFiniteType f
hfu : FormallyUnramified f
⊢ diagonal (@Etale) f
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure

Goal state before:
pp: W P Q : MorphismProperty Scheme
X✝ Y✝ : Scheme
inst✝³ : W.IsStableUnderBaseChange
inst✝² : Scheme.IsJointlySurjectivePreserving W
inst✝¹ : P.RespectsLeft Q
inst✝ : Q.IsStableUnderBaseChange
X Y Z : Scheme
f : X ⟶ Y
hf : Q f
g : Y ⟶ Z
x✝ : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) Y
hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g)
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
⊢ P ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f ≫ g)

Tactic:
simpa [pullback.condition_assoc] using
    RespectsLeft.precomp (Q := Q) _ (Q.pullback_snd _ _ hf) _ (hg i)

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

Goal state before:
pp: case refine_1
⊢ @IsLocalIso ≤ ⨅ P, ⨅ (_ : P.ContainsIdentities), ⨅ (_ : IsZariskiLocalAtSource P), P

Tactic:
simp only [le_iInf_iff]
    apply le_of_isZariskiLocalAtSource

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).OpenCover :=
  fun j ↦ ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).affineCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀
j : (𝒰X i).I₀
⊢ IsOpenImmersion
    (pullback.diagonal f ∣_
      Scheme.Hom.opensRange ((Scheme.Pullback.diagonalCover f 𝒰Y 𝒰X).f ⟨⟨i, j⟩.fst, (⟨i, j⟩.snd, ⟨i, j⟩.snd)⟩))

Tactic:
arrow_mk_iso_iff (P := @IsOpenImmersion)
      (Scheme.Pullback.diagonalRestrictIsoDiagonal f 𝒰Y 𝒰X i j)

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).OpenCover :=
  fun j ↦ ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).affineCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀
j : (𝒰X i).I₀
⊢ IsOpenImmersion (pullback.diagonal ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)))
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).OpenCover :=
  fun j ↦ ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).affineCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀
j : (𝒰X i).I₀
hu : FormallyUnramified ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i))
hfin : LocallyOfFiniteType ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i))
⊢ IsOpenImmersion (pullback.diagonal ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)))

Tactic:
exact this _ ⟨⟨_, rfl⟩, ⟨_, rfl⟩⟩

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

Goal state before:
pp: X Y : Scheme
f✝ : X ⟶ Y
S R : CommRingCat
f : R ⟶ S
inst✝¹ : FormallyUnramified (Spec.map f)
inst✝ : LocallyOfFiniteType (Spec.map f)
⊢ IsOpenImmersion (pullback.diagonal (Spec.map f))

Tactic:
HasRingHomProperty.Spec_iff (P := @FormallyUnramified),

Goal state after:
X Y : Scheme
f✝ : X ⟶ Y
S R : CommRingCat
f : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom f).FormallyUnramified
inst✝ : LocallyOfFiniteType (Spec.map f)
⊢ IsOpenImmersion (pullback.diagonal (Spec.map 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 : adjoin k (Set.range a) = ⊤
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
i : ι
hi : (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
⊢ ∃ i, (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ Algebra.IsSeparable (↥(adjoin k (a '' {i}ᶜ))) K

Tactic:
refine ⟨i, hi.1, ?_⟩

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 : adjoin k (Set.range a) = ⊤
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
i : ι
hi : (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
⊢ Algebra.IsSeparable (↥(adjoin k (a '' {i}ᶜ))) K
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : P.RespectsIso
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
f : Spec T ⟶ Spec R
g : Spec S ⟶ Spec R
h : P' f
hf : P (pullback.fst f g)
⊢ P g

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective g
  obtain ⟨ψ, rfl⟩ := Spec.map_surjective f
  algebraize [φ.hom, ψ.hom]
  replace hf : P (pullback.fst (Spec.map <| CommRingCat.ofHom <| algebraMap R T)
    (Spec.map <| CommRingCat.ofHom <| algebraMap R S)) := hf
  rw [H₂]
  refine hQQ'.algebraMap_tensorProduct (R := R) (S := T) (T := S) _ (H₁ h) ?_
  rwa [← pullbackSpecIso_hom_fst R T S, P.cancel_left_of_respectsIso, H₂] at hf

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

Goal state before:
pp: ⊢ (isomorphisms Scheme).DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
apply IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact
  · rw [inf_comm]
    exact inf_le_inf le_rfl (IsLocalIso.le_of_isZariskiLocalAtSource _)
  intro R S Y φ g h (hfst : IsIso _)
  have : IsAffine Y :=
    have : UniversallyInjective g :=
      of_pullback_fst_of_descendsAlong (P := @UniversallyInjective) (f := Spec.map φ)
        (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) ⟨h, inferInstance⟩ inferInstance
    have : Surjective g :=
      of_pullback_fst_of_descendsAlong (P := @Surjective) (f := Spec.map φ)
        (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) ⟨h, inferInstance⟩ inferInstance
    have hopen' : UniversallyOpen g :=
      of_pullback_fst_of_descendsAlong (P := @UniversallyOpen) (f := Spec.map φ)
        (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) ⟨h, inferInstance⟩ inferInstance
    have : IsHomeomorph g.base := ⟨g.continuous, g.isOpenMap, g.injective, g.surjective⟩
    have : IsAffineHom g :=
      isAffineHom_of_isInducing g this.isInducing this.isClosedEmbedding.isClosed_range
    isAffine_of_isAffineHom g
  wlog hY : ∃ T, Y = Spec T generalizing Y
  · rw [← (isomorphisms Scheme).cancel_left_of_respectsIso Y.isoSpec.inv]
    have heq : pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g) =
      pullback.map _ _ _ _ (𝟙 _) (Y.isoSpec.inv) (𝟙 _) (by simp) (by simp) ≫
        pullback.fst (Spec.map φ) g := (pullback.lift_fst _ _ _).symm
    refine this _ ?_ inferInstance ⟨_, rfl⟩
    change isomorphisms Scheme _
    rwa [heq, (isomorphisms Scheme).cancel_left_of_respectsIso]
  obtain ⟨T, rfl⟩ := hY
  obtain ⟨ψ, rfl⟩ := Spec.map_surjective g
  refine of_pullback_fst_Spec_of_codescendsAlong (P := isomorphisms Scheme.{u})
      (Q' := RingHom.FaithfullyFlat) (Q := fun f ↦ Function.Bijective f) (P' := @Surjective ⊓ @Flat)
      RingHom.FaithfullyFlat.codescendsAlong_bijective ?_ ?_ h hfst
  · intro _ _ f hf
    rwa [← flat_and_surjective_SpecMap_iff, and_comm]
  · simp_rw [← isIso_SpecMap_iff, implies_true]

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

Goal state before:
pp: case refine_1
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
⊢ @Surjective ⊓ @IsLocalIso ≤ @Surjective ⊓ @Flat

Tactic:
gcongr

Goal state after:
case h₂
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
⊢ @IsLocalIso ≤ @Flat
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case inr.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
hq : q.natDegree = p.natDegree
e :
  ∑ b ∈ Finset.range (p.natDegree + 1),
      ((algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (p.coeff b) * (C x * X) ^ b).coeff
        p.natDegree =
    0
i : ℕ
hi : i ≤ p.natDegree
⊢ (algebraMap R S) ((↑(p.coeff i)).coeff (p.natDegree - i)) * x ^ i =
    x ^ i * ((algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (p.coeff i) * X ^ i).coeff p.natDegree

Tactic:
coeff_mul_X_pow',

Goal state after:
case inr.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
hq : q.natDegree = p.natDegree
e :
  ∑ b ∈ Finset.range (p.natDegree + 1),
      ((algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (p.coeff b) * (C x * X) ^ b).coeff
        p.natDegree =
    0
i : ℕ
hi : i ≤ p.natDegree
⊢ (algebraMap R S) ((↑(p.coeff i)).coeff (p.natDegree - i)) * x ^ i =
    x ^ i *
      if i ≤ p.natDegree then
        ((algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (p.coeff i)).coeff (p.natDegree - i)
      else 0
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : x ∈ Ideal.map (algebraMap R S) I
p : R[X]
hp : p.Monic
e : (aeval x) p = 0
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
i : ℕ
hi✝ : i ≠ p.natDegree
hi : p.natDegree < i
⊢ p.coeff i ∈ I

Tactic:
simp [coeff_eq_zero_of_natDegree_lt hi]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
s : S
H : IsAlmostIntegral R s
inst✝ : IsNoetherianRing R
H' : R⁰ ≤ Submonoid.comap (algebraMap R S) S⁰
⊢ IsIntegral R s

Tactic:
obtain ⟨r, hr, hr'⟩ := H

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
s : S
inst✝ : IsNoetherianRing R
H' : R⁰ ≤ Submonoid.comap (algebraMap R S) S⁰
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • s ^ n ∈ (algebraMap R S).range
⊢ IsIntegral R s
Module: Mathlib.FieldTheory.RatFunc.Defs

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q : K[X]
hq : q ≠ 0
⊢ { toFractionRing := IsLocalization.mk' (FractionRing K[X]) p ⟨q, ⋯⟩ } = { toFractionRing := Localization.mk p ⟨q, ⋯⟩ }

Tactic:
Localization.mk_eq_mk'

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q : K[X]
hq : q ≠ 0
⊢ { toFractionRing := IsLocalization.mk' (FractionRing K[X]) p ⟨q, ⋯⟩ } =
    { toFractionRing := IsLocalization.mk' (Localization K[X]⁰) p ⟨q, ⋯⟩ }
Module: Mathlib.RingTheory.Valuation.IsTrivialOn

Goal state before:
pp: case inr
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : v y ≠ 1
this : ∀ (y : K), y ≠ 0 → v y ≠ 1 → 1 < v y → Transcendental A y
hlt : v y ≤ 1
⊢ ¬IsAlgebraic A y

Tactic:
← IsAlgebraic.inv_iff

Goal state after:
case inr
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : v y ≠ 1
this : ∀ (y : K), y ≠ 0 → v y ≠ 1 → 1 < v y → Transcendental A y
hlt : v y ≤ 1
⊢ ¬IsAlgebraic A y⁻¹
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: 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
⊢ eval f a (x * y) = eval f a x * eval f a y

Tactic:
unfold eval
  by_cases hxy : Polynomial.eval₂ f a (denom (x * y)) = 0
  · have := Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero f a (denom_mul_dvd x y) hxy
    rw [Polynomial.eval₂_mul] at this
    cases mul_eq_zero.mp this <;> contradiction
  rw [div_mul_div_comm, eq_div_iff (mul_ne_zero hx hy), div_eq_mul_inv, mul_right_comm, ←
    div_eq_mul_inv, div_eq_iff hxy]
  repeat' rw [← Polynomial.eval₂_mul]
  congr 1
  apply num_denom_mul

Goal state after: