awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
⊢ Set.image.{u_2, u_3} (α := P₁) (⇑e : (a : P₁) → P₂) ((⇑e : (a : P₁) → P₂) ⁻¹' s) = s

Tactic:
e.surjective.image_preimage s

Premises used: ContinuousAffineEquiv.surjective, Function.Surjective.image_preimage
-- 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₁
⊢ Set.preimage.{u_2, u_3} (β := P₂) (⇑e : (a : P₁) → P₂) ((⇑e : (a : P₁) → P₂) '' s) = s

Tactic:
e.injective.preimage_image s

Premises used: ContinuousAffineEquiv.injective, Function.Injective.preimage_image
-- 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₁
⊢ Set.image.{u_3, u_2} (α := P₂) (⇑e.symm : (a : P₂) → P₁) ((⇑e : (a : P₁) → P₂) '' s) = s

Tactic:
e.toEquiv.symm_image_image s

Premises used: AffineEquiv.toEquiv, ContinuousAffineEquiv.toAffineEquiv, Equiv.symm_image_image
-- 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₂
⊢ Set.image.{u_2, u_3} (α := P₁) (⇑e : (a : P₁) → P₂) ((⇑e.symm : (a : P₂) → P₁) '' s) = s

Tactic:
e.symm.symm_image_image s

Premises used: ContinuousAffineEquiv.symm, ContinuousAffineEquiv.symm_image_image
-- 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₁) (symm (refl k P₁)) (refl k P₁)

Tactic:
rfl

