awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
x_1 : R
⊢ ((↑x : R) + x_1)⁻¹ʳ - (↑x⁻¹ : R) + (↑x⁻¹ : R) * x_1 * (↑x⁻¹ : R) =
    ((↑x : R) + x_1)⁻¹ʳ - (∑ i ∈ range 2, (-(↑x⁻¹ : R) * x_1) ^ i) * (↑x⁻¹ : R)

Tactic:
simp only [sum_range_succ, sum_range_zero, zero_add, pow_zero, pow_one, add_mul, one_mul,
    ← sub_sub, neg_mul, sub_neg_eq_add]

Premises used: add_mul, Finset.sum_range_zero, zero_add, pow_zero, sub_sub, pow_one, neg_mul, Finset.sum_range_succ, one_mul, sub_neg_eq_add
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
⊢ IsLittleO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R)) fun (x : R) ↦ 1

Tactic:
have h_is_o : (fun t : R => (↑x + t)⁻¹ʳ - ↑x⁻¹) =o[𝓝 0] (fun _ => 1 : R → ℝ) :=
    (inverse_add_norm_diff_first_order x).trans_isLittleO (isLittleO_id_const one_ne_zero).norm_left
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h_is_o : IsLittleO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R)) fun (x : R) ↦ 1
⊢ Tendsto (β := R) (fun (y : R) ↦ y - (↑x : R)) (𝓝 (↑x : R)) (𝓝 0)

Tactic:
tendsto_zero_iff_norm_tendsto_zero.mpr ?_

Premises used: Iff.mpr, tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h_is_o : IsLittleO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R)) fun (x : R) ↦ 1
refine : Tendsto (β := ℝ) (fun (x_1 : R) ↦ ‖x_1 - (↑x : R)‖) (𝓝 (↑x : R)) (𝓝 0)
⊢ Tendsto (β := R) (fun (y : R) ↦ y - (↑x : R)) (𝓝 (↑x : R)) (𝓝 0)

Tactic:
refine tendsto_zero_iff_norm_tendsto_zero.mpr ?_

Premises used: Iff.mpr, tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h_is_o : IsLittleO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R)) fun (x : R) ↦ 1
⊢ Tendsto (β := ℝ) (fun (x_1 : R) ↦ ‖x_1 - (↑x : R)‖) (𝓝 (↑x : R)) (𝓝 0)

Tactic:
tendsto_iff_norm_sub_tendsto_zero.mp tendsto_id

Premises used: Filter.tendsto_id, Iff.mp, tendsto_iff_norm_sub_tendsto_zero
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h_is_o : IsLittleO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R)) fun (x : R) ↦ 1
⊢ Tendsto (β := ℝ) (fun (x_1 : R) ↦ ‖x_1 - (↑x : R)‖) (𝓝 (↑x : R)) (𝓝 0)

Tactic:
exact tendsto_iff_norm_sub_tendsto_zero.mp tendsto_id

Premises used: Filter.tendsto_id, Iff.mp, tendsto_iff_norm_sub_tendsto_zero
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h_is_o : IsLittleO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R)) fun (x : R) ↦ 1
⊢ Tendsto (β := R) (fun (y : R) ↦ y - (↑x : R)) (𝓝 (↑x : R)) (𝓝 0)

Tactic:
have h_lim : Tendsto (fun y : R => y - x) (𝓝 x) (𝓝 0) := by
    refine tendsto_zero_iff_norm_tendsto_zero.mpr ?_
    exact tendsto_iff_norm_sub_tendsto_zero.mp tendsto_id
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h_is_o : IsLittleO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R)) fun (x : R) ↦ 1
h_lim : Tendsto (β := R) (fun (y : R) ↦ y - (↑x : R)) (𝓝 (↑x : R)) (𝓝 0)
rw : Tendsto (β := ℝ) (fun (e : R) ↦ ‖e⁻¹ʳ - (↑x⁻¹ : R)‖) (𝓝 (↑x : R)) (𝓝 0)
⊢ ContinuousAt inverse (↑x : R)

