awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul G G
inst_3 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
rw : edist (a * a⁻¹) (a * b⁻¹) = edist a b
rw₁ : edist (a * a⁻¹ * b) (a * b⁻¹ * b) = edist a b
rw₂ : edist (1 * b) (a * b⁻¹ * b) = edist a b
rw₃ : edist b (a * b⁻¹ * b) = edist a b
rw₄ : edist b a = edist a b
rw₅ rw₆ : edist a b = edist a b
⊢ edist a⁻¹ b⁻¹ = edist a b

Tactic:
rw [← edist_mul_left a, ← edist_mul_right _ _ b, mul_inv_cancel, one_mul, inv_mul_cancel_right,
    edist_comm]

Premises used: PseudoEMetricSpace.edist_comm, edist_mul_right, edist_mul_left, mul_inv_cancel, inv_mul_cancel_right, one_mul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul G G
inst_3 : IsIsometricSMul Gᵐᵒᵖ G
⊢ Isometry.{v, v} (α := G) Inv.inv

Tactic:
edist_inv_inv

Premises used: edist_inv_inv, Isometry
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul G G
inst_3 : IsIsometricSMul Gᵐᵒᵖ G
x y : G
rw : edist x⁻¹⁻¹ y⁻¹ = edist x y⁻¹
rw₁ rw₂ : edist x y⁻¹ = edist x y⁻¹
⊢ edist x⁻¹ y = edist x y⁻¹

Tactic:
rw [← edist_inv_inv, inv_inv]

Premises used: inv_inv, edist_inv_inv
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul G G
inst_3 : IsIsometricSMul Gᵐᵒᵖ G
a b c : G
rw : edist (a * b⁻¹) (a / c) = edist b c
rw₁ : edist (a * b⁻¹) (a * c⁻¹) = edist b c
rw₂ : edist b⁻¹ c⁻¹ = edist b c
rw₃ rw₄ : edist b c = edist b c
⊢ edist (a / b) (a / c) = edist b c

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, edist_mul_left, edist_inv_inv]

Premises used: div_eq_mul_inv, edist_mul_left, edist_inv_inv
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
X : Type w
inst : PseudoEMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
⊢ Eq.{w + 1} (α := X ≃ᵢ X) (IsometryEquiv.symm (constSMul c)) (constSMul c⁻¹)

Tactic:
ext fun _ => rfl

Premises used: IsometryEquiv.ext, rfl
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul G G
x : G
⊢ Eq (α := G ≃ᵢ G) (IsometryEquiv.symm (mulLeft x)) (mulLeft x⁻¹)

Tactic:
constSMul_symm x

Premises used: IsometryEquiv.mulLeft, IsometryEquiv.constSMul, Equiv.mulLeft, IsometryEquiv.constSMul_symm, Units.mulLeft
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
x : G
⊢ Eq (α := G ≃ᵢ G) (IsometryEquiv.symm (mulRight x)) (mulRight x⁻¹)

Tactic:
ext fun _ => rfl

Premises used: IsometryEquiv.ext, rfl
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
c : G
⊢ Eq (α := G ≃ᵢ G) (IsometryEquiv.symm (divRight c)) (mulRight c)

Tactic:
ext fun _ => rfl

Premises used: IsometryEquiv.ext, rfl
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul G G
inst_3 : IsIsometricSMul Gᵐᵒᵖ G
⊢ Eq (α := G ≃ᵢ G) (IsometryEquiv.symm (inv G)) (inv G)

Tactic:
rfl

Premises used: IsometryEquiv.inv, Equiv.inv, IsometryEquiv.symm, Function.Involutive.toPerm, Equiv.symm, rfl
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
X : Type w
inst : PseudoEMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ≥0∞
⊢ c • eball x r = eball (c • x) r

Tactic:
(IsometryEquiv.constSMul c).image_eball _ _

