mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : ¬μ ≪ ν
⊢ klDiv (Measure.map g μ) (Measure.map g ν) ≤ klDiv μ ν

pp: case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
⊢ klDiv (Measure.map g μ) (Measure.map g ν) ≤ klDiv μ ν

Tactic:
;

Goal state after:
case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : ¬μ ≪ ν
⊢ klDiv (Measure.map g μ) (Measure.map g ν) ≤ klDiv μ ν

case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
⊢ klDiv (Measure.map g μ) (Measure.map g ν) ≤ klDiv μ ν
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ klDiv (Measure.map g μ) (Measure.map g ν) ≤ klDiv μ ν

pp: case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ klDiv (Measure.map g μ) (Measure.map g ν) ≤ klDiv μ ν

Tactic:
;

Goal state after:
case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ klDiv (Measure.map g μ) (Measure.map g ν) ≤ klDiv μ ν

case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ klDiv (Measure.map g μ) (Measure.map g ν) ≤ klDiv μ ν
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
m mα : MeasurableSpace α
μ : Measure α
f : α → E
hm : ¬m ≤ mα
⊢ (fun x ↦ 0) ≤ᵐ[μ] 0

Tactic:
;

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
m mα : MeasurableSpace α
μ : Measure α
f : α → E
hm : ¬m ≤ mα
⊢ (fun x ↦ 0) ≤ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
m mα : MeasurableSpace α
μ : Measure α
f : α → E
hm : m ≤ mα
hμm : ¬SigmaFinite (μ.trim hm)
⊢ (fun x ↦ 0) ≤ᵐ[μ] 0

Tactic:
;

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
m mα : MeasurableSpace α
μ : Measure α
f : α → E
hm : m ≤ mα
hμm : ¬SigmaFinite (μ.trim hm)
⊢ (fun x ↦ 0) ≤ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
m mα : MeasurableSpace α
μ : Measure α
f : α → E
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
⊢ (fun x ↦ ‖μ[f | m] x‖) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ | m]

Tactic:
by_cases! hf_int : ¬ Integrable f μ

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
m mα : MeasurableSpace α
μ : Measure α
f : α → E
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : ¬Integrable f μ
⊢ (fun x ↦ ‖μ[f | m] x‖) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ | m]

case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
m mα : MeasurableSpace α
μ : Measure α
f : α → E
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
⊢ (fun x ↦ ‖μ[f | m] x‖) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
m mα : MeasurableSpace α
μ : Measure α
f : α → E
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : ¬Integrable f μ
a : α
⊢ 0 a ≤ ‖f a‖

Tactic:
;

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
m mα : MeasurableSpace α
μ : Measure α
f : α → E
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : ¬Integrable f μ
a : α
⊢ 0 a ≤ ‖f a‖
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
p : ℝ
hp : 1 ≤ p
hfint : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : 0 < p
hm : ¬m ≤ mα
⊢ (fun x ↦ 0) ≤ᵐ[μ] 0

Tactic:
;

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
p : ℝ
hp : 1 ≤ p
hfint : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : 0 < p
hm : ¬m ≤ mα
⊢ (fun x ↦ 0) ≤ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
p : ℝ
hp : 1 ≤ p
hfint : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : 0 < p
hm : m ≤ mα
hμm : ¬SigmaFinite (μ.trim hm)
⊢ (fun x ↦ 0) ≤ᵐ[μ] 0

Tactic:
;

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
p : ℝ
hp : 1 ≤ p
hfint : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : 0 < p
hm : m ≤ mα
hμm : ¬SigmaFinite (μ.trim hm)
⊢ (fun x ↦ 0) ≤ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
p : ℝ
hp : 1 ≤ p
hfint : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : 0 < p
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
⊢ (fun x ↦ ‖μ[f | m] x‖ ^ p) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ ^ p | m]

Tactic:
by_cases! hf_int : ¬ Integrable f μ

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
p : ℝ
hp : 1 ≤ p
hfint : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : 0 < p
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : ¬Integrable f μ
⊢ (fun x ↦ ‖μ[f | m] x‖ ^ p) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ ^ p | m]

