awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ Eq (α := M ⧸ S) ((S.normedMk : (a : M) → M ⧸ S) m : M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m : M ⧸ S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
⊢ Function.Surjective (α := M) (β := M ⧸ S) (⇑S.normedMk : (a : M) → M ⧸ S)

Tactic:
Quot.mk_surjective

Premises used: Quotient, Quot.mk_surjective
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
⊢ S.normedMk.ker = S

Tactic:
QuotientAddGroup.ker_mk' _

Premises used: QuotientAddGroup.ker_mk', QuotientAddGroup.mk', NormedAddGroupHom.toAddMonoidHom, NormedAddGroupHom.ker
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ norm (E := M ⧸ S) ((S.normedMk : (a : M) → M ⧸ S) m : M ⧸ S) ≤ 1 * ‖m‖

Tactic:
simp [norm_mk_le_norm]

Premises used: QuotientAddGroup.norm_mk_le_norm
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
x : M ⧸ S
h : ‖f‖ = 0
inl :
  ∀ (x : M),
    norm.{u_2} (E := N) ((lift S f.toAddMonoidHom hf : (a : M ⧸ S) → N) (↑x : M ⧸ S) : N) ≤
      ‖f‖ * norm (E := M ⧸ S) (↑x : M ⧸ S)
⊢ norm.{u_2} (E := N) ((lift S f.toAddMonoidHom hf : (a : M ⧸ S) → N) x : N) ≤ ‖f‖ * ‖x‖

Tactic:
rcases mk_surjective x with ⟨x, rfl⟩

Premises used: QuotientAddGroup.mk_surjective, rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
h : ‖f‖ = 0
x : M
⊢ norm.{u_2} (E := N) ((lift S f.toAddMonoidHom hf : (a : M ⧸ S) → N) (↑x : M ⧸ S) : N) ≤
    ‖f‖ * norm (E := M ⧸ S) (↑x : M ⧸ S)

Tactic:
simpa [h] using le_opNorm f x

Premises used: NormedAddGroupHom.le_opNorm
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
x : M ⧸ S
h : 0 < ‖f‖
inr :
  ¬∃ (m : M), (↑m : M ⧸ S) = x ∧ ‖m‖ < norm.{u_2} (E := N) ((lift S f.toAddMonoidHom hf : (a : M ⧸ S) → N) x : N) / ‖f‖
⊢ norm.{u_2} (E := N) ((lift S f.toAddMonoidHom hf : (a : M ⧸ S) → N) x : N) ≤ ‖f‖ * ‖x‖

Tactic:
rw [← not_lt, ← lt_div_iff₀' h, norm_lt_iff]

Premises used: lt_div_iff₀', QuotientAddGroup.norm_lt_iff, not_lt
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
h : 0 < ‖f‖
x : M
hx : ‖x‖ < norm.{u_2} (E := N) ((lift S f.toAddMonoidHom hf : (a : M ⧸ S) → N) (↑x : M ⧸ S) : N) / ‖f‖
⊢ False

Tactic:
((lt_div_iff₀' h).1 hx).not_ge (le_opNorm f x)

Premises used: lt_div_iff₀', NormedAddGroupHom.le_opNorm, Iff.mp, LT.lt.not_ge
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
h : 0 < ‖f‖
x : M
hx : ‖x‖ < norm.{u_2} (E := N) ((lift S f.toAddMonoidHom hf : (a : M ⧸ S) → N) (↑x : M ⧸ S) : N) / ‖f‖
⊢ False

Tactic:
exact ((lt_div_iff₀' h).1 hx).not_ge (le_opNorm f x)

Premises used: lt_div_iff₀', NormedAddGroupHom.le_opNorm, Iff.mp, LT.lt.not_ge
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
x : M ⧸ S
⊢ ‖f‖ = 0 ∨ 0 < ‖f‖

Tactic:
cases (norm_nonneg f).eq_or_lt' with
  | inl h =>
    rcases mk_surjective x with ⟨x, rfl⟩
    simpa [h] using le_opNorm f x
  | inr h =>
    rw [← not_lt, ← lt_div_iff₀' h, norm_lt_iff]
    rintro ⟨x, rfl, hx⟩
    exact ((lt_div_iff₀' h).1 hx).not_ge (le_opNorm f x)

Premises used: QuotientAddGroup.mk_surjective, QuotientAddGroup.norm_lt_iff, not_lt, LE.le.eq_or_lt', norm_nonneg, rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) ≠ univ
⊢ ‖S.normedMk‖ = 1

Tactic:
le_antisymm (norm_normedMk_le S) ?_

Premises used: AddSubgroup.norm_normedMk_le, le_antisymm
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) ≠ univ
refine : 1 ≤ ‖S.normedMk‖
⊢ ‖S.normedMk‖ = 1

Tactic:
refine le_antisymm (norm_normedMk_le S) ?_

Premises used: AddSubgroup.norm_normedMk_le, le_antisymm
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) ≠ univ
⊢ ∃ (x : M), 0 < norm (E := M ⧸ S) (↑x : M ⧸ S)

Tactic:
(Set.nonempty_compl.2 h).imp fun x hx ↦ ?_

Premises used: Iff.mpr, Exists.imp, Set.nonempty_compl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) ≠ univ
refine : ∀ (x : M) (hx : x ∈ (↑S.topologicalClosure : Set M)ᶜ), 0 < norm (E := M ⧸ S) (↑x : M ⧸ S)
⊢ ∃ (x : M), 0 < norm (E := M ⧸ S) (↑x : M ⧸ S)

Tactic:
refine (Set.nonempty_compl.2 h).imp fun x hx ↦ ?_

Premises used: Iff.mpr, Exists.imp, Set.nonempty_compl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) ≠ univ
x : M
hx : x ∈ (↑S.topologicalClosure : Set M)ᶜ
⊢ 0 < norm (E := M ⧸ S) (↑x : M ⧸ S)

Tactic:
(norm_nonneg _).lt_of_ne' <| mt norm_mk_eq_zero_iff_mem_closure.1 hx

Premises used: QuotientAddGroup.norm_mk_eq_zero_iff_mem_closure, mt, Iff.mp, norm_nonneg, LE.le.lt_of_ne'
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) ≠ univ
x : M
hx : x ∈ (↑S.topologicalClosure : Set M)ᶜ
⊢ 0 < norm (E := M ⧸ S) (↑x : M ⧸ S)

Tactic:
exact (norm_nonneg _).lt_of_ne' <| mt norm_mk_eq_zero_iff_mem_closure.1 hx

Premises used: QuotientAddGroup.norm_mk_eq_zero_iff_mem_closure, mt, Iff.mp, norm_nonneg, LE.le.lt_of_ne'
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) ≠ univ
obtain : ∀ (x : M) (hx : 0 < norm (E := M ⧸ S) (↑x : M ⧸ S)), 1 ≤ ‖S.normedMk‖
⊢ 1 ≤ ‖S.normedMk‖

Tactic:
obtain ⟨x, hx⟩ : ∃ x : M, 0 < ‖(x : M ⧸ S)‖ := by
    refine (Set.nonempty_compl.2 h).imp fun x hx ↦ ?_
    exact (norm_nonneg _).lt_of_ne' <| mt norm_mk_eq_zero_iff_mem_closure.1 hx
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) ≠ univ
x : M
hx : 0 < norm (E := M ⧸ S) (↑x : M ⧸ S)
⊢ 1 ≤ ‖S.normedMk‖

Tactic:
(le_mul_iff_one_le_left hx).1 ?_

Premises used: le_mul_iff_one_le_left, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) ≠ univ
x : M
hx : 0 < norm (E := M ⧸ S) (↑x : M ⧸ S)
refine : norm (E := M ⧸ S) (↑x : M ⧸ S) ≤ ‖S.normedMk‖ * norm (E := M ⧸ S) (↑x : M ⧸ S)
⊢ 1 ≤ ‖S.normedMk‖

Tactic:
refine (le_mul_iff_one_le_left hx).1 ?_

Premises used: le_mul_iff_one_le_left, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) ≠ univ
x : M
hx : 0 < norm (E := M ⧸ S) (↑x : M ⧸ S)
⊢ norm (E := M ⧸ S) (↑x : M ⧸ S) ≤ ‖S.normedMk‖ * norm (E := M ⧸ S) (↑x : M ⧸ S)

