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 α
β : 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_1 b_1 : Completion R
a b : R
rw : (↑(a * b) : Completion R) = HMul.hMul (α := Completion R) (↑b : Completion R) (↑a : Completion R)
rw₁ : Eq (α := Completion R) (↑(a * b) : Completion R) (↑(b * a) : Completion R)
rw₂ rw₃ : Eq (α := Completion R) (↑(b * a) : Completion R) (↑(b * a) : Completion R)
⊢ HMul.hMul (α := Completion R) (↑a : Completion R) (↑b : Completion R) =
    HMul.hMul (α := Completion R) (↑b : Completion R) (↑a : Completion R)

Tactic:
rw [← coe_mul, ← coe_mul, mul_comm]

Premises used: UniformSpace.Completion.coe_mul, mul_comm
-- 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
⊢ Algebra R (Completion R)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_2
inst : Ring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalRing α
x y : α
⊢ Membership.mem (γ := Set α) (closure 0) (x - y) ↔ Membership.mem (γ := Submodule α α) (Ideal.closure ⊥) (x - y)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α_1 : Type u_1
α : Type u_2
inst : Ring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalRing α
x y : α
rw rw₁ : (Submodule.quotientRel ⊥.closure : α → α → Prop) x y ↔ (Submodule.quotientRel ⊥.closure : α → α → Prop) x y
⊢ (inseparableSetoid α : α → α → Prop) x y ↔ (Submodule.quotientRel ⊥.closure : α → α → Prop) x y

Tactic:
rw [inseparableSetoid_ring]

Premises used: UniformSpace.inseparableSetoid_ring
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α_1 : Type u_1
α : Type u_2
inst : Ring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalRing α
rw :
  Relator.LiftFun.{u_2 + 1, u_2 + 1, u_2 + 1, u_2 + 1} (α := α) (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop)
    (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop) id id
⊢ Relator.LiftFun.{u_2 + 1, u_2 + 1, u_2 + 1, u_2 + 1} (α := α) (⇑(inseparableSetoid α) : α → α → Prop)
    (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop) id id

Tactic:
rw [inseparableSetoid_ring]

Premises used: UniformSpace.inseparableSetoid_ring
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α_1 : Type u_1
α : Type u_2
inst : Ring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalRing α
⊢ Relator.LiftFun.{u_2 + 1, u_2 + 1, u_2 + 1, u_2 + 1} (α := α) (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop)
    (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop) id id

Tactic:
fun _ _ ↦ id

Premises used: Set.Mem, id, Relator.LiftFun
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α_1 : Type u_1
α : Type u_2
inst : Ring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalRing α
⊢ Relator.LiftFun.{u_2 + 1, u_2 + 1, u_2 + 1, u_2 + 1} (α := α) (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop)
    (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop) id id

Tactic:
exact fun _ _ ↦ id

Premises used: id
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α_1 : Type u_1
α : Type u_2
inst : Ring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalRing α
rw :
  Relator.LiftFun.{u_2 + 1, u_2 + 1, u_2 + 1, u_2 + 1} (α := α) (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop)
    (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop) id id
⊢ Relator.LiftFun.{u_2 + 1, u_2 + 1, u_2 + 1, u_2 + 1} (α := α) (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop)
    (⇑(inseparableSetoid α) : α → α → Prop) id id

Tactic:
rw [inseparableSetoid_ring]

Premises used: UniformSpace.inseparableSetoid_ring
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
⊢ Eq.{u_3 + 1} (α := γ) (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) 1) : γ) ((f : (a : α) → γ) 1 : γ)

Tactic:
IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous 1

Premises used: IsUniformInducing.isDenseInducing, UniformContinuous.continuous, OfNat.ofNat, IsDenseInducing.extend_eq
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Eq.{u_2 + 1} (α := β) (1 : β) ((i : (a : α) → β) 1 : β)
h₁ : Eq.{u_3 + 1} (α := γ) (1 : γ) ((f : (a : α) → γ) 1 : γ)
⊢ Eq.{u_3 + 1} (α := γ) (⋯.extend (⇑f : (a : α) → γ) 1) 1

Tactic:
convert! IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous 1

Premises used: IsUniformInducing.isDenseInducing, UniformContinuous.continuous, OfNat.ofNat, IsDenseInducing.extend_eq
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
⊢ Eq.{u_2 + 1} (α := β) (1 : β) ((i : (a : α) → β) 1 : β)