Premises used: IsometryEquiv.constSMul, IsometryEquiv.image_eball
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
X : Type w
inst : PseudoEMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ≥0∞
rw : c⁻¹ • eball x r = eball (c⁻¹ • x) r
rw₁ rw₂ : eball (c⁻¹ • x) r = eball (c⁻¹ • x) r
⊢ (fun (x : X) ↦ c • x) ⁻¹' eball x r = eball (c⁻¹ • x) r

Tactic:
rw [preimage_smul, smul_eball]

Premises used: Set.preimage_smul, Metric.smul_eball
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
X : Type w
inst : PseudoEMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ≥0∞
⊢ c • closedEBall x r = closedEBall (c • x) r

Tactic:
(IsometryEquiv.constSMul c).image_closedEBall _ _

Premises used: IsometryEquiv.constSMul, IsometryEquiv.image_closedEBall
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
X : Type w
inst : PseudoEMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ≥0∞
rw : c⁻¹ • closedEBall x r = closedEBall (c⁻¹ • x) r
rw₁ rw₂ : closedEBall (c⁻¹ • x) r = closedEBall (c⁻¹ • x) r
⊢ (fun (x : X) ↦ c • x) ⁻¹' closedEBall x r = closedEBall (c⁻¹ • x) r

Tactic:
rw [preimage_smul, smul_closedEBall]

Premises used: Metric.smul_closedEBall, Set.preimage_smul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul G G
a b : G
r : ℝ≥0∞
⊢ (fun (x : G) ↦ a * x) ⁻¹' eball b r = eball (a⁻¹ * b) r

Tactic:
preimage_smul_eball a b r

Premises used: Metric.preimage_smul_eball
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
rw : (fun (x : G) ↦ x * a) ⁻¹' eball b r = eball (b * a⁻¹) r
⊢ (fun (x : G) ↦ x * a) ⁻¹' eball b r = eball (b / a) r

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun (x : G) ↦ x * a) ⁻¹' eball b r = eball (b * a⁻¹) r

Tactic:
preimage_smul_eball (MulOpposite.op a) b r

Premises used: Metric.preimage_smul_eball, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun (x : G) ↦ x * a) ⁻¹' eball b r = eball (b * a⁻¹) r

Tactic:
exact preimage_smul_eball (MulOpposite.op a) b r

Premises used: Metric.preimage_smul_eball, MulOpposite.op
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul G G
a b : G
r : ℝ≥0∞
⊢ (fun (x : G) ↦ a * x) ⁻¹' closedEBall b r = closedEBall (a⁻¹ * b) r

Tactic:
preimage_smul_closedEBall a b r

Premises used: Metric.preimage_smul_closedEBall
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
rw : (fun (x : G) ↦ x * a) ⁻¹' closedEBall b r = closedEBall (b * a⁻¹) r
⊢ (fun (x : G) ↦ x * a) ⁻¹' closedEBall b r = closedEBall (b / a) r

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun (x : G) ↦ x * a) ⁻¹' closedEBall b r = closedEBall (b * a⁻¹) r

Tactic:
preimage_smul_closedEBall (MulOpposite.op a) b r

Premises used: Metric.preimage_smul_closedEBall, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun (x : G) ↦ x * a) ⁻¹' closedEBall b r = closedEBall (b * a⁻¹) r

Tactic:
exact preimage_smul_closedEBall (MulOpposite.op a) b r

Premises used: Metric.preimage_smul_closedEBall, MulOpposite.op
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
X : Type w
inst : PseudoMetricSpace X
inst_1 : SMul M X
inst_2 : IsIsometricSMul M X
c : M
x y : X
⊢ dist (c • x) (c • y) = dist x y

Tactic:
(isometry_smul X c).dist_eq x y

Premises used: Isometry.dist_eq, IsIsometricSMul.isometry_smul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
X : Type w
inst : PseudoMetricSpace X
inst_1 : SMul M X
inst_2 : IsIsometricSMul M X
c : M
x y : X
⊢ nndist (c • x) (c • y) = nndist x y

Tactic:
(isometry_smul X c).nndist_eq x y

Premises used: Isometry.nndist_eq, IsIsometricSMul.isometry_smul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
X : Type w
inst : PseudoMetricSpace X
inst_1 : SMul M X
inst_2 : IsIsometricSMul M X
c : M
s : Set X
⊢ Metric.diam (c • s) = Metric.diam s

