awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
this :
  Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal))
      ν ↔
    Integrable (llr μ ν) μ
h :
  ∀ (x : α),
    klFun (μ.rnDeriv ν x).toReal = (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν ↔ Integrable (llr μ ν) μ

Tactic:
convert! this using 3 with x
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
this :
  Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal))
      ν ↔
    Integrable (llr μ ν) μ
x : α
h :
  (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1 - (μ.rnDeriv ν x).toReal =
    (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)
h₁ h₂ :
  (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal) =
    (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)
⊢ klFun (μ.rnDeriv ν x).toReal = (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)

Tactic:
rw [klFun, add_sub_assoc]

Premises used: add_sub_assoc, InformationTheory.klFun
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
suffices :
  Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal))
      ν ↔
    Integrable (llr μ ν) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν ↔ Integrable (llr μ ν) μ

Tactic:
suffices Integrable (fun x ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal
      + (1 - (μ.rnDeriv ν x).toReal)) ν ↔ Integrable (llr μ ν) μ by
    convert! this using 3 with x
    rw [klFun, add_sub_assoc]
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
rw : Integrable (ε := ℝ) (fun (x : α) ↦ 1 - (μ.rnDeriv ν x).toReal) ν
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal))
      ν ↔
    Integrable (llr μ ν) μ

Tactic:
rw [integrable_add_iff_integrable_left', integrable_rnDeriv_mul_log_iff hμν]

Premises used: MeasureTheory.integrable_add_iff_integrable_left', MeasureTheory.integrable_rnDeriv_mul_log_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
funProp : enorm (E := ℝ) 1 ≠ ⊤
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ 1 - (μ.rnDeriv ν x).toReal) ν

Tactic:
fun_prop
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
rw :
  ∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν + ν.real univ - μ.real univ =
    ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ
hf : Integrable (ε := ℝ) (fun (a : α) ↦ (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal) ν
hg : Integrable (ε := ℝ) (fun (a : α) ↦ 1) ν
hf₁ : Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1) ν
hg₁ : Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal) ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1 - (μ.rnDeriv ν x).toReal ∂ν =
    ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ

Tactic:
rw [integral_sub, integral_add, integral_const, Measure.integral_toReal_rnDeriv hμν, smul_eq_mul,
    mul_one]

Premises used: MeasureTheory.Measure.integral_toReal_rnDeriv, MeasureTheory.integral_sub, MeasureTheory.integral_const, smul_eq_mul, mul_one, MeasureTheory.integral_add
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
e_a : Eq (α := ℝ) (∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν) (∫ (x : α), llr μ ν x ∂μ)
⊢ ∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν + ν.real univ - μ.real univ =
    ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ

Tactic:
congr 2
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Eq (α := ℝ) (∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν) (∫ (x : α), llr μ ν x ∂μ)

Tactic:
integral_rnDeriv_smul hμν

Premises used: MeasureTheory.llr, MeasureTheory.integral_rnDeriv_smul
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Eq (α := ℝ) (∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν) (∫ (x : α), llr μ ν x ∂μ)

Tactic:
exact integral_rnDeriv_smul hμν

Premises used: MeasureTheory.integral_rnDeriv_smul
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int hf hf₁ hf₂ hf₃ : Integrable (llr μ ν) μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal) ν

Tactic:
rwa [integrable_rnDeriv_mul_log_iff hμν]

Premises used: MeasureTheory.integrable_rnDeriv_mul_log_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
funProp : enorm (E := ℝ) 1 ≠ ⊤
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ 1) ν

Tactic:
fun_prop
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1) ν

Tactic:
Integrable.add ?_ (integrable_const _)

Premises used: MeasureTheory.Integrable.add, MeasureTheory.integrable_const
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal) ν
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1) ν

Tactic:
refine Integrable.add ?_ (integrable_const _)

Premises used: MeasureTheory.Integrable.add
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int hf hf₁ hf₂ hf₃ : Integrable (llr μ ν) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal) ν

Tactic:
rwa [integrable_rnDeriv_mul_log_iff hμν]

Premises used: MeasureTheory.integrable_rnDeriv_mul_log_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal) ν

Tactic:
fun_prop
-- Module: Mathlib.Lean.Meta.CongrTheorems
Goal:
α : Sort u
h : FastSubsingleton α
⊢ ∀ (a b : α), a = b

Tactic:
h.inst.allEq

Premises used: Subsingleton.allEq
-- Module: Mathlib.Lean.Meta.CongrTheorems
Goal:
α β : Sort u
inst : FastSubsingleton α
h₂ : α = β
a : α
b : β
⊢ Subsingleton α

Tactic:
have : Subsingleton α := FastSubsingleton.inst
-- Module: Mathlib.Lean.Meta.CongrTheorems
Goal:
α β : Sort u
inst : FastSubsingleton α
h₂ : α = β
a : α
b : β
this : Subsingleton α
⊢ a ≍ b

Tactic:
Subsingleton.helim h₂ a b

Premises used: Subsingleton.helim
-- Module: Mathlib.Lean.Meta.CongrTheorems
Goal:
α β : Sort u
inst : FastSubsingleton α
h₂ : α = β
a : α
b : β
this : Subsingleton α
⊢ a ≍ b

Tactic:
exact Subsingleton.helim h₂ a b

Premises used: Subsingleton.helim
-- Module: Mathlib.Lean.Meta.CongrTheorems
Goal:
p : Prop
⊢ FastSubsingleton p

Tactic:

Premises used: Lean.Meta.FastSubsingleton.mk
-- Module: Mathlib.Lean.Meta.CongrTheorems
Goal:
p : Prop
⊢ FastSubsingleton (Decidable p)

Tactic:

Premises used: Lean.Meta.FastSubsingleton.mk
-- Module: Mathlib.Lean.Meta.CongrTheorems
Goal:
⊢ FastSubsingleton (Fin 1)

Tactic:

Premises used: Lean.Meta.FastSubsingleton.mk
-- Module: Mathlib.Lean.Meta.CongrTheorems
Goal:
⊢ FastSubsingleton PUnit

Tactic:

Premises used: Lean.Meta.FastSubsingleton.mk
-- Module: Mathlib.Lean.Meta.CongrTheorems
Goal:
⊢ FastIsEmpty Empty

Tactic:

Premises used: Lean.Meta.FastIsEmpty.mk
-- Module: Mathlib.Lean.Meta.CongrTheorems
Goal:
⊢ FastIsEmpty False

Tactic:

Premises used: Lean.Meta.FastIsEmpty.mk
-- Module: Mathlib.Lean.Meta.CongrTheorems
Goal:
⊢ FastIsEmpty (Fin 0)

Tactic:

Premises used: Lean.Meta.FastIsEmpty.mk
-- Module: Mathlib.Lean.Thunk
Goal:
α : Type u_1
x : α
⊢ (Thunk.pure x).get = x

Tactic:
rfl

Premises used: Thunk.get, rfl
-- Module: Mathlib.Lean.Thunk
Goal:
α : Type u_1
f : Unit → α
⊢ { fn := f : Thunk α }.get = f ()

Tactic:
rfl

Premises used: Thunk.get, rfl
-- Module: Mathlib.Lean.Thunk
Goal:
α : Type u
β : Type v
inst : DecidableEq α
a b : Thunk α
x : a = b
rw rw₁ : b.get = b.get
⊢ a.get = b.get

Tactic:
rw [x]
-- Module: Mathlib.Lean.Thunk
Goal:
α : Type u
β : Type v
inst : DecidableEq α
a b : Thunk α
h a₁ : a.get = b.get
⊢ a = b

Tactic:
ext
-- Module: Mathlib.Lean.Thunk
Goal:
α : Type u
β : Type v
inst : DecidableEq α
a b : Thunk α
h : a.get = b.get
⊢ a.get = b.get

Tactic:
assumption
-- Module: Mathlib.Lean.Thunk
Goal:
α : Type u
β : Type v
inst : DecidableEq α
a b : Thunk α
⊢ a = b ↔ a.get = b.get

