awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
I : Ideal A
b : B
⊢ Eq (α := (A ⧸ I) ⊗[A] B)
    ((quotIdealMapEquivQuotTensor B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → (A ⧸ I) ⊗[A] B)
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) : (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
          b) :
      (A ⧸ I) ⊗[A] B)
    (1 ⊗ₜ[A] b : (A ⧸ I) ⊗[A] B)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : CommRing A
inst_6 : Algebra R A
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
I : Ideal T
a : A
t : T
⊢ Eq (α := HasQuotient.Quotient (A ⊗[R] T) (B := Ideal (A ⊗[R] T)) (Ideal.map (F := T →ₐ[R] A ⊗[R] T) includeRight I))
    (((tensorQuotientEquiv S T A I :
            TensorProduct.{u_1, u_4, u_3} R A (T ⧸ I) ≃ₐ[S]
              HasQuotient.Quotient (A ⊗[R] T) (B := Ideal (A ⊗[R] T))
                (Ideal.map (F := T →ₐ[R] A ⊗[R] T) includeRight I)) :
          (a : A ⊗[R] (T ⧸ I)) → A ⊗[R] T ⧸ Ideal.map includeRight I)
        (a ⊗ₜ[R] (Ideal.Quotient.mk I : (a : T) → T ⧸ I) t) :
      HasQuotient.Quotient (A ⊗[R] T) (B := Ideal (A ⊗[R] T)) (Ideal.map (F := T →ₐ[R] A ⊗[R] T) includeRight I))
    ((Ideal.Quotient.mk (Ideal.map (F := T →ₐ[R] A ⊗[R] T) includeRight I) :
          (a : A ⊗[R] T) → A ⊗[R] T ⧸ Ideal.map includeRight I)
        (a ⊗ₜ[R] t) :
      HasQuotient.Quotient (A ⊗[R] T) (B := Ideal (A ⊗[R] T)) (Ideal.map (F := T →ₐ[R] A ⊗[R] T) includeRight I))

Tactic:
rfl

Premises used: iInf, Set.iInter, Submodule.Quotient.mk, Submodule.restrictScalars, setOf, Ideal.map, Quotient, Quot.map, Submodule.span, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : CommRing A
inst_6 : Algebra R A
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
I : Ideal T
a : A
t : T
⊢ Eq (α := TensorProduct.{u_1, u_4, u_3} R A (T ⧸ I))
    (((AlgEquiv.symm (tensorQuotientEquiv S T A I) :
            HasQuotient.Quotient (A ⊗[R] T) (B := Ideal (A ⊗[R] T))
                (Ideal.map (F := T →ₐ[R] A ⊗[R] T) includeRight I) ≃ₐ[S]
              TensorProduct.{u_1, u_4, u_3} R A (T ⧸ I)) :
          (a : A ⊗[R] T ⧸ Ideal.map includeRight I) → A ⊗[R] (T ⧸ I))
        ((Ideal.Quotient.mk (Ideal.map (F := T →ₐ[R] A ⊗[R] T) includeRight I) :
            (a : A ⊗[R] T) → A ⊗[R] T ⧸ Ideal.map includeRight I)
          (a ⊗ₜ[R] t)) :
      TensorProduct.{u_1, u_4, u_3} R A (T ⧸ I))
    (a ⊗ₜ[R] (Ideal.Quotient.mk I : (a : T) → T ⧸ I) t : TensorProduct.{u_1, u_4, u_3} R A (T ⧸ I))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Submodule.restrictScalars, List.foldl, Submodule.quotientRel, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : CommRing A