Tactic:
rw [ContinuousAt, tendsto_iff_norm_sub_tendsto_zero, inverse_unit]

Premises used: ContinuousAt, Ring.inverse_unit, tendsto_iff_norm_sub_tendsto_zero
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h_is_o : IsLittleO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R)) fun (x : R) ↦ 1
h_lim : Tendsto (β := R) (fun (y : R) ↦ y - (↑x : R)) (𝓝 (↑x : R)) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (e : R) ↦ ‖e⁻¹ʳ - (↑x⁻¹ : R)‖) (𝓝 (↑x : R)) (𝓝 0)

Tactic:
simpa [Function.comp_def] using h_is_o.norm_left.tendsto_div_nhds_zero.comp h_lim

Premises used: Asymptotics.IsLittleO.tendsto_div_nhds_zero, Function.comp_def, Asymptotics.IsLittleO.norm_left, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
⊢ IsOpenMap.{u_1, u_1} (X := Rˣ) val

Tactic:
isOpenEmbedding_val.isOpenMap

Premises used: Topology.IsOpenEmbedding.isOpenMap, Units.isOpenEmbedding_val
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
I : Ideal R
x : R
hxI : x ∈ I
hx : ‖1 - x‖ < 1
u : Rˣ := Units.oneSub (1 - x) hx
⊢ u.inv * x = 1

Tactic:
simp [u]
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
I : Ideal R
x : R
hxI : x ∈ I
hx : ‖1 - x‖ < 1
u : Rˣ := Units.oneSub (1 - x) hx
⊢ 1 ∈ I

Tactic:
simpa only [show u.inv * x = 1 by simp [u]] using I.mul_mem_left u.inv hxI

Premises used: Ideal.mul_mem_left, Units.inv
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
I : Ideal R
hI : I ≠ ⊤
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I : Set R) ⊆ nonunits R

Tactic:
have h := closure_minimal (coe_subset_nonunits hI) nonunits.isClosed
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
I : Ideal R
hI : I ≠ ⊤
h : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I : Set R) ⊆ nonunits R
⊢ I.closure ≠ ⊤

Tactic:
simpa only [I.closure.eq_top_iff_one, Ne] using mt (@h 1) one_notMem_nonunits

Premises used: mt, Ideal.closure, Ne, Ideal.eq_top_iff_one, one_notMem_nonunits
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
I : Ideal R
hI : I.IsMaximal
⊢ I.closure = I

Tactic:
(hI.eq_of_le (I.closure_ne_top hI.ne_top) subset_closure).symm

Premises used: subset_closure, Ideal.IsMaximal.eq_of_le, Ideal.IsMaximal.ne_top, Eq.symm, Ideal.closure_ne_top
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
I : Ideal R
hI : I.IsMaximal
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I : Set R)

Tactic:
isClosed_of_closure_subset <| Eq.subset <| congr_arg ((↑) : Ideal R → Set R) hI.closure_eq

Premises used: congr_arg, Eq.subset, SetLike.coe, isClosed_of_closure_subset, Ideal.IsMaximal.closure_eq
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
x : R
⊢ (toAbs v x).ofAbs = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
x : WithAbs v
⊢ toAbs v x.ofAbs = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := WithAbs v) ofAbs

Tactic:
Function.RightInverse.surjective <| ofAbs_toAbs _

Premises used: WithAbs.ofAbs_toAbs, Function.RightInverse.surjective
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
⊢ Function.Surjective (toAbs v)

Tactic:
Function.RightInverse.surjective <| toAbs_ofAbs _

Premises used: WithAbs.toAbs_ofAbs, Function.RightInverse.surjective
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := WithAbs v) ofAbs

Tactic:
Function.LeftInverse.injective <| toAbs_ofAbs _

Premises used: Function.LeftInverse.injective, WithAbs.toAbs_ofAbs
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
⊢ Function.Injective (toAbs v)

Tactic:
Function.LeftInverse.injective <| ofAbs_toAbs _

Premises used: Function.LeftInverse.injective, WithAbs.ofAbs_toAbs
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := WithAbs v) ofAbs

Tactic:
⟨ofAbs_injective v, ofAbs_surjective v⟩

