-- Mathlib/RingTheory/FiniteType.lean
theorem freeAlgebra_lift_of_surjective_of_closure [CommSemiring R] {S : Set M}
    (hS : closure S = ⊤) :
    Function.Surjective
      (FreeAlgebra.lift R fun s : S => of R M ↑s : FreeAlgebra R S → MonoidAlgebra R M)

Proof state:
case hadd
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f g : MonoidAlgebra R M
ihf : ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = f
ihg : ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = g
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = f + g

Tactic:
rcases ihf with ⟨P, rfl⟩

Result:
case hadd.intro
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
g : MonoidAlgebra R M
ihg : ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = g
P : FreeAlgebra R ↑S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = ((FreeAlgebra.lift R) fun s => (of R M) ↑s) P + g

Proof state:
case hM
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) m

Tactic:
refine Submonoid.closure_induction (fun m hm => ?_) ?_ ?_ this

Result:
case hM.refine_1
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) m

case hM.refine_2
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) 1

case hM.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) x) →
          (∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) y) →
            ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) (x * y)

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f : MonoidAlgebra R M
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = f

Tactic:
induction' f using induction_on with m f g ihf ihg r f ih

Result:
case hM
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) m

case hadd
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f g : MonoidAlgebra R M
ihf : ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = f
ihg : ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = g
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = f + g

case hsmul
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : MonoidAlgebra R M
ih : ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = f
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = r • f

Proof state:
case hsmul.intro
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
P : FreeAlgebra R ↑S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = r • ((FreeAlgebra.lift R) fun s => (of R M) ↑s) P

Tactic:
exact ⟨r • P, map_smul _ _ _⟩

Result:
no goals

Proof state:
case hadd.intro.intro
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : FreeAlgebra R ↑S
⊢ ∃ a,
    ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a =
      ((FreeAlgebra.lift R) fun s => (of R M) ↑s) P + ((FreeAlgebra.lift R) fun s => (of R M) ↑s) Q

Tactic:
exact ⟨P + Q, map_add _ _ _⟩

Result:
no goals

Proof state:
case hM.refine_1
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) m

Tactic:
exact ⟨FreeAlgebra.ι R ⟨m, hm⟩, FreeAlgebra.lift_ι_apply _ _⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
⊢ Surjective ⇑((FreeAlgebra.lift R) fun s => (of R M) ↑s)

Tactic:
intro f

Result:
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f : MonoidAlgebra R M
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = f

Proof state:
case hM.refine_3.intro.intro
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s => (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s => (of R M) ↑s) P₂ = (of R M) m₂
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) (m₁ * m₂)

Tactic:
exact
  ⟨P₁ * P₂, by
    rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩

Result:
no goals

Proof state:
case hM
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) m

Tactic:
have : m ∈ closure S := hS.symm ▸ mem_top _

Result:
case hM
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) m

Proof state:
case hsmul
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : MonoidAlgebra R M
ih : ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = f
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = r • f

Tactic:
rcases ih with ⟨P, rfl⟩

Result:
case hsmul.intro
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
P : FreeAlgebra R ↑S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = r • ((FreeAlgebra.lift R) fun s => (of R M) ↑s) P

Proof state:
case hM.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) x) →
          (∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) y) →
            ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) (x * y)

Tactic:
rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩

Result:
case hM.refine_3.intro.intro
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s => (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s => (of R M) ↑s) P₂ = (of R M) m₂
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) (m₁ * m₂)

Proof state:
case hM.refine_2
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) 1

Tactic:
exact ⟨1, map_one _⟩

Result:
no goals