[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
⊢ map id = id
[PROOFSTEP]
ext ⟨f⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g h : α → β
x✝ : Germ l β
f : α → β
⊢ map id (Quot.mk Setoid.r f) = id (Quot.mk Setoid.r f)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h : α → β
op : β → γ → δ
f f' : α → β
Hf✝ : Setoid.r f f'
g g' : α → γ
Hg✝ : Setoid.r g g'
x : α
Hf : f x = f' x
Hg : g x = g' x
⊢ (fun f g x => op (f x) (g x)) f g x = (fun f g x => op (f x) (g x)) f' g' x
[PROOFSTEP]
simp only [Hf, Hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
f✝ : Germ l β
f : α → β
⊢ 1 • ↑f = ↑f
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
f✝ : Germ l β
f : α → β
⊢ 1 • f =ᶠ[l] f
[PROOFSTEP]
simp only [one_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
f✝ : Germ l β
f : α → β
⊢ f =ᶠ[l] f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁ c₂ : M
f✝ : Germ l β
f : α → β
⊢ (c₁ * c₂) • ↑f = c₁ • c₂ • ↑f
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁ c₂ : M
f✝ : Germ l β
f : α → β
⊢ (c₁ * c₂) • f =ᶠ[l] c₁ • c₂ • f
[PROOFSTEP]
simp only [mul_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁ c₂ : M
f✝ : Germ l β
f : α → β
⊢ c₁ • c₂ • f =ᶠ[l] c₁ • c₂ • f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
f✝ : Germ l β
f : α → β
⊢ 1 • ↑f = ↑f
[PROOFSTEP]
simp only [← coe_one, ← coe_smul', one_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁✝ c₂✝ : Germ l M
f✝ : Germ l β
c₁ c₂ : α → M
f : α → β
⊢ (↑c₁ * ↑c₂) • ↑f = ↑c₁ • ↑c₂ • ↑f
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁✝ c₂✝ : Germ l M
f✝ : Germ l β
c₁ c₂ : α → M
f : α → β
⊢ (c₁ * c₂) • f =ᶠ[l] c₁ • c₂ • f
[PROOFSTEP]
simp only [mul_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁✝ c₂✝ : Germ l M
f✝ : Germ l β
c₁ c₂ : α → M
f : α → β
⊢ c₁ • c₂ • f =ᶠ[l] c₁ • c₂ • f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c : M
⊢ c • 0 = 0
[PROOFSTEP]
simp only [← coe_zero, ← coe_smul, smul_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c : M
f✝ g✝ : Germ l N
f g : α → N
⊢ c • (↑f + ↑g) = c • ↑f + c • ↑g
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c : M
f✝ g✝ : Germ l N
f g : α → N
⊢ c • (f + g) =ᶠ[l] c • f + c • g
[PROOFSTEP]
simp only [smul_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c : M
f✝ g✝ : Germ l N
f g : α → N
⊢ c • f + c • g =ᶠ[l] c • f + c • g
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c✝ : Germ l M
c : α → M
⊢ ↑c • 0 = 0
[PROOFSTEP]
simp only [← coe_zero, ← coe_smul', smul_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c✝ : Germ l M
f✝ g✝ : Germ l N
c : α → M
f g : α → N
⊢ ↑c • (↑f + ↑g) = ↑c • ↑f + ↑c • ↑g
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c✝ : Germ l M
f✝ g✝ : Germ l N
c : α → M
f g : α → N
⊢ c • (f + g) =ᶠ[l] c • f + c • g
[PROOFSTEP]
simp only [smul_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c✝ : Germ l M
f✝ g✝ : Germ l N
c : α → M
f g : α → N
⊢ c • f + c • g =ᶠ[l] c • f + c • g
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁ c₂ : R
f✝ : Germ l M
f : α → M
⊢ (c₁ + c₂) • ↑f = c₁ • ↑f + c₂ • ↑f
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁ c₂ : R
f✝ : Germ l M
f : α → M
⊢ (c₁ + c₂) • f =ᶠ[l] c₁ • f + c₂ • f
[PROOFSTEP]
simp only [add_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁ c₂ : R
f✝ : Germ l M
f : α → M
⊢ c₁ • f + c₂ • f =ᶠ[l] c₁ • f + c₂ • f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f✝ : Germ l M
f : α → M
⊢ 0 • ↑f = 0
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f✝ : Germ l M
f : α → M
⊢ 0 • f =ᶠ[l] 0
[PROOFSTEP]
simp only [zero_smul, coe_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f✝ : Germ l M
f : α → M
⊢ 0 =ᶠ[l] 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁✝ c₂✝ : Germ l R
f✝ : Germ l M
c₁ c₂ : α → R
f : α → M
⊢ (↑c₁ + ↑c₂) • ↑f = ↑c₁ • ↑f + ↑c₂ • ↑f
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁✝ c₂✝ : Germ l R
f✝ : Germ l M
c₁ c₂ : α → R
f : α → M
⊢ (c₁ + c₂) • f =ᶠ[l] c₁ • f + c₂ • f
[PROOFSTEP]
simp only [add_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁✝ c₂✝ : Germ l R
f✝ : Germ l M
c₁ c₂ : α → R
f : α → M
⊢ c₁ • f + c₂ • f =ᶠ[l] c₁ • f + c₂ • f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f✝ : Germ l M
f : α → M
⊢ 0 • ↑f = 0
[PROOFSTEP]
simp only [← coe_zero, ← coe_smul', zero_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x y : Germ l β
f g : α → β
h : f ≤ᶠ[l] g
⊢ ∃ c, ↑g = ↑f * c
[PROOFSTEP]
classical
choose c hc using fun x (hx : f x ≤ g x) ↦ exists_mul_of_le hx
refine ⟨ofFun <| fun x ↦ if hx : f x ≤ g x then c x hx else f x, coe_eq.2 ?_⟩
filter_upwards [h] with x hx
rw [dif_pos hx, hc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x y : Germ l β
f g : α → β
h : f ≤ᶠ[l] g
⊢ ∃ c, ↑g = ↑f * c
[PROOFSTEP]
choose c hc using fun x (hx : f x ≤ g x) ↦ exists_mul_of_le hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x y : Germ l β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → f x ≤ g x → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
⊢ ∃ c, ↑g = ↑f * c
[PROOFSTEP]
refine ⟨ofFun <| fun x ↦ if hx : f x ≤ g x then c x hx else f x, coe_eq.2 ?_⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x y : Germ l β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → f x ≤ g x → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
⊢ g =ᶠ[l] (fun f g x => (fun x x_1 => x * x_1) (f x) (g x)) f fun x => if hx : f x ≤ g x then c x hx else f x
[PROOFSTEP]
filter_upwards [h] with x hx
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x✝ y : Germ l β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → f x ≤ g x → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
x : α
hx : f x ≤ g x
⊢ g x = f x * if hx : f x ≤ g x then c x hx else f x
[PROOFSTEP]
rw [dif_pos hx, hc]