inst_6 : Algebra R A
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
I : Ideal A
a : A
t : T
⊢ Eq (α :=
    HasQuotient.Quotient (A ⊗[R] T) (B := Ideal (A ⊗[R] T))
      (Ideal.map (F := A →+* A ⊗[R] T) (algebraMap A (A ⊗[R] T)) I))
    (((quotientTensorEquiv S T A I :
            TensorProduct.{u_1, u_4, u_3} R (A ⧸ I) T ≃ₐ[S]
              HasQuotient.Quotient (A ⊗[R] T) (B := Ideal (A ⊗[R] T))
                (Ideal.map (F := A →+* A ⊗[R] T) (algebraMap A (A ⊗[R] T)) I)) :
          (a : (A ⧸ I) ⊗[R] T) → A ⊗[R] T ⧸ Ideal.map (algebraMap A (A ⊗[R] T)) I)
        ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) a ⊗ₜ[R] t) :
      HasQuotient.Quotient (A ⊗[R] T) (B := Ideal (A ⊗[R] T))
        (Ideal.map (F := A →+* A ⊗[R] T) (algebraMap A (A ⊗[R] T)) I))
    ((Ideal.Quotient.mk (Ideal.map (F := A →+* A ⊗[R] T) (algebraMap A (A ⊗[R] T)) I) :
          (a : A ⊗[R] T) → A ⊗[R] T ⧸ Ideal.map (algebraMap A (A ⊗[R] T)) I)
        (a ⊗ₜ[R] t) :
      HasQuotient.Quotient (A ⊗[R] T) (B := Ideal (A ⊗[R] T))
        (Ideal.map (F := A →+* A ⊗[R] T) (algebraMap A (A ⊗[R] T)) I))

Tactic:
rfl

Premises used: Algebra.TensorProduct.includeLeftRingHom, Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, MonoidHomClass.toMonoidHom, List.foldl, Quotient, RingHomClass.toRingHom, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : CommRing A
inst_6 : Algebra R A
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
I : Ideal A
a : A
t : T
⊢ Eq (α := TensorProduct.{u_1, u_4, u_3} R (A ⧸ I) T)
    (((AlgEquiv.symm (quotientTensorEquiv S T A I) :
            HasQuotient.Quotient (A ⊗[R] T) (B := Ideal (A ⊗[R] T))
                (Ideal.map (F := A →+* A ⊗[R] T) (algebraMap A (A ⊗[R] T)) I) ≃ₐ[S]
              TensorProduct.{u_1, u_4, u_3} R (A ⧸ I) T) :
          (a : A ⊗[R] T ⧸ Ideal.map (algebraMap A (A ⊗[R] T)) I) → (A ⧸ I) ⊗[R] T)
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* A ⊗[R] T) (algebraMap A (A ⊗[R] T)) I) :
            (a : A ⊗[R] T) → A ⊗[R] T ⧸ Ideal.map (algebraMap A (A ⊗[R] T)) I)
          (a ⊗ₜ[R] t)) :
      TensorProduct.{u_1, u_4, u_3} R (A ⧸ I) T)
    ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) a ⊗ₜ[R] t : TensorProduct.{u_1, u_4, u_3} R (A ⧸ I) T)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Submodule.restrictScalars, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
rw :
  Eq (α := Submodule R (R ⊗[R] M)) (LinearMap.ker (M₂ := (R ⧸ I) ⊗[R] M) (LinearMap.rTensor M (Submodule.mkQ I)))
    (LinearMap.range (LinearMap.rTensor M (Submodule.subtype I)))
⊢ LinearMap.range ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ LinearMap.rTensor M (Submodule.subtype I)) =
    HSMul.hSMul (β := Submodule R M) I ⊤

Tactic:
rw [← Submodule.ker_mkQ (I • (⊤ : Submodule R M)), LinearMap.range_comp,
    ← Submodule.map_symm_eq_iff, ← Submodule.comap_equiv_eq_map_symm, ← LinearMap.ker_comp,
    ← TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor, LinearEquiv.ker_comp]

Premises used: Submodule.comap_equiv_eq_map_symm, TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor, LinearMap.range_comp, LinearMap.ker_comp, LinearEquiv.ker_comp, Submodule.map_symm_eq_iff, HSMul.hSMul, Submodule.ker_mkQ, Top.top
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
⊢ Eq (α := Submodule R (R ⊗[R] M)) (LinearMap.ker (M₂ := (R ⧸ I) ⊗[R] M) (LinearMap.rTensor M (Submodule.mkQ I)))
    (LinearMap.range (LinearMap.rTensor M (Submodule.subtype I)))

