awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : Ideal S
hI : Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I
J : ↥(Ideal S)⁰
mk0_eq_mk0 :
  Eq (α := ClassGroup S)
    ((mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S)
        (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) I hI) :
      ClassGroup S)
    ((mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S) J : ClassGroup S)
J_dvd : Membership.mem (α := S) (↑J : Ideal S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S)
⊢ ∃ (a :
    { J : Ideal S // Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S) }),
    mkMMem bS adm a =
      (mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S)
        (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) I hI)

Tactic:
⟨⟨J, J_dvd⟩, mk0_eq_mk0.symm⟩

Premises used: Subtype.mk, Exists.intro, Eq.symm, Subtype.val
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : Ideal S
hI : Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I
J : ↥(Ideal S)⁰
mk0_eq_mk0 :
  Eq (α := ClassGroup S)
    ((mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S)
        (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) I hI) :
      ClassGroup S)
    ((mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S) J : ClassGroup S)
J_dvd : Membership.mem (α := S) (↑J : Ideal S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S)
⊢ ∃ (a :
    { J : Ideal S // Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S) }),
    mkMMem bS adm a =
      (mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S)
        (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) I hI)

Tactic:
exact ⟨⟨J, J_dvd⟩, mk0_eq_mk0.symm⟩
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsDedekindDomain S
inst_18 : Algebra.IsAlgebraic R S
rw : ¬Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S) (0 : S)
⊢ Ne (α := Ideal S)
    (Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S))) 0

Tactic:
rw [Ne, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]

Premises used: Ideal.span_singleton_eq_bot, Ne, Ideal.zero_eq_bot
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsDedekindDomain S
inst_18 : Algebra.IsAlgebraic R S
⊢ ¬Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S) (0 : S)

Tactic:
prod_finsetApprox_ne_zero bS adm

Premises used: ClassGroup.prod_finsetApprox_ne_zero
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsDedekindDomain S
inst_18 : Algebra.IsAlgebraic R S
⊢ ¬Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S) (0 : S)

Tactic:
exact prod_finsetApprox_ne_zero bS adm

Premises used: ClassGroup.prod_finsetApprox_ne_zero
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsDedekindDomain S
inst_18 : Algebra.IsAlgebraic R S
I : Ideal S
rw :
  Membership.mem (α := S) (↑I : Set S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S) ↔
    Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S)
⊢ Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S)) ≤ I ↔
    Membership.mem (α := S) (γ := Ideal S) ((Equiv.refl (Ideal S) : (a : Ideal S) → Ideal S) I : Ideal S)
      ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S)

Tactic:
rw [Equiv.refl_apply, Ideal.span_le, Set.singleton_subset_iff]

Premises used: Ideal.span_le, Set.singleton_subset_iff, Equiv.refl_apply
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsDedekindDomain S
inst_18 : Algebra.IsAlgebraic R S
I : Ideal S
⊢ Membership.mem (α := S) (↑I : Set S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S) ↔
    Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this : IsDedekindDomain S := ⋯
choose :
  (s : Finset L) →
    (b : Basis (↥s) K L) →
      (hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b : (a : ↥s) → L) x : L)) → Fintype (ClassGroup S)
⊢ Fintype (ClassGroup S)

Tactic:
choose s b hb_int using FiniteDimensional.exists_is_basis_integral R K L

Premises used: FiniteDimensional.exists_is_basis_integral
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this : IsDedekindDomain S := ⋯
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b : (a : ↥s) → L) x : L)
apply : Function.Injective.{u_1 + 1, u_3 + 1} (β := K) fun (r : R) ↦ HSMul.hSMul (β := K) r 1
⊢ LinearIndependent.{u_4, u_1, u_4} (ι := ↥s) R (M := L)
    (⇑(LinearMap.BilinForm.dualBasis.{u_4, u_3, u_4} (V := L) (K := K) (ι := ↥s) (Algebra.traceForm K L) ⋯ b :
          Basis (↥s) K L) :
      (a : ↥s) → L)