Premises used: LinearEquiv.symm, ContinuousAffineEquiv.refl, AffineEquiv.symm, LinearEquiv.refl, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
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₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
e : P₁ ≃ᴬ[k] P₂
e' : P₂ ≃ᴬ[k] P₃
⊢ Eq (α := (a : P₁) → P₃) (⇑(e.trans e') : (a : P₁) → P₃)
    (comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := P₂) (⇑e' : (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
P₃ : Type u_4
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
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₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
e : P₁ ≃ᴬ[k] P₂
e' : P₂ ≃ᴬ[k] P₃
p : P₁
⊢ Eq.{u_4 + 1} (α := P₃) ((e.trans e' : (a : P₁) → P₃) p : P₃) ((e' : (a : P₂) → P₃) ((e : (a : P₁) → P₂) p : 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
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : AddCommGroup V₄
inst_14 : Module k V₄
inst_15 : AddTorsor V₄ P₄
inst_16 : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₂ ≃ᴬ[k] P₃
e₃ : P₃ ≃ᴬ[k] P₄
⊢ (e₁.trans e₂).trans e₃ = e₁.trans (e₂.trans e₃)

Tactic:
ext fun _ ↦ rfl

Premises used: ContinuousAffineEquiv.ext, 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.trans (refl k P₂) = e

Tactic:
ext fun _ ↦ rfl

Premises used: ContinuousAffineEquiv.ext, 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₂
⊢ trans (refl k P₁) e = e

Tactic:
ext fun _ ↦ rfl

Premises used: ContinuousAffineEquiv.ext, 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.trans e.symm = refl k P₁

Tactic:
ext e.symm_apply_apply

Premises used: ContinuousAffineEquiv.symm_apply_apply, ContinuousAffineEquiv.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₂
⊢ e.symm.trans e = refl k P₂

Tactic:
ext e.apply_symm_apply

Premises used: ContinuousAffineEquiv.apply_symm_apply, ContinuousAffineEquiv.ext
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
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₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
e : P₁ ≃ᴬ[k] P₂
e' : P₂ ≃ᴬ[k] P₃
⊢ (e.trans e').toContinuousAffineMap = e'.toContinuousAffineMap.comp e.toContinuousAffineMap

Tactic:
rfl

Premises used: ContinuousAffineEquiv.toContinuousAffineMap, ContinuousAffineMap.comp, AffineMap.comp, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
inst : Ring k
E : Type u_10
F : Type u_11
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module k F
inst_6 : TopologicalSpace F
e : E ≃L[k] F
⊢ Eq (α := (a : E) → F) (⇑e.toContinuousAffineEquiv : (a : E) → F) (⇑e : (a : E) → F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
inst : Ring k
E : Type u_10
F : Type u_11
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module k F
inst_6 : TopologicalSpace F
L : E ≃L[k] F
⊢ L.toContinuousAffineEquiv.toContinuousAffineMap = (↑L : E →L[k] F).toContinuousAffineMap

Tactic:
rfl

Premises used: ContinuousLinearMap.toContinuousAffineMap, ContinuousAffineEquiv.toContinuousAffineMap, 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₁
inst_5 : ContinuousConstVAdd V₁ P₁
v : V₁
⊢ Eq (α := P₁ ≃ᵃ[k] P₁) (↑(constVAdd k P₁ v) : P₁ ≃ᵃ[k] P₁) (AffineEquiv.constVAdd k P₁ v)

Tactic:
rfl

Premises used: AffineEquiv.constVAdd, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : AddCommGroup V₄
inst_14 : Module k V₄
inst_15 : AddTorsor V₄ P₄
inst_16 : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
dsimp : Continuous (Y := P₂ × P₄) fun (a : P₁ × P₃) ↦ ((e₁ : (a : P₁) → P₂) a.1, (e₂ : (a : P₃) → P₄) a.2)
⊢ Continuous (Y := P₂ × P₄) fun (a : P₁ × P₃) ↦ ((↑e₁ : P₁ ≃ᵃ[k] P₂).prodCongr (↑e₂ : P₃ ≃ᵃ[k] P₄)).toFun a

Tactic:
dsimp
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : AddCommGroup V₄
inst_14 : Module k V₄
inst_15 : AddTorsor V₄ P₄
inst_16 : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous (Y := P₂ × P₄) fun (a : P₁ × P₃) ↦ ((e₁ : (a : P₁) → P₂) a.1, (e₂ : (a : P₃) → P₄) a.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : AddCommGroup V₄
inst_14 : Module k V₄
inst_15 : AddTorsor V₄ P₄
inst_16 : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
dsimp : Continuous (Y := P₁ × P₃) fun (a : P₂ × P₄) ↦ ((e₁.symm : (a : P₂) → P₁) a.1, (e₂.symm : (a : P₄) → P₃) a.2)
⊢ Continuous (Y := P₁ × P₃) fun (a : P₂ × P₄) ↦ ((↑e₁ : P₁ ≃ᵃ[k] P₂).prodCongr (↑e₂ : P₃ ≃ᵃ[k] P₄)).invFun a

Tactic:
dsimp
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : AddCommGroup V₄
inst_14 : Module k V₄
inst_15 : AddTorsor V₄ P₄
inst_16 : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous (Y := P₁ × P₃) fun (a : P₂ × P₄) ↦ ((e₁.symm : (a : P₂) → P₁) a.1, (e₂.symm : (a : P₄) → P₃) a.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : AddCommGroup V₄
inst_14 : Module k V₄
inst_15 : AddTorsor V₄ P₄
inst_16 : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.prodCongr, Prod.map, AffineEquiv.symm, ContinuousAffineEquiv.prodCongr, AffineEquiv.prodCongr, ContinuousAffineEquiv.symm, Equiv.symm, Equiv.prodCongr, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : AddCommGroup V₄
inst_14 : Module k V₄
inst_15 : AddTorsor V₄ P₄
inst_16 : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
p : P₁ × P₃
⊢ Eq (α := P₂ × P₄) ((e₁.prodCongr e₂ : (a : P₁ × P₃) → P₂ × P₄) p : P₂ × P₄)
    (((e₁ : (a : P₁) → P₂) p.1, (e₂ : (a : P₃) → P₄) p.2) : P₂ × P₄)

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : AddCommGroup V₄
inst_14 : Module k V₄
inst_15 : AddTorsor V₄ P₄
inst_16 : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ (e₁.prodCongr e₂).toContinuousAffineMap = e₁.toContinuousAffineMap.prodMap e₂.toContinuousAffineMap

Tactic:
rfl

Premises used: AffineMap.prodMap, ContinuousAffineEquiv.toContinuousAffineMap, Prod.map, Function.prod, LinearMap.prod, ContinuousAffineMap.prodMap, rfl, LinearMap.prodMap
-- 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₂
⊢ Eq (α := P₂ × P₁ ≃ᴬ[k] P₁ × P₂) (symm (prodComm k P₁ P₂)) (prodComm k P₂ P₁)

Tactic:
rfl

Premises used: LinearEquiv.symm, Equiv.prodComm, ContinuousAffineEquiv.prodComm, AffineEquiv.symm, LinearEquiv.prodComm, ContinuousAffineEquiv.symm, AffineEquiv.prodComm, Prod.swap, Equiv.symm, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : AddCommGroup V₄
inst_14 : Module k V₄
inst_15 : AddTorsor V₄ P₄
inst_16 : TopologicalSpace P₄
⊢ Continuous (Y := P₁ × P₂ × P₃) fun (a : (P₁ × P₂) × P₃) ↦ (a.1.1, a.1.2, a.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : AddCommGroup V₄
inst_14 : Module k V₄
inst_15 : AddTorsor V₄ P₄
inst_16 : TopologicalSpace P₄
⊢ Continuous (Y := (P₁ × P₂) × P₃) fun (a : P₁ × P₂ × P₃) ↦ ((a.1, a.2.1), a.2.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
f g : P →ᴬ[R] Q
h : (↑f : P →ᵃ[R] Q) = (↑g : P →ᵃ[R] Q)
mk :
  ∀ (toAffineMap : P →ᵃ[R] Q) (cont : Continuous toAffineMap.toFun)
    (h : (↑{ toAffineMap := toAffineMap, cont := cont : P →ᴬ[R] Q } : P →ᵃ[R] Q) = (↑g : P →ᵃ[R] Q)),
    { toAffineMap := toAffineMap, cont := cont : P →ᴬ[R] Q } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
g : P →ᴬ[R] Q
toAffineMap : P →ᵃ[R] Q
cont : Continuous toAffineMap.toFun
h : (↑{ toAffineMap := toAffineMap, cont := cont : P →ᴬ[R] Q } : P →ᵃ[R] Q) = (↑g : P →ᵃ[R] Q)
mk :
  ∀ (toAffineMap_1 : P →ᵃ[R] Q) (cont_1 : Continuous toAffineMap_1.toFun)
    (h :
      (↑{ toAffineMap := toAffineMap, cont := cont : P →ᴬ[R] Q } : P →ᵃ[R] Q) =
        (↑{ toAffineMap := toAffineMap_1, cont := cont_1 : P →ᴬ[R] Q } : P →ᵃ[R] Q)),
    { toAffineMap := toAffineMap, cont := cont : P →ᴬ[R] Q } = { toAffineMap := toAffineMap_1, cont := cont_1 }
⊢ { toAffineMap := toAffineMap, cont := cont : P →ᴬ[R] Q } = g

Tactic:
cases g
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
toAffineMap : P →ᵃ[R] Q
cont : Continuous toAffineMap.toFun
toAffineMap_1 : P →ᵃ[R] Q
cont_1 : Continuous toAffineMap_1.toFun
h :
  (↑{ toAffineMap := toAffineMap, cont := cont : P →ᴬ[R] Q } : P →ᵃ[R] Q) =
    (↑{ toAffineMap := toAffineMap_1, cont := cont_1 : P →ᴬ[R] Q } : P →ᵃ[R] Q)
⊢ { toAffineMap := toAffineMap, cont := cont : P →ᴬ[R] Q } = { toAffineMap := toAffineMap_1, cont := cont_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
f : P →ᴬ[R] Q
⊢ (↑f : P →ᵃ[R] Q).toFun = (⇑f : (a : P) → Q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
⊢ Function.Injective (α := P →ᴬ[R] Q) (β := P → Q) (DFunLike.coe (β := fun (x : P) ↦ Q))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
f g : P →ᴬ[R] Q
h : ∀ (x : P), Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) x : Q) ((g : (a : P) → Q) x : Q)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
f g : P →ᴬ[R] Q
h : f = g
x : P
⊢ Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) x : Q) ((g : (a : P) → Q) x : Q)

Tactic:
DFunLike.congr_fun h _

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
f : P →ᴬ[R] Q
⊢ f.toContinuousMap = (↑f : C(P, Q))

Tactic:
rfl

Premises used: toContinuousMap, ContinuousAffineMap.toContinuousMap, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
f : P →ᴬ[R] Q
⊢ Eq (α := (a : P) → Q) (⇑(↑f : P →ᵃ[R] Q) : (a : P) → Q) (⇑f : (a : P) → Q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
f : P →ᴬ[R] Q
⊢ Eq (α := (a : P) → Q) (⇑(↑f : C(P, Q)) : (a : P) → Q) (⇑f : (a : P) → Q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
f g : P →ᴬ[R] Q
h : Eq (α := C(P, Q)) (↑f : C(P, Q)) (↑g : C(P, Q))
h₁ : ∀ (a : P), Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) a : Q) ((g : (a : P) → Q) a : Q)
⊢ f = g

Tactic:
ext a
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
f g : P →ᴬ[R] Q
h : Eq (α := C(P, Q)) (↑f : C(P, Q)) (↑g : C(P, Q))
a : P
⊢ Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) a : Q) ((g : (a : P) → Q) a : Q)

Tactic:
ContinuousMap.congr_fun h a

Premises used: ContinuousMap.congr_fun
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
f g : P →ᴬ[R] Q
h : Eq (α := C(P, Q)) (↑f : C(P, Q)) (↑g : C(P, Q))
a : P
⊢ Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) a : Q) ((g : (a : P) → Q) a : Q)

Tactic:
exact ContinuousMap.congr_fun h a

Premises used: ContinuousMap.congr_fun