case h₁
R : Type u_2
R₁ : Type ?u.154967
R₂ : Type ?u.154970
R₃ : Type ?u.154973
k : Type ?u.154976
S : Type u_3
S₃ : Type ?u.154982
T : Type ?u.154985
M : Type u_4
M₁ : Type ?u.154991
M₂ : Type ?u.154994
M₃ : Type u_5
N₁ : Type ?u.155000
N₂ : Type ?u.155003
N₃ : Type ?u.155006
ι : Type ?u.155009
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_1
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
⊢ ↑h ⁻¹' (↑σ c • s) ⊆ c • ↑h ⁻¹' s

case h₂
R : Type u_2
R₁ : Type ?u.154967
R₂ : Type ?u.154970
R₃ : Type ?u.154973
k : Type ?u.154976
S : Type u_3
S₃ : Type ?u.154982
T : Type ?u.154985
M : Type u_4
M₁ : Type ?u.154991
M₂ : Type ?u.154994
M₃ : Type u_5
N₁ : Type ?u.155000
N₂ : Type ?u.155003
N₃ : Type ?u.155006
ι : Type ?u.155009
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_1
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
⊢ c • ↑h ⁻¹' s ⊆ ↑h ⁻¹' (↑σ c • s)
R : Type u_2
R₁ : Type ?u.154967
R₂ : Type ?u.154970
R₃ : Type ?u.154973
k : Type ?u.154976
S : Type u_3
S₃ : Type ?u.154982
T : Type ?u.154985
M : Type u_4
M₁ : Type ?u.154991
M₂ : Type ?u.154994
M₃ : Type u_5
N₁ : Type ?u.155000
N₂ : Type ?u.155003
N₃ : Type ?u.155006
ι : Type ?u.155009
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_1
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
⊢ ↑h ⁻¹' (↑σ c • s) = c • ↑h ⁻¹' s
apply Set.Subset.antisymm
case h₁.intro.intro
R : Type u_2
R₁ : Type ?u.154967
R₂ : Type ?u.154970
R₃ : Type ?u.154973
k : Type ?u.154976
S : Type u_3
S₃ : Type ?u.154982
T : Type ?u.154985
M : Type u_4
M₁ : Type ?u.154991
M₂ : Type ?u.154994
M₃ : Type u_5
N₁ : Type ?u.155000
N₂ : Type ?u.155003
N₃ : Type ?u.155006
ι : Type ?u.155009
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_1
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
x : M
y : M₃
ys : y ∈ s
hy : (fun x => ↑σ c • x) y = ↑h x
⊢ x ∈ c • ↑h ⁻¹' s
case h₁
R : Type u_2
R₁ : Type ?u.154967
R₂ : Type ?u.154970
R₃ : Type ?u.154973
k : Type ?u.154976
S : Type u_3
S₃ : Type ?u.154982
T : Type ?u.154985
M : Type u_4
M₁ : Type ?u.154991
M₂ : Type ?u.154994
M₃ : Type u_5
N₁ : Type ?u.155000
N₂ : Type ?u.155003
N₃ : Type ?u.155006
ι : Type ?u.155009
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_1
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
⊢ ↑h ⁻¹' (↑σ c • s) ⊆ c • ↑h ⁻¹' s
rintro x ⟨y, ys, hy⟩
case h₁.intro.intro.refine'_1
R : Type u_2
R₁ : Type ?u.154967
R₂ : Type ?u.154970
R₃ : Type ?u.154973
k : Type ?u.154976
S : Type u_3
S₃ : Type ?u.154982
T : Type ?u.154985
M : Type u_4
M₁ : Type ?u.154991
M₂ : Type ?u.154994
M₃ : Type u_5
N₁ : Type ?u.155000
N₂ : Type ?u.155003
N₃ : Type ?u.155006
ι : Type ?u.155009
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_1
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
x : M
y : M₃
ys : y ∈ s
hy : (fun x => ↑σ c • x) y = ↑h x
⊢ (IsUnit.unit hc).inv • x ∈ ↑h ⁻¹' s

