awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
t : Finset T
ht :
  ∀ (s : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)
x y : T
hy₁ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) y
hy₂ : IsUnit y
hy₃ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (x * y)
t₁ : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₁
h₂ : IsUnit t₁
h₃ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₁ • y)
t₂ : S
h₄ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₂
h₅ : IsUnit t₂
h₆ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • (x * y))
h :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • t₁ • y)
h₇ : IsUnit (t₂ • t₁ • y)
h₈ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (x * t₂ • t₁ • y)
⊢ ∃ (t_1 : T),
    Membership.mem (γ := Subalgebra R T)
        (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) t_1 ∧
      IsUnit t_1 ∧
        Membership.mem (γ := Subalgebra R T)
          (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (x * t_1)

Tactic:
refine ⟨t₂ • t₁ • y, ?_, ?_, ?_⟩
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
t : Finset T
ht :
  ∀ (s : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)
x y : T
hy₁ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) y
hy₂ : IsUnit y
hy₃ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (x * y)
t₁ : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₁
h₂ : IsUnit t₁
h₃ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₁ • y)
t₂ : S
h₄ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₂
h₅ : IsUnit t₂
h₆ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • (x * y))
h :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T))
    (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) t₂ : T) (t₁ • y))
⊢ Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • t₁ • y)

Tactic:
rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
t : Finset T
ht :
  ∀ (s : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)
x y : T
hy₁ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) y
hy₂ : IsUnit y
hy₃ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (x * y)
t₁ : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₁
h₂ : IsUnit t₁
h₃ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₁ • y)
t₂ : S
h₄ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₂
h₅ : IsUnit t₂
h₆ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • (x * y))
⊢ Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T))
    (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) t₂ : T) (t₁ • y))

Tactic:
mul_mem (Algebra.mem_sup_left ⟨_, h₄, rfl⟩) h₃

Premises used: Algebra.mem_sup_left, And.intro, Exists.intro, rfl, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
t : Finset T
ht :
  ∀ (s : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)
x y : T
hy₁ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) y
hy₂ : IsUnit y
hy₃ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (x * y)
t₁ : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₁
h₂ : IsUnit t₁
h₃ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₁ • y)
t₂ : S
h₄ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₂
h₅ : IsUnit t₂
h₆ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • (x * y))
⊢ Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T))
    (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) t₂ : T) (t₁ • y))

Tactic:
exact mul_mem (Algebra.mem_sup_left ⟨_, h₄, rfl⟩) h₃
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
t : Finset T
ht :
  ∀ (s : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)
x y : T
hy₁ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) y
hy₂ : IsUnit y
hy₃ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (x * y)
t₁ : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₁
h₂ : IsUnit t₁
h₃ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₁ • y)
t₂ : S
h₄ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₂
h₅ : IsUnit t₂
h₆ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • (x * y))
h :
  IsUnit
    (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) t₂ : T)
      (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) t₁ : T) y))
⊢ IsUnit (t₂ • t₁ • y)

Tactic:
rw [Algebra.smul_def, Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
t : Finset T
ht :
  ∀ (s : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)
x y : T
hy₁ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) y
hy₂ : IsUnit y
hy₃ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (x * y)
t₁ : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₁
h₂ : IsUnit t₁
h₃ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₁ • y)
t₂ : S
h₄ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₂
h₅ : IsUnit t₂
h₆ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • (x * y))
⊢ IsUnit
    (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) t₂ : T)
      (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) t₁ : T) y))

Tactic:
(h₅.map _).mul ((h₂.map _).mul hy₂)

Premises used: IsUnit.mul, IsUnit.map
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
t : Finset T
ht :
  ∀ (s : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)
x y : T
hy₁ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) y
hy₂ : IsUnit y
hy₃ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (x * y)
t₁ : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₁
h₂ : IsUnit t₁
h₃ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₁ • y)
t₂ : S
h₄ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₂
h₅ : IsUnit t₂
h₆ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • (x * y))
⊢ IsUnit
    (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) t₂ : T)
      (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) t₁ : T) y))

Tactic:
exact (h₅.map _).mul ((h₂.map _).mul hy₂)

Premises used: IsUnit.mul, IsUnit.map
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
t : Finset T
ht :
  ∀ (s : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)
x y : T
hy₁ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) y
hy₂ : IsUnit y
hy₃ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (x * y)
t₁ : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₁
h₂ : IsUnit t₁
h₃ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₁ • y)
t₂ : S
h₄ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₂
h₅ : IsUnit t₂
h₆ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • (x * y))
h :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T))
    (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) t₁ : T) (t₂ • (x * y)))
⊢ Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (x * t₂ • t₁ • y)

Tactic:
rw [← mul_smul, mul_comm, smul_mul_assoc, mul_comm, mul_comm y, mul_smul, Algebra.smul_def]

Premises used: smul_mul_assoc, mul_comm, Algebra.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
t : Finset T
ht :
  ∀ (s : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)
x y : T
hy₁ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) y
hy₂ : IsUnit y
hy₃ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (x * y)
t₁ : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₁
h₂ : IsUnit t₁
h₃ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₁ • y)
t₂ : S
h₄ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₂
h₅ : IsUnit t₂
h₆ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • (x * y))
⊢ Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T))
    (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) t₁ : T) (t₂ • (x * y)))