Tactic:
norm_lift_apply_le S.normedMk (fun x ↦ (eq_zero_iff x).2) x

Premises used: Iff.mpr, Quotient.liftOn', AddCon.liftOn, AddSubgroup.normedMk, setOf, QuotientAddGroup.mk, QuotientAddGroup.norm_lift_apply_le, QuotientAddGroup.eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) ≠ univ
x : M
hx : 0 < norm (E := M ⧸ S) (↑x : M ⧸ S)
⊢ norm (E := M ⧸ S) (↑x : M ⧸ S) ≤ ‖S.normedMk‖ * norm (E := M ⧸ S) (↑x : M ⧸ S)

Tactic:
exact norm_lift_apply_le S.normedMk (fun x ↦ (eq_zero_iff x).2) x

Premises used: Iff.mpr, AddSubgroup.normedMk, QuotientAddGroup.mk, QuotientAddGroup.norm_lift_apply_le, QuotientAddGroup.eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) = univ
⊢ ‖S.normedMk‖ = 0

Tactic:
le_antisymm (opNorm_le_bound _ le_rfl fun x => ?_) (norm_nonneg _)

Premises used: le_rfl, NormedAddGroupHom.opNorm_le_bound, le_antisymm, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) = univ
refine : ∀ (x : M), norm (E := M ⧸ S) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) ≤ 0 * ‖x‖
⊢ ‖S.normedMk‖ = 0

