-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
/-- If `M` is a finite `R`-module, then the canonical map
`AdicCompletion I R ⊗[R] M →ₗ AdicCompletion I M` is surjective. -/
lemma ofTensorProduct_surjective_of_finite [Module.Finite R M] :
    Function.Surjective (ofTensorProduct I M)

Proof state:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
hfg : f = g
⊢ Function.Surjective ⇑f

Tactic:
simp only [hfg, LinearMap.coe_comp, g]

Result:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
hfg : f = g
⊢ Function.Surjective (⇑(map I p) ∘ ⇑(ofTensorProduct I (Fin n → R)))

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
hfg : f = g
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(ofTensorProduct I M)

Tactic:
exact Function.Surjective.of_comp hf

Result:
no goals

Proof state:
case hf
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
hfg : f = g
⊢ Function.Surjective ⇑(ofTensorProduct I (Fin n → R))

Tactic:
exact (ofTensorProduct_bijective_of_pi_of_fintype I (Fin n)).surjective

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
⊢ Function.Surjective ⇑(ofTensorProduct I M)

Tactic:
obtain ⟨n, p, hp⟩ := Module.Finite.exists_fin' R M

Result:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
⊢ Function.Surjective ⇑(ofTensorProduct I M)

Proof state:
case a.h.h.h.h
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
i✝ : Fin n
n✝ : ℕ
⊢ ↑(((AlgebraTensorModule.curry f) 1 ∘ₗ LinearMap.single R (fun i => R) i✝) 1) n✝ =
    ↑(((AlgebraTensorModule.curry g) 1 ∘ₗ LinearMap.single R (fun i => R) i✝) 1) n✝

Tactic:
simp [f, g]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
hfg : f = g
⊢ Function.Surjective (⇑(map I p) ∘ ⇑(ofTensorProduct I (Fin n → R)))

Tactic:
apply Function.Surjective.comp

Result:
case hg
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
hfg : f = g
⊢ Function.Surjective ⇑(map I p)

case hf
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
hfg : f = g
⊢ Function.Surjective ⇑(ofTensorProduct I (Fin n → R))

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
⊢ Function.Surjective ⇑(ofTensorProduct I M)

Tactic:
have hfg : f = g := by
  ext
  simp [f, g]

Result:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
hfg : f = g
⊢ Function.Surjective ⇑(ofTensorProduct I M)

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
⊢ Function.Surjective ⇑(ofTensorProduct I M)

Tactic:
let f := ofTensorProduct I M ∘ₗ p.baseChange (AdicCompletion I R)

Result:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
⊢ Function.Surjective ⇑(ofTensorProduct I M)