awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Affine
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)))
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)
⊢ 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:
rw [this]
-- Module: Mathlib.Topology.Algebra.Affine
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)
      (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:
simp only [Homeomorph.comp_isOpenMap_iff, Homeomorph.comp_isOpenMap_iff']

Premises used: Homeomorph.comp_isOpenMap_iff, Homeomorph.comp_isOpenMap_iff'
-- Module: Mathlib.Topology.Algebra.Affine
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
simp : Continuous (Y := P) fun (pqt : P × P × R) ↦ pqt.2.2 • (pqt.2.1 -ᵥ pqt.1) +ᵥ pqt.1
⊢ Continuous (Y := P) fun (pqt : P × P × R) ↦ (lineMap pqt.1 pqt.2.1 : (a : R) → P) pqt.2.2

Tactic:
simp only [coe_lineMap]

Premises used: AffineMap.coe_lineMap
-- Module: Mathlib.Topology.Algebra.Affine
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) ↦ pqt.2.2 • (pqt.2.1 -ᵥ pqt.1) +ᵥ pqt.1

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Affine
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
p q : P
⊢ Continuous.{u_1, u_3} (X := R) (Y := P) (⇑(lineMap p q) : (a : R) → P)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Affine
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
α : Type u_6
l : Filter α
f₁ f₂ : α → P
g : α → R
p₁ p₂ : P
c : R
h₁ : Tendsto f₁ l (𝓝 p₁)
h₂ : Tendsto f₂ l (𝓝 p₂)
hg : Tendsto g l (𝓝 c)
⊢ Tendsto.{u_6, u_3} (β := P) (fun (x : α) ↦ ((lineMap (f₁ x) (f₂ x) : (a : R) → P) (g x) : P)) l
    (𝓝 ((lineMap p₁ p₂ : (a : R) → P) c) : Filter P)

Tactic:
(hg.smul (h₂.vsub h₁)).vadd h₁

Premises used: Filter.Tendsto.vsub, Filter.Tendsto.vadd, Filter.Tendsto.smul
-- Module: Mathlib.Topology.Algebra.Affine
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
α : Type u_6
l : Filter α
inst_9 : Invertible (α := R) 2
f₁ f₂ : α → P
p₁ p₂ : P
h₁ : Tendsto f₁ l (𝓝 p₁)
h₂ : Tendsto f₂ l (𝓝 p₂)
⊢ Tendsto (fun (x : α) ↦ midpoint R (f₁ x) (f₂ x)) l (𝓝 (midpoint R p₁ p₂))

Tactic:
h₁.lineMap h₂ tendsto_const_nhds

Premises used: Filter.Tendsto.lineMap, tendsto_const_nhds, midpoint
-- Module: Mathlib.Topology.Algebra.Affine
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
X : Type u_6
inst_9 : TopologicalSpace X
f₁ f₂ : X → P
g : X → R
s : Set X
x : X
h₁ : ContinuousWithinAt f₁ s x
h₂ : ContinuousWithinAt f₂ s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt.{u_6, u_3} (Y := P) (fun (x : X) ↦ (lineMap (f₁ x) (f₂ x) : (a : R) → P) (g x)) s x

Tactic:
Tendsto.lineMap h₁ h₂ hg

Premises used: Filter.Tendsto.lineMap, ContinuousWithinAt
-- Module: Mathlib.Topology.Algebra.Affine
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
X : Type u_6
inst_9 : TopologicalSpace X
f₁ f₂ : X → P
g : X → R
x : X
h₁ : ContinuousAt f₁ x
h₂ : ContinuousAt f₂ x
hg : ContinuousAt g x
⊢ ContinuousAt.{u_6, u_3} (Y := P) (fun (x : X) ↦ (AffineMap.lineMap (f₁ x) (f₂ x) : (a : R) → P) (g x)) x

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Affine
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
X : Type u_6
inst_9 : TopologicalSpace X
f₁ f₂ : X → P
g : X → R
s : Set X
h₁ : ContinuousOn f₁ s
h₂ : ContinuousOn f₂ s
hg : ContinuousOn g s
⊢ ContinuousOn.{u_6, u_3} (Y := P) (fun (x : X) ↦ (AffineMap.lineMap (f₁ x) (f₂ x) : (a : R) → P) (g x)) s

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Affine
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
X : Type u_6
inst_9 : TopologicalSpace X
f₁ f₂ : X → P
g : X → R
h₁ : Continuous[inst_9, inst_3] f₁
h₂ : Continuous[inst_9, inst_3] f₂
hg : Continuous[inst_9, inst_7] g
⊢ Continuous[inst_9, inst_3] fun (x : X) ↦ (AffineMap.lineMap (f₁ x) (f₂ x) : (a : R) → P) (g x)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Affine
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
rw : Continuous (Y := P) fun (p : P) ↦ t • (p -ᵥ x) +ᵥ x
⊢ Continuous.{u_3, u_3} (X := P) (Y := P) (⇑(homothety x t) : (a : P) → P)

Tactic:
rw [coe_homothety]

Premises used: AffineMap.coe_homothety
-- Module: Mathlib.Topology.Algebra.Affine
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 (Y := P) fun (p : P) ↦ t • (p -ᵥ x) +ᵥ x

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Affine
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
⊢ Continuous[inst_6, inst_3] fun (δ : R) ↦ (homothety x δ : (a : Q) → Q) y

Tactic:
have cont : Continuous (fun δ : R => homothety x δ y) := lineMap_continuous
-- Module: Mathlib.Topology.Algebra.Affine
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
⊢ (homothety x 1 : (a : Q) → Q) y = y

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Affine
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
a : R
h : 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:
interior_subset h

Premises used: interior_subset
-- Module: Mathlib.Topology.Algebra.Affine
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
h₁ h₂ :
  ∀ (a : R) (h : 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)
⊢ ∀ᶠ (δ : R) in 𝓝 1, Membership.mem (α := Q) s ((homothety x δ : (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

Premises used: IsOpen.eventually_mem, isOpen_interior, Filter.Tendsto.eventually, Continuous.tendsto', OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Affine
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)
simp_rw : ∀ᶠ (δ : R) in 𝓝 1, t ⊆ (⇑(homothety x δ) : (a : Q) → Q) ⁻¹' s
⊢ ∀ᶠ (δ : R) in 𝓝 1, (⇑(homothety x δ) : (a : Q) → Q) '' t ⊆ s

Tactic:
simp_rw [Set.image_subset_iff]

Premises used: Set.image_subset_iff
-- Module: Mathlib.Topology.Algebra.Affine
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, t ⊆ (⇑(homothety x δ) : (a : Q) → Q) ⁻¹' s

Tactic:
(Filter.eventually_all_finite ht).mpr this

Premises used: Iff.mpr, Set.Subset, Filter.eventually_all_finite
-- Module: Mathlib.Topology.Algebra.Affine
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, t ⊆ (⇑(homothety x δ) : (a : Q) → Q) ⁻¹' s

Tactic:
exact (Filter.eventually_all_finite ht).mpr this

Premises used: Iff.mpr, Filter.eventually_all_finite
-- Module: Mathlib.Topology.Algebra.Affine
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
suffices : ∀ 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

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
-- Module: Mathlib.Topology.Algebra.Affine
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
y : Q
hy : y ∈ t
⊢ ∀ᶠ (δ : R) in 𝓝 1, Membership.mem (α := Q) s ((homothety x δ : (a : Q) → Q) y : Q)

Tactic:
eventually_homothety_mem_of_mem_interior R x (h hy)

Premises used: eventually_homothety_mem_of_mem_interior
-- Module: Mathlib.Topology.Algebra.Affine
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
y : Q
hy : y ∈ t
⊢ ∀ᶠ (δ : R) in 𝓝 1, Membership.mem (α := Q) s ((homothety x δ : (a : Q) → Q) y : Q)

Tactic:
exact eventually_homothety_mem_of_mem_interior R x (h hy)

Premises used: eventually_homothety_mem_of_mem_interior
-- Module: Mathlib.Topology.Algebra.Affine
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)
r_inv :
  Function.RightInverse.{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)

Tactic:
apply IsOpenMap.of_inverse (homothety_continuous x t⁻¹)

Premises used: AffineMap.homothety_continuous, IsOpenMap.of_inverse, Inv.inv
-- Module: Mathlib.Topology.Algebra.Affine
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
e : P
⊢ (homothety x t : (a : P) → P) ((homothety x t⁻¹ : (a : P) → P) e : P) = e

Tactic:
simp [← AffineMap.comp_apply, ← homothety_mul, ht]

Premises used: AffineMap.comp_apply, AffineMap.homothety_mul
-- Module: Mathlib.Topology.Algebra.Affine
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
e : P
⊢ (homothety x t⁻¹ : (a : P) → P) ((homothety x t : (a : P) → P) e : P) = e

Tactic:
simp [← AffineMap.comp_apply, ← homothety_mul, ht]

Premises used: AffineMap.comp_apply, AffineMap.homothety_mul
-- Module: Mathlib.Topology.Algebra.AffineSubspace
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
s : AffineSubspace R P
inst_5 : Nonempty.{u_3 + 1} ↥s
⊢ Eq.{u_3 + 1} (α := (a : ↥s) → P) (⇑s.subtypeA : (a : ↥s) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ s))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.AffineSubspace
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
s : AffineSubspace R P
inst_5 : Nonempty.{u_3 + 1} ↥s
⊢ Eq (α := ↥s →ᵃ[R] P) (↑s.subtypeA : ↥s →ᵃ[R] P) s.subtype

Tactic:
rfl

Premises used: AffineSubspace.subtype, rfl
-- Module: Mathlib.Topology.Algebra.AffineSubspace
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
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)
⊢ Continuous (Y := ↥s) fun (p : Prod.{u_2, u_3} ↥s.direction ↥s) ↦ p.1 +ᵥ p.2

