awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf_inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hf : IsOpenMap.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap :
  IsOpenMap.{u_1, u_2} (X := M × Mᵐᵒᵖ) (Y := N × Nᵐᵒᵖ)
    (Prod.map (⇑f : (a : M) → N)
      (Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
        (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M))))
y : Nˣ
h_1 :
  ∃ (a : M) (a_1 : M),
    (a, op a_1) ∈ U ∧
      (f : (a : M) → N) a = (↑y : N) ∧
        Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
            (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op a_1) =
          op (↑y⁻¹ : N)
a b : M
h : (a, op b) ∈ U
ha : (f : (a : M) → N) a = (↑y : N)
hb :
  Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
      (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op b) =
    op (↑y⁻¹ : N)
⊢ ((↑{ val := a, inv := b, val_inv := ⋯, inv_val := ⋯ : Mˣ } : M),
        op (↑{ val := a, inv := b, val_inv := ⋯, inv_val := ⋯ : Mˣ }⁻¹ : M)) ∈
      U ∧
    (map f : (a : Mˣ) → Nˣ) { val := a, inv := b, val_inv := ⋯, inv_val := ⋯ } = y

Tactic:
simp_all
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf : IsInducing.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
⊢ IsInducing.{u_1, u_2} (X := Mˣ) (Y := Nˣ) (⇑(map f) : (a : Mˣ) → Nˣ)

Tactic:
.of_comp (continuous_map hf.continuous) continuous_embedProduct ?_

Premises used: Units.continuous_embedProduct, Units.continuous_map, Topology.IsInducing.continuous, Topology.IsInducing.of_comp
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf : IsInducing.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
refine :
  IsInducing.{u_1, u_2} (X := Mˣ) (Y := N × Nᵐᵒᵖ)
    (Function.comp (β := Nˣ) (⇑(embedProduct N) : (a : Nˣ) → N × Nᵐᵒᵖ) (⇑(map f) : (a : Mˣ) → Nˣ))
⊢ IsInducing.{u_1, u_2} (X := Mˣ) (Y := Nˣ) (⇑(map f) : (a : Mˣ) → Nˣ)

Tactic:
refine .of_comp (continuous_map hf.continuous) continuous_embedProduct ?_
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf : IsInducing.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
⊢ IsInducing.{u_1, u_2} (X := Mˣ) (Y := N × Nᵐᵒᵖ)
    (Function.comp (β := Nˣ) (⇑(embedProduct N) : (a : Nˣ) → N × Nᵐᵒᵖ) (⇑(map f) : (a : Mˣ) → Nˣ))

Tactic:
hf.prodMap (opHomeomorph.isInducing.comp <| hf.comp opHomeomorph.symm.isInducing)
    |>.comp isInducing_embedProduct

Premises used: Homeomorph.isInducing, MulOpposite.opHomeomorph, Topology.IsInducing.comp, Prod.map, Topology.IsInducing.prodMap, Homeomorph.symm, MulOpposite.unop, Units.isInducing_embedProduct, MulOpposite.op
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf : IsInducing.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
⊢ IsInducing.{u_1, u_2} (X := Mˣ) (Y := N × Nᵐᵒᵖ)
    (Function.comp (β := Nˣ) (⇑(embedProduct N) : (a : Nˣ) → N × Nᵐᵒᵖ) (⇑(map f) : (a : Mˣ) → Nˣ))

Tactic:
exact hf.prodMap (opHomeomorph.isInducing.comp <| hf.comp opHomeomorph.symm.isInducing)
    |>.comp isInducing_embedProduct

Premises used: Homeomorph.isInducing, MulOpposite.opHomeomorph, Topology.IsInducing.comp, Topology.IsInducing.prodMap, Homeomorph.symm, Units.isInducing_embedProduct
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf : IsEmbedding.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
⊢ IsEmbedding.{u_1, u_2} (X := Mˣ) (Y := Nˣ) (⇑(map f) : (a : Mˣ) → Nˣ)

Tactic:
.of_comp (continuous_map hf.continuous) continuous_embedProduct ?_

Premises used: Units.continuous_embedProduct, Units.continuous_map, Topology.IsEmbedding.of_comp, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf : IsEmbedding.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
refine :
  IsEmbedding.{u_1, u_2} (X := Mˣ) (Y := N × Nᵐᵒᵖ)
    (Function.comp (β := Nˣ) (⇑(embedProduct N) : (a : Nˣ) → N × Nᵐᵒᵖ) (⇑(map f) : (a : Mˣ) → Nˣ))
