awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
ι_1 : Sort u_1
κ : ι_1 → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
ι : Type u_5
inst_4 : Finite ι
X : ι → Type u_6
inst_5 : (i : ι) → TopologicalSpace (X i)
inst_6 : ∀ (i : ι), AlexandrovDiscrete.{u_6} (X i)
simp_rw : ∀ (a : (i : ι) → X i), 𝓝 a = 𝓟 (nhdsKer {a})
⊢ AlexandrovDiscrete ((i : ι) → X i)
have simp_rw₁ : ∀ (a : (i : ι) → X i), Eq (α := Filter ((i : ι) → X i)) (Filter.pi (α := X) fun (i : ι) ↦ 𝓝 (a i)) (𝓟 (nhdsKer {a}))
Tactic: simp_rw [alexandrovDiscrete_iff_nhds, nhds_pi, ← principal_nhdsKer_singleton,
    pi_principal, nhdsKer_singleton_pi, forall_true_iff]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
ι_1 : Sort u_1
κ : ι_1 → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
ι : Type u_5
inst_4 : Finite ι
X : ι → Type u_6
inst_5 : (i : ι) → TopologicalSpace (X i)
inst_6 : ∀ (i : ι), AlexandrovDiscrete.{u_6} (X i)
simp_rw : ∀ (a : (i : ι) → X i), 𝓝 a = 𝓟 (nhdsKer {a})
simp_rw₁ :
  ∀ (a : (i : ι) → X i), Eq (α := Filter ((i : ι) → X i)) (Filter.pi (α := X) fun (i : ι) ↦ 𝓝 (a i)) (𝓟 (nhdsKer {a}))
⊢ AlexandrovDiscrete ((i : ι) → X i)
have simp_rw₂ : ∀ (a : (i : ι) → X i),
  Eq (α := Filter ((i : ι) → X i)) (Filter.pi (α := X) fun (i : ι) ↦ 𝓟 (nhdsKer {a i})) (𝓟 (nhdsKer {a}))
Tactic: simp_rw [alexandrovDiscrete_iff_nhds, nhds_pi, ← principal_nhdsKer_singleton,
    pi_principal, nhdsKer_singleton_pi, forall_true_iff]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
ι_1 : Sort u_1
κ : ι_1 → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
ι : Type u_5
inst_4 : Finite ι
X : ι → Type u_6
inst_5 : (i : ι) → TopologicalSpace (X i)
inst_6 : ∀ (i : ι), AlexandrovDiscrete.{u_6} (X i)
simp_rw : ∀ (a : (i : ι) → X i), 𝓝 a = 𝓟 (nhdsKer {a})
simp_rw₁ :
  ∀ (a : (i : ι) → X i), Eq (α := Filter ((i : ι) → X i)) (Filter.pi (α := X) fun (i : ι) ↦ 𝓝 (a i)) (𝓟 (nhdsKer {a}))
simp_rw₂ :
  ∀ (a : (i : ι) → X i),
    Eq (α := Filter ((i : ι) → X i)) (Filter.pi (α := X) fun (i : ι) ↦ 𝓟 (nhdsKer {a i})) (𝓟 (nhdsKer {a}))
⊢ AlexandrovDiscrete ((i : ι) → X i)
have simp_rw₃ : ∀ (a : (i : ι) → X i),
  Eq (α := Filter ((i : ι) → X i)) (𝓟 (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer {a i})) (𝓟 (nhdsKer {a}))
Tactic: simp_rw [alexandrovDiscrete_iff_nhds, nhds_pi, ← principal_nhdsKer_singleton,
    pi_principal, nhdsKer_singleton_pi, forall_true_iff]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
ι_1 : Sort u_1
κ : ι_1 → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
ι : Type u_5
inst_4 : Finite ι
X : ι → Type u_6
inst_5 : (i : ι) → TopologicalSpace (X i)
inst_6 : ∀ (i : ι), AlexandrovDiscrete.{u_6} (X i)
simp_rw : ∀ (a : (i : ι) → X i), 𝓝 a = 𝓟 (nhdsKer {a})
simp_rw₁ :
  ∀ (a : (i : ι) → X i), Eq (α := Filter ((i : ι) → X i)) (Filter.pi (α := X) fun (i : ι) ↦ 𝓝 (a i)) (𝓟 (nhdsKer {a}))
