awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst_1 : Flat (Spec.map φ)
inst_2 : IsFinite (Spec.map φ)
inst_3 : LocallyOfFinitePresentation (Spec.map φ)
inst : (CommRingCat.Hom.hom φ).Flat
⊢ IsLocallyConstant (finrank (Spec.map φ))
have inst₁ : (CommRingCat.Hom.hom φ).Finite
Tactic: simp only [Flat.SpecMap_iff, IsFinite.SpecMap_iff, LocallyOfFinitePresentation.SpecMap_iff] at *
Cleared hypotheses: inst_1, inst_2, inst_3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst_1 : Flat (Spec.map φ)
inst_2 : IsFinite (Spec.map φ)
inst_3 : LocallyOfFinitePresentation (Spec.map φ)
inst : (CommRingCat.Hom.hom φ).Flat
inst₁ : (CommRingCat.Hom.hom φ).Finite
⊢ IsLocallyConstant (finrank (Spec.map φ))
have inst₂ : (CommRingCat.Hom.hom φ).FinitePresentation
Tactic: simp only [Flat.SpecMap_iff, IsFinite.SpecMap_iff, LocallyOfFinitePresentation.SpecMap_iff] at *
Cleared hypotheses: inst_1, inst_2, inst_3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
inst_2 : (CommRingCat.Hom.hom φ).FinitePresentation
⊢ IsLocallyConstant (finrank (Spec.map φ))
have rw : IsLocallyConstant (CommRingCat.Hom.hom φ).finrank
Tactic: rw [finrank_SpecMap_eq_finrank ‹_› ‹_›]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
inst_2 : (CommRingCat.Hom.hom φ).FinitePresentation
⊢ IsLocallyConstant (CommRingCat.Hom.hom φ).finrank
have algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
inst_2 : (CommRingCat.Hom.hom φ).FinitePresentation
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
⊢ IsLocallyConstant (CommRingCat.Hom.hom φ).finrank
have algebraizeInst₁ : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
inst_2 : (CommRingCat.Hom.hom φ).FinitePresentation
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst₁ : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
⊢ IsLocallyConstant (CommRingCat.Hom.hom φ).finrank
have algebraizeInst₂ : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
inst_2 : (CommRingCat.Hom.hom φ).FinitePresentation
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_2 : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
⊢ IsLocallyConstant (CommRingCat.Hom.hom φ).finrank
have this : ∀ (R S : Type u) [inst : CommRing R] [inst_3 : CommRing S] [inst_4 : Algebra R S] [Module.Finite R S]
  [Algebra.FinitePresentation R S], Module.FinitePresentation R S