Tactic:
LinearMap.exact_iff.mp (rTensor_exact M (LinearMap.exact_subtype_mkQ I) I.mkQ_surjective)

Premises used: LinearMap.exact_subtype_mkQ, rTensor_exact, Iff.mp, Submodule.mkQ_surjective, LinearMap.exact_iff
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
⊢ Eq (α := Submodule R (R ⊗[R] M)) (LinearMap.ker (M₂ := (R ⧸ I) ⊗[R] M) (LinearMap.rTensor M (Submodule.mkQ I)))
    (LinearMap.range (LinearMap.rTensor M (Submodule.subtype I)))

Tactic:
exact LinearMap.exact_iff.mp (rTensor_exact M (LinearMap.exact_subtype_mkQ I) I.mkQ_surjective)

Premises used: LinearMap.exact_subtype_mkQ, rTensor_exact, Iff.mp, Submodule.mkQ_surjective, LinearMap.exact_iff
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : IsFiniteSplit R S
obtain : ∀ (n : ℕ) (e : S ≃ₐ[R] Fin n → R), IsFiniteSplit T (T ⊗[R] S)
⊢ IsFiniteSplit T (T ⊗[R] S)

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Algebra.IsFiniteSplit.nonempty_algEquiv_fun R S

Premises used: Algebra.IsFiniteSplit.nonempty_algEquiv_fun
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : IsFiniteSplit R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ IsFiniteSplit T (T ⊗[R] S)

Tactic:
⟨n, ⟨?_⟩⟩

Premises used: Nonempty.intro, Exists.intro, Algebra.IsFiniteSplit.mk
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : IsFiniteSplit R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
refine : T ⊗[R] S ≃ₐ[T] Fin n → T
⊢ IsFiniteSplit T (T ⊗[R] S)

Tactic:
refine ⟨n, ⟨?_⟩⟩
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : IsFiniteSplit R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ T ⊗[R] S ≃ₐ[T] Fin n → T

Tactic:
exact (TensorProduct.congr AlgEquiv.refl e).trans
    ((TensorProduct.piRight R T T (fun _ : Fin n ↦ R)).trans <|
      AlgEquiv.piCongrRight fun i ↦ TensorProduct.rid R T T)

Premises used: AlgEquiv.piCongrRight, AlgEquiv.trans, Algebra.TensorProduct.piRight, Algebra.TensorProduct.congr, Algebra.TensorProduct.rid, AlgEquiv.refl
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
inst_3 : Finite ι
intro : ∀ (val : Fintype ι), ∃ (n : ℕ), Nonempty ((ι → R) ≃ₐ[R] Fin n → R)
⊢ ∃ (n : ℕ), Nonempty ((ι → R) ≃ₐ[R] Fin n → R)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
inst_3 : Finite ι
val : Fintype ι
⊢ ∃ (n : ℕ), Nonempty ((ι → R) ≃ₐ[R] Fin n → R)

Tactic:
⟨_, ⟨AlgEquiv.piCongrLeft' _ _ (Fintype.equivFin ι)⟩⟩

Premises used: Nonempty.intro, Fintype.equivFin, Exists.intro, AlgEquiv.piCongrLeft'
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
inst_3 : Finite ι
val : Fintype ι
⊢ ∃ (n : ℕ), Nonempty ((ι → R) ≃ₐ[R] Fin n → R)

Tactic:
exact ⟨_, ⟨AlgEquiv.piCongrLeft' _ _ (Fintype.equivFin ι)⟩⟩
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
S' : Type u_3
inst_3 : CommRing S'
inst_4 : Algebra R S'
e : S ≃ₐ[R] S'
inst_5 : IsFiniteSplit R S
obtain : ∀ (n : ℕ) (f : S ≃ₐ[R] Fin n → R), IsFiniteSplit R S'
⊢ IsFiniteSplit R S'