Tactic:
refine le_antisymm (opNorm_le_bound _ le_rfl fun x => ?_) (norm_nonneg _)

Premises used: le_rfl, NormedAddGroupHom.opNorm_le_bound, le_antisymm, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) = univ
x : M
rw : Membership.mem (γ := Set M) univ x
⊢ x ∈ S.normedMk.ker.topologicalClosure

Tactic:
rw [S.ker_normedMk, ← SetLike.mem_coe, h]

Premises used: SetLike.mem_coe, AddSubgroup.ker_normedMk
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) = univ
x : M
⊢ Membership.mem (γ := Set M) univ x

Tactic:
trivial
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) = univ
x : M
⊢ x ∈ S.normedMk.ker.topologicalClosure

Tactic:
have hker : x ∈ S.normedMk.ker.topologicalClosure := by
    rw [S.ker_normedMk, ← SetLike.mem_coe, h]
    trivial
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) = univ
x : M
hker : x ∈ S.normedMk.ker.topologicalClosure
⊢ x ∈ S.topologicalClosure

Tactic:
rw [ker_normedMk] at hker

Premises used: AddSubgroup.ker_normedMk
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) = univ
x : M
hker : x ∈ S.topologicalClosure
⊢ norm (E := M ⧸ S) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) ≤ 0 * ‖x‖

Tactic:
simp [norm_mk_eq_zero_iff_mem_closure.mpr hker]

Premises used: Iff.mpr, QuotientAddGroup.norm_mk_eq_zero_iff_mem_closure
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
N : Type u_3
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) s : N) (0 : N)
m : M
⊢ Eq.{u_3 + 1} (α := N) ((lift S f hf : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) m : M ⧸ S) : N)
    ((f : (a : M) → N) m : N)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
N : Type u_3
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) s : N) (0 : N)
g : NormedAddGroupHom.{u_1, u_3} (M ⧸ S) N
h : g.comp S.normedMk = f
H : ∀ (x : M ⧸ S), Eq.{u_3 + 1} (α := N) ((g : (a : M ⧸ S) → N) x : N) ((lift S f hf : (a : M ⧸ S) → N) x : N)
⊢ g = lift S f hf

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
N : Type u_3
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) s : N) (0 : N)
g : NormedAddGroupHom.{u_1, u_3} (M ⧸ S) N
h : g.comp S.normedMk = f
x : M ⧸ S
H :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := N) ((g : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) : N)
      ((lift S f hf : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) : N)
