awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
h :
  ∃ (σ : Finset T),
    ∀ (s : T),
      ∃ (t : T),
        Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (s * t)
obtain :
  ∀ (σ : Finset T)
    (hσ :
      ∀ (s : T),
        ∃ (t : T),
          Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) t ∧
            IsUnit t ∧ Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (s * t)),
    ∃ (σ : Finset T),
      ∀ (s : T),
        ∃ (t : T),
          Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) t ∧
            IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (s * t)
h₁ h₂ :
  ∀ (σ : Finset T)
    (hσ :
      ∀ (s : T),
        ∃ (t : T),
          Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) t ∧
            IsUnit t ∧ Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (s * t))
    (x : T),
    ∃ (t : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (x * t)
h₃ :
  ∀ (σ : Finset T)
    (hσ :
      ∀ (s : T),
        ∃ (t : T),
          Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) t ∧
            IsUnit t ∧ Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (s * t))
    (x y : T) (hy₁ : Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) y) (hy₂ : IsUnit y)
    (hy₃ : Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (x * y)),
    ∃ (t : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (x * t)
⊢ ∃ (σ : Finset T),
    ∀ (s : T),
      ∃ (t : T),
        Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (s * t)
have h₄ : ∀ (σ : Finset T)
  (hσ :
    ∀ (s : T),
      ∃ (t : T),
        Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (s * t))
  (x y : T) (hy₁ : Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) y) (hy₂ : IsUnit y)
  (hy₃ : Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (x * y)),
  ∃ (t : T),
    Membership.mem (γ := Subalgebra S T) (adjoin S (↑(adjoin R (↑σ : Set T)) : Set T)) t ∧
      IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑(adjoin R (↑σ : Set T)) : Set T)) (x * t)
Tactic: classical
  obtain ⟨σ, hσ⟩ := h
  use σ
  intro x
  obtain ⟨y, hy₁, hy₂, hy₃⟩ := hσ x
  simp_rw [← Algebra.adjoin_adjoin_of_tower R (S := S) (σ : Set T)]
  exact ⟨y, Algebra.subset_adjoin hy₁, hy₂, Algebra.subset_adjoin hy₃⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
inst_5 : EssFiniteType R S
this : Algebra S T := f.toAlgebra
⊢ EssFiniteType R T
have this₁ : IsScalarTower R S T
Tactic: have : IsScalarTower R S T := .of_algebraMap_eq' f.comp_algebraMap.symm
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
inst_5 : EssFiniteType R S
this_1 : Algebra S T := f.toAlgebra
this : IsScalarTower R S T
⊢ EssFiniteType R T
have this₁ : Module.Finite S T
Tactic: have : Module.Finite S T := .of_surjective (Algebra.linearMap S T) hf
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
this : f.toRingHom = g.toRingHom
⊢ f = g
have H₁ : ∀ (x : S), Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) x : T) ((g : (a : S) → T) x : T)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
⊢ f = g
have suffices : f.toRingHom = g.toRingHom
Tactic: suffices f.toRingHom = g.toRingHom by ext; exact RingHom.congr_fun this _
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
⊢ f.toRingHom = g.toRingHom
have h : Eq (α := RingHom.{u_2, u_3} (↥(subalgebra R S)) T) (f.comp (algebraMap (↥(subalgebra R S)) S))
  (g.comp (algebraMap (↥(subalgebra R S)) S))
