awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
a b c : Completion α
⊢ Continuous (Y := Completion α) fun (x : Completion α × Completion α × Completion α) ↦ x.1 * x.2.2 + x.2.1 * x.2.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
a_1 b_1 c_1 : Completion α
a b c : α
rw :
  HMul.hMul (α := Completion α) (↑(a + b) : Completion α) (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₁ :
  (↑((a + b) * c) : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₂ :
  (↑((a + b) * c) : Completion α) =
    (↑(a * c) : Completion α) + HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₃ :
  (↑((a + b) * c) : Completion α) = HAdd.hAdd (α := Completion α) (↑(a * c) : Completion α) (↑(b * c) : Completion α)
rw₄ : Eq (α := Completion α) (↑((a + b) * c) : Completion α) (↑(a * c + b * c) : Completion α)
rw₅ rw₆ : Eq (α := Completion α) (↑(a * c + b * c) : Completion α) (↑(a * c + b * c) : Completion α)
⊢ HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α) * (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)

Tactic:
rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, add_mul]

Premises used: add_mul, UniformSpace.Completion.coe_mul, UniformSpace.Completion.coe_add
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
⊢ Continuous.{u_1, u_1} (X := α) (Y := Completion α) (⇑coeRingHom : (a : α) → Completion α)

Tactic:
continuous_coe α

Premises used: UniformSpace.Completion.coe', UniformSpace.Completion.continuous_coe, SeparationQuotient.mk
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
rw : Eq.{u + 1} (α := β) (Completion.extension.{u_1, u} (α := α) (⇑f : (a : α) → β) (↑1 : Completion α)) 1
rw₁ : Eq.{u + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)
rw₂ rw₃ : Eq.{u + 1} (α := β) 1 1
⊢ Eq.{u + 1} (α := β) (Completion.extension.{u_1, u} (α := α) (⇑f : (a : α) → β) 1) 1

Tactic:
rw [← coe_one, extension_coe hf, f.map_one]

Premises used: UniformSpace.Completion.extension_coe, RingHom.map_one, UniformSpace.Completion.coe_one
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
a b : Completion α
⊢ Continuous.{u_1, u} (Y := β) fun (x : Completion α × Completion α) ↦
    Completion.extension (⇑f : (a : α) → β) (x.1 * x.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
a b : Completion α
⊢ Continuous.{u_1, u} (Y := β) fun (x : Completion α × Completion α) ↦
    HMul.hMul (α := β) (Completion.extension (⇑f : (a : α) → β) x.1) (Completion.extension (⇑f : (a : α) → β) x.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
a_1 b_1 : Completion α
a b : α
simp_rw :
  Completion.extension (⇑f : (a : α) → β) (↑(a * b) : Completion α) =
    HMul.hMul (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
simp_rw₁ : (f : (a : α) → β) (a * b) = HMul.hMul (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
⊢ Completion.extension (⇑f : (a : α) → β) (HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α)) =
    HMul.hMul (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))

Tactic:
simp_rw [← coe_mul, extension_coe hf, f.map_mul]

Premises used: UniformSpace.Completion.extension_coe, UniformSpace.Completion.coe_mul, RingHom.map_mul
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
simp_rw : Eq.{u + 1} (α := β) (Completion.extension.{u_1, u} (α := α) (⇑f : (a : α) → β) (↑0 : Completion α)) 0
simp_rw₁ : Eq.{u + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
⊢ Eq.{u + 1} (α := β) (Completion.extension.{u_1, u} (α := α) (⇑f : (a : α) → β) 0) 0

Tactic:
simp_rw [← coe_zero, extension_coe hf, f.map_zero]

Premises used: UniformSpace.Completion.extension_coe, UniformSpace.Completion.coe_zero, RingHom.map_zero
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
a b : Completion α
⊢ Continuous.{u_1, u} (Y := β) fun (x : Completion α × Completion α) ↦
    Completion.extension (⇑f : (a : α) → β) (x.1 + x.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
a b : Completion α
⊢ Continuous.{u_1, u} (Y := β) fun (x : Completion α × Completion α) ↦
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) x.1) (Completion.extension (⇑f : (a : α) → β) x.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
a_1 b_1 : Completion α
a b : α
simp_rw :
  Completion.extension (⇑f : (a : α) → β) (↑(a + b) : Completion α) =
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
simp_rw₁ : (f : (a : α) → β) (a + b) = HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
⊢ Completion.extension (⇑f : (a : α) → β) (HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α)) =
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))