simp_rw₂ :
  ∀ (a : (i : ι) → X i),
    Eq (α := Filter ((i : ι) → X i)) (Filter.pi (α := X) fun (i : ι) ↦ 𝓟 (nhdsKer {a i})) (𝓟 (nhdsKer {a}))
simp_rw₃ :
  ∀ (a : (i : ι) → X i),
    Eq (α := Filter ((i : ι) → X i)) (𝓟 (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer {a i})) (𝓟 (nhdsKer {a}))
⊢ AlexandrovDiscrete ((i : ι) → X i)
have simp_rw₄ : ∀ (a : (i : ι) → X i), True
Tactic: simp_rw [alexandrovDiscrete_iff_nhds, nhds_pi, ← principal_nhdsKer_singleton,
    pi_principal, nhdsKer_singleton_pi, forall_true_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
inst_10 : Ring R
inst_11 : Module R V
inst_12 : Module R W
f : P →ᵃ[R] Q
⊢ Continuous.{u_2, u_4} (X := V) (Y := W) (⇑f.linear : (a : V) → W) ↔
    Continuous.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)
have inhabit : ∀ (inhabited_h : Inhabited P),
  Continuous.{u_2, u_4} (X := V) (Y := W) (⇑f.linear : (a : V) → W) ↔
    Continuous.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)
Tactic: inhabit P
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
inst_10 : Ring R
inst_11 : Module R V
inst_12 : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
⊢ Eq (α := (a : V) → W) (⇑f.linear : (a : V) → W)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
      (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
        (⇑(Homeomorph.vaddConst default) : (a : V) → P)))
have h : ∀ (v : V),
  Eq.{u_4 + 1} (α := W) ((f.linear : (a : V) → W) v : W)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
        (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
        (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
          (⇑(Homeomorph.vaddConst default) : (a : V) → P))
        v :
      W)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
inst_10 : Ring R
inst_11 : Module R V
inst_12 : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
⊢ Continuous.{u_2, u_4} (X := V) (Y := W) (⇑f.linear : (a : V) → W) ↔
    Continuous.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)
have this : Eq (α := (a : V) → W) (⇑f.linear : (a : V) → W)
  (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
    (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
    (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
      (⇑(Homeomorph.vaddConst default) : (a : V) → P)))
Tactic: have :
    (f.linear : V → W) =
      (Homeomorph.vaddConst <| f default).symm ∘ f ∘ (Homeomorph.vaddConst default) := by
    ext v
    simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
inst_10 : Ring R
inst_11 : Module R V
inst_12 : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
this :
  Eq (α := (a : V) → W) (⇑f.linear : (a : V) → W)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
      (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
        (⇑(Homeomorph.vaddConst default) : (a : V) → P)))
⊢ Continuous.{u_2, u_4} (X := V) (Y := W) (⇑f.linear : (a : V) → W) ↔
    Continuous.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)
have rw : Continuous.{u_2, u_4} (X := V) (Y := W)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
      (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
        (⇑(Homeomorph.vaddConst default) : (a : V) → P))) ↔
  Continuous.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
inst_10 : Ring R
inst_11 : Module R V
inst_12 : Module R W
f : P →ᵃ[R] Q
⊢ IsOpenMap.{u_2, u_4} (X := V) (Y := W) (⇑f.linear : (a : V) → W) ↔
    IsOpenMap.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)
have inhabit : ∀ (inhabited_h : Inhabited P),
  IsOpenMap.{u_2, u_4} (X := V) (Y := W) (⇑f.linear : (a : V) → W) ↔
    IsOpenMap.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)
Tactic: inhabit P
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
inst_10 : Ring R
inst_11 : Module R V
inst_12 : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
⊢ IsOpenMap.{u_2, u_4} (X := V) (Y := W) (⇑f.linear : (a : V) → W) ↔
    IsOpenMap.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)
have this : Eq (α := (a : V) → W) (⇑f.linear : (a : V) → W)
  (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
    (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
    (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
      (⇑(Homeomorph.vaddConst default) : (a : V) → P)))
Tactic: have :
    (f.linear : V → W) =
      (Homeomorph.vaddConst <| f default).symm ∘ f ∘ (Homeomorph.vaddConst default) := by
    ext v
    simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
inst_10 : Ring R
inst_11 : Module R V
inst_12 : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
this :
  Eq (α := (a : V) → W) (⇑f.linear : (a : V) → W)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
      (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
        (⇑(Homeomorph.vaddConst default) : (a : V) → P)))
⊢ IsOpenMap.{u_2, u_4} (X := V) (Y := W) (⇑f.linear : (a : V) → W) ↔
    IsOpenMap.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)
have rw : IsOpenMap.{u_2, u_4} (X := V) (Y := W)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
      (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
        (⇑(Homeomorph.vaddConst default) : (a : V) → P))) ↔
  IsOpenMap.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : Ring R
inst_6 : Module R V
inst_7 : TopologicalSpace R
inst_8 : ContinuousSMul R V
⊢ Continuous (Y := P) fun (pqt : P × P × R) ↦ (lineMap pqt.1 pqt.2.1 : (a : R) → P) pqt.2.2
have simp : Continuous (Y := P) fun (pqt : P × P × R) ↦ pqt.2.2 • (pqt.2.1 -ᵥ pqt.1) +ᵥ pqt.1
Tactic: simp only [coe_lineMap]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : CommRing R
inst_6 : Module R V
inst_7 : ContinuousConstSMul R V
x : P
t : R
⊢ Continuous.{u_3, u_3} (X := P) (Y := P) (⇑(homothety x t) : (a : P) → P)
have rw : Continuous (Y := P) fun (p : P) ↦ t • (p -ᵥ x) +ᵥ x
Tactic: rw [coe_homothety]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (hypothesis)
Goal:
R : Type u_1
W : Type u_4
Q : Type u_5
inst : AddCommGroup W
inst_1 : TopologicalSpace W
inst_2 : AddTorsor W Q
inst_3 : TopologicalSpace Q
inst_4 : IsTopologicalAddTorsor Q
inst_5 : CommRing R
inst_6 : TopologicalSpace R
inst_7 : Module R W
inst_8 : ContinuousSMul R W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
⊢ ∀ᶠ (δ : R) in 𝓝 1, Membership.mem (α := Q) s ((homothety x δ : (a : Q) → Q) y : Q)
have cont : Continuous[inst_6, inst_3] fun (δ : R) ↦ (homothety x δ : (a : Q) → Q) y
Tactic: have cont : Continuous (fun δ : R => homothety x δ y) := lineMap_continuous
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (goal)
Goal:
R : Type u_1
W : Type u_4
Q : Type u_5
inst : AddCommGroup W
inst_1 : TopologicalSpace W
inst_2 : AddTorsor W Q
inst_3 : TopologicalSpace Q
inst_4 : IsTopologicalAddTorsor Q
inst_5 : CommRing R
inst_6 : TopologicalSpace R
inst_7 : Module R W
inst_8 : ContinuousSMul R W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
cont : Continuous[inst_6, inst_3] fun (δ : R) ↦ (homothety x δ : (a : Q) → Q) y
⊢ ∀ᶠ (δ : R) in 𝓝 1, Membership.mem (α := Q) s ((homothety x δ : (a : Q) → Q) y : Q)
have h : ∀ (a : R),
  Membership.mem (γ := Set R)
    {x_1 : R |
      Membership.mem (γ := Set R)
          {x_2 : R | (fun (x_3 : R) ↦ Membership.mem (α := Q) (interior s) ((homothety x x_3 : (a : Q) → Q) y : Q)) x_2}
          x_1 →
        Membership.mem (γ := Set R)
          {x_2 : R | (fun (δ : R) ↦ Membership.mem (α := Q) s ((homothety x δ : (a : Q) → Q) y : Q)) x_2} x_1}
    a