Tactic:
rw [Topology.IsEmbedding.subtypeVal.continuous_iff]

Premises used: Topology.IsEmbedding.subtypeVal, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Algebra.AffineSubspace
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 (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:
fun_prop
-- Module: Mathlib.Topology.Algebra.AffineSubspace
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
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)
⊢ Continuous.{u_3, u_2} (Y := ↥s.direction) fun (x : ↥s × ↥s) ↦ x.1 -ᵥ x.2

Tactic:
rw [Topology.IsEmbedding.subtypeVal.continuous_iff]

Premises used: Topology.IsEmbedding.subtypeVal, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Algebra.AffineSubspace
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} (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:
fun_prop
-- Module: Mathlib.Topology.Algebra.AffineSubspace
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)
inr : ∀ (x : P) (hx : x ∈ (↑s : Set P)), IsClosed (↑s.direction : Set V) ↔ IsClosed (↑s : Set P)
⊢ IsClosed (↑s.direction : Set V) ↔ IsClosed (↑s : Set P)

Tactic:
rcases s.eq_bot_or_nonempty with (rfl | ⟨x, hx⟩)

Premises used: AffineSubspace.eq_bot_or_nonempty, rfl
-- Module: Mathlib.Topology.Algebra.AffineSubspace
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
⊢ IsClosed (↑(direction.{u_1, u_2, u_3} (P := P) ⊥) : Set V) ↔ IsClosed (↑⊥ : Set P)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.AffineSubspace
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)
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))
⊢ IsClosed (↑s.direction : Set V) ↔ IsClosed (↑s : Set P)

Tactic:
rw [← (Homeomorph.vaddConst x).symm.isClosed_image,
    AffineSubspace.coe_direction_eq_vsub_set_right hx]

Premises used: Homeomorph.isClosed_image, Homeomorph.symm, AffineSubspace.coe_direction_eq_vsub_set_right, Homeomorph.vaddConst
-- Module: Mathlib.Topology.Algebra.AffineSubspace
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.{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:
simp only [Homeomorph.vaddConst_symm_apply]

Premises used: Homeomorph.vaddConst_symm_apply
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
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
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
⊢ f = g

Tactic:
obtain ⟨f', _⟩ := f