Tactic:
(isometry_smul _ _).diam_image s

Premises used: Isometry.diam_image, IsIsometricSMul.isometry_smul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
inst : PseudoMetricSpace M
inst_1 : Mul M
inst_2 : IsIsometricSMul M M
a b c : M
⊢ dist (a * b) (a * c) = dist b c

Tactic:
dist_smul a b c

Premises used: dist_smul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
inst : PseudoMetricSpace M
inst_1 : Mul M
inst_2 : IsIsometricSMul M M
a b c : M
⊢ nndist (a * b) (a * c) = nndist b c

Tactic:
nndist_smul a b c

Premises used: nndist_smul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
inst : Mul M
inst_1 : PseudoMetricSpace M
inst_2 : IsIsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ dist (a * c) (b * c) = dist a b

Tactic:
dist_smul (MulOpposite.op c) a b

Premises used: dist_smul, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
inst : PseudoMetricSpace M
inst_1 : Mul M
inst_2 : IsIsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ nndist (a * c) (b * c) = nndist a b

Tactic:
nndist_smul (MulOpposite.op c) a b

Premises used: MulOpposite.unop, nndist_smul, MulOpposite.op
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
inst : DivInvMonoid M
inst_1 : PseudoMetricSpace M
inst_2 : IsIsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ dist (a / c) (b / c) = dist a b

Tactic:
simp only [div_eq_mul_inv, dist_mul_right]

Premises used: div_eq_mul_inv, dist_mul_right
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
inst : DivInvMonoid M
inst_1 : PseudoMetricSpace M
inst_2 : IsIsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ nndist (a / c) (b / c) = nndist a b

Tactic:
simp only [div_eq_mul_inv, nndist_mul_right]

Premises used: nndist_mul_right, div_eq_mul_inv
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoMetricSpace G
inst_2 : IsIsometricSMul G G
inst_3 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
⊢ dist a⁻¹ b⁻¹ = dist a b

Tactic:
(IsometryEquiv.inv G).dist_eq a b

Premises used: IsometryEquiv.inv, IsometryEquiv.dist_eq
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoMetricSpace G
inst_2 : IsIsometricSMul G G
inst_3 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
⊢ nndist a⁻¹ b⁻¹ = nndist a b

Tactic:
(IsometryEquiv.inv G).nndist_eq a b

Premises used: IsometryEquiv.inv, IsometryEquiv.nndist_eq
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoMetricSpace G
inst_2 : IsIsometricSMul G G
inst_3 : IsIsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ dist (a / b) (a / c) = dist b c

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoMetricSpace G
inst_2 : IsIsometricSMul G G
inst_3 : IsIsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ nndist (a / b) (a / c) = nndist b c

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
X : Type w
inst : PseudoMetricSpace X
inst_1 : SMul G X
inst_2 : IsIsometricSMul G X
s : Set X
hs : IsBounded s
c : G
⊢ IsBounded (c • s)

Tactic:
(isometry_smul X c).lipschitz.isBounded_image hs

Premises used: LipschitzWith.isBounded_image, Isometry.lipschitz, IsIsometricSMul.isometry_smul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
X : Type w
inst : PseudoMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ c • ball x r = ball (c • x) r

Tactic:
(IsometryEquiv.constSMul c).image_ball _ _

Premises used: IsometryEquiv.constSMul, IsometryEquiv.image_ball
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
X : Type w
inst : PseudoMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ
rw : c⁻¹ • ball x r = ball (c⁻¹ • x) r
rw₁ rw₂ : ball (c⁻¹ • x) r = ball (c⁻¹ • x) r
⊢ (fun (x : X) ↦ c • x) ⁻¹' ball x r = ball (c⁻¹ • x) r

Tactic:
rw [preimage_smul, smul_ball]

Premises used: Metric.smul_ball, Set.preimage_smul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
X : Type w
inst : PseudoMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ c • closedBall x r = closedBall (c • x) r

