-- Mathlib/Algebra/Algebra/Quasispectrum.lean
/-- A version of `NonUnitalAlgHom.quasispectrum_apply_subset` which allows for `quasispectrum R`,
where `R` is a *semi*ring, but `φ` must still function over a scalar ring `S`. In this case, we
need `S` to be explicit. The primary use case is, for instance, `R := ℝ≥0` and `S := ℝ` or
`S := ℂ`. -/
lemma NonUnitalAlgHom.quasispectrum_apply_subset' {F R : Type*} (S : Type*) {A B : Type*}
    [CommSemiring R] [CommRing S] [NonUnitalRing A] [NonUnitalRing B] [Module R S]
    [Module S A] [Module R A] [Module S B] [Module R B] [IsScalarTower R S A] [IsScalarTower R S B]
    [FunLike F A B] [NonUnitalAlgHomClass F S A B] (φ : F) (a : A) :
    quasispectrum R (φ a) ⊆ quasispectrum R a

Proof state:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : NonUnitalRing B
inst✝⁸ : Module R S
inst✝⁷ : Module S A
inst✝⁶ : Module R A
inst✝⁵ : Module S B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R S A
inst✝² : IsScalarTower R S B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
hx : IsUnit x
this : IsQuasiregular (-((↑⋯.unit⁻¹ • 1) • a))
⊢ IsQuasiregular (-((↑⋯.unit⁻¹ • 1) • φ a))

Tactic:
simpa [- smul_assoc] using this.map φ

Result:
no goals

Proof state:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : NonUnitalRing B
inst✝⁸ : Module R S
inst✝⁷ : Module S A
inst✝⁶ : Module R A
inst✝⁵ : Module S B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R S A
inst✝² : IsScalarTower R S B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F S A B
φ : F
a : A
⊢ quasispectrum R (φ a) ⊆ quasispectrum R a

Tactic:
refine Set.compl_subset_compl.mp fun x ↦ ?_

Result:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : NonUnitalRing B
inst✝⁸ : Module R S
inst✝⁷ : Module S A
inst✝⁶ : Module R A
inst✝⁵ : Module S B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R S A
inst✝² : IsScalarTower R S B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
⊢ x ∈ (quasispectrum R a)ᶜ → x ∈ (quasispectrum R (φ a))ᶜ

Proof state:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : NonUnitalRing B
inst✝⁸ : Module R S
inst✝⁷ : Module S A
inst✝⁶ : Module R A
inst✝⁵ : Module S B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R S A
inst✝² : IsScalarTower R S B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
⊢ x ∈ (quasispectrum R a)ᶜ → x ∈ (quasispectrum R (φ a))ᶜ

Tactic:
simp only [quasispectrum, Set.mem_compl_iff, Set.mem_setOf_eq, not_forall, not_not,
  forall_exists_index]

Result:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : NonUnitalRing B
inst✝⁸ : Module R S
inst✝⁷ : Module S A
inst✝⁶ : Module R A
inst✝⁵ : Module S B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R S A
inst✝² : IsScalarTower R S B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
⊢ ∀ (x_1 : IsUnit x), IsQuasiregular (-(⋯.unit⁻¹ • a)) → ∃ (h : IsUnit x), IsQuasiregular (-(⋯.unit⁻¹ • φ a))

Proof state:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : NonUnitalRing B
inst✝⁸ : Module R S
inst✝⁷ : Module S A
inst✝⁶ : Module R A
inst✝⁵ : Module S B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R S A
inst✝² : IsScalarTower R S B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
hx : IsUnit x
this : IsQuasiregular (-(⋯.unit⁻¹ • a))
⊢ IsQuasiregular (-(⋯.unit⁻¹ • φ a))

Tactic:
rw [Units.smul_def, ← smul_one_smul S] at this ⊢

Result:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : NonUnitalRing B
inst✝⁸ : Module R S
inst✝⁷ : Module S A
inst✝⁶ : Module R A
inst✝⁵ : Module S B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R S A
inst✝² : IsScalarTower R S B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
hx : IsUnit x
this : IsQuasiregular (-((↑⋯.unit⁻¹ • 1) • a))
⊢ IsQuasiregular (-((↑⋯.unit⁻¹ • 1) • φ a))

Proof state:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : NonUnitalRing B
inst✝⁸ : Module R S
inst✝⁷ : Module S A
inst✝⁶ : Module R A
inst✝⁵ : Module S B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R S A
inst✝² : IsScalarTower R S B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
⊢ ∀ (x_1 : IsUnit x), IsQuasiregular (-(⋯.unit⁻¹ • a)) → ∃ (h : IsUnit x), IsQuasiregular (-(⋯.unit⁻¹ • φ a))

Tactic:
refine fun hx this ↦ ⟨hx, ?_⟩

Result:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : NonUnitalRing B
inst✝⁸ : Module R S
inst✝⁷ : Module S A
inst✝⁶ : Module R A
inst✝⁵ : Module S B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R S A
inst✝² : IsScalarTower R S B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
hx : IsUnit x
this : IsQuasiregular (-(⋯.unit⁻¹ • a))
⊢ IsQuasiregular (-(⋯.unit⁻¹ • φ a))