Tactic: apply IsLocalization.ringHom_ext (EssFiniteType.submonoid R S)
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
this :
  Eq (α := AlgHom.{u_1, u_2, u_3} R (↥(subalgebra R S)) T) (f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
    (g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
⊢ Eq (α := RingHom.{u_2, u_3} (↥(subalgebra R S)) T) (f.comp (algebraMap (↥(subalgebra R S)) S))
    (g.comp (algebraMap (↥(subalgebra R S)) S))
have a : ∀ (x : ↥(subalgebra R S)),
  Eq.{u_3 + 1} (α := T) ((f.comp (algebraMap (↥(subalgebra R S)) S) : (a : ↥(subalgebra R S)) → T) x : T)
    ((g.comp (algebraMap (↥(subalgebra R S)) S) : (a : ↥(subalgebra R S)) → T) x : T)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
⊢ Eq (α := RingHom.{u_2, u_3} (↥(subalgebra R S)) T) (f.comp (algebraMap (↥(subalgebra R S)) S))
    (g.comp (algebraMap (↥(subalgebra R S)) S))
have h : Eq (α := AlgHom.{u_1, u_2, u_3} R (↥(subalgebra R S)) T) (f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
  (g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
Tactic: suffices f.comp (IsScalarTower.toAlgHom R _ S) = g.comp (IsScalarTower.toAlgHom R _ S) by
    ext; exact AlgHom.congr_fun this _
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
⊢ Eq (α := AlgHom.{u_1, u_2, u_3} R (↥(subalgebra R S)) T) (f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
    (g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
have h : Eq.{u_2 + 1} (α := Subalgebra R ↥(subalgebra R S)) (adjoin R {x : ↥(subalgebra R S) | (↑x : S) ∈ finset R S}) ⊤
Tactic: apply AlgHom.ext_of_adjoin_eq_top (s := { x | x.1 ∈ finset R S })
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
h : Eq.{u_2 + 1} (α := Subalgebra R ↥(subalgebra R S)) (adjoin R {x : ↥(subalgebra R S) | (↑x : S) ∈ finset R S}) ⊤
⊢ Eq (α := AlgHom.{u_1, u_2, u_3} R (↥(subalgebra R S)) T) (f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
    (g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
have h₁ : Set.EqOn.{u_2, u_3} (α := ↥(subalgebra R S)) (β := T)
  (⇑(f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)) : (a : ↥(subalgebra R S)) → T)
  (⇑(g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)) : (a : ↥(subalgebra R S)) → T)
  {x : ↥(subalgebra R S) | (↑x : S) ∈ finset R S}
Tactic: apply AlgHom.ext_of_adjoin_eq_top (s := { x | x.1 ∈ finset R S })
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ EssFiniteType (algebraMap R S) ↔ Algebra.EssFiniteType R S
have rw : Algebra.EssFiniteType R S ↔ Algebra.EssFiniteType R S
Tactic: rw [RingHom.EssFiniteType, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Algebra.EssFiniteType R S ↔ Algebra.EssFiniteType R S
⊢ EssFiniteType (algebraMap R S) ↔ Algebra.EssFiniteType R S
have rw₁ : Algebra.EssFiniteType R S ↔ Algebra.EssFiniteType R S
Tactic: rw [RingHom.EssFiniteType, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FiniteType
⊢ f.EssFiniteType
have algebraizeInst : Algebra.FiniteType R S
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FiniteType
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.FiniteType R S
⊢ f.EssFiniteType
have change : Algebra.EssFiniteType R S
Tactic: change Algebra.EssFiniteType R S
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.EssFiniteType
g₁ g₂ : S →+* T
h₁ : g₁.comp f = g₂.comp f
h₂ : ∀ x ∈ hf.finset, Eq.{u_3 + 1} (α := T) ((g₁ : (a : S) → T) x : T) ((g₂ : (a : S) → T) x : T)
⊢ g₁ = g₂
have algebraizeInst : Algebra.EssFiniteType R S
Tactic: algebraize [f, g₁.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.EssFiniteType
g₁ g₂ : S →+* T
h₁ : g₁.comp f = g₂.comp f
h₂ : ∀ x ∈ hf.finset, Eq.{u_3 + 1} (α := T) ((g₁ : (a : S) → T) x : T) ((g₂ : (a : S) → T) x : T)
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra R T := (g₁.comp f).toAlgebra
algebraizeInst : Algebra.EssFiniteType R S
⊢ g₁ = g₂
have a : ∀ (x : S), Eq.{u_3 + 1} (α := T) ((g₁ : (a : S) → T) x : T) ((g₂ : (a : S) → T) x : T)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ FormallyEtale R S ↔ IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
have rw : FormallyUnramified R S ∧ FormallySmooth R S ↔
  IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
Tactic: rw [FormallyEtale.iff_formallyUnramified_and_formallySmooth, ← FormallySmooth.iff_of_surjective h,
    and_iff_right (FormallyUnramified.of_surjective (Algebra.ofId R S) h)]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
rw :
  FormallyUnramified R S ∧ FormallySmooth R S ↔
    IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
⊢ FormallyEtale R S ↔ IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
have rw₁ : FormallyUnramified R S ∧ FormallySmooth R S ↔ FormallySmooth R S
Tactic: rw [FormallyEtale.iff_formallyUnramified_and_formallySmooth, ← FormallySmooth.iff_of_surjective h,
    and_iff_right (FormallyUnramified.of_surjective (Algebra.ofId R S) h)]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
rw :
  FormallyUnramified R S ∧ FormallySmooth R S ↔
    IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
rw₁ : FormallyUnramified R S ∧ FormallySmooth R S ↔ FormallySmooth R S
⊢ FormallyEtale R S ↔ IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
have rw₂ : FormallySmooth R S ↔ FormallySmooth R S
Tactic: rw [FormallyEtale.iff_formallyUnramified_and_formallySmooth, ← FormallySmooth.iff_of_surjective h,
    and_iff_right (FormallyUnramified.of_surjective (Algebra.ofId R S) h)]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (hypothesis)
Goal:
R : Type u_2
S : Type u_3
Rₘ : Type u_4
Sₘ : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R S
inst_5 : Algebra R Sₘ
inst_6 : Algebra S Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R S Sₘ
inst_11 : IsLocalization M Rₘ
inst_12 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) Sₘ
inst_13 : FormallyEtale R S
⊢ FormallyEtale Rₘ Sₘ
have this : FormallyEtale S Sₘ
Tactic: haveI : FormallyEtale S Sₘ := FormallyEtale.of_isLocalization (M.map (algebraMap R S))
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (hypothesis)
Goal:
R : Type u_2
S : Type u_3
Rₘ : Type u_4
Sₘ : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R S
inst_5 : Algebra R Sₘ
inst_6 : Algebra S Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R S Sₘ
inst_11 : IsLocalization M Rₘ
inst_12 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) Sₘ
inst_13 : FormallyEtale R S
this : FormallyEtale S Sₘ
⊢ FormallyEtale Rₘ Sₘ
have this₁ : FormallyEtale R Sₘ
Tactic: haveI : FormallyEtale R Sₘ := FormallyEtale.comp R S Sₘ
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ Etale R A ↔ FormallyUnramified R A ∧ Smooth R A
have rw : autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
    autoParam (FinitePresentation R A) finitePresentation._autoParam ↔
  FormallyUnramified R A ∧
    autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
      autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
Tactic: rw [etale_iff, FormallyEtale.iff_formallyUnramified_and_formallySmooth, smooth_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam ↔
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
have mp : autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
    autoParam (FinitePresentation R A) finitePresentation._autoParam →
  FormallyUnramified R A ∧
    autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
      autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
mp :
  autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
⊢ autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam ↔
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
have mpr : FormallyUnramified R A ∧
    autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
      autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam →
  autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
    autoParam (FinitePresentation R A) finitePresentation._autoParam
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
mp :
  autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mpr :
  FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam →
    autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam
⊢ autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam ↔
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
have mp₁ : autoParam (FinitePresentation R A) finitePresentation._autoParam →
  FormallyUnramified R A →
    FormallySmooth R A →
      FormallyUnramified R A ∧
        autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
          autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
mp :
  autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mpr :
  FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam →
    autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam
mp₁ mp₂ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A →
      FormallySmooth R A →
        FormallyUnramified R A ∧
          autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
            autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
⊢ autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam ↔
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
have mp₃ : autoParam (FinitePresentation R A) finitePresentation._autoParam →
  FormallyUnramified R A → FormallySmooth R A → FormallyUnramified R A
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
mp :
  autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mpr :
  FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam →
    autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam
mp₁ mp₂ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A →
      FormallySmooth R A →
        FormallyUnramified R A ∧
          autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
            autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mp₃ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A → FormallySmooth R A → FormallyUnramified R A
⊢ autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam ↔
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
have mp₄ : autoParam (FinitePresentation R A) finitePresentation._autoParam →
  FormallyUnramified R A → FormallySmooth R A → autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam
Tactic: tauto