Tactic:
obtain ⟨n, ⟨f⟩⟩ := nonempty_algEquiv_fun R S

Premises used: Algebra.IsFiniteSplit.nonempty_algEquiv_fun
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
S' : Type u_3
inst_3 : CommRing S'
inst_4 : Algebra R S'
e : S ≃ₐ[R] S'
inst_5 : IsFiniteSplit R S
n : ℕ
f : S ≃ₐ[R] Fin n → R
⊢ IsFiniteSplit R S'

Tactic:
⟨n, ⟨e.symm.trans f⟩⟩

Premises used: AlgEquiv.symm, Nonempty.intro, AlgEquiv.trans, Exists.intro, Algebra.IsFiniteSplit.mk
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
S' : Type u_3
inst_3 : CommRing S'
inst_4 : Algebra R S'
e : S ≃ₐ[R] S'
inst_5 : IsFiniteSplit R S
n : ℕ
f : S ≃ₐ[R] Fin n → R
⊢ IsFiniteSplit R S'

Tactic:
exact ⟨n, ⟨e.symm.trans f⟩⟩
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ IsFiniteSplit R R

Tactic:
.of_algEquiv (AlgEquiv.funUnique (ι := Fin 1) _ _)

Premises used: Algebra.IsFiniteSplit.of_algEquiv, OfNat.ofNat, Fin, AlgEquiv.funUnique
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Subsingleton S
⊢ IsFiniteSplit R S

Tactic:
⟨0, ⟨default⟩⟩

Premises used: Inhabited.default, Nonempty.intro, Exists.intro, Algebra.IsFiniteSplit.mk, OfNat.ofNat
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Subsingleton R
⊢ Subsingleton S

Tactic:
have : Subsingleton S := RingHom.codomain_trivial (algebraMap R S)
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Subsingleton R
this : Subsingleton S
⊢ IsFiniteSplit R S

Tactic:
of_subsingleton_top

Premises used: Algebra.IsFiniteSplit.of_subsingleton_top
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Subsingleton R
this : Subsingleton S
⊢ IsFiniteSplit R S

Tactic:
exact of_subsingleton_top

Premises used: Algebra.IsFiniteSplit.of_subsingleton_top
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsFiniteSplit R S
obtain : ∀ (n : ℕ) (e : S ≃ₐ[R] Fin n → R), Module.Free R S
⊢ Module.Free R S

Tactic:
obtain ⟨n, ⟨e⟩⟩ := nonempty_algEquiv_fun R S

Premises used: Algebra.IsFiniteSplit.nonempty_algEquiv_fun
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsFiniteSplit R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ Module.Free R S

Tactic:
Module.Free.of_equiv e.symm.toLinearEquiv

Premises used: AlgEquiv.symm, Module.Free.of_equiv, AlgEquiv.toLinearEquiv
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsFiniteSplit R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ Module.Free R S

Tactic:
exact Module.Free.of_equiv e.symm.toLinearEquiv

Premises used: AlgEquiv.symm, Module.Free.of_equiv, AlgEquiv.toLinearEquiv
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsFiniteSplit R S
obtain : ∀ (n : ℕ) (e : S ≃ₐ[R] Fin n → R), Module.FinitePresentation R S
⊢ Module.FinitePresentation R S

Tactic:
obtain ⟨n, ⟨e⟩⟩ := nonempty_algEquiv_fun R S

Premises used: Algebra.IsFiniteSplit.nonempty_algEquiv_fun
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsFiniteSplit R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ Module.FinitePresentation R S

Tactic:
apply Module.FinitePresentation.of_equiv e.symm.toLinearEquiv

Premises used: AlgEquiv.symm, Module.FinitePresentation.of_equiv, AlgEquiv.toLinearEquiv
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsFiniteSplit R S
obtain : ∀ (n : ℕ) (e : S ≃ₐ[R] Fin n → R), Etale R S
⊢ Etale R S