Tactic:
mul_mem (Algebra.mem_sup_left ⟨_, h₁, rfl⟩) h₆

Premises used: Algebra.mem_sup_left, And.intro, Exists.intro, rfl, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ EssFiniteType R S ↔ ∃ (S₀ : Subalgebra R S) (M : Submonoid ↥S₀), FiniteType.{u_1, u_2} R ↥S₀ ∧ IsLocalization M S

Tactic:
⟨fun h ↦ ⟨subalgebra R S, submonoid R S, inferInstance, inferInstance⟩, ?_⟩

Premises used: Algebra.EssFiniteType.subalgebra, Algebra.EssFiniteType.submonoid, inferInstance, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
refine :
  (∃ (S₀ : Subalgebra R S) (M : Submonoid ↥S₀), FiniteType.{u_1, u_2} R ↥S₀ ∧ IsLocalization M S) → EssFiniteType R S
⊢ EssFiniteType R S ↔ ∃ (S₀ : Subalgebra R S) (M : Submonoid ↥S₀), FiniteType.{u_1, u_2} R ↥S₀ ∧ IsLocalization M S

Tactic:
refine ⟨fun h ↦ ⟨subalgebra R S, submonoid R S, inferInstance, inferInstance⟩, ?_⟩
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
S₀ : Subalgebra R S
M : Submonoid ↥S₀
left : FiniteType.{u_1, u_2} R ↥S₀
right : IsLocalization M S
this : EssFiniteType (↥S₀) S := ⋯
⊢ EssFiniteType R S

Tactic:
comp R S₀ S

Premises used: Algebra.EssFiniteType.comp, Membership.mem, Subtype
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
S₀ : Subalgebra R S
M : Submonoid ↥S₀
left : FiniteType.{u_1, u_2} R ↥S₀
right : IsLocalization M S
this : EssFiniteType (↥S₀) S := ⋯
⊢ EssFiniteType R S

Tactic:
exact comp R S₀ S

Premises used: Algebra.EssFiniteType.comp, Membership.mem, Subtype
-- Module: Mathlib.RingTheory.EssentialFiniteness
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 : EssFiniteType R S
rw :
  ∀
    (h :
      ∃ (σ : Finset S),
        ∀ (s : S),
          ∃ (t : S),
            Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
              IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)),
    ∃ (σ : Finset (T ⊗[R] S)),
      ∀ (s : T ⊗[R] S),
        ∃ (t : T ⊗[R] S),
          Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) t ∧
            IsUnit t ∧ Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) (s * t)
⊢ EssFiniteType T (T ⊗[R] S)

Tactic:
rw [essFiniteType_iff] at h ⊢

Premises used: Algebra.essFiniteType_iff
-- Module: Mathlib.RingTheory.EssentialFiniteness
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 S),
    ∀ (s : S),
      ∃ (t : S),
        Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
obtain :
  ∀ (σ : Finset S)
    (hσ :
      ∀ (s : S),
        ∃ (t : S),
          Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
            IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)),
    ∃ (σ : Finset (T ⊗[R] S)),
      ∀ (s : T ⊗[R] S),
        ∃ (t : T ⊗[R] S),
          Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) t ∧
            IsUnit t ∧ Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) (s * t)
⊢ ∃ (σ : Finset (T ⊗[R] S)),
    ∀ (s : T ⊗[R] S),
      ∃ (t : T ⊗[R] S),
        Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) (s * t)

Tactic:
obtain ⟨σ, hσ⟩ := h
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
h :
  ∀ (s : T ⊗[R] S),
    ∃ (t : T ⊗[R] S),
      Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
        IsUnit t ∧
          Membership.mem (γ := Subalgebra T (T ⊗[R] S))
            (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (s * t)
⊢ ∃ (σ : Finset (T ⊗[R] S)),
    ∀ (s : T ⊗[R] S),
      ∃ (t : T ⊗[R] S),
        Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) (s * t)

Tactic:
use σ.image Algebra.TensorProduct.includeRight

Premises used: DFunLike.coe, Finset.image, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
⊢ Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
    (HMul.hMul (α := T ⊗[R] S) 0 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
⊢ ∃ (t : T ⊗[R] S),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
      IsUnit t ∧
        Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (0 * t)

Tactic:
exact ⟨1, one_mem _, isUnit_one, by simp⟩
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x : T
y : S
h :
  ∀ (t : S) (h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t) (h₂ : IsUnit t)
    (h₃ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (y * t)),
    ∃ (t : T ⊗[R] S),
      Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
        IsUnit t ∧
          Membership.mem (γ := Subalgebra T (T ⊗[R] S))
            (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
            (x ⊗ₜ[R] y * t)
⊢ ∃ (t : T ⊗[R] S),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
      IsUnit t ∧
        Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
          (x ⊗ₜ[R] y * t)

Tactic:
obtain ⟨t, h₁, h₂, h₃⟩ := hσ y