-- 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:
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)

Tactic:
rintro a b (e : x • a = x • b)

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
a b : S'
e : x • a = x • b
⊢ a = b

Proof state:
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
a b : S'
e : x • a = x • b
⊢ a = b

Tactic:
simp_rw [Submonoid.smul_def, Algebra.smul_def] at e

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
a b : S'
e : (algebraMap R S') ↑x * a = (algebraMap R S') ↑x * b
⊢ a = b

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:
rw [Module.End_isUnit_iff]

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
⊢ Function.Bijective ⇑((algebraMap R (Module.End R S')) ↑x)

Proof state:
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₂

Tactic:
intros x y

Result:
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 y : S
⊢ f.toLinearMap x = f.toLinearMap y → ∃ c, c • x = c • y

Proof state:
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 y : S
⊢ (∃ m, m • x = m • y) → ∃ c, c • x = c • y

Tactic:
exact id

Result:
no goals

Proof state:
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

Tactic:
exact h₂

Result:
no goals

Proof state:
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 y : S
⊢ (∃ m, m • (x - y) = 0) → ∃ c, c • x = c • y

Tactic:
simp_rw [smul_sub, sub_eq_zero]

Result:
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 y : S
⊢ (∃ m, m • x = m • y) → ∃ c, c • x = c • y

Proof state:
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
a b : S'
e : (algebraMap R S') ↑x * a = (algebraMap R S') ↑x * b
⊢ a = b

Tactic:
exact (h₁ x x.2).mul_left_cancel e

Result:
no goals

Proof state:
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 y : S
⊢ f x = f y → ∃ c, c • x = c • y

Tactic:
rw [← sub_eq_zero, ← map_sub, h₃]

Result:
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 y : S
⊢ (∃ m, m • (x - y) = 0) → ∃ c, c • x = c • y

Proof state:
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 y : S
⊢ f.toLinearMap x = f.toLinearMap y → ∃ c, c • x = c • y

Tactic:
dsimp only [AlgHom.toLinearMap_apply]

Result:
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 y : S
⊢ f x = f y → ∃ c, c • x = c • y