Tactic:
(IsometryEquiv.constSMul c).image_closedBall _ _

Premises used: IsometryEquiv.constSMul, IsometryEquiv.image_closedBall
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
X : Type w
inst : PseudoMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ
rw : c⁻¹ • closedBall x r = closedBall (c⁻¹ • x) r
rw₁ rw₂ : closedBall (c⁻¹ • x) r = closedBall (c⁻¹ • x) r
⊢ (fun (x : X) ↦ c • x) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r

Tactic:
rw [preimage_smul, smul_closedBall]

Premises used: Set.preimage_smul, Metric.smul_closedBall
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
X : Type w
inst : PseudoMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ c • sphere x r = sphere (c • x) r

Tactic:
(IsometryEquiv.constSMul c).image_sphere _ _

Premises used: IsometryEquiv.image_sphere, IsometryEquiv.constSMul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
X : Type w
inst : PseudoMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ
rw : c⁻¹ • sphere x r = sphere (c⁻¹ • x) r
rw₁ rw₂ : sphere (c⁻¹ • x) r = sphere (c⁻¹ • x) r
⊢ (fun (x : X) ↦ c • x) ⁻¹' sphere x r = sphere (c⁻¹ • x) r

Tactic:
rw [preimage_smul, smul_sphere]

Premises used: Metric.smul_sphere, Set.preimage_smul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoMetricSpace G
inst_2 : IsIsometricSMul G G
a b : G
r : ℝ
⊢ (fun (x : G) ↦ a * x) ⁻¹' ball b r = ball (a⁻¹ * b) r

Tactic:
preimage_smul_ball a b r

Premises used: Metric.preimage_smul_ball
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
rw : (fun (x : G) ↦ x * a) ⁻¹' ball b r = ball (b * a⁻¹) r
⊢ (fun (x : G) ↦ x * a) ⁻¹' ball b r = ball (b / a) r

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun (x : G) ↦ x * a) ⁻¹' ball b r = ball (b * a⁻¹) r

Tactic:
preimage_smul_ball (MulOpposite.op a) b r

Premises used: MulOpposite.unop, Metric.preimage_smul_ball, MulOpposite.op
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun (x : G) ↦ x * a) ⁻¹' ball b r = ball (b * a⁻¹) r

Tactic:
exact preimage_smul_ball (MulOpposite.op a) b r

Premises used: Metric.preimage_smul_ball, MulOpposite.op
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoMetricSpace G
inst_2 : IsIsometricSMul G G
a b : G
r : ℝ
⊢ (fun (x : G) ↦ a * x) ⁻¹' closedBall b r = closedBall (a⁻¹ * b) r

Tactic:
preimage_smul_closedBall a b r

Premises used: Metric.preimage_smul_closedBall
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
rw : (fun (x : G) ↦ x * a) ⁻¹' closedBall b r = closedBall (b * a⁻¹) r
⊢ (fun (x : G) ↦ x * a) ⁻¹' closedBall b r = closedBall (b / a) r

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun (x : G) ↦ x * a) ⁻¹' closedBall b r = closedBall (b * a⁻¹) r

Tactic:
preimage_smul_closedBall (MulOpposite.op a) b r

Premises used: Metric.preimage_smul_closedBall, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
G : Type v
inst : Group G
inst_1 : PseudoMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun (x : G) ↦ x * a) ⁻¹' closedBall b r = closedBall (b * a⁻¹) r

Tactic:
exact preimage_smul_closedBall (MulOpposite.op a) b r

Premises used: Metric.preimage_smul_closedBall, MulOpposite.op
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
G : Type v
X : Type w
Y : Type u_1
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M X
inst_3 : IsIsometricSMul M X
inst_4 : SMul M Y
inst_5 : IsIsometricSMul M Y
⊢ IsIsometricSMul M (X × Y)

Tactic:
⟨fun c => (isometry_smul X c).prodMap (isometry_smul Y c)⟩