case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
p : ℝ
hp : 1 ≤ p
hfint : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : 0 < p
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
⊢ (fun x ↦ ‖μ[f | m] x‖ ^ p) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ ^ p | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
p : ℝ
hp : 1 ≤ p
hfint : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : 0 < p
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : ¬Integrable f μ
a : α
⊢ 0 a ≤ ‖f a‖ ^ p

Tactic:
;

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
p : ℝ
hp : 1 ≤ p
hfint : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : 0 < p
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : ¬Integrable f μ
a : α
⊢ 0 a ≤ ‖f a‖ ^ p
Module: Mathlib.Lean.Thunk

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq α
a b : Thunk α
x : a = b
⊢ a.get = b.get

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : Thunk α
x : a = b
⊢ a.get = b.get
Module: Mathlib.Lean.Thunk

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq α
a b : Thunk α
a✝ : a.get = b.get
⊢ a = b

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : Thunk α
a✝ : a.get = b.get
⊢ a = b
Module: Mathlib.Lean.Thunk

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq α
a b : Thunk α
a✝ : a.get = b.get
⊢ a.get = b.get

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : Thunk α
a✝ : a.get = b.get
⊢ a.get = b.get
Module: Mathlib.LinearAlgebra.Basis.Flag

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ b.flag k.castSucc ≤ R ∙ b k ⊔ b.flag k.castSucc

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ b.flag k.castSucc ≤ R ∙ b k ⊔ b.flag k.castSucc
Module: Mathlib.LinearAlgebra.BilinearForm.Isometry

Goal state before:
pp: case mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
g : B₁ →bᵢ B₂
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m m' : M₁), (B₂ (toLinearMap✝.toFun m)) (toLinearMap✝.toFun m') = (B₁ m) m'
h : (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ } = (fun f ↦ ⇑f.toLinearMap) g
⊢ { toLinearMap := toLinearMap✝, map_app' := map_app'✝ } = g

Tactic:
;

Goal state after:
case mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
g : B₁ →bᵢ B₂
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m m' : M₁), (B₂ (toLinearMap✝.toFun m)) (toLinearMap✝.toFun m') = (B₁ m) m'
h : (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ } = (fun f ↦ ⇑f.toLinearMap) g
⊢ { toLinearMap := toLinearMap✝, map_app' := map_app'✝ } = g
Module: Mathlib.LinearAlgebra.BilinearForm.Isometry

Goal state before:
pp: case mk.mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
toLinearMap✝¹ : M₁ →ₗ[R] M₂
map_app'✝¹ : ∀ (m m' : M₁), (B₂ (toLinearMap✝¹.toFun m)) (toLinearMap✝¹.toFun m') = (B₁ m) m'
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m m' : M₁), (B₂ (toLinearMap✝.toFun m)) (toLinearMap✝.toFun m') = (B₁ m) m'
h :
  (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } =
    (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }
⊢ { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } = { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
toLinearMap✝¹ : M₁ →ₗ[R] M₂
map_app'✝¹ : ∀ (m m' : M₁), (B₂ (toLinearMap✝¹.toFun m)) (toLinearMap✝¹.toFun m') = (B₁ m) m'
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m m' : M₁), (B₂ (toLinearMap✝.toFun m)) (toLinearMap✝.toFun m') = (B₁ m) m'
h :
  (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } =
    (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }
⊢ { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } = { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }
Module: Mathlib.LinearAlgebra.BilinearForm.Isometry

Goal state before:
pp: case mk.mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
toLinearMap✝¹ : M₁ →ₗ[R] M₂
map_app'✝¹ : ∀ (m m' : M₁), (B₂ (toLinearMap✝¹.toFun m)) (toLinearMap✝¹.toFun m') = (B₁ m) m'
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m m' : M₁), (B₂ (toLinearMap✝.toFun m)) (toLinearMap✝.toFun m') = (B₁ m) m'
h :
  (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } =
    (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }
⊢ toLinearMap✝¹ = toLinearMap✝

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
toLinearMap✝¹ : M₁ →ₗ[R] M₂
map_app'✝¹ : ∀ (m m' : M₁), (B₂ (toLinearMap✝¹.toFun m)) (toLinearMap✝¹.toFun m') = (B₁ m) m'
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m m' : M₁), (B₂ (toLinearMap✝.toFun m)) (toLinearMap✝.toFun m') = (B₁ m) m'
h :
  (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } =
    (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }
⊢ toLinearMap✝¹ = toLinearMap✝
Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv

Goal state before:
pp: case mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
g : B₁.IsometryEquiv B₂
toLinearEquiv✝ : M₁ ≃ₗ[R] M₂
map_app'✝ : ∀ (n m : M₁), (B₂ ((↑toLinearEquiv✝).toFun n)) ((↑toLinearEquiv✝).toFun m) = (B₁ n) m
⊢ ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.toLinearEquiv = ⇑g.toLinearEquiv →
    ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.symm = ⇑g.symm →
      { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ } = g

Tactic:
;

Goal state after:
case mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
g : B₁.IsometryEquiv B₂
toLinearEquiv✝ : M₁ ≃ₗ[R] M₂
map_app'✝ : ∀ (n m : M₁), (B₂ ((↑toLinearEquiv✝).toFun n)) ((↑toLinearEquiv✝).toFun m) = (B₁ n) m
⊢ ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.toLinearEquiv = ⇑g.toLinearEquiv →
    ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.symm = ⇑g.symm →
      { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ } = g
Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv

Goal state before:
pp: case mk.mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
toLinearEquiv✝¹ : M₁ ≃ₗ[R] M₂
map_app'✝¹ : ∀ (n m : M₁), (B₂ ((↑toLinearEquiv✝¹).toFun n)) ((↑toLinearEquiv✝¹).toFun m) = (B₁ n) m
toLinearEquiv✝ : M₁ ≃ₗ[R] M₂
map_app'✝ : ∀ (n m : M₁), (B₂ ((↑toLinearEquiv✝).toFun n)) ((↑toLinearEquiv✝).toFun m) = (B₁ n) m
⊢ ⇑{ toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ }.toLinearEquiv =
      ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.toLinearEquiv →
    ⇑{ toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ }.symm =
        ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.symm →
      { toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ } =
        { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
toLinearEquiv✝¹ : M₁ ≃ₗ[R] M₂
map_app'✝¹ : ∀ (n m : M₁), (B₂ ((↑toLinearEquiv✝¹).toFun n)) ((↑toLinearEquiv✝¹).toFun m) = (B₁ n) m
toLinearEquiv✝ : M₁ ≃ₗ[R] M₂
map_app'✝ : ∀ (n m : M₁), (B₂ ((↑toLinearEquiv✝).toFun n)) ((↑toLinearEquiv✝).toFun m) = (B₁ n) m
⊢ ⇑{ toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ }.toLinearEquiv =
      ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.toLinearEquiv →
    ⇑{ toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ }.symm =
        ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.symm →
      { toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ } =
        { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }
Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
n✝ m✝ : M₂
⊢ (B₁ ((↑f.symm).toFun n✝)) ((↑f.symm).toFun m✝) = (B₂ n✝) m✝

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
n✝ m✝ : M₂
⊢ (B₁ ((↑f.symm).toFun n✝)) ((↑f.symm).toFun m✝) = (B₂ n✝) m✝
Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
n✝ m✝ : M₂
⊢ (B₂ (f ((↑f.symm).toFun n✝))) (f ((↑f.symm).toFun m✝)) = (B₂ n✝) m✝

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
n✝ m✝ : M₂
⊢ (B₂ (f ((↑f.symm).toFun n✝))) (f ((↑f.symm).toFun m✝)) = (B₂ n✝) m✝
Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv

Goal state before:
pp: case e_5.e_6
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
n✝ m✝ : M₂
⊢ f ((↑f.symm).toFun n✝) = n✝

pp: case e_6
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
n✝ m✝ : M₂
⊢ f ((↑f.symm).toFun m✝) = m✝

Tactic:
repeat exact f.toLinearEquiv.apply_symm_apply _

Goal state after: