awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ P₂
e : P₁ ≃ᵃ[k] P₂
⊢ e.symm.toEquiv = e.symm

Tactic:
rfl

Premises used: Equiv.symm, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ P₂
e : P₁ ≃ᵃ[k] P₂
⊢ Eq (α := (a : P₂) → P₁) (⇑e.symm : (a : P₂) → P₁) (⇑e.symm : (a : P₂) → P₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ P₂
e : P₁ ≃ᵃ[k] P₂
⊢ e.symm.linear = e.linear.symm

Tactic:
rfl

Premises used: LinearEquiv.symm, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ 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
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ 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, Equiv.surjective
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ 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, Equiv.injective
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Bijective.{u_2 + 1, u_3 + 1} (α := P₁) (β := P₂) (⇑φ : (a : P₁) → P₂)
⊢ (ofBijective hφ).symm.toEquiv = (Equiv.ofBijective (⇑φ : (a : P₁) → P₂) hφ).symm

Tactic:
rfl

Premises used: Equiv.symm, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ P₂
e : P₁ ≃ᵃ[k] P₂
⊢ Eq.{u_3 + 1} (α := Set P₂) (range.{u_3, u_2 + 1} (ι := P₁) (⇑e : (a : P₁) → P₂)) univ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ 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
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ 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
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ 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, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ 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:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ 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: AffineEquiv.symm, Equiv.image_eq_preimage_symm, AffineEquiv.toEquiv
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ 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: AffineEquiv.symm, AffineEquiv.image_symm, Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
⊢ Eq.{u_2 + 1} (α := (a : P₁) → P₁) (⇑(refl k P₁) : (a : P₁) → P₁) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
⊢ Eq (α := P₁ →ᵃ[k] P₁) (↑(refl k P₁) : P₁ →ᵃ[k] P₁) (AffineMap.id k P₁)

Tactic:
rfl

Premises used: AffineEquiv.toAffineMap, AffineMap.id, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
x : P₁
⊢ (refl k P₁ : (a : P₁) → P₁) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
⊢ toEquiv (refl k P₁) = Equiv.refl P₁

Tactic:
rfl

Premises used: Equiv.refl, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
⊢ Eq (α := V₁ ≃ₗ[k] V₁) (linear (refl k P₁)) (LinearEquiv.refl k V₁)

Tactic:
rfl

Premises used: LinearEquiv.refl, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
⊢ Eq (α := P₁ ≃ᵃ[k] P₁) (symm (refl k P₁)) (refl k P₁)

Tactic:
rfl

Premises used: LinearEquiv.symm, AffineEquiv.refl, AffineEquiv.symm, LinearEquiv.refl, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
e : P₁ ≃ᵃ[k] P₂
e' : P₂ ≃ᵃ[k] P₃
p : P₁
v : V₁
⊢ (e.trans e'.toEquiv : (a : P₁) → P₃) (v +ᵥ p) =
    HVAdd.hVAdd.{u_8, u_4, u_4} (α := V₃) (β := P₃) ((e.linear ≪≫ₗ e'.linear : (a : V₁) → V₃) v : V₃)
      ((e.trans e'.toEquiv : (a : P₁) → P₃) p : P₃)

Tactic:
simp only [LinearEquiv.trans_apply, coe_toEquiv, (· ∘ ·), Equiv.coe_trans, map_vadd]

Premises used: AffineEquiv.coe_toEquiv, Function.comp, AffineEquiv.map_vadd, LinearEquiv.trans_apply, Equiv.coe_trans
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : Module k V₁
inst_5 : Module k V₂
inst_6 : Module k V₃
inst_7 : AffineSpace V₁ P₁
inst_8 : AffineSpace V₂ P₂
inst_9 : AffineSpace V₃ 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.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : Module k V₁
inst_5 : Module k V₂
inst_6 : Module k V₃
inst_7 : AffineSpace V₁ P₁
inst_8 : AffineSpace V₂ P₂
inst_9 : AffineSpace V₃ P₃
e : P₁ ≃ᵃ[k] P₂
e' : P₂ ≃ᵃ[k] P₃
⊢ (↑(e.trans e') : P₁ →ᵃ[k] P₃) = (↑e' : P₂ →ᵃ[k] P₃).comp (↑e : P₁ →ᵃ[k] P₂)

Tactic:
rfl

Premises used: AffineEquiv.toAffineMap, AffineMap.comp, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : Module k V₁
inst_5 : Module k V₂
inst_6 : Module k V₃
inst_7 : AffineSpace V₁ P₁
inst_8 : AffineSpace V₂ P₂
inst_9 : AffineSpace V₃ 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.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ 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: AffineEquiv.ext, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ P₂
e : P₁ ≃ᵃ[k] P₂
⊢ e.trans (refl k P₂) = e

Tactic:
ext fun _ => rfl

Premises used: AffineEquiv.ext, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ P₂
e : P₁ ≃ᵃ[k] P₂
⊢ trans (refl k P₁) e = e

Tactic:
ext fun _ => rfl

Premises used: AffineEquiv.ext, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ P₂
e : P₁ ≃ᵃ[k] P₂
⊢ e.trans e.symm = refl k P₁

Tactic:
ext e.symm_apply_apply

Premises used: AffineEquiv.symm_apply_apply, AffineEquiv.ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ P₂
e : P₁ ≃ᵃ[k] P₂
⊢ e.symm.trans e = refl k P₂

Tactic:
ext e.apply_symm_apply

Premises used: AffineEquiv.apply_symm_apply, AffineEquiv.ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ P₂
e : P₁ ≃ᵃ[k] P₂
a b : P₁
c : k
⊢ Eq.{u_3 + 1} (α := P₂) ((e : (a : P₁) → P₂) ((AffineMap.lineMap a b : (a : k) → P₁) c : P₁) : P₂)
    (((AffineMap.lineMap ((e : (a : P₁) → P₂) a) ((e : (a : P₁) → P₂) b) : k →ᵃ[k] P₂) : (a : k) → P₂) c : P₂)

Tactic:
e.toAffineMap.apply_lineMap a b c

Premises used: AffineMap.apply_lineMap, AffineEquiv.toAffineMap
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
⊢ Eq (α := P₁ ≃ᵃ[k] P₁) 1 (refl k P₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
⊢ Eq.{u_2 + 1} (α := (a : P₁) → P₁) (⇑1 : (a : P₁) → P₁) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
e e' : P₁ ≃ᵃ[k] P₁
⊢ e * e' = e'.trans e

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
e e' : P₁ ≃ᵃ[k] P₁
⊢ Eq.{u_2 + 1} (α := (a : P₁) → P₁) (⇑(e * e') : (a : P₁) → P₁)
    (comp (β := P₁) (⇑e : (a : P₁) → P₁) (⇑e' : (a : P₁) → P₁))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
e : P₁ ≃ᵃ[k] P₁
⊢ e⁻¹ = e.symm

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
e₁ : P₁ ≃ᵃ[k] P₂
e₂ : P₃ ≃ᵃ[k] P₄
⊢ ∀ (p : P₁ × P₃) (v : V₁ × V₃),
    ((↑e₁ : P₁ ≃ P₂).prodCongr (↑e₂ : P₃ ≃ P₄) : (a : P₁ × P₃) → P₂ × P₄) (v +ᵥ p) =
      HVAdd.hVAdd (α := V₂ × V₄) (β := P₂ × P₄) ((e₁.linear.prodCongr e₂.linear : (a : V₁ × V₃) → V₂ × V₄) v : V₂ × V₄)
        (((↑e₁ : P₁ ≃ P₂).prodCongr (↑e₂ : P₃ ≃ P₄) : (a : P₁ × P₃) → P₂ × P₄) p : P₂ × P₄)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ 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, AffineEquiv.prodCongr, Equiv.symm, Equiv.prodCongr, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ 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.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
e₁ : P₁ ≃ᵃ[k] P₂
e₂ : P₃ ≃ᵃ[k] P₄
⊢ (↑(e₁.prodCongr e₂) : P₁ × P₃ →ᵃ[k] P₂ × P₄) = (↑e₁ : P₁ →ᵃ[k] P₂).prodMap (↑e₂ : P₃ →ᵃ[k] P₄)

Tactic:
rfl

Premises used: AffineMap.prodMap, Prod.map, AffineEquiv.toAffineMap, Function.prod, LinearMap.prod, rfl, LinearMap.prodMap
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
⊢ ∀ (p : P₁ × P₂) (v : V₁ × V₂),
    (Equiv.prodComm P₁ P₂ : (a : P₁ × P₂) → P₂ × P₁) (v +ᵥ p) =
      HVAdd.hVAdd (α := V₂ × V₁) (β := P₂ × P₁)
        (((LinearEquiv.prodComm k V₁ V₂ : (V₁ × V₂) ≃ₗ[k] V₂ × V₁) : (a : V₁ × V₂) → V₂ × V₁) v : V₂ × V₁)
        ((Equiv.prodComm P₁ P₂ : (a : P₁ × P₂) → P₂ × P₁) p : P₂ × P₁)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ P₂
⊢ Eq (α := P₂ × P₁ ≃ᵃ[k] P₁ × P₂) (symm (prodComm k P₁ P₂)) (prodComm k P₂ P₁)

Tactic:
rfl

Premises used: LinearEquiv.symm, Equiv.prodComm, AffineEquiv.symm, LinearEquiv.prodComm, AffineEquiv.prodComm, Prod.swap, Equiv.symm, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
⊢ ∀ (p : (P₁ × P₂) × P₃) (v : (V₁ × V₂) × V₃),
    (Equiv.prodAssoc P₁ P₂ P₃ : (a : (P₁ × P₂) × P₃) → P₁ × P₂ × P₃) (v +ᵥ p) =
      HVAdd.hVAdd (α := V₁ × V₂ × V₃) (β := P₁ × P₂ × P₃)
        (((LinearEquiv.prodAssoc k V₁ V₂ V₃ : ((V₁ × V₂) × V₃) ≃ₗ[k] V₁ × V₂ × V₃) :
              (a : (V₁ × V₂) × V₃) → V₁ × V₂ × V₃)
            v :
          V₁ × V₂ × V₃)
        ((Equiv.prodAssoc P₁ P₂ P₃ : (a : (P₁ × P₂) × P₃) → P₁ × P₂ × P₃) p : P₁ × P₂ × P₃)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
p p' : P₁
v : V₁
⊢ (Equiv.constVSub p : (a : P₁) → V₁) (v +ᵥ p') =
    HVAdd.hVAdd (α := V₁) (β := V₁) ((LinearEquiv.neg k : (a : V₁) → V₁) v : V₁)
      ((Equiv.constVSub p : (a : P₁) → V₁) p' : V₁)

Tactic:
simp [vsub_vadd_eq_vsub_sub, neg_add_eq_sub]

Premises used: neg_add_eq_sub, vsub_vadd_eq_vsub_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
p : P₁
⊢ Eq (α := (a : P₁) → V₁) (⇑(constVSub k p) : (a : P₁) → V₁) fun (x : P₁) ↦ p -ᵥ x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
p : P₁
⊢ Eq (α := (a : V₁) → P₁) (⇑(symm (constVSub k p)) : (a : V₁) → P₁) fun (v : V₁) ↦ -v +ᵥ p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
⊢ Eq (α := P₁ ≃ᵃ[k] P₁) (constVAdd k P₁ 0) (refl k P₁)

Tactic:
ext <| zero_vadd _

Premises used: zero_vadd, AffineEquiv.ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
v w : V₁
⊢ Eq (α := P₁ ≃ᵃ[k] P₁) (constVAdd k P₁ (v + w)) (trans (constVAdd k P₁ w) (constVAdd k P₁ v))

Tactic:
ext <| add_vadd _ _

Premises used: AddSemigroupAction.add_vadd, AffineEquiv.ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
v : V₁
⊢ Eq (α := P₁ ≃ᵃ[k] P₁) (symm (constVAdd k P₁ v)) (constVAdd k P₁ (-v))

Tactic:
ext fun _ => rfl

Premises used: AffineEquiv.ext, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
n : ℕ
v : V₁
⊢ constVAdd k P₁ (n • v) = HPow.hPow (α := P₁ ≃ᵃ[k] P₁) (constVAdd k P₁ v) n

Tactic:
(constVAddHom k P₁).map_pow _ _

Premises used: AffineEquiv.constVAdd, AffineEquiv.constVAddHom, MonoidHom.map_pow
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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 : AffineSpace V₁ P₁
z : ℤ
v : V₁
⊢ constVAdd k P₁ (z • v) = HPow.hPow (α := P₁ ≃ᵃ[k] P₁) (constVAdd k P₁ v) z

Tactic:
(constVAddHom k P₁).map_zpow _ _

Premises used: AffineEquiv.constVAdd, AffineEquiv.constVAddHom, MonoidHom.map_zpow