Tactic:
i.map_one.symm

Premises used: RingHom.map_one, Eq.symm
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
⊢ Eq.{u_3 + 1} (α := γ) (1 : γ) ((f : (a : α) → γ) 1 : γ)

Tactic:
f.map_one.symm

Premises used: RingHom.map_one, Eq.symm
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
⊢ Eq.{u_2 + 1} (α := β) (1 : β) ((i : (a : α) → β) 1 : β)

Tactic:
exacts [i.map_one.symm, f.map_one.symm]

Premises used: RingHom.map_one, Eq.symm
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
⊢ Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))

Tactic:
have h := (uniformContinuous_uniformly_extend ue dr hf).continuous
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
⊢ ∀ (x y : β),
    ⋯.extend (⇑f : (a : α) → γ) (x * y) =
      HMul.hMul (α := γ) (⋯.extend (⇑f : (a : α) → γ) x) (⋯.extend (⇑f : (a : α) → γ) y)

Tactic:
fun x y => DenseRange.induction_on₂ dr ?_ (fun a b => ?_) x y

Premises used: DenseRange.induction_on₂
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
refine_1 :
  ∀ (x y : β),
    IsClosed.{u_2} (X := β × β)
      {q : β × β |
        ⋯.extend (⇑f : (a : α) → γ) (q.1 * q.2) =
          HMul.hMul (α := γ) (⋯.extend (⇑f : (a : α) → γ) q.1) (⋯.extend (⇑f : (a : α) → γ) q.2)}
refine_2 :
  ∀ (x y : β) (a b : α),
    ⋯.extend (⇑f : (a : α) → γ) (HMul.hMul (α := β) (β := β) ((i : (a : α) → β) a : β) ((i : (a : α) → β) b : β)) =
      HMul.hMul (α := γ) (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
        (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))
⊢ ∀ (x y : β),
    ⋯.extend (⇑f : (a : α) → γ) (x * y) =
      HMul.hMul (α := γ) (⋯.extend (⇑f : (a : α) → γ) x) (⋯.extend (⇑f : (a : α) → γ) y)

Tactic:
refine fun x y => DenseRange.induction_on₂ dr ?_ (fun a b => ?_) x y
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
x y : β
⊢ Continuous.{u_2, u_3} (Y := γ) fun (q : β × β) ↦ ⋯.extend (⇑f : (a : α) → γ) (q.1 * q.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
x y : β
⊢ Continuous.{u_2, u_3} (Y := γ) fun (q : β × β) ↦
    HMul.hMul (α := γ) (⋯.extend (⇑f : (a : α) → γ) q.1) (⋯.extend (⇑f : (a : α) → γ) q.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
x y : β
⊢ IsClosed.{u_2} (X := β × β)
    {q : β × β |
      ⋯.extend (⇑f : (a : α) → γ) (q.1 * q.2) =
        HMul.hMul (α := γ) (⋯.extend (⇑f : (a : α) → γ) q.1) (⋯.extend (⇑f : (a : α) → γ) q.2)}

Tactic:
exact isClosed_eq (by fun_prop) (by fun_prop)

Premises used: isClosed_eq
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
x y : β
a b : α
refine_2 :
  ⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) (a * b)) =
    HMul.hMul (α := γ) (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
      (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))
refine_2₁ : (f : (a : α) → γ) (a * b) = HMul.hMul (α := γ) (β := γ) ((f : (a : α) → γ) a : γ) ((f : (a : α) → γ) b : γ)
⊢ ⋯.extend (⇑f : (a : α) → γ) (HMul.hMul (α := β) (β := β) ((i : (a : α) → β) a : β) ((i : (a : α) → β) b : β)) =
    HMul.hMul (α := γ) (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
      (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))

Tactic:
simp_rw [← i.map_mul, IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous _,
        ← f.map_mul]

Premises used: IsUniformInducing.isDenseInducing, UniformContinuous.continuous, RingHom.map_mul, IsDenseInducing.extend_eq
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
⊢ Eq.{u_3 + 1} (α := γ) (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) 0) : γ) ((f : (a : α) → γ) 0 : γ)

Tactic:
IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous 0