case h₁.intro.intro.refine'_2
R : Type u_2
R₁ : Type ?u.154967
R₂ : Type ?u.154970
R₃ : Type ?u.154973
k : Type ?u.154976
S : Type u_3
S₃ : Type ?u.154982
T : Type ?u.154985
M : Type u_4
M₁ : Type ?u.154991
M₂ : Type ?u.154994
M₃ : Type u_5
N₁ : Type ?u.155000
N₂ : Type ?u.155003
N₃ : Type ?u.155006
ι : Type ?u.155009
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_1
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
x : M
y : M₃
ys : y ∈ s
hy : (fun x => ↑σ c • x) y = ↑h x
⊢ (fun x => c • x) ((IsUnit.unit hc).inv • x) = x
case h₁.intro.intro
R : Type u_2
R₁ : Type ?u.154967
R₂ : Type ?u.154970
R₃ : Type ?u.154973
k : Type ?u.154976
S : Type u_3
S₃ : Type ?u.154982
T : Type ?u.154985
M : Type u_4
M₁ : Type ?u.154991
M₂ : Type ?u.154994
M₃ : Type u_5
N₁ : Type ?u.155000
N₂ : Type ?u.155003
N₃ : Type ?u.155006
ι : Type ?u.155009
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_1
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
x : M
y : M₃
ys : y ∈ s
hy : (fun x => ↑σ c • x) y = ↑h x
⊢ x ∈ c • ↑h ⁻¹' s
refine' ⟨(hc.unit.inv : R) • x, _, _⟩
no goals
case h₁.intro.intro.refine'_1
R : Type u_2
R₁ : Type ?u.154967
R₂ : Type ?u.154970
R₃ : Type ?u.154973
k : Type ?u.154976
S : Type u_3
S₃ : Type ?u.154982
T : Type ?u.154985
M : Type u_4
M₁ : Type ?u.154991
M₂ : Type ?u.154994
M₃ : Type u_5
N₁ : Type ?u.155000
N₂ : Type ?u.155003
N₃ : Type ?u.155006
ι : Type ?u.155009
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_1
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
x : M
y : M₃
ys : y ∈ s
hy : (fun x => ↑σ c • x) y = ↑h x
⊢ (IsUnit.unit hc).inv • x ∈ ↑h ⁻¹' s
simp only [← hy, smul_smul, Set.mem_preimage, Units.inv_eq_val_inv, map_smulₛₗ h, ← map_mul,
  IsUnit.val_inv_mul, one_smul, map_one, ys]
no goals
case h₁.intro.intro.refine'_2
R : Type u_2
R₁ : Type ?u.154967
R₂ : Type ?u.154970
R₃ : Type ?u.154973
k : Type ?u.154976
S : Type u_3
S₃ : Type ?u.154982
T : Type ?u.154985
M : Type u_4
M₁ : Type ?u.154991
M₂ : Type ?u.154994
M₃ : Type u_5
N₁ : Type ?u.155000
N₂ : Type ?u.155003
N₃ : Type ?u.155006
ι : Type ?u.155009
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_1
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
x : M
y : M₃
ys : y ∈ s
hy : (fun x => ↑σ c • x) y = ↑h x
⊢ (fun x => c • x) ((IsUnit.unit hc).inv • x) = x
simp only [smul_smul, IsUnit.mul_val_inv, one_smul, Units.inv_eq_val_inv]
case h₂.intro.intro
R : Type u_2
R₁ : Type ?u.154967
R₂ : Type ?u.154970
R₃ : Type ?u.154973
k : Type ?u.154976
S : Type u_3
S₃ : Type ?u.154982
T : Type ?u.154985
M : Type u_4
M₁ : Type ?u.154991
M₂ : Type ?u.154994
M₃ : Type u_5
N₁ : Type ?u.155000
N₂ : Type ?u.155003
N₃ : Type ?u.155006
ι : Type ?u.155009
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_1
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
y : M
hy : y ∈ ↑h ⁻¹' s
⊢ (fun x => c • x) y ∈ ↑h ⁻¹' (↑σ c • s)
case h₂
R : Type u_2
R₁ : Type ?u.154967
R₂ : Type ?u.154970
R₃ : Type ?u.154973
k : Type ?u.154976
S : Type u_3
S₃ : Type ?u.154982
T : Type ?u.154985
M : Type u_4
M₁ : Type ?u.154991
M₂ : Type ?u.154994
M₃ : Type u_5
N₁ : Type ?u.155000
N₂ : Type ?u.155003
N₃ : Type ?u.155006
ι : Type ?u.155009
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_1
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
⊢ c • ↑h ⁻¹' s ⊆ ↑h ⁻¹' (↑σ c • s)
rintro x ⟨y, hy, rfl⟩
no goals
case h₂.intro.intro
R : Type u_2
R₁ : Type ?u.154967
R₂ : Type ?u.154970
R₃ : Type ?u.154973
k : Type ?u.154976
S : Type u_3
S₃ : Type ?u.154982
T : Type ?u.154985
M : Type u_4
M₁ : Type ?u.154991
M₂ : Type ?u.154994
M₃ : Type u_5
N₁ : Type ?u.155000
N₂ : Type ?u.155003
N₃ : Type ?u.155006
ι : Type ?u.155009
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_1
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
y : M
hy : y ∈ ↑h ⁻¹' s
⊢ (fun x => c • x) y ∈ ↑h ⁻¹' (↑σ c • s)
refine' ⟨h y, hy, by simp only [RingHom.id_apply, map_smulₛₗ h]⟩
no goals
R : Type u_2
R₁ : Type ?u.154967
R₂ : Type ?u.154970
R₃ : Type ?u.154973
k : Type ?u.154976
S : Type u_3
S₃ : Type ?u.154982
T : Type ?u.154985
M : Type u_4
M₁ : Type ?u.154991
M₂ : Type ?u.154994
M₃ : Type u_5
N₁ : Type ?u.155000
N₂ : Type ?u.155003
N₃ : Type ?u.155006
ι : Type ?u.155009
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_1
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
y : M
hy : y ∈ ↑h ⁻¹' s
⊢ (fun x => ↑σ c • x) (↑h y) = ↑h ((fun x => c • x) y)
simp only [RingHom.id_apply, map_smulₛₗ h]