Tactic:
simp_rw [← coe_add, extension_coe hf, f.map_add]

Premises used: UniformSpace.Completion.extension_coe, RingHom.map_add, UniformSpace.Completion.coe_add
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
a : α
⊢ Eq.{u + 1} (α := β) ((extensionHom f hf : (a : Completion α) → β) (↑a : Completion α) : β) ((f : (a : α) → β) a : β)

Tactic:
simp only [Completion.extensionHom, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    UniformSpace.Completion.extension_coe <| uniformContinuous_addMonoidHom_of_continuous hf]

Premises used: UniformSpace.Completion.extensionHom, UniformSpace.Completion.extension_coe, OneHom.coe_mk, MonoidHom.coe_mk, RingHom.coe_mk, uniformContinuous_addMonoidHom_of_continuous
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
x : Completion α
⊢ Eq.{u + 1} (α := Completion β)
    (((mapRingHom f hf : RingHom.{u_1, u} (Completion α) (Completion β)) : (a : Completion α) → Completion β) x :
      Completion β)
    (Completion.map (⇑f : (a : α) → β) x : Completion β)

Tactic:
rfl

Premises used: UniformSpace.Completion.map, UniformSpace.Completion.coe', Quotient, SeparationQuotient, SeparationQuotient.mk, UniformSpace.Completion.extension, AbstractCompletion.map, AbstractCompletion.extend, UniformSpace.Completion, rfl, ite
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
⊢ Eq (α := (a : Completion α) → Completion β) (⇑(mapRingHom f hf) : (a : Completion α) → Completion β)
    (Completion.map (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: UniformSpace.Completion.map, UniformSpace.Completion.coe', Quotient, SeparationQuotient, SeparationQuotient.mk, UniformSpace.Completion.extension, AbstractCompletion.map, AbstractCompletion.extend, UniformSpace.Completion, rfl, ite
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
a : α
rw :
  Eq.{u + 1} (α := Completion β) (Completion.map (⇑f : (a : α) → β) (↑a : Completion α) : Completion β)
    ((↑((f : (a : α) → β) a) : Completion β) : Completion β)
rw₁ rw₂ :
  Eq.{u + 1} (α := Completion β) ((↑((f : (a : α) → β) a) : Completion β) : Completion β)
    ((↑((f : (a : α) → β) a) : Completion β) : Completion β)
⊢ Eq.{u + 1} (α := Completion β)
    (((mapRingHom f hf : RingHom.{u_1, u} (Completion α) (Completion β)) : (a : Completion α) → Completion β)
        (↑a : Completion α) :
      Completion β)
    ((↑((f : (a : α) → β) a) : Completion β) : Completion β)

Tactic:
rw [mapRingHom_apply, map_coe (uniformContinuous_addMonoidHom_of_continuous hf)]

Premises used: UniformSpace.Completion.mapRingHom_apply, UniformSpace.Completion.map_coe, uniformContinuous_addMonoidHom_of_continuous
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
γ : Type u_2
inst_8 : UniformSpace γ
inst_9 : Ring γ
inst_10 : IsUniformAddGroup γ
inst_11 : IsTopologicalRing γ
g : β →+* γ
hg : Continuous.{u, u_2} (X := β) (Y := γ) (⇑g : (a : β) → γ)
hf : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
⊢ Eq (α := RingHom.{u_1, u_2} (Completion α) (Completion γ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (mapRingHom g hg) (mapRingHom f hf)) (mapRingHom (g.comp f) ⋯)

Tactic:
DFunLike.ext' <| map_comp
    (uniformContinuous_addMonoidHom_of_continuous hg)
    (uniformContinuous_addMonoidHom_of_continuous hf)

Premises used: UniformSpace.Completion.map_comp, uniformContinuous_addMonoidHom_of_continuous, DFunLike.ext'
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
⊢ Eq (α := Completion α →+* Completion α) (mapRingHom (RingHom.id α) ⋯) (RingHom.id (Completion α))

Tactic:
simp [RingHom.ext_iff, mapRingHom_apply]

Premises used: UniformSpace.Completion.mapRingHom_apply, RingHom.ext_iff
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f_1 : α →+* β
hf_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f_1 : (a : α) → β)
f : α ≃+* β
hf : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
hf' : Continuous.{u, u_1} (X := β) (Y := α) (⇑f.symm : (a : β) → α)
⊢ Eq (α := Completion β →+* Completion β)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (mapRingHom f.toRingHom hf) (mapRingHom f.symm.toRingHom hf'))
    (RingHom.id (Completion β))

Tactic:
simp [mapRingHom_comp]

Premises used: UniformSpace.Completion.mapRingHom_comp
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f_1 : α →+* β
hf_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f_1 : (a : α) → β)
f : α ≃+* β
hf : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
hf' : Continuous.{u, u_1} (X := β) (Y := α) (⇑f.symm : (a : β) → α)
⊢ Eq (α := Completion α →+* Completion α)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (mapRingHom f.symm.toRingHom hf') (mapRingHom f.toRingHom hf))
    (RingHom.id (Completion α))

Tactic:
simp [mapRingHom_comp]

Premises used: UniformSpace.Completion.mapRingHom_comp
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
A : Type u_2
inst : Ring A
inst_1 : UniformSpace A
inst_2 : IsUniformAddGroup A
inst_3 : IsTopologicalRing A
R : Type u_3
inst_4 : CommSemiring R
inst_5 : Algebra R A
inst_6 : UniformContinuousConstSMul R A
r : R
h :
  ∀ (x : Completion A),
    Completion.map (fun (x : A) ↦ r • x) x =
      HMul.hMul (α := Completion A) ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) x
⊢ Eq.{u_2 + 1} (α := Completion A → Completion A) (Completion.map fun (x : A) ↦ r • x) fun (x : Completion A) ↦
    HMul.hMul (α := Completion A) ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) x

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
A : Type u_2
inst : Ring A
inst_1 : UniformSpace A
inst_2 : IsUniformAddGroup A
inst_3 : IsTopologicalRing A
R : Type u_3
inst_4 : CommSemiring R
inst_5 : Algebra R A
inst_6 : UniformContinuousConstSMul R A
r : R
x : Completion A
⊢ Completion.map (fun (x : A) ↦ r • x) x =
    HMul.hMul (α := Completion A) ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) x