Tactic: have := Module.FinitePresentation.of_finite_of_finitePresentation
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
⊢ finrank f = 1
have h : ∀ (y : ↥Y), finrank f y = 1 y
Tactic: ext y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
y : ↥Y
⊢ finrank f y = 1 y
have h : ∀ (R : CommRingCat.{u}) (g : Spec R ⟶ Y), IsOpenImmersion g → ∀ (y : ↥(Spec R)), finrank f (g y) = 1 (g y)
Tactic: obtain ⟨R, g, _, y, rfl⟩ := Y.exists_Spec_apply_eq y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
y : ↥(Spec R)
⊢ finrank f (g y) = 1 (g y)
have this : Nontrivial.{u} (↑R : Type u)
Tactic: have : Nontrivial R := y.nontrivial
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial.{u} (↑R : Type u)
⊢ finrank f (g y) = 1 (g y)
have h : Module.rankAtStalk (↑R : Type u) y = 1
Tactic: rw [← finrank_pullback_snd, ← Category.comp_id (pullback.snd f g), finrank_comp_left_of_isIso,
    ← Spec.map_id, finrank_SpecMap_eq_finrank, CommRingCat.hom_id, Pi.one_apply,
    ← Algebra.algebraMap_self, RingHom.finrank_algebraMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial.{u} (↑R : Type u)
h : Module.rankAtStalk (↑R : Type u) y = 1
⊢ finrank f (g y) = 1 (g y)
have h₁ : (CommRingCat.Hom.hom (𝟙 R)).Finite
Tactic: rw [← finrank_pullback_snd, ← Category.comp_id (pullback.snd f g), finrank_comp_left_of_isIso,
    ← Spec.map_id, finrank_SpecMap_eq_finrank, CommRingCat.hom_id, Pi.one_apply,
    ← Algebra.algebraMap_self, RingHom.finrank_algebraMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial.{u} (↑R : Type u)
h : Module.rankAtStalk (↑R : Type u) y = 1
h₁ : (CommRingCat.Hom.hom (𝟙 R)).Finite
⊢ finrank f (g y) = 1 (g y)
have h₂ : (CommRingCat.Hom.hom (𝟙 R)).Flat
Tactic: rw [← finrank_pullback_snd, ← Category.comp_id (pullback.snd f g), finrank_comp_left_of_isIso,
    ← Spec.map_id, finrank_SpecMap_eq_finrank, CommRingCat.hom_id, Pi.one_apply,
    ← Algebra.algebraMap_self, RingHom.finrank_algebraMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
⊢ IsIso f ↔ finrank f = 1
have refine : ∀ (h : finrank f = 1), IsIso f
Tactic: refine ⟨fun h ↦ finrank_eq_one_of_isIso f, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
⊢ IsIso f
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1)
      (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIso f)
  (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsIso f
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1)
        (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIso f)
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsIso f
⊢ IsIso f
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
  IsIso f
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: X, Y, f, inst, inst_1, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIso f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ IsIso f
have inr : ∀ (i : Y.affineCover.toPreZeroHypercover.1),
  MorphismProperty.isomorphisms Scheme (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
Tactic: rw [← MorphismProperty.isomorphisms.iff,
      IsZariskiLocalAtTarget.iff_of_openCover (P := .isomorphisms Scheme) Y.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIso f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ MorphismProperty.isomorphisms Scheme (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i))
have inr : finrank (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) = 1
Tactic: refine this _ ?_ ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIso f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ finrank (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) = 1
have inr : ∀ (y : ↥(Y.affineCover.X i)), finrank (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) y = 1 y
Tactic: ext y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIso f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ finrank (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) y = 1 y
have inr : finrank f ((Y.affineCover.f i) y) = 1 y
Tactic: rw [finrank_pullback_snd, h, Pi.one_apply, Pi.one_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIso f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
inr : finrank f ((Y.affineCover.f i) y) = 1 y
⊢ finrank (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) y = 1 y
have inr₁ : Eq (α := ℕ) (1 ((Y.affineCover.f i) y)) (1 y)
Tactic: rw [finrank_pullback_snd, h, Pi.one_apply, Pi.one_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIso f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
inr : finrank f ((Y.affineCover.f i) y) = 1 y
inr₁ : Eq (α := ℕ) (1 ((Y.affineCover.f i) y)) (1 y)
⊢ finrank (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) y = 1 y
have inr₂ : Eq (α := ℕ) 1 (1 y)
Tactic: rw [finrank_pullback_snd, h, Pi.one_apply, Pi.one_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIso f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
inr : finrank f ((Y.affineCover.f i) y) = 1 y
inr₁ : Eq (α := ℕ) (1 ((Y.affineCover.f i) y)) (1 y)
inr₂ : Eq (α := ℕ) 1 (1 y)
⊢ finrank (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) y = 1 y
have inr₃ : Eq (α := ℕ) 1 1
Tactic: rw [finrank_pullback_snd, h, Pi.one_apply, Pi.one_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
⊢ IsIso f
have obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : finrank f = 1), IsIso f
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, inst_1, h, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
⊢ IsIso f
have inr : ∀
  (this :
    ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : finrank f = 1)
      (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIso f)
  (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), IsIso f
Tactic: wlog hX : ∃ S, X = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : finrank f = 1)
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIso f)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), IsIso f
⊢ IsIso f
have wlog : ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : finrank f = 1)
  (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIso f
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, R, f, inst, inst_1, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : finrank f = 1)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIso f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ IsIso f
have x : IsAffine X
Tactic: have _ : IsAffine X := isAffine_of_isAffineHom f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : finrank f = 1)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIso f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h_1 : IsAffine X
⊢ IsIso f
have inr : IsIso (X.isoSpec.inv ≫ f)
Tactic: rw [← isIso_comp_left_iff X.isoSpec.inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : finrank f = 1)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIso f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h_1 : IsAffine X
⊢ IsIso (X.isoSpec.inv ≫ f)
have inr : finrank (X.isoSpec.inv ≫ f) = 1
Tactic: refine this _ _ ?_ ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : finrank f = 1)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIso f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h_1 : IsAffine X
inr : finrank f = 1
⊢ finrank (X.isoSpec.inv ≫ f) = 1
have inr₁ : Eq.{u + 1} (α := (s : ↥(Spec R)) → ℕ) 1 1
Tactic: rw [finrank_comp_left_of_isIso, h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
hX : ∃ (S : CommRingCat.{u}), X = Spec S
⊢ IsIso f
have obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [Flat f] [IsFinite f] (h : finrank f = 1), IsIso f
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, f, inst, inst_1, h, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
f : Spec S ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
⊢ IsIso f
have obtain : ∀ (φ : R ⟶ S) [Flat (Spec.map φ)] [IsFinite (Spec.map φ)] (h : finrank (Spec.map φ) = 1), IsIso (Spec.map φ)
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst, inst_1, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : IsFinite (Spec.map φ)
h : finrank (Spec.map φ) = 1
⊢ IsIso (Spec.map φ)
have inst : (CommRingCat.Hom.hom φ).Flat
Tactic: simp only [IsFinite.SpecMap_iff, Flat.SpecMap_iff] at *
Cleared hypotheses: inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst_1 : Flat (Spec.map φ)
inst_2 : IsFinite (Spec.map φ)
h : finrank (Spec.map φ) = 1
inst : (CommRingCat.Hom.hom φ).Flat
⊢ IsIso (Spec.map φ)
have inst₁ : (CommRingCat.Hom.hom φ).Finite
Tactic: simp only [IsFinite.SpecMap_iff, Flat.SpecMap_iff] at *
Cleared hypotheses: inst_1, inst_2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
⊢ IsIso (Spec.map φ)
have algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
⊢ IsIso (Spec.map φ)
have algebraizeInst₁ : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
⊢ IsIso φ
have rw : Function.Bijective (α := (↑R : Type u)) (β := (↑S : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) φ) :
    (a : (↑R : Type u)) → (↑S : Type u))