Premises used: WithAbs.ofAbs_surjective, And.intro, Function.Bijective, WithAbs.ofAbs_injective
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
⊢ Function.Bijective (toAbs v)

Tactic:
⟨toAbs_injective v, toAbs_surjective v⟩

Premises used: WithAbs.toAbs_surjective, WithAbs.toAbs_injective, And.intro, Function.Bijective
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
⊢ toAbs v 0 = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
⊢ Eq.{u_1 + 1} (α := R) (ofAbs.{u_1, u_2} (S := S) (v := v) 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
⊢ toAbs v 1 = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
⊢ Eq.{u_1 + 1} (α := R) (ofAbs.{u_1, u_2} (S := S) (v := v) 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
x y : R
⊢ toAbs v (x + y) = toAbs v x + toAbs v y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
x y : WithAbs v
⊢ (x + y).ofAbs = x.ofAbs + y.ofAbs

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
x y : R
⊢ toAbs v (x * y) = toAbs v x * toAbs v y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
x y : WithAbs v
⊢ (x * y).ofAbs = x.ofAbs * y.ofAbs

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
x : R
⊢ toAbs v x = 0 ↔ x = 0

Tactic:
(toAbs_injective v).eq_iff

Premises used: Function.Injective.eq_iff, WithAbs.toAbs_injective
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
x : WithAbs v
⊢ x.ofAbs = 0 ↔ x = 0

Tactic:
(ofAbs_injective v).eq_iff

Premises used: Function.Injective.eq_iff, WithAbs.ofAbs_injective
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
x : R
n : ℕ
⊢ toAbs v (x ^ n) = toAbs v x ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
x : WithAbs v
n : ℕ
⊢ (x ^ n).ofAbs = x.ofAbs ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
inst_3 : Nontrivial R
⊢ Nontrivial.{u_1} (WithAbs v)

Tactic:
(equiv v).nontrivial

Premises used: RingEquiv.toEquiv, Equiv.nontrivial, WithAbs.equiv
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
⊢ map v v (RingHom.id R) = RingHom.id (WithAbs v)

Tactic:
rfl

Premises used: WithAbs.map, rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
T : Type u_3
U : Type u_4
inst_3 : Semiring T
inst_4 : Semiring U
w : AbsoluteValue T S
u : AbsoluteValue U S
f : R →+* T
g : T →+* U
⊢ map v u (g.comp f) = (map w u g).comp (map v w f)

Tactic:
rfl

Premises used: WithAbs.map, MulEquiv.toMonoidHom, RingEquiv.toRingHom, rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
T : Type u_3
inst_3 : Semiring T
w : AbsoluteValue T S
f : R →+* T
x : WithAbs v
⊢ (map v w f : (a : WithAbs v) → WithAbs w) x = toAbs w ((f : (a : R) → T) x.ofAbs)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
T : Type u_3
U : Type u_4
inst_3 : Semiring T
inst_4 : Semiring U
w : AbsoluteValue T S
u : AbsoluteValue U S
f_1 : R →+* T
g_1 : T →+* U
f : R ≃+* T
g : T ≃+* U
x : WithAbs v
⊢ (map w v f.symm.toRingHom : (a : WithAbs w) → WithAbs v)
      ((↑(↑(map v w f.toRingHom) : WithAbs v →* WithAbs w) : OneHom (WithAbs v) (WithAbs w)).toFun x) =
    x

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
T : Type u_3
U : Type u_4
inst_3 : Semiring T
inst_4 : Semiring U
w : AbsoluteValue T S
u : AbsoluteValue U S
f_1 : R →+* T
g_1 : T →+* U
f : R ≃+* T
g : T ≃+* U
x : WithAbs w
⊢ (↑(↑(map v w f.toRingHom) : WithAbs v →* WithAbs w) : OneHom (WithAbs v) (WithAbs w)).toFun
      ((map w v f.symm.toRingHom : (a : WithAbs w) → WithAbs v) x) =
    x

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
⊢ congr v v (RingEquiv.refl R) = RingEquiv.refl (WithAbs v)

Tactic:
rfl

Premises used: RingEquiv.refl, WithAbs.congr, Equiv.refl, rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
T : Type u_3
U : Type u_4
inst_3 : Semiring T
inst_4 : Semiring U
w : AbsoluteValue T S
u : AbsoluteValue U S
f : R ≃+* T
g : T ≃+* U
⊢ congr v u (f.trans g) = (congr v w f).trans (congr w u g)

Tactic:
rfl

Premises used: Equiv.trans, RingEquiv.trans, WithAbs.congr, rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
T : Type u_3
inst_3 : Semiring T
w : AbsoluteValue T S
f : R ≃+* T
⊢ (congr v w f).symm = congr w v f.symm

Tactic:
rfl

Premises used: WithAbs.congr, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
T : Type u_3
inst_3 : Semiring T
w : AbsoluteValue T S
f : R ≃+* T
x : WithAbs v
⊢ (congr v w f : (a : WithAbs v) → WithAbs w) x = toAbs w ((f : (a : R) → T) x.ofAbs)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v : AbsoluteValue R S
T : Type u_3
inst_3 : Semiring T
w : AbsoluteValue T S
f : R ≃+* T
x : WithAbs w
⊢ ((congr v w f).symm : (a : WithAbs w) → WithAbs v) x = toAbs v ((f.symm : (a : T) → R) x.ofAbs)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v w : AbsoluteValue R S
⊢ (congr v w (RingEquiv.refl R)).symm = congr w v (RingEquiv.symm (RingEquiv.refl R))

Tactic:
congr_symm _ _ _

Premises used: WithAbs.congr_symm
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v w : AbsoluteValue R S
x : WithAbs w
⊢ Eq (α := R)
    ((equiv v : (a : WithAbs v) → R)
        (((congr v w (RingEquiv.refl R)).symm : (a : WithAbs w) → WithAbs v) x : WithAbs v) :
      R)
    ((equiv w : (a : WithAbs w) → R) x : R)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v w : AbsoluteValue R S
x : R
⊢ Eq (α := WithAbs w)
    ((congr v w (RingEquiv.refl R) : (a : WithAbs v) → WithAbs w)
        (((equiv v).symm : (a : R) → WithAbs v) x : WithAbs v) :
      WithAbs w)
    (((equiv w).symm : (a : R) → WithAbs w) x : WithAbs w)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Semiring R
v w : AbsoluteValue R S
x : R
⊢ Eq (α := WithAbs v)
    (((congr v w (RingEquiv.refl R)).symm : (a : WithAbs w) → WithAbs v)
        (((equiv w).symm : (a : R) → WithAbs w) x : WithAbs w) :
      WithAbs v)
    (((equiv v).symm : (a : R) → WithAbs v) x : WithAbs v)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
inst : Ring R
v : AbsoluteValue R ℝ
x : WithAbs v
⊢ ‖x‖ = (v : (a : R) → ℝ) x.ofAbs

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
inst : Ring R
v : AbsoluteValue R ℝ
x : R
⊢ ‖toAbs v x‖ = (v : (a : R) → ℝ) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Ring R
v : AbsoluteValue R S
x y : R
⊢ toAbs v (x - y) = toAbs v x - toAbs v y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Ring R
v : AbsoluteValue R S
x y : WithAbs v
⊢ (x - y).ofAbs = x.ofAbs - y.ofAbs

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Ring R
v : AbsoluteValue R S
x : R
⊢ toAbs v (-x) = -toAbs v x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Ring R
v : AbsoluteValue R S
x : WithAbs v
⊢ (-x).ofAbs = -x.ofAbs

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : Semiring R
v : AbsoluteValue R S
inst_3 : SMul R T
x : WithAbs v
t : T
⊢ x • t = x.ofAbs • t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : Semiring R
v : AbsoluteValue R S
inst_3 : SMul T R
t : T
x : WithAbs v
⊢ t • x = toAbs v (t • x.ofAbs)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R_1 : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : Semiring R
v : AbsoluteValue R S
inst_3 : SMul T R
inst_4 : FaithfulSMul T R
m₁ m₂ : T
h : ∀ (a : WithAbs v), m₁ • a = m₂ • a
⊢ ∀ (a : WithAbs v), m₁ • a.ofAbs = m₂ • a.ofAbs

Tactic:
simp only [smul_right_def, toAbs.injEq] at h

Premises used: WithAbs.toAbs.injEq, WithAbs.smul_right_def
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R_1 : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : Semiring R
v : AbsoluteValue R S
inst_3 : SMul T R
inst_4 : FaithfulSMul T R
m₁ m₂ : T
h : ∀ (a : WithAbs v), m₁ • a.ofAbs = m₂ • a.ofAbs
⊢ m₁ = m₂

Tactic:
FaithfulSMul.eq_of_smul_eq_smul fun _ ↦ h (toAbs v _)

Premises used: FaithfulSMul.eq_of_smul_eq_smul, WithAbs.toAbs
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R_1 : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : Semiring R
v : AbsoluteValue R S
inst_3 : SMul T R
inst_4 : FaithfulSMul T R
m₁ m₂ : T
h : ∀ (a : WithAbs v), m₁ • a.ofAbs = m₂ • a.ofAbs
⊢ m₁ = m₂

Tactic:
exact FaithfulSMul.eq_of_smul_eq_smul fun _ ↦ h (toAbs v _)

Premises used: FaithfulSMul.eq_of_smul_eq_smul, WithAbs.toAbs
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R_1 : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : Semiring R
v : AbsoluteValue R S
P : Type u_5
inst_3 : SMul T P
inst_4 : SMul R T
inst_5 : SMul R P
inst_6 : IsScalarTower R T P
⊢ ∀ (x : WithAbs v) (y : T) (z : P), (x • y) • z = x • y • z

Tactic:
simp [smul_left_def]

Premises used: WithAbs.smul_left_def
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R_1 : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : Semiring R
v : AbsoluteValue R S
P : Type u_5
inst_3 : SMul P R
inst_4 : SMul T R
inst_5 : SMul P T
inst_6 : IsScalarTower P T R
⊢ IsScalarTower.{u_5, u_4, u_3} P T (WithAbs v)

Tactic:
(equiv v).isScalarTower P T

Premises used: RingEquiv.toEquiv, WithAbs.equiv, Equiv.isScalarTower
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
R_1 : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : Semiring R
v : AbsoluteValue R S
P : Type u_5
inst_3 : SMul P R
inst_4 : SMul P T
inst_5 : SMul R T
inst_6 : IsScalarTower P R T
⊢ ∀ (x : P) (y : WithAbs v) (z : T), (x • y) • z = x • y • z

Tactic:
simp [smul_right_def, smul_left_def]

Premises used: WithAbs.smul_left_def, WithAbs.smul_right_def
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : Semiring R
inst_3 : Semiring T
inst_4 : Module R T
v : AbsoluteValue T S
x : WithAbs v
⊢ (linearEquiv R v : (a : WithAbs v) → T) x = x.ofAbs

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : Semiring R
inst_3 : Semiring T
inst_4 : Module R T
v : AbsoluteValue T S
x : T
⊢ (LinearEquiv.symm (linearEquiv R v) : (a : T) → WithAbs v) x = toAbs v x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : CommSemiring R
inst_3 : Semiring T
inst_4 : Algebra R T
v : AbsoluteValue R S
x : WithAbs v
⊢ Eq.{u_4 + 1} (α := T) ((algebraMap (WithAbs v) T : (a : WithAbs v) → T) x : T)
    ((algebraMap R T : (a : R) → T) x.ofAbs : T)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : CommSemiring R
inst_3 : Semiring T
inst_4 : Algebra R T
v : AbsoluteValue R S
h : Function.Injective.{u_3 + 1, u_4 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
⊢ Function.Injective.{u_3 + 1, u_4 + 1} (α := WithAbs v) (β := T) (⇑(algebraMap (WithAbs v) T) : (a : WithAbs v) → T)

Tactic:
h.comp (ofAbs_injective v)

Premises used: Function.Injective.comp, WithAbs.ofAbs_injective