Tactic:
Completion.induction_on x ?_ fun a => ?_

Premises used: UniformSpace.Completion.induction_on
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
A : Type u_2
inst : Ring A
inst_1 : UniformSpace A
inst_2 : IsUniformAddGroup A
inst_3 : IsTopologicalRing A
R : Type u_3
inst_4 : CommSemiring R
inst_5 : Algebra R A
inst_6 : UniformContinuousConstSMul R A
r : R
x : Completion A
h :
  IsClosed.{u_2} (X := Completion A)
    {a : Completion A |
      Completion.map (fun (x : A) ↦ r • x) a =
        HMul.hMul (α := Completion A) ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) a}
h₁ :
  ∀ (a : A),
    Completion.map (fun (x : A) ↦ r • x) (↑a : Completion A) =
      HMul.hMul (α := Completion A) (β := Completion A)
        ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) (↑a : Completion A)
⊢ Completion.map (fun (x : A) ↦ r • x) x =
    HMul.hMul (α := Completion A) ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) x

Tactic:
refine Completion.induction_on x ?_ fun a => ?_
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
A : Type u_2
inst : Ring A
inst_1 : UniformSpace A
inst_2 : IsUniformAddGroup A
inst_3 : IsTopologicalRing A
R : Type u_3
inst_4 : CommSemiring R
inst_5 : Algebra R A
inst_6 : UniformContinuousConstSMul R A
r : R
x : Completion A
⊢ IsClosed.{u_2} (X := Completion A)
    {a : Completion A |
      Completion.map (fun (x : A) ↦ r • x) a =
        HMul.hMul (α := Completion A) ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) a}

Tactic:
isClosed_eq Completion.continuous_map (continuous_const_mul _)