Premises used: IsUniformInducing.isDenseInducing, UniformContinuous.continuous, OfNat.ofNat, IsDenseInducing.extend_eq
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Eq.{u_2 + 1} (α := β) (0 : β) ((i : (a : α) → β) 0 : β)
h₁ : Eq.{u_3 + 1} (α := γ) (0 : γ) ((f : (a : α) → γ) 0 : γ)
⊢ Eq.{u_3 + 1} (α := γ) (⋯.extend (⇑f : (a : α) → γ) 0) 0

Tactic:
convert! IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous 0

Premises used: IsUniformInducing.isDenseInducing, UniformContinuous.continuous, OfNat.ofNat, IsDenseInducing.extend_eq
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
⊢ Eq.{u_2 + 1} (α := β) (0 : β) ((i : (a : α) → β) 0 : β)

Tactic:
simp only [map_zero]

Premises used: map_zero
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
⊢ Eq.{u_3 + 1} (α := γ) (0 : γ) ((f : (a : α) → γ) 0 : γ)

Tactic:
simp only [map_zero]

Premises used: map_zero
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
⊢ ∀ (x y : β),
    ⋯.extend (⇑f : (a : α) → γ) (x + y) =
      HAdd.hAdd (α := γ) (⋯.extend (⇑f : (a : α) → γ) x) (⋯.extend (⇑f : (a : α) → γ) y)

Tactic:
fun x y => DenseRange.induction_on₂ dr ?_ (fun a b => ?_) x y

Premises used: DenseRange.induction_on₂
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
refine_1 :
  ∀ (x y : β),
    IsClosed.{u_2} (X := β × β)
      {q : β × β |
        ⋯.extend (⇑f : (a : α) → γ) (q.1 + q.2) =
          HAdd.hAdd (α := γ) (⋯.extend (⇑f : (a : α) → γ) q.1) (⋯.extend (⇑f : (a : α) → γ) q.2)}
refine_2 :
  ∀ (x y : β) (a b : α),
    ⋯.extend (⇑f : (a : α) → γ) (HAdd.hAdd (α := β) (β := β) ((i : (a : α) → β) a : β) ((i : (a : α) → β) b : β)) =
      HAdd.hAdd (α := γ) (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
        (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))
⊢ ∀ (x y : β),
    ⋯.extend (⇑f : (a : α) → γ) (x + y) =
      HAdd.hAdd (α := γ) (⋯.extend (⇑f : (a : α) → γ) x) (⋯.extend (⇑f : (a : α) → γ) y)

Tactic:
refine fun x y => DenseRange.induction_on₂ dr ?_ (fun a b => ?_) x y
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
x y : β
⊢ Continuous.{u_2, u_3} (Y := γ) fun (q : β × β) ↦ ⋯.extend (⇑f : (a : α) → γ) (q.1 + q.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
x y : β
⊢ Continuous.{u_2, u_3} (Y := γ) fun (q : β × β) ↦
    HAdd.hAdd (α := γ) (⋯.extend (⇑f : (a : α) → γ) q.1) (⋯.extend (⇑f : (a : α) → γ) q.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
x y : β
⊢ IsClosed.{u_2} (X := β × β)
    {q : β × β |
      ⋯.extend (⇑f : (a : α) → γ) (q.1 + q.2) =
        HAdd.hAdd (α := γ) (⋯.extend (⇑f : (a : α) → γ) q.1) (⋯.extend (⇑f : (a : α) → γ) q.2)}

Tactic:
exact isClosed_eq (by fun_prop) (by fun_prop)

Premises used: isClosed_eq
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
x y : β
a b : α
refine_2 :
  ⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) (a + b)) =
    HAdd.hAdd (α := γ) (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
      (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))
refine_2₁ : (f : (a : α) → γ) (a + b) = HAdd.hAdd (α := γ) (β := γ) ((f : (a : α) → γ) a : γ) ((f : (a : α) → γ) b : γ)
⊢ ⋯.extend (⇑f : (a : α) → γ) (HAdd.hAdd (α := β) (β := β) ((i : (a : α) → β) a : β) ((i : (a : α) → β) b : β)) =
    HAdd.hAdd (α := γ) (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
      (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))

Tactic:
simp_rw [← i.map_add, IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous _,
        ← f.map_add]

Premises used: IsUniformInducing.isDenseInducing, UniformContinuous.continuous, RingHom.map_add, IsDenseInducing.extend_eq