Tactic:
have : a = b ↔ a.get = b.get := ⟨by intro x; rw [x], by intro; ext; assumption⟩
-- Module: Mathlib.Lean.Thunk
Goal:
α : Type u
β : Type v
inst : DecidableEq α
a b : Thunk α
this : a = b ↔ a.get = b.get
rw : Decidable (a.get = b.get)
⊢ Decidable (a = b)

Tactic:
rw [this]
-- Module: Mathlib.Lean.Thunk
Goal:
α : Type u
β : Type v
inst : DecidableEq α
a b : Thunk α
this : a = b ↔ a.get = b.get
⊢ Decidable (a.get = b.get)

Tactic:
infer_instance
-- Module: Mathlib.Lean.Thunk
Goal:
α : Type u
β : Type v
a : Thunk α
b : Thunk β
⊢ (a.prod b).get.fst = a.get

Tactic:
rfl

Premises used: Thunk.get, rfl
-- Module: Mathlib.Lean.Thunk
Goal:
α : Type u
β : Type v
a : Thunk α
b : Thunk β
⊢ (a.prod b).get.snd = b.get

Tactic:
rfl

Premises used: Thunk.get, rfl
-- Module: Mathlib.Lean.Thunk
Goal:
α : Type u
inst : Add α
a b : Thunk α
⊢ (a + b).get = a.get + b.get

Tactic:
rfl