Tactic:
obtain ⟨n, ⟨e⟩⟩ := nonempty_algEquiv_fun R S

Premises used: Algebra.IsFiniteSplit.nonempty_algEquiv_fun
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsFiniteSplit R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ Etale R S

Tactic:
.of_equiv e.symm

Premises used: AlgEquiv.symm, Algebra.Etale.of_equiv
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsFiniteSplit R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ Etale R S

Tactic:
exact .of_equiv e.symm
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑0 : (p : PrimeSpectrum R) → ℕ)
h : IsFiniteSplit R (R ⊗[R] S)
⊢ ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
    Etale R T), IsFiniteSplit T (T ⊗[R] S)

Tactic:
use R, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑0 : (p : PrimeSpectrum R) → ℕ)
e : R ⊗[R] S ≃ₐ[R] S := TensorProduct.lid R S
⊢ Subsingleton S

Tactic:
rw [Nat.cast_zero, Module.rankAtStalk_eq_zero_iff_subsingleton] at hn

Premises used: Module.rankAtStalk_eq_zero_iff_subsingleton, Nat.cast_zero
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Subsingleton S
e : R ⊗[R] S ≃ₐ[R] S := TensorProduct.lid R S
⊢ IsFiniteSplit R S

Tactic:
of_subsingleton_top

Premises used: Algebra.IsFiniteSplit.of_subsingleton_top
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Subsingleton S
e : R ⊗[R] S ≃ₐ[R] S := TensorProduct.lid R S
⊢ IsFiniteSplit R S

Tactic:
exact of_subsingleton_top

Premises used: Algebra.IsFiniteSplit.of_subsingleton_top
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑0 : (p : PrimeSpectrum R) → ℕ)
e : R ⊗[R] S ≃ₐ[R] S := TensorProduct.lid R S
⊢ IsFiniteSplit R S

Tactic:
have : IsFiniteSplit R S := by
      rw [Nat.cast_zero, Module.rankAtStalk_eq_zero_iff_subsingleton] at hn
      exact of_subsingleton_top
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑0 : (p : PrimeSpectrum R) → ℕ)
e : R ⊗[R] S ≃ₐ[R] S := TensorProduct.lid R S
this : IsFiniteSplit R S
⊢ IsFiniteSplit R (R ⊗[R] S)

Tactic:
apply IsFiniteSplit.of_algEquiv e.symm

Premises used: AlgEquiv.symm, Algebra.IsFiniteSplit.of_algEquiv
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n + 1) : (p : PrimeSpectrum R) → ℕ)
succ :
  Subsingleton R →
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
succ₁ :
  Nontrivial R →
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
⊢ ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
    Etale R T), IsFiniteSplit T (T ⊗[R] S)

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n + 1) : (p : PrimeSpectrum R) → ℕ)
h_1 : Subsingleton R
h : IsFiniteSplit R (R ⊗[R] S)
⊢ ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
    Etale R T), IsFiniteSplit T (T ⊗[R] S)

Tactic:
use R, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n + 1) : (p : PrimeSpectrum R) → ℕ)
h : Subsingleton R
⊢ IsFiniteSplit R S

Tactic:
have : IsFiniteSplit R S := .of_subsingleton
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n + 1) : (p : PrimeSpectrum R) → ℕ)
h : Subsingleton R
this : IsFiniteSplit R S
⊢ IsFiniteSplit R (R ⊗[R] S)

Tactic:
.of_algEquiv (TensorProduct.lid R S).symm

Premises used: AlgEquiv.symm, Algebra.TensorProduct.lid, Algebra.IsFiniteSplit.of_algEquiv
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n + 1) : (p : PrimeSpectrum R) → ℕ)
h : Subsingleton R
this : IsFiniteSplit R S
⊢ IsFiniteSplit R (R ⊗[R] S)

Tactic:
exact .of_algEquiv (TensorProduct.lid R S).symm