Tactic:
apply (Basis.linearIndependent _).restrict_scalars

Premises used: Module.Basis.linearIndependent, LinearIndependent.restrict_scalars
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this : IsDedekindDomain S := ⋯
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b : (a : ↥s) → L) x : L)
simp : Function.Injective.{u_1 + 1, u_3 + 1} (β := K) fun (r : R) ↦ (algebraMap R K : (a : R) → K) r
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (β := K) fun (r : R) ↦ HSMul.hSMul (β := K) r 1

Tactic:
simp only [Algebra.smul_def, mul_one]

Premises used: Algebra.smul_def, mul_one
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this : IsDedekindDomain S := ⋯
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b : (a : ↥s) → L) x : L)
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (β := K) fun (r : R) ↦ (algebraMap R K : (a : R) → K) r

Tactic:
apply IsFractionRing.injective

Premises used: IsFractionRing.injective
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this : IsDedekindDomain S := ⋯
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b : (a : ↥s) → L) x : L)
⊢ LinearIndependent.{u_4, u_1, u_4} (ι := ↥s) R (M := L)
    (⇑(LinearMap.BilinForm.dualBasis.{u_4, u_3, u_4} (V := L) (K := K) (ι := ↥s) (Algebra.traceForm K L) ⋯ b :
          Basis (↥s) K L) :
      (a : ↥s) → L)

Tactic:
have : LinearIndependent R ((Algebra.traceForm K L).dualBasis
      (traceForm_nondegenerate K L) b) := by
    apply (Basis.linearIndependent _).restrict_scalars
    simp only [Algebra.smul_def, mul_one]
    apply IsFractionRing.injective
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this_3 : IsDedekindDomain S := ⋯
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b : (a : ↥s) → L) x : L)
this :
  LinearIndependent.{u_4, u_1, u_4} (ι := ↥s) R (M := L)
    (⇑(LinearMap.BilinForm.dualBasis.{u_4, u_3, u_4} (V := L) (K := K) (ι := ↥s) (Algebra.traceForm K L) ⋯ b :
          Basis (↥s) K L) :
      (a : ↥s) → L)
obtain :
  (n : ℕ) →
    (b :
        Basis.{0, u_1, u_4} (Fin n) R
          ↥(LinearMap.range
              ((↑R :
                  {S M : Type u_2} →
                    {M₂ : Type u_4} →
                      [inst : Semiring R] →
                        [inst_18 : Semiring S] →
                          [inst_19 : AddCommMonoid M] →
                            [inst_20 : AddCommMonoid M₂] →
                              [inst_21 : Module R M] →
                                [inst_22 : Module R M₂] →
                                  [inst_23 : Module S M] →
                                    [inst_24 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (Algebra.linearMap S L)))) →
      Fintype (ClassGroup S)
⊢ Fintype (ClassGroup S)

Tactic:
obtain ⟨n, b⟩ :=
    Submodule.basisOfPidOfLESpan this (IsIntegralClosure.range_le_span_dualBasis S b hb_int)

Premises used: Submodule.basisOfPidOfLESpan, IsIntegralClosure.range_le_span_dualBasis
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this_3 : IsDedekindDomain S := ⋯
s : Finset L
b_1 : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b_1 : (a : ↥s) → L) x : L)
this :
  LinearIndependent.{u_4, u_1, u_4} (ι := ↥s) R (M := L)
    (⇑(LinearMap.BilinForm.dualBasis.{u_4, u_3, u_4} (V := L) (K := K) (ι := ↥s) (Algebra.traceForm K L) ⋯ b_1 :
          Basis (↥s) K L) :
      (a : ↥s) → L)