⊢ IsEmbedding.{u_1, u_2} (X := Mˣ) (Y := Nˣ) (⇑(map f) : (a : Mˣ) → Nˣ)

Tactic:
refine .of_comp (continuous_map hf.continuous) continuous_embedProduct ?_
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf : IsEmbedding.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
⊢ IsEmbedding.{u_1, u_2} (X := Mˣ) (Y := N × Nᵐᵒᵖ)
    (Function.comp (β := Nˣ) (⇑(embedProduct N) : (a : Nˣ) → N × Nᵐᵒᵖ) (⇑(map f) : (a : Mˣ) → Nˣ))

Tactic:
hf.prodMap (opHomeomorph.isEmbedding.comp <| hf.comp opHomeomorph.symm.isEmbedding)
    |>.comp isEmbedding_embedProduct

Premises used: MulOpposite.opHomeomorph, Homeomorph.isEmbedding, Topology.IsEmbedding.prodMap, Prod.map, Units.isEmbedding_embedProduct, Topology.IsEmbedding.comp, Homeomorph.symm, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf : IsEmbedding.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
⊢ IsEmbedding.{u_1, u_2} (X := Mˣ) (Y := N × Nᵐᵒᵖ)
    (Function.comp (β := Nˣ) (⇑(embedProduct N) : (a : Nˣ) → N × Nᵐᵒᵖ) (⇑(map f) : (a : Mˣ) → Nˣ))

Tactic:
exact hf.prodMap (opHomeomorph.isEmbedding.comp <| hf.comp opHomeomorph.symm.isEmbedding)
    |>.comp isEmbedding_embedProduct