Tactic: filter_upwards [cont.tendsto' 1 y (by simp) |>.eventually (isOpen_interior.eventually_mem hy)]
    with _ h using interior_subset h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (goal)
Goal:
R : Type u_1
W : Type u_4
Q : Type u_5
inst : AddCommGroup W
inst_1 : TopologicalSpace W
inst_2 : AddTorsor W Q
inst_3 : TopologicalSpace Q
inst_4 : IsTopologicalAddTorsor Q
inst_5 : CommRing R
inst_6 : TopologicalSpace R
inst_7 : Module R W
inst_8 : ContinuousSMul R W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
cont : Continuous[inst_6, inst_3] fun (δ : R) ↦ (homothety x δ : (a : Q) → Q) y
h :
  ∀ (a : R),
    Membership.mem (γ := Set R)
      {x_1 : R |
        Membership.mem (γ := Set R)
            {x_2 : R |
              (fun (x_3 : R) ↦ Membership.mem (α := Q) (interior s) ((homothety x x_3 : (a : Q) → Q) y : Q)) x_2}
            x_1 →
          Membership.mem (γ := Set R)
            {x_2 : R | (fun (δ : R) ↦ Membership.mem (α := Q) s ((homothety x δ : (a : Q) → Q) y : Q)) x_2} x_1}
      a
⊢ ∀ᶠ (δ : R) in 𝓝 1, Membership.mem (α := Q) s ((homothety x δ : (a : Q) → Q) y : Q)
have h₁ : ∀ (a : R),
  Membership.mem (α := Q) (interior s) ((homothety x a : (a : Q) → Q) y : Q) →
    Membership.mem (α := Q) s ((homothety x a : (a : Q) → Q) y : Q)
Tactic: filter_upwards [cont.tendsto' 1 y (by simp) |>.eventually (isOpen_interior.eventually_mem hy)]
    with _ h using interior_subset h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (goal)
Goal:
R : Type u_1
W : Type u_4
Q : Type u_5
inst : AddCommGroup W
inst_1 : TopologicalSpace W
inst_2 : AddTorsor W Q
inst_3 : TopologicalSpace Q
inst_4 : IsTopologicalAddTorsor Q
inst_5 : CommRing R
inst_6 : TopologicalSpace R
inst_7 : Module R W
inst_8 : ContinuousSMul R W
x : Q
s t : Set Q
ht : t.Finite
h : t ⊆ interior s
this : ∀ y ∈ t, ∀ᶠ (δ : R) in 𝓝 1, Membership.mem (α := Q) s ((homothety x δ : (a : Q) → Q) y : Q)
⊢ ∀ᶠ (δ : R) in 𝓝 1, (⇑(homothety x δ) : (a : Q) → Q) '' t ⊆ s
have simp_rw : ∀ᶠ (δ : R) in 𝓝 1, t ⊆ (⇑(homothety x δ) : (a : Q) → Q) ⁻¹' s
Tactic: simp_rw [Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (goal)
Goal:
R : Type u_1
W : Type u_4
Q : Type u_5
inst : AddCommGroup W
inst_1 : TopologicalSpace W
inst_2 : AddTorsor W Q
inst_3 : TopologicalSpace Q
inst_4 : IsTopologicalAddTorsor Q
inst_5 : CommRing R
inst_6 : TopologicalSpace R
inst_7 : Module R W
inst_8 : ContinuousSMul R W
x : Q
s t : Set Q
ht : t.Finite
h : t ⊆ interior s
⊢ ∀ᶠ (δ : R) in 𝓝 1, (⇑(homothety x δ) : (a : Q) → Q) '' t ⊆ s
have suffices : ∀ y ∈ t, ∀ᶠ (δ : R) in 𝓝 1, Membership.mem (α := Q) s ((homothety x δ : (a : Q) → Q) y : Q)
Tactic: suffices ∀ y ∈ t, ∀ᶠ δ in 𝓝 (1 : R), homothety x δ y ∈ s by
    simp_rw [Set.image_subset_iff]
    exact (Filter.eventually_all_finite ht).mpr this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : Field R
inst_6 : Module R V
inst_7 : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
⊢ IsOpenMap.{u_3, u_3} (X := P) (Y := P) (⇑(homothety x t) : (a : P) → P)
have l_inv : Function.LeftInverse.{u_3 + 1, u_3 + 1} (α := P) (β := P) (⇑(homothety x t) : (a : P) → P)
  (⇑(homothety x t⁻¹) : (a : P) → P)
Tactic: apply IsOpenMap.of_inverse (homothety_continuous x t⁻¹)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Affine (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : Field R
inst_6 : Module R V
inst_7 : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
l_inv :
  Function.LeftInverse.{u_3 + 1, u_3 + 1} (α := P) (β := P) (⇑(homothety x t) : (a : P) → P)
    (⇑(homothety x t⁻¹) : (a : P) → P)
⊢ IsOpenMap.{u_3, u_3} (X := P) (Y := P) (⇑(homothety x t) : (a : P) → P)
have r_inv : Function.RightInverse.{u_3 + 1, u_3 + 1} (α := P) (β := P) (⇑(homothety x t) : (a : P) → P)
  (⇑(homothety x t⁻¹) : (a : P) → P)
Tactic: apply IsOpenMap.of_inverse (homothety_continuous x t⁻¹)
-- Lean 4 proof step from Mathlib.Topology.Algebra.AffineSubspace (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : IsTopologicalAddTorsor P
s : AffineSubspace R P
inst_7 : Nonempty.{u_3 + 1} ↥s
⊢ Continuous (Y := ↥s) fun (p : Prod.{u_2, u_3} ↥s.direction ↥s) ↦ p.1 +ᵥ p.2
have rw : Continuous (X := Prod.{u_2, u_3} ↥s.direction ↥s) (Y := P)
  (Function.comp (β := ↥s) (Subtype.val (p := fun (x : P) ↦ x ∈ s)) fun (p : Prod.{u_2, u_3} ↥s.direction ↥s) ↦
    p.1 +ᵥ p.2)
Tactic: rw [Topology.IsEmbedding.subtypeVal.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AffineSubspace (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : IsTopologicalAddTorsor P
s : AffineSubspace R P
inst_7 : Nonempty.{u_3 + 1} ↥s
⊢ Continuous.{u_3, u_2} (Y := ↥s.direction) fun (x : ↥s × ↥s) ↦ x.1 -ᵥ x.2
have rw : Continuous.{u_3, u_2} (X := ↥s × ↥s) (Y := V)
  (Function.comp (β := ↥s.direction) (Subtype.val (p := fun (x : V) ↦ x ∈ s.direction)) fun (x : ↥s × ↥s) ↦ x.1 -ᵥ x.2)
Tactic: rw [Topology.IsEmbedding.subtypeVal.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AffineSubspace (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : IsTopologicalAddTorsor P
inst_7 : T1Space V
s : AffineSubspace R P
⊢ IsClosed (↑s.direction : Set V) ↔ IsClosed (↑s : Set P)
have inl : IsClosed (↑(direction.{u_1, u_2, u_3} (P := P) ⊥) : Set V) ↔ IsClosed (↑⊥ : Set P)
Tactic: rcases s.eq_bot_or_nonempty with (rfl | ⟨x, hx⟩)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.Algebra.AffineSubspace (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : IsTopologicalAddTorsor P
inst_7 : T1Space V
s : AffineSubspace R P
inl : IsClosed (↑(direction.{u_1, u_2, u_3} (P := P) ⊥) : Set V) ↔ IsClosed (↑⊥ : Set P)
⊢ IsClosed (↑s.direction : Set V) ↔ IsClosed (↑s : Set P)
have inr : ∀ (x : P) (hx : x ∈ (↑s : Set P)), IsClosed (↑s.direction : Set V) ↔ IsClosed (↑s : Set P)
Tactic: rcases s.eq_bot_or_nonempty with (rfl | ⟨x, hx⟩)
-- Lean 4 proof step from Mathlib.Topology.Algebra.AffineSubspace (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : IsTopologicalAddTorsor P
inst_7 : T1Space V
s : AffineSubspace R P
x : P
hx : x ∈ (↑s : Set P)
⊢ IsClosed (↑s.direction : Set V) ↔ IsClosed (↑s : Set P)
have inr : IsClosed.{u_2} (X := V) ((fun (x_1 : P) ↦ x_1 -ᵥ x) '' (↑s : Set P)) ↔
  IsClosed.{u_2} (X := V) ((⇑(Homeomorph.symm (Homeomorph.vaddConst x)) : (a : P) → V) '' (↑s : Set P))
Tactic: rw [← (Homeomorph.vaddConst x).symm.isClosed_image,
    AffineSubspace.coe_direction_eq_vsub_set_right hx]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
f g : A ≃A[R] B
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g
have obtain : ∀ (f' : A ≃ₐ[R] B) (continuous_toFun : Continuous[inst_2, inst_4] f'.toFun)
  (continuous_invFun : Continuous[inst_4, inst_2] f'.invFun)
  (h₁ :
    { toAlgEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
          A ≃A[R] B }.toFun =
      g.toFun)
  (h₂ :
    { toAlgEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
          A ≃A[R] B }.invFun =
      g.invFun),
  { toAlgEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun : A ≃A[R] B } = g
Tactic: obtain ⟨f', _⟩ := f
Cleared hypotheses: f, h₁, h₂