Tactic: rw [ConcreteCategory.isIso_iff_bijective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
⊢ Function.Bijective (α := (↑R : Type u)) (β := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑R : Type u)) → (↑S : Type u))
have a : Eq.{u + 1} (α := (p : PrimeSpectrum (↑R : Type u)) → ℕ) (Module.rankAtStalk (↑S : Type u)) 1
Tactic: apply Module.algebraMap_bijective_of_rankAtStalk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
⊢ Eq.{u + 1} (α := (p : PrimeSpectrum (↑R : Type u)) → ℕ) (Module.rankAtStalk (↑S : Type u)) 1
have a : ∀ (h : (CommRingCat.Hom.hom φ).finrank = 1),
  (CommRingCat.Hom.hom φ).Flat →
    (CommRingCat.Hom.hom φ).Finite →
      let algInst := (CommRingCat.Hom.hom φ).toAlgebra;
      Module.Flat.{u, u} (↑R : Type u) (↑S : Type u) →
        Module.Finite.{u, u} (↑R : Type u) (↑S : Type u) →
          Eq.{u + 1} (α := (p : PrimeSpectrum (↑R : Type u)) → ℕ) (Module.rankAtStalk (↑S : Type u)) 1
Tactic: rwa [finrank_SpecMap_eq_finrank ‹_› ‹_›] at h
Cleared hypotheses: h, inst, inst_1, algInst, algebraizeInst, algebraizeInst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
⊢ IsIso (Spec.map φ)
have this : IsIso φ
Tactic: have : IsIso φ := by
    rw [ConcreteCategory.isIso_iff_bijective]
    apply Module.algebraMap_bijective_of_rankAtStalk
    rwa [finrank_SpecMap_eq_finrank ‹_› ‹_›] at h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
⊢ IsOpenImmersion.{u} (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of (TensorProduct R S S)))
    (Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (TensorProduct.lmul' R))))
have rw : ∃ (e : (↑(CommRingCat.of (TensorProduct R S S)) : Type u)),
  IsIdempotentElem e ∧
    Eq (α := Ideal (↑(CommRingCat.of (TensorProduct R S S)) : Type u))
      (RingHom.ker (F := (↑(CommRingCat.of (TensorProduct R S S)) : Type u) →+* (↑(CommRingCat.of S) : Type u))
        (CommRingCat.Hom.hom (CommRingCat.ofHom (AlgHom.toRingHom (TensorProduct.lmul' R)))))
      (Ideal.span {e})
Tactic: rw [isOpenImmersion_SpecMap_iff_of_surjective _ (fun x ↦ ⟨1 ⊗ₜ x, by simp⟩)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
⊢ ∃ (e : (↑(CommRingCat.of (TensorProduct R S S)) : Type u)),
    IsIdempotentElem e ∧
      Eq (α := Ideal (↑(CommRingCat.of (TensorProduct R S S)) : Type u))
        (RingHom.ker (F := (↑(CommRingCat.of (TensorProduct R S S)) : Type u) →+* (↑(CommRingCat.of S) : Type u))
          (CommRingCat.Hom.hom (CommRingCat.ofHom (AlgHom.toRingHom (TensorProduct.lmul' R)))))
        (Ideal.span {e})
have apply : IsIdempotentElem (M := Ideal (TensorProduct R S S)) (KaehlerDifferential.ideal R S)
Tactic: apply (Ideal.isIdempotentElem_iff_of_fg _ (KaehlerDifferential.ideal_fg R S)).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
⊢ IsIdempotentElem (M := Ideal (TensorProduct R S S)) (KaehlerDifferential.ideal R S)
have apply : Subsingleton.{u + 1} (Ideal.Cotangent (R := TensorProduct R S S) (KaehlerDifferential.ideal R S))
Tactic: apply (Ideal.cotangent_subsingleton_iff _).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ @FormallyUnramified = affineLocally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FormallyUnramified
have h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
  FormallyUnramified f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FormallyUnramified) f
Tactic: ext X Y f