Premises used: Isometry.prodMap, IsIsometricSMul.isometry_smul, IsIsometricSMul.mk
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
G : Type v
X : Type w
Y : Type u_1
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M X
inst_3 : IsIsometricSMul M X
N : Type u_2
inst_4 : Mul M
inst_5 : PseudoEMetricSpace M
inst_6 : IsIsometricSMul M M
inst_7 : Mul N
inst_8 : PseudoEMetricSpace N
inst_9 : IsIsometricSMul N N
⊢ IsIsometricSMul (M × N) (M × N)

Tactic:
⟨fun c => (isometry_smul M c.1).prodMap (isometry_smul N c.2)⟩

Premises used: Prod.fst, Isometry.prodMap, IsIsometricSMul.isometry_smul, IsIsometricSMul.mk, Prod.snd
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
G : Type v
X : Type w
Y : Type u_1
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M X
inst_3 : IsIsometricSMul M X
N : Type u_2
inst_4 : Mul M
inst_5 : PseudoEMetricSpace M
inst_6 : IsIsometricSMul Mᵐᵒᵖ M
inst_7 : Mul N
inst_8 : PseudoEMetricSpace N
inst_9 : IsIsometricSMul Nᵐᵒᵖ N
⊢ IsIsometricSMul (M × N)ᵐᵒᵖ (M × N)

Tactic:
⟨fun c => (isometry_mul_right c.unop.1).prodMap (isometry_mul_right c.unop.2)⟩

Premises used: Prod.fst, Isometry.prodMap, isometry_mul_right, MulOpposite.unop, IsIsometricSMul.mk, Prod.snd
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
G : Type v
X : Type w
Y : Type u_1
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M X
inst_3 : IsIsometricSMul M X
inst_4 : Monoid M
⊢ IsIsometricSMul.{u, w} Mˣ X

Tactic:
⟨fun c => isometry_smul X (c : M)⟩

Premises used: Units.val, IsIsometricSMul.isometry_smul, IsIsometricSMul.mk
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
G : Type v
X : Type w
Y : Type u_1
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M X
inst_3 : IsIsometricSMul M X
c : M
x y : Xᵐᵒᵖ
⊢ edist.{w} (α := Xᵐᵒᵖ) ((fun (x : Xᵐᵒᵖ) ↦ c • x) x) ((fun (x : Xᵐᵒᵖ) ↦ c • x) y) = edist x y

Tactic:
simpa only using edist_smul_left c x.unop y.unop

Premises used: edist_smul_left, MulOpposite.unop
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
G : Type v
X : Type w
Y : Type u_1
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M X
inst_3 : IsIsometricSMul M X
c : ULift.{u_2, u} M
⊢ Isometry (β := X) fun (x : X) ↦ c • x

Tactic:
simpa only using isometry_smul X c.down

Premises used: IsIsometricSMul.isometry_smul, ULift.down
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
G : Type v
X : Type w
Y : Type u_1
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M X
inst_3 : IsIsometricSMul M X
c : M
x y : ULift.{u_2, w} X
⊢ edist (α := ULift.{u_2, w} X) ((fun (x : ULift.{u_2, w} X) ↦ c • x) x) ((fun (x : ULift.{u_2, w} X) ↦ c • x) y) =
    edist x y

Tactic:
simpa only using edist_smul_left c x.1 y.1

Premises used: edist_smul_left, ULift.down
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
G : Type v
X_1 : Type w
Y : Type u_1
inst : PseudoEMetricSpace X_1
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M X_1
inst_3 : IsIsometricSMul M X_1
ι : Type u_3
X : ι → Type u_2
inst_4 : Fintype ι
inst_5 : (i : ι) → SMul.{u, u_2} M (X i)
inst_6 : (i : ι) → PseudoEMetricSpace (X i)
inst_7 : ∀ (i : ι), IsIsometricSMul.{u, u_2} M (X i)
⊢ IsIsometricSMul M ((i : ι) → X i)

Tactic:
⟨fun c => .piMap (fun _ => (c • ·)) fun i => isometry_smul (X i) c⟩

