-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mkOfAlgebra {R S S' : Type*} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S]
    [Algebra R S'] (M : Submonoid R) (f : S →ₐ[R] S') (h₁ : ∀ x ∈ M, IsUnit (algebraMap R S' x))
    (h₂ : ∀ y, ∃ x : S × M, x.2 • y = f x.1) (h₃ : ∀ x, f x = 0 → ∃ m : M, m • x = 0) :
    IsLocalizedModule M f.toLinearMap

Proof state:
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 → ∃ m, m • x = 0
x : S
x✝ : ∃ m, m • x = 0
m : R
hm : m ∈ M
e : ⟨m, hm⟩ • x = 0
⊢ (algebraMap R S') m * f x = (algebraMap R S') m * 0

Tactic:
rw [← Algebra.smul_def]

Result:
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 → ∃ m, m • x = 0
x : S
x✝ : ∃ m, m • x = 0
m : R
hm : m ∈ M
e : ⟨m, hm⟩ • x = 0
⊢ m • f x = (algebraMap R S') m * 0

Proof state:
case map_units.right
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
a : S'
⊢ ∃ a_1, ((algebraMap R (Module.End R S')) ↑x) a_1 = a

Tactic:
refine ⟨((h₁ x x.2).unit⁻¹ :) * a, ?_⟩

Result:
case map_units.right
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
a : S'
⊢ ((algebraMap R (Module.End R S')) ↑x) (↑⋯.unit⁻¹ * a) = a

Proof state:
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 → ∃ m, m • x = 0
⊢ IsLocalizedModule M f.toLinearMap

Tactic:
replace h₃ := fun x =>
  Iff.intro (h₃ x) fun ⟨⟨m, hm⟩, e⟩ =>
    (h₁ m hm).mul_left_cancel <| by
      rw [← Algebra.smul_def]
      simpa [Submonoid.smul_def] using f.congr_arg e

Result:
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
⊢ IsLocalizedModule M f.toLinearMap

Proof state:
case map_units.right
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
⊢ Function.Surjective ⇑((algebraMap R (Module.End R S')) ↑x)

Tactic:
intro a

Result:
case map_units.right
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
a : S'
⊢ ∃ a_1, ((algebraMap R (Module.End R S')) ↑x) a_1 = a

Proof state:
case map_units.right
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
a : S'
⊢ ((algebraMap R (Module.End R S')) ↑x) (↑⋯.unit⁻¹ * a) = a

Tactic:
rw [Module.algebraMap_end_apply, Algebra.smul_def, ← mul_assoc, IsUnit.mul_val_inv, one_mul]

Result:
no goals

Proof state:
case map_units
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
⊢ ∀ (x : ↥M), IsUnit ((algebraMap R (Module.End R S')) ↑x)

Tactic:
intro x

Result:
case map_units
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
⊢ IsUnit ((algebraMap R (Module.End R S')) ↑x)

Proof state:
case map_units
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
⊢ Function.Bijective ⇑((algebraMap R (Module.End R S')) ↑x)

Tactic:
constructor

Result:
case map_units.left
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
⊢ Function.Injective ⇑((algebraMap R (Module.End R S')) ↑x)

case map_units.right
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
⊢ Function.Surjective ⇑((algebraMap R (Module.End R S')) ↑x)

Proof state:
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
⊢ IsLocalizedModule M f.toLinearMap

Tactic:
constructor

Result:
case map_units
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
⊢ ∀ (x : ↥M), IsUnit ((algebraMap R (Module.End R S')) ↑x)

case surj'
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
⊢ ∀ (y : S'), ∃ x, x.2 • y = f.toLinearMap x.1

case exists_of_eq
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
⊢ ∀ {x₁ x₂ : S}, f.toLinearMap x₁ = f.toLinearMap x₂ → ∃ c, c • x₁ = c • x₂