Premises used: Thunk.get, 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₂
f : P₁ ≃ P₂
f' : V₁ ≃ₗ[k] V₂
h :
  ∀ (p : P₁) (v : V₁),
    (f : (a : P₁) → P₂) (v +ᵥ p) =
      HVAdd.hVAdd.{u_7, u_3, u_3} (α := V₂) (β := P₂) ((f' : (a : V₁) → V₂) v : V₂) ((f : (a : P₁) → P₂) p : P₂)
⊢ (↑{ toEquiv := f, linear := f', map_vadd' := h : P₁ ≃ᵃ[k] P₂ } : P₁ →ᵃ[k] P₂) =
    { toFun := (⇑f : (a : P₁) → P₂), linear := (↑f' : V₁ →ₗ[k] V₂), map_vadd' := h }

Tactic:
rfl

Premises used: AffineEquiv.toAffineMap, 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 : P₁ →ᵃ[k] P₂).linear = (↑e.linear : V₁ →ₗ[k] V₂)

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₁ ≃ P₂
el : V₁ ≃ₗ[k] V₂
h :
  ∀ (p : P₁) (v : V₁),
    (e : (a : P₁) → P₂) (v +ᵥ p) =
      HVAdd.hVAdd.{u_7, u_3, u_3} (α := V₂) (β := P₂) ((el : (a : V₁) → V₂) v : V₂) ((e : (a : P₁) → P₂) p : P₂)
e' : P₁ ≃ P₂
el' : V₁ ≃ₗ[k] V₂
h' :
  ∀ (p : P₁) (v : V₁),
    (e' : (a : P₁) → P₂) (v +ᵥ p) =
      HVAdd.hVAdd.{u_7, u_3, u_3} (α := V₂) (β := P₂) ((el' : (a : V₁) → V₂) v : V₂) ((e' : (a : P₁) → P₂) p : P₂)
H :
  (↑{ toEquiv := e, linear := el, map_vadd' := h : P₁ ≃ᵃ[k] P₂ } : P₁ →ᵃ[k] P₂) =
    (↑{ toEquiv := e', linear := el', map_vadd' := h' } : P₁ →ᵃ[k] P₂)
⊢ { toEquiv := e, linear := el, map_vadd' := h : P₁ ≃ᵃ[k] P₂ } = { toEquiv := e', linear := el', map_vadd' := h' }

Tactic:
simp_all
-- 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 e' : P₁ ≃ᵃ[k] P₂
⊢ (↑e : P₁ →ᵃ[k] P₂) = (↑e' : P₁ →ᵃ[k] P₂) ↔ e = e'

Tactic:
toAffineMap_injective.eq_iff

Premises used: Function.Injective.eq_iff, AffineEquiv.toAffineMap_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₂
e : P₁ ≃ᵃ[k] P₂
p : P₁
v : V₁
⊢ (e : (a : P₁) → P₂) (v +ᵥ p) =
    HVAdd.hVAdd.{u_7, u_3, u_3} (α := V₂) (β := P₂) ((e.linear : (a : V₁) → V₂) v : V₂) ((e : (a : P₁) → P₂) p : P₂)

Tactic:
e.map_vadd' p v

Premises used: AffineEquiv.map_vadd'
-- 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.toEquiv : (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
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 : P₁ →ᵃ[k] P₂) : (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
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 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.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₂
⊢ Injective (α := P₁ ≃ᵃ[k] P₂) (β := P₁ → P₂) (DFunLike.coe (β := fun (x : P₁) ↦ P₂))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_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₂
e e' : P₁ ≃ᵃ[k] P₂
⊢ Eq (α := (a : P₁) → P₂) (⇑e : (a : P₁) → P₂) (⇑e' : (a : P₁) → P₂) ↔ e = e'

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₂
⊢ Injective (α := P₁ ≃ᵃ[k] P₂) toEquiv

Tactic:
fun _ _ H =>
  ext <| Equiv.ext_iff.1 H

Premises used: Equiv.ext_iff, Iff.mp, AffineEquiv.ext, Function.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₂
e e' : P₁ ≃ᵃ[k] P₂
⊢ e.toEquiv = e'.toEquiv ↔ e = e'

Tactic:
toEquiv_injective.eq_iff

Premises used: Function.Injective.eq_iff, AffineEquiv.toEquiv_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₂
e : P₁ ≃ P₂
e' : V₁ ≃ₗ[k] V₂
h :
  ∀ (p : P₁) (v : V₁),
    (e : (a : P₁) → P₂) (v +ᵥ p) =
      HVAdd.hVAdd.{u_7, u_3, u_3} (α := V₂) (β := P₂) ((e' : (a : V₁) → V₂) v : V₂) ((e : (a : P₁) → P₂) p : P₂)
⊢ Eq (α := (a : P₁) → P₂) (⇑{ toEquiv := e, linear := e', map_vadd' := h : P₁ ≃ᵃ[k] P₂ } : (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
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₁ → P₂
e' : V₁ ≃ₗ[k] V₂
p : P₁
h : ∀ (p' : P₁), e p' = HVAdd.hVAdd.{u_7, u_3, u_3} (α := V₂) ((e' : (a : V₁) → V₂) (p' -ᵥ p) : V₂) (e p)
p' : P₁
⊢ (fun (q' : P₂) ↦ HVAdd.hVAdd.{u_6, u_2, u_2} (α := V₁) ((e'.symm : (a : V₂) → V₁) (q' -ᵥ e p) : V₁) p) (e p') = p'

Tactic:
simp [h p', vadd_vsub, vsub_vadd]

Premises used: vsub_vadd, vadd_vsub
-- 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₁ → P₂
e' : V₁ ≃ₗ[k] V₂
p : P₁
h : ∀ (p' : P₁), e p' = HVAdd.hVAdd.{u_7, u_3, u_3} (α := V₂) ((e' : (a : V₁) → V₂) (p' -ᵥ p) : V₂) (e p)
q' : P₂
⊢ e ((fun (q' : P₂) ↦ HVAdd.hVAdd.{u_6, u_2, u_2} (α := V₁) ((e'.symm : (a : V₂) → V₁) (q' -ᵥ e p) : V₁) p) q') = q'

Tactic:
simp [h (e'.symm (q' -ᵥ e p) +ᵥ p), vadd_vsub, vsub_vadd]

Premises used: LinearEquiv.symm, VSub.vsub, HVAdd.hVAdd, vsub_vadd, vadd_vsub, DFunLike.coe
-- 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₁ → P₂
e' : V₁ ≃ₗ[k] V₂
p : P₁
h : ∀ (p' : P₁), e p' = HVAdd.hVAdd.{u_7, u_3, u_3} (α := V₂) ((e' : (a : V₁) → V₂) (p' -ᵥ p) : V₂) (e p)
p' : P₁
v : V₁
⊢ ({ toFun := e,
          invFun := fun (q' : P₂) ↦
            HVAdd.hVAdd.{u_6, u_2, u_2} (α := V₁) ((e'.symm : (a : V₂) → V₁) (q' -ᵥ e p) : V₁) p,
          left_inv := ⋯, right_inv := ⋯ : P₁ ≃ P₂ } :
        (a : P₁) → P₂)
      (v +ᵥ p') =
    HVAdd.hVAdd.{u_7, u_3, u_3} (α := V₂) (β := P₂) ((e' : (a : V₁) → V₂) v : V₂)
      (({ toFun := e,
              invFun := fun (q' : P₂) ↦
                HVAdd.hVAdd.{u_6, u_2, u_2} (α := V₁) ((e'.symm : (a : V₂) → V₁) (q' -ᵥ e p) : V₁) p,
              left_inv := ⋯, right_inv := ⋯ : P₁ ≃ P₂ } :
            (a : P₁) → P₂)
          p' :
        P₂)

Tactic:
simp [h p', h (v +ᵥ p'), vadd_vsub_assoc, vadd_vadd]

Premises used: vadd_vsub_assoc, vadd_vadd, HVAdd.hVAdd
-- 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₁ ≃ P₂
e' : V₁ ≃ₗ[k] V₂
p : P₁
h :
  ∀ (p' : P₁),
    (e : (a : P₁) → P₂) p' =
      HVAdd.hVAdd.{u_7, u_3, u_3} (α := V₂) (β := P₂) ((e' : (a : V₁) → V₂) (p' -ᵥ p) : V₂) ((e : (a : P₁) → P₂) p : P₂)
⊢ Eq (α := (a : P₁) → P₂) (⇑(mk' (⇑e : (a : P₁) → P₂) e' p h) : (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
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₁ ≃ P₂
e' : V₁ ≃ₗ[k] V₂
p : P₁
h :
  ∀ (p' : P₁),
    (e : (a : P₁) → P₂) p' =
      HVAdd.hVAdd.{u_7, u_3, u_3} (α := V₂) (β := P₂) ((e' : (a : V₁) → V₂) (p' -ᵥ p) : V₂) ((e : (a : P₁) → P₂) p : P₂)
⊢ (mk' (⇑e : (a : P₁) → P₂) e' p h).linear = e'

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₂
p : P₂
v : V₂
rw :
  v +ᵥ p =
    (e.toEquiv : (a : P₁) → P₂)
      (HVAdd.hVAdd.{u_6, u_2, u_2} (α := V₁) (β := P₁) ((e.linear.symm : (a : V₂) → V₁) v : V₁)
        ((e.symm : (a : P₂) → P₁) p : P₁))
rw₁ :
  v +ᵥ p =
    HVAdd.hVAdd.{u_7, u_3, u_3} (α := V₂) (β := P₂)
      ((e.linear : (a : V₁) → V₂) ((e.linear.symm : (a : V₂) → V₁) v : V₁) : V₂)
      ((e.toEquiv : (a : P₁) → P₂) ((e.symm : (a : P₂) → P₁) p : P₁) : P₂)
rw₂ : v +ᵥ p = HVAdd.hVAdd (β := P₂) v ((e.toEquiv : (a : P₁) → P₂) ((e.symm : (a : P₂) → P₁) p : P₁) : P₂)
rw₃ rw₄ : v +ᵥ p = v +ᵥ p
⊢ v +ᵥ p =
    (e.symm.symm : (a : P₁) → P₂)
      (HVAdd.hVAdd.{u_6, u_2, u_2} (α := V₁) (β := P₁) ((e.linear.symm : (a : V₂) → V₁) v : V₁)
        ((e.symm : (a : P₂) → P₁) p : P₁))

Tactic:
rw [Equiv.symm_symm, e.map_vadd' ((Equiv.symm e.toEquiv) p) ((LinearEquiv.symm e.linear) v),
        LinearEquiv.apply_symm_apply, Equiv.apply_symm_apply]

Premises used: AffineEquiv.linear, LinearEquiv.symm, Equiv.apply_symm_apply, Equiv.symm_symm, LinearEquiv.apply_symm_apply, AffineEquiv.toEquiv, Equiv.symm, AffineEquiv.map_vadd', DFunLike.coe