awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
⊢ ∀ (i : ℕ), ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ (n : ℕ), N ≤ n → u n - u m ∈ I ^ i

Tactic:
simpa using hI.hasBasis_nhds_zero.uniformity_of_nhds_zero.cauchySeq_iff.mp hu

Premises used: Filter.HasBasis.cauchySeq_iff, IsAdic.hasBasis_nhds_zero, Filter.HasBasis.uniformity_of_nhds_zero, Iff.mp
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
⊢ ∀ (i : ℕ), ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ (n : ℕ), N ≤ n → u n - u m ∈ I ^ i

Tactic:
have : ∀ i, ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → u n - u m ∈ I ^ i := by
      simpa using hI.hasBasis_nhds_zero.uniformity_of_nhds_zero.cauchySeq_iff.mp hu
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this_2 : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
this : ∀ (i : ℕ), ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ (n : ℕ), N ≤ n → u n - u m ∈ I ^ i
mp :
  ∀ (N : (i : ℕ) → ℕ) (hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i),
    ∃ (a : R), Filter.Tendsto u Filter.atTop (𝓝 a)
⊢ ∃ (a : R), Filter.Tendsto u Filter.atTop (𝓝 a)

Tactic:
choose N hN using this
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : (i : ℕ) → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
m n : ℕ
h : m ≤ n
⊢ m ∈ Finset.Iic n

Tactic:
simpa
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : (i : ℕ) → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
m n : ℕ
h : m ≤ n
⊢ m ∈ Finset.Iic m

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : (i : ℕ) → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
mp : ∀ (L : R) (hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n), ∃ (a : R), Filter.Tendsto u Filter.atTop (𝓝 a)
⊢ ∃ (a : R), Filter.Tendsto u Filter.atTop (𝓝 a)

Tactic:
obtain ⟨L, hL⟩ := H (fun i ↦ u ((Finset.Iic i).sup N))
      fun _ ↦ hN _ _ (Finset.le_sup (by simpa)) _ (Finset.le_sup (by simp))

Premises used: Finset.Iic, Finset.sup, Finset.le_sup
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : (i : ℕ) → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
h : Filter.Tendsto u Filter.atTop (𝓝 L)
⊢ ∃ (a : R), Filter.Tendsto u Filter.atTop (𝓝 a)