Premises used: MulOpposite.opHomeomorph, Homeomorph.isEmbedding, Topology.IsEmbedding.prodMap, Units.isEmbedding_embedProduct, Topology.IsEmbedding.comp, Homeomorph.symm
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᵃ[k] P₂
econt : Continuous e.toFun
einv_cont : Continuous e.invFun
e' : P₁ ≃ᵃ[k] P₂
e'cont : Continuous e'.toFun
e'inv_cont : Continuous e'.invFun
H :
  { toAffineEquiv := e, continuous_toFun := econt, continuous_invFun := einv_cont : P₁ ≃ᴬ[k] P₂ }.toAffineEquiv =
    { toAffineEquiv := e', continuous_toFun := e'cont, continuous_invFun := e'inv_cont : P₁ ≃ᴬ[k] P₂ }.toAffineEquiv
⊢ { toAffineEquiv := e, continuous_toFun := econt, continuous_invFun := einv_cont : P₁ ≃ᴬ[k] P₂ } =
    { toAffineEquiv := e', continuous_toFun := e'cont, continuous_invFun := e'inv_cont }

Tactic:
congr
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
⊢ Eq (α := (a : P₁) → P₂) (⇑(↑e : P₁ ≃ᵃ[k] P₂) : (a : P₁) → P₂) (⇑e : (a : P₁) → P₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
⊢ Eq (α := (a : P₁) → P₂) (⇑(↑e : P₁ ≃ᵃ[k] P₂).toEquiv : (a : P₁) → P₂) (⇑e : (a : P₁) → P₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e e' : P₁ ≃ᴬ[k] P₂
h : ∀ (x : P₁), Eq.{u_3 + 1} (α := P₂) ((e : (a : P₁) → P₂) x : P₂) ((e' : (a : P₁) → P₂) x : P₂)
⊢ e = e'

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
⊢ Continuous.{u_2, u_3} (X := P₁) (Y := P₂) (⇑e : (a : P₁) → P₂)

Tactic:
e.2

Premises used: ContinuousAffineEquiv.continuous_toFun
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
⊢ Eq (α := (a : P₁) → P₂) (⇑e.toContinuousAffineMap : (a : P₁) → P₂) (⇑e : (a : P₁) → P₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e e' : P₁ ≃ᴬ[k] P₂
h : e.toContinuousAffineMap = e'.toContinuousAffineMap
h₁ : ∀ (p : P₁), Eq.{u_3 + 1} (α := P₂) ((e : (a : P₁) → P₂) p : P₂) ((e' : (a : P₁) → P₂) p : P₂)
⊢ e = e'

Tactic:
ext p
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e e' : P₁ ≃ᴬ[k] P₂
h : e.toContinuousAffineMap = e'.toContinuousAffineMap
p : P₁
h₁ :
  Eq.{u_3 + 1} (α := P₂) ((e.toContinuousAffineMap : (a : P₁) → P₂) p : P₂)
    ((e'.toContinuousAffineMap : (a : P₁) → P₂) p : P₂)
⊢ Eq.{u_3 + 1} (α := P₂) ((e : (a : P₁) → P₂) p : P₂) ((e' : (a : P₁) → P₂) p : P₂)

Tactic:
simp_rw [← coe_toContinuousAffineMap, h]

Premises used: ContinuousAffineEquiv.coe_toContinuousAffineMap
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
⊢ (↑e.toContinuousAffineMap : P₁ →ᵃ[k] P₂) = (↑(↑e : P₁ ≃ᵃ[k] P₂) : P₁ →ᵃ[k] P₂)

Tactic:
rfl

Premises used: AffineEquiv.toAffineMap, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
⊢ e.toContinuousAffineMap.toContinuousMap = (↑e.toHomeomorph : C(P₁, P₂))

Tactic:
rfl

Premises used: toContinuousMap, ContinuousAffineMap.toContinuousMap, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
⊢ Eq.{u_2 + 1} (α := (a : P₁) → P₁) (⇑(refl k P₁) : (a : P₁) → P₁) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
x : P₁
⊢ (refl k P₁ : (a : P₁) → P₁) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
⊢ Eq (α := P₁ ≃ᵃ[k] P₁) (↑(refl k P₁) : P₁ ≃ᵃ[k] P₁) (AffineEquiv.refl k P₁)

Tactic:
rfl

Premises used: AffineEquiv.refl, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
⊢ AffineEquiv.toEquiv (↑(refl k P₁) : P₁ ≃ᵃ[k] P₁) = Equiv.refl P₁

Tactic:
rfl

Premises used: Equiv.refl, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
⊢ (↑e.symm : P₂ ≃ᵃ[k] P₁) = (↑e : P₁ ≃ᵃ[k] P₂).symm

Tactic:
rfl

Premises used: AffineEquiv.symm, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
⊢ Eq (α := (a : P₂) → P₁) (⇑(↑e : P₁ ≃ᵃ[k] P₂).symm : (a : P₂) → P₁) (⇑e.symm : (a : P₂) → P₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
⊢ (↑e.symm : P₂ ≃ᵃ[k] P₁).toEquiv = (↑e : P₁ ≃ᵃ[k] P₂).symm

Tactic:
rfl

Premises used: Equiv.symm, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
p : P₂
⊢ (e : (a : P₁) → P₂) ((e.symm : (a : P₂) → P₁) p : P₁) = p

Tactic:
e.toEquiv.apply_symm_apply p

Premises used: Equiv.apply_symm_apply, AffineEquiv.toEquiv, ContinuousAffineEquiv.toAffineEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
p : P₁
⊢ (e.symm : (a : P₂) → P₁) ((e : (a : P₁) → P₂) p : P₂) = p

Tactic:
e.toEquiv.symm_apply_apply p

Premises used: Equiv.symm_apply_apply, AffineEquiv.toEquiv, ContinuousAffineEquiv.toAffineEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
p₁ : P₁
p₂ : P₂
⊢ (e : (a : P₁) → P₂) p₁ = p₂ ↔ p₁ = (e.symm : (a : P₂) → P₁) p₂

Tactic:
e.toEquiv.apply_eq_iff_eq_symm_apply

Premises used: AffineEquiv.toEquiv, ContinuousAffineEquiv.toAffineEquiv, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
p₁ p₂ : P₁
⊢ Eq.{u_3 + 1} (α := P₂) ((e : (a : P₁) → P₂) p₁ : P₂) ((e : (a : P₁) → P₂) p₂ : P₂) ↔ p₁ = p₂

Tactic:
e.toEquiv.apply_eq_iff_eq

Premises used: AffineEquiv.toEquiv, ContinuousAffineEquiv.toAffineEquiv, Equiv.apply_eq_iff_eq
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: LinearEquiv.symm, AffineEquiv.symm, ContinuousAffineEquiv.symm, Equiv.symm, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
⊢ Bijective (α := P₁ ≃ᴬ[k] P₂) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, And.intro, Exists.intro, ContinuousAffineEquiv.symm_symm
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
x : P₁
⊢ Eq.{u_3 + 1} (α := P₂) ((e.symm.symm : (a : P₁) → P₂) x : P₂) ((e : (a : P₁) → P₂) x : P₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
x : P₂
y : P₁
⊢ (e.symm : (a : P₂) → P₁) x = y ↔ x = (e : (a : P₁) → P₂) y

Tactic:
e.toAffineEquiv.symm_apply_eq

Premises used: Equiv.symm_apply_eq, AffineEquiv.toEquiv, ContinuousAffineEquiv.toAffineEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
x : P₂
y : P₁
⊢ y = (e.symm : (a : P₂) → P₁) x ↔ (e : (a : P₁) → P₂) y = x

Tactic:
e.toAffineEquiv.eq_symm_apply

Premises used: AffineEquiv.toEquiv, ContinuousAffineEquiv.toAffineEquiv, Equiv.eq_symm_apply
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
f : P₁ ≃ᴬ[k] P₂
s : Set P₂
⊢ Eq.{u_2 + 1} (α := Set P₁) ((⇑f.symm : (a : P₂) → P₁) '' s) ((⇑f : (a : P₁) → P₂) ⁻¹' s)

Tactic:
f.symm.toEquiv.image_eq_preimage_symm _

Premises used: ContinuousAffineEquiv.symm, Equiv.image_eq_preimage_symm, AffineEquiv.toEquiv, ContinuousAffineEquiv.toAffineEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
f : P₁ ≃ᴬ[k] P₂
s : Set P₁
⊢ Eq.{u_3 + 1} (α := Set P₂) ((⇑f.symm : (a : P₂) → P₁) ⁻¹' s) ((⇑f : (a : P₁) → P₂) '' s)

Tactic:
(f.symm.image_symm _).symm

Premises used: ContinuousAffineEquiv.symm, Eq.symm, ContinuousAffineEquiv.image_symm
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
⊢ Bijective.{u_2 + 1, u_3 + 1} (α := P₁) (β := P₂) (⇑e : (a : P₁) → P₂)

Tactic:
e.toEquiv.bijective

Premises used: Equiv.bijective, AffineEquiv.toEquiv, ContinuousAffineEquiv.toAffineEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
⊢ Surjective.{u_2 + 1, u_3 + 1} (α := P₁) (β := P₂) (⇑e : (a : P₁) → P₂)

Tactic:
e.toEquiv.surjective

Premises used: AffineEquiv.toEquiv, ContinuousAffineEquiv.toAffineEquiv, Equiv.surjective
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
⊢ Injective.{u_2 + 1, u_3 + 1} (α := P₁) (β := P₂) (⇑e : (a : P₁) → P₂)

Tactic:
e.toEquiv.injective

Premises used: AffineEquiv.toEquiv, ContinuousAffineEquiv.toAffineEquiv, Equiv.injective
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
s : Set P₁
⊢ Eq.{u_3 + 1} (α := Set P₂) ((⇑e : (a : P₁) → P₂) '' s) ((⇑e.symm : (a : P₂) → P₁) ⁻¹' s)

Tactic:
e.toEquiv.image_eq_preimage_symm s

Premises used: Equiv.image_eq_preimage_symm, AffineEquiv.toEquiv, ContinuousAffineEquiv.toAffineEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
s : Set P₂
rw : Eq.{u_2 + 1} (α := Set P₁) ((⇑e.symm.symm : (a : P₁) → P₂) ⁻¹' s) ((⇑e : (a : P₁) → P₂) ⁻¹' s)
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set P₁) ((⇑e : (a : P₁) → P₂) ⁻¹' s) ((⇑e : (a : P₁) → P₂) ⁻¹' s)
⊢ Eq.{u_2 + 1} (α := Set P₁) ((⇑e.symm : (a : P₂) → P₁) '' s) ((⇑e : (a : P₁) → P₂) ⁻¹' s)

Tactic:
rw [e.symm.image_eq_preimage_symm, e.symm_symm]

Premises used: ContinuousAffineEquiv.symm, ContinuousAffineEquiv.image_eq_preimage_symm, ContinuousAffineEquiv.symm_symm