Premises used: Isometry.piMap, IsIsometricSMul.isometry_smul, HSMul.hSMul, IsIsometricSMul.mk
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M_1 : Type u
G : Type v
X_1 : Type w
Y : Type u_1
inst : PseudoEMetricSpace X_1
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M_1 X_1
inst_3 : IsIsometricSMul M_1 X_1
ι : Type u_4
M : ι → Type u_2
X : ι → Type u_3
inst_4 : Fintype ι
inst_5 : (i : ι) → SMul.{u_2, u_3} (M i) (X i)
inst_6 : (i : ι) → PseudoEMetricSpace (X i)
inst_7 : ∀ (i : ι), IsIsometricSMul.{u_2, u_3} (M i) (X i)
⊢ IsIsometricSMul ((i : ι) → M i) ((i : ι) → X i)

Tactic:
⟨fun c => .piMap (fun i => (c i • ·)) fun _ => isometry_smul _ _⟩

Premises used: Isometry.piMap, IsIsometricSMul.isometry_smul, HSMul.hSMul, IsIsometricSMul.mk
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M_1 : Type u
G : Type v
X : Type w
Y : Type u_1
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M_1 X
inst_3 : IsIsometricSMul M_1 X
ι : Type u_3
M : ι → Type u_2
inst_4 : Fintype ι
inst_5 : (i : ι) → Mul (M i)
inst_6 : (i : ι) → PseudoEMetricSpace (M i)
inst_7 : ∀ (i : ι), IsIsometricSMul.{u_2, u_2} (M i)ᵐᵒᵖ (M i)
⊢ IsIsometricSMul ((i : ι) → M i)ᵐᵒᵖ ((i : ι) → M i)

Tactic:
⟨fun c => .piMap (fun i (x : M i) => x * c.unop i) fun _ => isometry_mul_right _⟩

Premises used: HMul.hMul, Isometry.piMap, isometry_mul_right, MulOpposite.unop, IsIsometricSMul.mk
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
G : Type v
X : Type w
Y : Type u_1
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M X
inst_3 : IsIsometricSMul M X
⊢ IsIsometricVAdd.{u, w} (Additive M) X

Tactic:
⟨fun c => isometry_smul X c.toMul⟩

Premises used: IsIsometricVAdd.mk, Additive.toMul, IsIsometricSMul.isometry_smul, DFunLike.coe
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
G : Type v
X : Type w
Y : Type u_1
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M X
inst_3 : IsIsometricSMul M X
inst_4 : Mul M
inst_5 : PseudoEMetricSpace M
inst_6 : IsIsometricSMul M M
⊢ IsIsometricVAdd.{u, u} (Additive M) (Additive M)

Tactic:
⟨fun c x y => edist_smul_left c.toMul x.toMul y.toMul⟩

Premises used: IsIsometricVAdd.mk, Additive.toMul, edist_smul_left, DFunLike.coe
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
G : Type v
X : Type w
Y : Type u_1
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M X
inst_3 : IsIsometricSMul M X
inst_4 : Mul M
inst_5 : PseudoEMetricSpace M
inst_6 : IsIsometricSMul Mᵐᵒᵖ M
⊢ IsIsometricVAdd.{u, u} (Additive M)ᵃᵒᵖ (Additive M)

Tactic:
⟨fun c x y => edist_smul_left (MulOpposite.op c.unop.toMul) x.toMul y.toMul⟩

Premises used: IsIsometricVAdd.mk, Additive.toMul, edist_smul_left, AddOpposite.unop, DFunLike.coe, MulOpposite.op
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M_1 : Type u
G : Type v
X_1 : Type w
Y : Type u_1
inst : PseudoEMetricSpace X_1
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M_1 X_1
inst_3 : IsIsometricSMul M_1 X_1
M : Type u_2
X : Type u_3
inst_4 : VAdd M X
inst_5 : PseudoEMetricSpace X
inst_6 : IsIsometricVAdd M X
⊢ IsIsometricSMul.{u_2, u_3} (Multiplicative M) X

Tactic:
⟨fun c => isometry_vadd X c.toAdd⟩

Premises used: IsIsometricVAdd.isometry_vadd, Multiplicative.toAdd, IsIsometricSMul.mk, DFunLike.coe