Tactic:
use L
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this_2 : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : (i : ℕ) → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
this : ∀ (i : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → u n - L ∈ I ^ i
⊢ Filter.Tendsto u Filter.atTop (𝓝 L)

Tactic:
simpa [(hI.hasBasis_nhds L).tendsto_right_iff, sub_eq_neg_add]

Premises used: IsAdic.hasBasis_nhds, sub_eq_neg_add, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : (i : ℕ) → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
h : ∀ (i : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → u n - L ∈ I ^ i
⊢ Filter.Tendsto u Filter.atTop (𝓝 L)

Tactic:
suffices ∀ i, ∃ N, ∀ n, N ≤ n → u n - L ∈ I ^ i by
      simpa [(hI.hasBasis_nhds L).tendsto_right_iff, sub_eq_neg_add]
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : (i : ℕ) → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
⊢ ∀ (i : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → u n - L ∈ I ^ i

Tactic:
fun i ↦ ⟨(Finset.Iic i).sup N, fun n hn ↦ ?_⟩

Premises used: Exists.intro, Finset.Iic, Finset.sup
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : (i : ℕ) → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
h : ∀ (i n : ℕ) (hn : (Finset.Iic i).sup N ≤ n), u n - L ∈ I ^ i
⊢ ∀ (i : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → u n - L ∈ I ^ i

Tactic:
refine fun i ↦ ⟨(Finset.Iic i).sup N, fun n hn ↦ ?_⟩
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : (i : ℕ) → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
i n : ℕ
hn : (Finset.Iic i).sup N ≤ n
⊢ i ∈ Finset.Iic i

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : (i : ℕ) → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
i n : ℕ
hn : (Finset.Iic i).sup N ≤ n
⊢ u n - u ((Finset.Iic i).sup N) + (u ((Finset.Iic i).sup N) - L) ∈ I ^ i

Tactic:
have := Ideal.add_mem _ (hN i ((Finset.Iic i).sup N) (Finset.le_sup (by simp))
      n (.trans (Finset.le_sup (by simp)) hn)) (hL i)
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this_2 : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : (i : ℕ) → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
i n : ℕ
hn : (Finset.Iic i).sup N ≤ n
this : u n - u ((Finset.Iic i).sup N) + (u ((Finset.Iic i).sup N) - L) ∈ I ^ i
h h₁ h₂ h₃ : ∀ (this : u n - L ∈ I ^ i), u n - L ∈ I ^ i
⊢ u n - L ∈ I ^ i

Tactic:
rwa [sub_add_sub_cancel] at this

Premises used: sub_add_sub_cancel
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
i : ℕ
h : True
m : ℕ
hm : i ≤ m
n : ℕ
hn : i ≤ n
⊢ Membership.mem (γ := SetRel R R) {x : R × R | x.2 - x.1 ∈ (↑(I ^ i) : Set R)} (f m, f n)

Tactic:
simpa using Ideal.sub_mem _ (hf hm) (hf hn)

Premises used: Ideal.sub_mem
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
mpr : ∀ (L : R) (hL : Filter.map f Filter.atTop ≤ 𝓝 L), ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
⊢ ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n

Tactic:
obtain ⟨L, hL⟩ := CompleteSpace.complete (f := Filter.atTop.map f)
      (hI.hasBasis_nhds_zero.uniformity_of_nhds_zero.cauchySeq_iff.mpr fun i _ ↦
        ⟨i, fun m hm n hn ↦ by simpa using Ideal.sub_mem _ (hf hm) (hf hn)⟩)

Premises used: Iff.mpr, Filter.HasBasis.cauchySeq_iff, IsAdic.hasBasis_nhds_zero, Filter.HasBasis.uniformity_of_nhds_zero, CompleteSpace.complete, Exists.intro
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
L : R
hL : Filter.map f Filter.atTop ≤ 𝓝 L
⊢ ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n

Tactic:
⟨L, fun i ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
L : R
hL : Filter.map f Filter.atTop ≤ 𝓝 L
mpr : ∀ (i : ℕ), f i - L ∈ I ^ i
⊢ ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n

Tactic:
refine ⟨L, fun i ↦ ?_⟩
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
L : R
hL : Filter.map f Filter.atTop ≤ 𝓝 L
i : ℕ
⊢ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → f n - L ∈ I ^ i

Tactic:
simpa [sub_eq_neg_add] using (hI.hasBasis_nhds L).tendsto_right_iff.mp hL i

Premises used: IsAdic.hasBasis_nhds, sub_eq_neg_add, Iff.mp, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
L : R
hL : Filter.map f Filter.atTop ≤ 𝓝 L
i : ℕ
mpr : ∀ (N : ℕ) (hN : ∀ (n : ℕ), N ≤ n → f n - L ∈ I ^ i), f i - L ∈ I ^ i
⊢ f i - L ∈ I ^ i

Tactic:
obtain ⟨N, hN⟩ : ∃ N, ∀ n, N ≤ n → f n - L ∈ I ^ i := by
      simpa [sub_eq_neg_add] using (hI.hasBasis_nhds L).tendsto_right_iff.mp hL i
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
L : R
hL : Filter.map f Filter.atTop ≤ 𝓝 L
i N : ℕ
hN : ∀ (n : ℕ), N ≤ n → f n - L ∈ I ^ i
⊢ f i - L ∈ I ^ i

Tactic:
simpa using Ideal.add_mem _ (hN (max i N) le_sup_right) (hf (le_max_left i N))

Premises used: Ideal.add_mem, le_sup_right, Max.max, le_max_left
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
rw : IsHausdorff I R ∧ IsPrecomplete I R ↔ CompleteSpace R ∧ T2Space R
rw₁ : T2Space R ∧ IsPrecomplete I R ↔ CompleteSpace R ∧ T2Space R
rw₂ : T2Space R ∧ CompleteSpace R ↔ CompleteSpace R ∧ T2Space R
rw₃ rw₄ : CompleteSpace R ∧ T2Space R ↔ CompleteSpace R ∧ T2Space R
⊢ IsAdicComplete I R ↔ CompleteSpace R ∧ T2Space R

Tactic:
rw [isAdicComplete_iff, hI.isHausdorff_iff, hI.isPrecomplete_iff, and_comm]

Premises used: IsAdic.isPrecomplete_iff, and_comm, IsAdic.isHausdorff_iff, isAdicComplete_iff
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
e : R ≃+* S
this_1 : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ IsAdic I

Tactic:
rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
e : R ≃+* S
this_1 : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ IsAdic.{u_2} (R := S) (Ideal.map e I)

Tactic:
rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
e : R ≃+* S
this_1 : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
rw : CompleteSpace R ↔ CompleteSpace S
⊢ IsPrecomplete (R := S) (Ideal.map e I) S ↔ IsPrecomplete I R

Tactic:
rw [iff_comm, IsAdic.isPrecomplete_iff (by rfl), IsAdic.isPrecomplete_iff (by rfl)]

Premises used: IsAdic.isPrecomplete_iff, iff_comm
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
e : R ≃+* S
this_1 : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ IsUniformEmbedding.{u_1, u_2} (α := R) (β := S) (⇑(↑(WithIdeal.uniformEquiv e ⋯) : R ≃ S) : (a : R) → S)

Tactic:
simpa using UniformEquiv.isUniformEmbedding ..

Premises used: UniformEquiv.isUniformEmbedding
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
e : R ≃+* S
this_1 : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ CompleteSpace R ↔ CompleteSpace S

Tactic:
exact completeSpace_congr (e := WithIdeal.uniformEquiv e rfl) (by
    simpa using UniformEquiv.isUniformEmbedding ..)

Premises used: completeSpace_congr
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
e : R ≃+* S
this_1 : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
rw : T2Space R ↔ T2Space S
⊢ IsHausdorff (R := S) (Ideal.map e I) S ↔ IsHausdorff I R

Tactic:
rw [iff_comm, IsAdic.isHausdorff_iff rfl, IsAdic.isHausdorff_iff rfl]

Premises used: iff_comm, IsAdic.isHausdorff_iff, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
e : R ≃+* S
this_1 : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ T2Space R ↔ T2Space S

Tactic:
⟨fun _ ↦ (WithIdeal.uniformEquiv e rfl).toHomeomorph.t2Space, fun _ ↦
    (WithIdeal.uniformEquiv e rfl).toHomeomorph.symm.t2Space⟩

Premises used: UniformEquiv.toHomeomorph, WithIdeal.uniformEquiv, Homeomorph.symm, Iff.intro, Homeomorph.t2Space, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
e : R ≃+* S
this_1 : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ T2Space R ↔ T2Space S

Tactic:
exact ⟨fun _ ↦ (WithIdeal.uniformEquiv e rfl).toHomeomorph.t2Space, fun _ ↦
    (WithIdeal.uniformEquiv e rfl).toHomeomorph.symm.t2Space⟩
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
e : R ≃+* S
⊢ IsAdicComplete (R := S) (Ideal.map e I) S ↔ IsAdicComplete I R

Tactic:
simp [isAdicComplete_iff, IsHausdorff.congr_ringEquiv, IsPrecomplete.congr_ringEquiv]

Premises used: IsPrecomplete.congr_ringEquiv, IsHausdorff.congr_ringEquiv, isAdicComplete_iff
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
t : Set B
⊢ LE.le (α := Subalgebra R (A × B)) (adjoin R (s ×ˢ t)) (Subalgebra.prod (adjoin R s) (adjoin R t))

Tactic:
adjoin_le <| Set.prod_mono subset_adjoin subset_adjoin

Premises used: Algebra.subset_adjoin, Algebra.adjoin_le, Set.prod_mono
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
t : Set B
a :
  LE.le (α := Subalgebra R (A × B))
    (adjoin R
      ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪
        (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1})))
    (Subalgebra.prod (adjoin R s) (adjoin R t))
a₁ :
  LE.le (α := Subalgebra R (A × B)) (Subalgebra.prod (adjoin R s) (adjoin R t))
    (adjoin R
      ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪
        (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1})))
