-- Mathlib/RingTheory/FiniteType.lean
theorem iff_quotient_freeAlgebra :
    FiniteType R A ↔
      ∃ (s : Finset A) (f : FreeAlgebra R s →ₐ[R] A), Surjective f

Proof state:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ FiniteType R A ↔ ∃ s f, Surjective ⇑f

Tactic:
constructor

Result:
case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ FiniteType R A → ∃ s f, Surjective ⇑f

case mpr
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (∃ s f, Surjective ⇑f) → FiniteType R A

Proof state:
case mp.mk.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
x : A
hrw : ↑s = fun x => x ∈ s.val
⊢ x ∈ ↑(adjoin R (Membership.mem s.val))

Tactic:
simp_rw [← hrw, hs]

Result:
case mp.mk.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
x : A
hrw : ↑s = fun x => x ∈ s.val
⊢ x ∈ ↑⊤

Proof state:
case mp.mk.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
x : A
⊢ ∃ a, ((FreeAlgebra.lift R) Subtype.val) a = x

Tactic:
have hrw : (↑s : Set A) = fun x : A => x ∈ s.val := rfl

Result:
case mp.mk.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
x : A
hrw : ↑s = fun x => x ∈ s.val
⊢ ∃ a, ((FreeAlgebra.lift R) Subtype.val) a = x

Proof state:
case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ FiniteType R A → ∃ s f, Surjective ⇑f

Tactic:
rintro ⟨s, hs⟩

Result:
case mp.mk.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ ∃ s f, Surjective ⇑f

Proof state:
case mpr.intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
f : FreeAlgebra R { x // x ∈ s } →ₐ[R] A
hsur : Surjective ⇑f
⊢ FiniteType R A

Tactic:
exact FiniteType.of_surjective (FiniteType.freeAlgebra R s) f hsur

Result:
no goals

Proof state:
case mp.mk.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
x : A
hrw : ↑s = fun x => x ∈ s.val
⊢ ∃ a, ((FreeAlgebra.lift R) Subtype.val) a = x

Tactic:
rw [← Set.mem_range, ← AlgHom.coe_range]

Result:
case mp.mk.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
x : A
hrw : ↑s = fun x => x ∈ s.val
⊢ x ∈ ↑((FreeAlgebra.lift R) Subtype.val).range

Proof state:
case mp.mk.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ ∃ s f, Surjective ⇑f

Tactic:
refine ⟨s, FreeAlgebra.lift _ (↑), ?_⟩

Result:
case mp.mk.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ Surjective ⇑((FreeAlgebra.lift R) Subtype.val)

Proof state:
case mp.mk.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
x : A
hrw : ↑s = fun x => x ∈ s.val
⊢ x ∈ ↑((FreeAlgebra.lift R) Subtype.val).range

Tactic:
erw [← adjoin_eq_range_freeAlgebra_lift]

Result:
case mp.mk.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
x : A
hrw : ↑s = fun x => x ∈ s.val
⊢ x ∈ ↑(adjoin R (Membership.mem s.val))

Proof state:
case mp.mk.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ Surjective ⇑((FreeAlgebra.lift R) Subtype.val)

Tactic:
intro x

Result:
case mp.mk.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
x : A
⊢ ∃ a, ((FreeAlgebra.lift R) Subtype.val) a = x

Proof state:
case mp.mk.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
x : A
hrw : ↑s = fun x => x ∈ s.val
⊢ x ∈ ↑⊤

Tactic:
exact Set.mem_univ x

Result:
no goals

Proof state:
case mpr
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (∃ s f, Surjective ⇑f) → FiniteType R A

Tactic:
rintro ⟨s, ⟨f, hsur⟩⟩

Result:
case mpr.intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
f : FreeAlgebra R { x // x ∈ s } →ₐ[R] A
hsur : Surjective ⇑f
⊢ FiniteType R A