Premises used: continuous_const_mul, isClosed_eq, UniformSpace.Completion.continuous_map
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
A : Type u_2
inst : Ring A
inst_1 : UniformSpace A
inst_2 : IsUniformAddGroup A
inst_3 : IsTopologicalRing A
R : Type u_3
inst_4 : CommSemiring R
inst_5 : Algebra R A
inst_6 : UniformContinuousConstSMul R A
r : R
x : Completion A
⊢ IsClosed.{u_2} (X := Completion A)
    {a : Completion A |
      Completion.map (fun (x : A) ↦ r • x) a =
        HMul.hMul (α := Completion A) ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) a}

Tactic:
exact isClosed_eq Completion.continuous_map (continuous_const_mul _)

Premises used: continuous_const_mul, isClosed_eq, UniformSpace.Completion.continuous_map
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
A : Type u_2
inst : Ring A
inst_1 : UniformSpace A
inst_2 : IsUniformAddGroup A
inst_3 : IsTopologicalRing A
R : Type u_3
inst_4 : CommSemiring R
inst_5 : Algebra R A
inst_6 : UniformContinuousConstSMul R A
r : R
x : Completion A
a : A
h :
  (↑(r • a) : Completion A) =
    HMul.hMul (α := Completion A) (β := Completion A)
      ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) (↑a : Completion A)
h₁ :
  (↑(HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) : Completion A) =
    HMul.hMul (α := Completion A) (β := Completion A)
      ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) (↑a : Completion A)
⊢ Completion.map (fun (x : A) ↦ r • x) (↑a : Completion A) =
    HMul.hMul (α := Completion A) (β := Completion A)
      ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) (↑a : Completion A)

Tactic:
simp_rw [map_coe (uniformContinuous_const_smul r) a, Algebra.smul_def, coe_mul]

Premises used: UniformSpace.Completion.map_coe, UniformSpace.Completion.coe_mul, Algebra.smul_def, UniformContinuousConstSMul.uniformContinuous_const_smul
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
A : Type u_2
inst_8 : Ring A
inst_9 : UniformSpace A
inst_10 : IsUniformAddGroup A
inst_11 : IsTopologicalRing A
R : Type u_3
inst_12 : CommSemiring R
inst_13 : Algebra R A
inst_14 : UniformContinuousConstSMul R A
r : R
x : Completion A
a : A
⊢ HMul.hMul (α := Completion A) (β := Completion A)
      (((RingHom.comp coeRingHom (algebraMap R A) : RingHom.{u_3, u_2} R (Completion A)) : (a : R) → Completion A) r :
        Completion A)
      (↑a : Completion A) =
    HMul.hMul (α := Completion A) (β := Completion A) (↑a : Completion A)
      (((RingHom.comp coeRingHom (algebraMap R A) : RingHom.{u_3, u_2} R (Completion A)) : (a : R) → Completion A) r :
        Completion A)

Tactic:
simpa only [coe_mul] using congr_arg ((↑) : A → Completion A) (Algebra.commutes r a)

Premises used: UniformSpace.Completion.coe', congr_arg, UniformSpace.Completion.coe_mul, Algebra.commutes
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
A : Type u_2
inst : Ring A
inst_1 : UniformSpace A
inst_2 : IsUniformAddGroup A
inst_3 : IsTopologicalRing A
R : Type u_3
inst_4 : CommSemiring R
inst_5 : Algebra R A
inst_6 : UniformContinuousConstSMul R A
r : R
⊢ Eq.{u_2 + 1} (α := Completion A) ((algebraMap R (Completion A) : (a : R) → Completion A) r : Completion A)
    ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A)

Tactic:
rfl

Premises used: UniformSpace.Completion.coe', SeparationQuotient.mk, rfl
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
R : Type u_2
inst_8 : CommRing R
inst_9 : UniformSpace R
inst_10 : IsUniformAddGroup R
inst_11 : IsTopologicalRing R
a b : Completion R
⊢ Continuous (Y := Completion R) fun (x : Completion R × Completion R) ↦ x.1 * x.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
R : Type u_2
inst_8 : CommRing R
inst_9 : UniformSpace R
inst_10 : IsUniformAddGroup R
inst_11 : IsTopologicalRing R
a b : Completion R
⊢ Continuous (Y := Completion R) fun (x : Completion R × Completion R) ↦ x.2 * x.1

Tactic:
fun_prop