⊢ Eq (α := Subalgebra R (A × B))
    (adjoin R
      ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪
        (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1})))
    (Subalgebra.prod (adjoin R s) (adjoin R t))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
t : Set B
⊢ LE.le (α := Subalgebra R (A × B))
    (adjoin R
      ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪
        (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1})))
    (Subalgebra.prod (adjoin R s) (adjoin R t))

Tactic:
simp only [adjoin_le_iff, Set.insert_subset_iff, Subalgebra.zero_mem, Subalgebra.one_mem,
      subset_adjoin, -- the rest comes from `squeeze_simp`
      Set.union_subset_iff,
      LinearMap.coe_inl, Set.mk_preimage_prod_right, Set.image_subset_iff, SetLike.mem_coe,
      Set.mk_preimage_prod_left, LinearMap.coe_inr, and_self_iff, Set.union_singleton,
      Subalgebra.coe_prod]

Premises used: LinearMap.coe_inr, Set.union_subset_iff, Subalgebra.zero_mem, Algebra.subset_adjoin, Set.mk_preimage_prod_left, Set.insert_subset_iff, LinearMap.coe_inl, Algebra.adjoin_le_iff, SetLike.mem_coe, Set.mk_preimage_prod_right, Set.image_subset_iff, and_self_iff, Subalgebra.one_mem, Set.union_singleton, Subalgebra.coe_prod
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ (↑(adjoin R s) : Set A)
hb : (a, b).2 ∈ (↑(adjoin R t) : Set B)
P : Subalgebra R (A × B) :=
  adjoin R
    ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪ (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1}))
⊢ Membership.mem (γ := Subalgebra R (A × B)) (adjoin R ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}))) (a, 0)

Tactic:
have Ha : (a, (0 : B)) ∈ adjoin R (LinearMap.inl R A B '' (s ∪ {1})) :=
      mem_adjoin_of_map_mul R LinearMap.inl_map_mul ha
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ (↑(adjoin R s) : Set A)
hb : (a, b).2 ∈ (↑(adjoin R t) : Set B)
P : Subalgebra R (A × B) :=
  adjoin R
    ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪ (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1}))
Ha :
  Membership.mem (γ := Subalgebra R (A × B)) (adjoin R ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}))) (a, 0)
⊢ Membership.mem (γ := Subalgebra R (A × B)) (adjoin R ((⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1}))) (0, b)

Tactic:
have Hb : ((0 : A), b) ∈ adjoin R (LinearMap.inr R A B '' (t ∪ {1})) :=
      mem_adjoin_of_map_mul R LinearMap.inr_map_mul hb
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ (↑(adjoin R s) : Set A)
hb : (a, b).2 ∈ (↑(adjoin R t) : Set B)
P : Subalgebra R (A × B) :=
  adjoin R
    ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪ (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1}))
Ha :
  Membership.mem (γ := Subalgebra R (A × B)) (adjoin R ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}))) (a, 0)
Hb :
  Membership.mem (γ := Subalgebra R (A × B)) (adjoin R ((⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1}))) (0, b)
⊢ (a, 0) ∈ P

Tactic:
replace Ha : (a, (0 : B)) ∈ P := adjoin_mono Set.subset_union_left Ha
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ (↑(adjoin R s) : Set A)
hb : (a, b).2 ∈ (↑(adjoin R t) : Set B)
P : Subalgebra R (A × B) :=
  adjoin R
    ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪ (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1}))
Hb :
  Membership.mem (γ := Subalgebra R (A × B)) (adjoin R ((⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1}))) (0, b)
Ha : (a, 0) ∈ P
⊢ (0, b) ∈ P

Tactic:
replace Hb : ((0 : A), b) ∈ P := adjoin_mono Set.subset_union_right Hb