⊢ Eq.{u_3 + 1} (α := N) ((g : (a : M ⧸ S) → N) x : N) ((lift S f hf : (a : M ⧸ S) → N) x : N)

Tactic:
rcases AddSubgroup.surjective_normedMk _ x with ⟨x, rfl⟩

Premises used: AddSubgroup.surjective_normedMk, rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
N : Type u_3
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) s : N) (0 : N)
g : NormedAddGroupHom.{u_1, u_3} (M ⧸ S) N
h : g.comp S.normedMk = f
x : M
H :
  Eq.{u_3 + 1} (α := N) ((g.comp S.normedMk : (a : M) → N) x : N)
    ((lift S f hf : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) : N)
⊢ Eq.{u_3 + 1} (α := N) ((g : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) : N)
    ((lift S f hf : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) : N)

Tactic:
change g.comp S.normedMk x = _

Premises used: AddSubgroup.normedMk, NormedAddGroupHom.comp, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
N : Type u_3
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) s : N) (0 : N)
g : NormedAddGroupHom.{u_1, u_3} (M ⧸ S) N
h : g.comp S.normedMk = f
x : M
H :
  Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N)
    ((lift S f hf : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) : N)
⊢ Eq.{u_3 + 1} (α := N) ((g.comp S.normedMk : (a : M) → N) x : N)
    ((lift S f hf : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) : N)

Tactic:
simp only [h]
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
N : Type u_3
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) s : N) (0 : N)
g : NormedAddGroupHom.{u_1, u_3} (M ⧸ S) N
h : g.comp S.normedMk = f
x : M
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N)
    ((lift S f hf : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) : N)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ norm (E := M ⧸ S) ((S.normedMk : (a : M) → M ⧸ S) m : M ⧸ S) =
    sInf ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑S.normedMk.ker : Set M))

Tactic:
simpa [S.ker_normedMk] using quotient_norm_mk_eq _ m

Premises used: quotient_norm_mk_eq, AddSubgroup.ker_normedMk
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
n : N
obtain :
  ∀ (m : M),
    ∃ (m_1 : M),
      Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m_1 : N) ((f : (a : M) → N) m : N) ∧
        ‖m_1‖ < norm.{u_2} (E := N) ((f : (a : M) → N) m : N) + ε
⊢ ∃ (m : M), (f : (a : M) → N) m = n ∧ ‖m‖ < ‖n‖ + ε

Tactic:
obtain ⟨m, rfl⟩ := hquot.surjective n

Premises used: NormedAddGroupHom.IsQuotient.surjective, rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
rw : (↑f.ker : Set M).Nonempty
⊢ Set.Nonempty (α := ℝ) ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M))

Tactic:
rw [Set.image_nonempty]

Premises used: Set.image_nonempty
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ (↑f.ker : Set M).Nonempty

Tactic:
⟨0, f.ker.zero_mem⟩

Premises used: Set.Nonempty, Exists.intro, OfNat.ofNat, NormedAddGroupHom.ker, AddSubgroup.zero_mem
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ (↑f.ker : Set M).Nonempty

Tactic:
exact ⟨0, f.ker.zero_mem⟩
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ Set.Nonempty (α := ℝ) ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M))

Tactic:
have nonemp : ((fun m' => ‖m + m'‖) '' f.ker).Nonempty := by
    rw [Set.image_nonempty]
    exact ⟨0, f.ker.zero_mem⟩
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty (α := ℝ) ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M))
rcases :
  ∀ (x : M) (hx : x ∈ (↑f.ker : Set M)) (H : ‖m + x‖ < sInf ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M)) + ε),
    ∃ (m_1 : M),
      Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m_1 : N) ((f : (a : M) → N) m : N) ∧
        ‖m_1‖ < norm.{u_2} (E := N) ((f : (a : M) → N) m : N) + ε
⊢ ∃ (m_1 : M),
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m_1 : N) ((f : (a : M) → N) m : N) ∧
      ‖m_1‖ < norm.{u_2} (E := N) ((f : (a : M) → N) m : N) + ε

