-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_series_injective [Nontrivial E] : Function.Injective (ofScalars E (𝕜 := 𝕜))

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
h : ¬a₁✝ = a₂✝
⊢ ¬ofScalars E a₁✝ = ofScalars E a₂✝

Tactic:
simp_rw [FormalMultilinearSeries.ext_iff, ofScalars, ContinuousMultilinearMap.ext_iff,
  ContinuousMultilinearMap.smul_apply]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
h : ¬a₁✝ = a₂✝
⊢ ¬∀ (n : ℕ) (x : Fin n → E),
      a₁✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x =
        a₂✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
h : ¬a₁✝ = a₂✝
⊢ ¬∀ (n : ℕ) (x : Fin n → E),
      a₁✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x =
        a₂✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x

Tactic:
push_neg

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
h : ¬a₁✝ = a₂✝
⊢ ∃ n x,
    a₁✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x ≠
      a₂✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
h : ¬a₁✝ = a₂✝
n : ℕ
hn : a₁✝ n ≠ a₂✝ n
⊢ ¬a₁✝ n • 1 = a₂✝ n • 1

Tactic:
exact (smul_left_injective 𝕜 one_ne_zero).ne hn

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
h : ¬a₁✝ = a₂✝
n : ℕ
hn : a₁✝ n ≠ a₂✝ n
⊢ (a₁✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) fun x => 1) ≠
    a₂✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) fun x => 1

Tactic:
simp only [mkPiAlgebraFin_apply, List.ofFn_const, List.prod_replicate, one_pow, ne_eq]

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
h : ¬a₁✝ = a₂✝
n : ℕ
hn : a₁✝ n ≠ a₂✝ n
⊢ ¬a₁✝ n • 1 = a₂✝ n • 1

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
h : ¬a₁✝ = a₂✝
⊢ ∃ n x,
    a₁✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x ≠
      a₂✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x

Tactic:
obtain ⟨n, hn⟩ := Function.ne_iff.1 h

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
h : ¬a₁✝ = a₂✝
n : ℕ
hn : a₁✝ n ≠ a₂✝ n
⊢ ∃ n x,
    a₁✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x ≠
      a₂✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
⊢ Function.Injective (ofScalars E)

Tactic:
intro _ _

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
⊢ ofScalars E a₁✝ = ofScalars E a₂✝ → a₁✝ = a₂✝

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
⊢ ofScalars E a₁✝ = ofScalars E a₂✝ → a₁✝ = a₂✝

Tactic:
refine Function.mtr fun h ↦ ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
h : ¬a₁✝ = a₂✝
⊢ ¬ofScalars E a₁✝ = ofScalars E a₂✝

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
h : ¬a₁✝ = a₂✝
n : ℕ
hn : a₁✝ n ≠ a₂✝ n
⊢ ∃ n x,
    a₁✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x ≠
      a₂✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x

Tactic:
refine ⟨n, fun _ ↦ 1, ?_⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
h : ¬a₁✝ = a₂✝
n : ℕ
hn : a₁✝ n ≠ a₂✝ n
⊢ (a₁✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) fun x => 1) ≠
    a₂✝ n • (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) fun x => 1