n : ℕ
b :
  Basis.{0, u_1, u_4} (Fin n) R
    ↥(LinearMap.range
        ((↑R :
            {S M : Type u_2} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_18 : Semiring S] →
                    [inst_19 : AddCommMonoid M] →
                      [inst_20 : AddCommMonoid M₂] →
                        [inst_21 : Module R M] →
                          [inst_22 : Module R M₂] →
                            [inst_23 : Module S M] →
                              [inst_24 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Algebra.linearMap S L)))
⊢ HasQuotient.Quotient S (B := Submodule R S) ⊥ ≃ₗ[R] S

Tactic:
exact Submodule.quotEquivOfEqBot _ rfl

Premises used: Submodule.quotEquivOfEqBot, rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this_3 : IsDedekindDomain S := ⋯
s : Finset L
b_1 : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b_1 : (a : ↥s) → L) x : L)
this :
  LinearIndependent.{u_4, u_1, u_4} (ι := ↥s) R (M := L)
    (⇑(LinearMap.BilinForm.dualBasis.{u_4, u_3, u_4} (V := L) (K := K) (ι := ↥s) (Algebra.traceForm K L) ⋯ b_1 :
          Basis (↥s) K L) :
      (a : ↥s) → L)
n : ℕ
b :
  Basis.{0, u_1, u_4} (Fin n) R
    ↥(LinearMap.range
        ((↑R :
            {S M : Type u_2} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_18 : Semiring S] →
                    [inst_19 : AddCommMonoid M] →
                      [inst_20 : AddCommMonoid M₂] →
                        [inst_21 : Module R M] →
                          [inst_22 : Module R M₂] →
                            [inst_23 : Module S M] →
                              [inst_24 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Algebra.linearMap S L)))
⊢ Function.Injective.{u_2 + 1, u_4 + 1} (α := S) (β := L)
    (⇑((↑R :
            {S M : Type u_2} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_18 : Semiring S] →
                    [inst_19 : AddCommMonoid M] →
                      [inst_20 : AddCommMonoid M₂] →
                        [inst_21 : Module R M] →
                          [inst_22 : Module R M₂] →
                            [inst_23 : Module S M] →
                              [inst_24 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Algebra.linearMap S L)) :
      (a : S) → L)

Tactic:
IsIntegralClosure.algebraMap_injective _ R _

Premises used: IsIntegralClosure.algebraMap_injective
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this_3 : IsDedekindDomain S := ⋯
s : Finset L
b_1 : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b_1 : (a : ↥s) → L) x : L)
this :
  LinearIndependent.{u_4, u_1, u_4} (ι := ↥s) R (M := L)
    (⇑(LinearMap.BilinForm.dualBasis.{u_4, u_3, u_4} (V := L) (K := K) (ι := ↥s) (Algebra.traceForm K L) ⋯ b_1 :
          Basis (↥s) K L) :
      (a : ↥s) → L)
n : ℕ
b :
  Basis.{0, u_1, u_4} (Fin n) R
    ↥(LinearMap.range
        ((↑R :
            {S M : Type u_2} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_18 : Semiring S] →
                    [inst_19 : AddCommMonoid M] →
                      [inst_20 : AddCommMonoid M₂] →
                        [inst_21 : Module R M] →
                          [inst_22 : Module R M₂] →
                            [inst_23 : Module S M] →
                              [inst_24 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Algebra.linearMap S L)))
⊢ Function.Injective.{u_2 + 1, u_4 + 1} (α := S) (β := L)
    (⇑((↑R :
            {S M : Type u_2} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_18 : Semiring S] →
                    [inst_19 : AddCommMonoid M] →
                      [inst_20 : AddCommMonoid M₂] →
                        [inst_21 : Module R M] →
                          [inst_22 : Module R M₂] →
                            [inst_23 : Module S M] →
                              [inst_24 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Algebra.linearMap S L)) :
      (a : S) → L)

Tactic:
exact IsIntegralClosure.algebraMap_injective _ R _

Premises used: IsIntegralClosure.algebraMap_injective