Tactic:
rcases Real.lt_sInf_add_pos nonemp hε
    with ⟨_, ⟨⟨x, hx, rfl⟩, H : ‖m + x‖ < sInf ((fun m' : M => ‖m + m'‖) '' f.ker) + ε⟩⟩

Premises used: Norm.norm, SetLike.coe, HAdd.hAdd, Set.image, NormedAddGroupHom.ker, InfSet.sInf, rfl, Real.lt_sInf_add_pos
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty (α := ℝ) ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M))
x : M
hx : x ∈ (↑f.ker : Set M)
H : ‖m + x‖ < sInf ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M)) + ε
rw : HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) m : N) ((f : (a : M) → N) x : N) = (f : (a : M) → N) m
rw₁ : HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) m : N) (0 : N) = (f : (a : M) → N) m
rw₂ rw₃ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m : N) ((f : (a : M) → N) m : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (m + x) : N) ((f : (a : M) → N) m : N)

Tactic:
rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero]

Premises used: NormedAddGroupHom.mem_ker, map_add, Iff.mp, add_zero
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty (α := ℝ) ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M))
x : M
hx : x ∈ (↑f.ker : Set M)
H rwa rwa₁ rwa₂ rwa₃ : ‖m + x‖ < sInf ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M)) + ε
⊢ ‖m + x‖ < norm.{u_2} (E := N) ((f : (a : M) → N) m : N) + ε

Tactic:
rwa [hquot.norm]

Premises used: NormedAddGroupHom.IsQuotient.norm
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty (α := ℝ) ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M))
x : M
hx : x ∈ (↑f.ker : Set M)
H : ‖m + x‖ < sInf ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M)) + ε
⊢ ∃ (m_1 : M),
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m_1 : N) ((f : (a : M) → N) m : N) ∧
      ‖m_1‖ < norm.{u_2} (E := N) ((f : (a : M) → N) m : N) + ε

Tactic:
exact ⟨m + x, by rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero], by
    rwa [hquot.norm]⟩
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
rw : sInf ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M)) ≤ ‖m‖
⊢ norm.{u_2} (E := N) ((f : (a : M) → N) m : N) ≤ ‖m‖

Tactic:
rw [hquot.norm]

Premises used: NormedAddGroupHom.IsQuotient.norm
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
h₁ : BddBelow (α := ℝ) ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M))
h₂ : Membership.mem (γ := Set ℝ) ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M)) ‖m‖
⊢ sInf ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M)) ≤ ‖m‖

Tactic:
apply csInf_le

Premises used: csInf_le
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
h : Membership.mem (γ := Set ℝ) (lowerBounds ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M))) 0
⊢ BddBelow (α := ℝ) ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M))

Tactic:
use 0
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m m' : M
⊢ LE.le (α := ℝ) 0 ((fun (m_1 : M) ↦ ‖m + m_1‖) m')

Tactic:
apply norm_nonneg

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ (fun (m_1 : M) ↦ ‖m + m_1‖) 0 = ‖m‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ Membership.mem (γ := Set ℝ) ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M)) ‖m‖

Tactic:
exact ⟨0, f.ker.zero_mem, by simp⟩
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
N : Type u_3
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) s : N) (0 : N)
⊢ ‖lift S f hf‖ ≤ ‖f‖

Tactic:
opNorm_le_bound _ (norm_nonneg f) (norm_lift_apply_le f hf)

Premises used: NormedAddGroupHom.opNorm_le_bound, QuotientAddGroup.norm_lift_apply_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
N : Type u_3
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) s : N) (0 : N)
c : ℝ≥0
fb : ‖f‖ ≤ (↑c : ℝ)
⊢ ‖lift S f hf‖ ≤ (↑c : ℝ)

Tactic:
(norm_lift_le S f hf).trans fb

Premises used: NormedAddGroupHom.norm_lift_le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
N : Type u_3
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) s : N) (0 : N)
fb : f.NormNoninc
x : M ⧸ S
⊢ ‖f‖ ≤ (↑1 : ℝ)

Tactic:
have fb' : ‖f‖ ≤ (1 : ℝ≥0) := NormNoninc.normNoninc_iff_norm_le_one.mp fb