awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (hypothesis)
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
hc : Eq.{u_6 + 1} (α := M) (∑ i ∈ s, c i • v i) 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
⊢ ∀ i ∈ s, c i = 0
have hc₁ : x = y
Tactic: replace hc : x = y := by
    classical
    simp_rw [hx, hy, neg_smul, Finset.sum_neg_distrib, ← add_eq_zero_iff_eq_neg]
    rw [← hc, ← Finset.sum_union, Finset.sum_subset]
    · grind only [= Finset.subset_iff, = Finset.mem_union, = Finset.mem_filter]
    · simp +contextual [eq_comm (a := (0 : R))]
    · grind only [Finset.disjoint_filter]
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
hc : x = y
⊢ x = 0
have suffices : LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
Tactic: suffices B x y ≤ 0 by simpa [hc, ← hB.le_zero_iff, B.toQuadraticMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
hc : x = y
⊢ LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
have suffices : LE.le.{u_5} (α := R) 0
  (∑ x ∈ s with c x < 0,
    ∑ i ∈ s with 0 < c i,
      c x * HMul.hMul (β := R) (c i) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v x) : R))
Tactic: suffices 0 ≤ ∑ x ∈ s with c x < 0, ∑ i ∈ s with 0 < c i, c x * (c i * (B (v i)) (v x)) by
      simpa [hx, hy, map_neg, Finset.mul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
hc : x = y
⊢ LE.le.{u_5} (α := R) 0
    (∑ x ∈ s with c x < 0,
      ∑ i ∈ s with 0 < c i,
        c x * HMul.hMul (β := R) (c i) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v x) : R))
have refine : ∀ (i : ι) (hi : i ∈ {x ∈ s | c x < 0}) (j : ι) (hj : j ∈ {i ∈ s | 0 < c i}),
  0 ≤ c i * HMul.hMul (β := R) (c j) ((((B : (a : M) → M →ₗ[R] R) (v j) : M →ₗ[R] R) : (a : M) → R) (v i) : R)
Tactic: refine Finset.sum_nonneg fun i hi ↦ Finset.sum_nonneg fun j hj ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (hypothesis)
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
hc : x = y
⊢ ∀ i ∈ s, c i = 0
have hx₀ : x = 0
Tactic: have hx₀ : x = 0 := by
    suffices B x y ≤ 0 by simpa [hc, ← hB.le_zero_iff, B.toQuadraticMap_apply]
    suffices 0 ≤ ∑ x ∈ s with c x < 0, ∑ i ∈ s with 0 < c i, c x * (c i * (B (v i)) (v x)) by
      simpa [hx, hy, map_neg, Finset.mul_sum]
    refine Finset.sum_nonneg fun i hi ↦ Finset.sum_nonneg fun j hj ↦ ?_
    grind [Pairwise, mul_nonneg_iff, mul_nonpos_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (hypothesis)
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c_1 : ι → R
x : M := ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
hx : x = ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
y : M := ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hy : y = ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hc : x = y
hx₀ : x = 0
c : ι → R
h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0
i : ι
hi : i ∈ s
⊢ c i ≤ 0
have this : Eq.{u_5 + 1} (α := R) (∑ i ∈ s with 0 < c i, HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R)) 0
Tactic: have : ∑ i ∈ s with 0 < c i, c i * f (v i) = 0 := by simpa using (congr(f $h))
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (hypothesis)
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c_1 : ι → R
x : M := ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
hx : x = ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
y : M := ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hy : y = ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hc : x = y
hx₀ : x = 0
c : ι → R
h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0
i : ι
hi : i ∈ s
this : Eq.{u_5 + 1} (α := R) (∑ i ∈ s with 0 < c i, HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R)) 0
⊢ c i ≤ 0
have this₁ : ∀ i ∈ {i ∈ s | 0 < c i}, HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R) = 0
Tactic: rw [Finset.sum_eq_zero_iff_of_nonneg (by grind [mul_nonneg])] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c_1 : ι → R
x : M := ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
hx : x = ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
y : M := ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hy : y = ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hc : x = y
hx₀ : x = 0
c : ι → R
h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0
i : ι
hi : i ∈ s
this : ∀ i ∈ {i ∈ s | 0 < c i}, HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R) = 0
⊢ c i ≤ 0
have by_contra! : ∀ (hi' : 0 < c i), False
Tactic: by_contra! hi'
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (hypothesis)
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c_1 : ι → R
x : M := ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
hx : x = ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
y : M := ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hy : y = ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hc : x = y
hx₀ : x = 0
c : ι → R
h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0
i : ι
hi : i ∈ s
this : ∀ i ∈ {i ∈ s | 0 < c i}, HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R) = 0
hi' : 0 < c i
⊢ False
have this₁ : 0 < HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R)
Tactic: have : 0 < c i * f (v i) := mul_pos hi' (hp i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (hypothesis)
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
hc : x = y
hx₀ : x = 0
⊢ ∀ i ∈ s, c i = 0
have H : ∀ (c : ι → R) (h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0) (i : ι) (hi : i ∈ s), c i ≤ 0
Tactic: have H (c : ι → R) (h : ∑ i ∈ s with 0 < c i, c i • v i = 0) (i : ι) (hi : i ∈ s) : c i ≤ 0 := by
    have : ∑ i ∈ s with 0 < c i, c i * f (v i) = 0 := by simpa using (congr(f $h))
    rw [Finset.sum_eq_zero_iff_of_nonneg (by grind [mul_nonneg])] at this
    by_contra! hi'
    have : 0 < c i * f (v i) := mul_pos hi' (hp i)
    grind
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (hypothesis)
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
hc : x = y
hx₀ : x = 0
H : ∀ (c : ι → R) (h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0) (i : ι) (hi : i ∈ s), c i ≤ 0
⊢ ∀ i ∈ s, c i = 0
have hx₁ : ∀ (i : ι) (hi : i ∈ s), c i ≤ 0
Tactic: replace hx (i : ι) (hi : i ∈ s) : c i ≤ 0 := H _ (by grind) i hi
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (hypothesis)
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
x : M := ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
hc : x = y
hx₀ : x = 0
H : ∀ (c : ι → R) (h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0) (i : ι) (hi : i ∈ s), c i ≤ 0
hx : ∀ (i : ι) (hi : i ∈ s), c i ≤ 0
⊢ ∀ i ∈ s, c i = 0
have hy₁ : ∀ (i : ι) (hi : i ∈ s), -c i ≤ 0
Tactic: replace hy (i : ι) (hi : i ∈ s) : -c i ≤ 0 := H (-c ·) (by grind) i hi
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Isometry (goal)
Goal:
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_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
f g : Q₁ →qᵢ Q₂
h :
  Eq (α := (a : M₁) → M₂) ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂)) f)
    ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂)) g)
⊢ f = g
have mk : ∀ (toLinearMap : M₁ →ₗ[R] M₂)
  (map_app' :
    ∀ (m : M₁), Eq.{u_7 + 1} (α := N) ((Q₂ : (a : M₂) → N) (toLinearMap.toFun m) : N) ((Q₁ : (a : M₁) → N) m : N))
  (h :
    Eq (α := (a : M₁) → M₂)
      ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
        { toLinearMap := toLinearMap, map_app' := map_app' })
      ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂)) g)),
  { toLinearMap := toLinearMap, map_app' := map_app' : Q₁ →qᵢ Q₂ } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Isometry (goal)
Goal:
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_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
g : Q₁ →qᵢ Q₂
toLinearMap : M₁ →ₗ[R] M₂
map_app' : ∀ (m : M₁), Eq.{u_7 + 1} (α := N) ((Q₂ : (a : M₂) → N) (toLinearMap.toFun m) : N) ((Q₁ : (a : M₁) → N) m : N)
h :
  Eq (α := (a : M₁) → M₂)
    ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
      { toLinearMap := toLinearMap, map_app' := map_app' })
    ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂)) g)
⊢ { toLinearMap := toLinearMap, map_app' := map_app' : Q₁ →qᵢ Q₂ } = g
have mk : ∀ (toLinearMap_1 : M₁ →ₗ[R] M₂)
  (map_app'_1 :
    ∀ (m : M₁), Eq.{u_7 + 1} (α := N) ((Q₂ : (a : M₂) → N) (toLinearMap_1.toFun m) : N) ((Q₁ : (a : M₁) → N) m : N))
  (h :
    Eq (α := (a : M₁) → M₂)
      ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
        { toLinearMap := toLinearMap, map_app' := map_app' })
      ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
        { toLinearMap := toLinearMap_1, map_app' := map_app'_1 })),
  { toLinearMap := toLinearMap, map_app' := map_app' : Q₁ →qᵢ Q₂ } =
    { toLinearMap := toLinearMap_1, map_app' := map_app'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Isometry (goal)
Goal:
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_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
toLinearMap : M₁ →ₗ[R] M₂
map_app' : ∀ (m : M₁), Eq.{u_7 + 1} (α := N) ((Q₂ : (a : M₂) → N) (toLinearMap.toFun m) : N) ((Q₁ : (a : M₁) → N) m : N)
toLinearMap_1 : M₁ →ₗ[R] M₂
map_app'_1 :
  ∀ (m : M₁), Eq.{u_7 + 1} (α := N) ((Q₂ : (a : M₂) → N) (toLinearMap_1.toFun m) : N) ((Q₁ : (a : M₁) → N) m : N)
h :
  Eq (α := (a : M₁) → M₂)
    ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
      { toLinearMap := toLinearMap, map_app' := map_app' })
    ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
      { toLinearMap := toLinearMap_1, map_app' := map_app'_1 })
⊢ { toLinearMap := toLinearMap, map_app' := map_app' : Q₁ →qᵢ Q₂ } =
    { toLinearMap := toLinearMap_1, map_app' := map_app'_1 }
have mk : toLinearMap = toLinearMap_1
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Isometry (goal)
Goal:
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_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
g : Q₂ →qᵢ Q₃
f : Q₁ →qᵢ Q₂
x : M₁
⊢ Eq.{u_7 + 1} (α := N) ((Q₃ : (a : M₃) → N) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x : M₂) : M₃) : N)
    ((Q₁ : (a : M₁) → N) x : N)
have rw : Eq.{u_7 + 1} (α := N) ((Q₃ : (a : M₃) → N) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x : M₂) : M₃) : N)
  ((Q₂ : (a : M₂) → N) ((f : (a : M₁) → M₂) x : M₂) : N)
Tactic: rw [← f.map_app, ← g.map_app]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Isometry (goal)
Goal:
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_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
g : Q₂ →qᵢ Q₃
f : Q₁ →qᵢ Q₂
x : M₁
rw :
  Eq.{u_7 + 1} (α := N) ((Q₃ : (a : M₃) → N) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x : M₂) : M₃) : N)
    ((Q₂ : (a : M₂) → N) ((f : (a : M₁) → M₂) x : M₂) : N)
⊢ Eq.{u_7 + 1} (α := N) ((Q₃ : (a : M₃) → N) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x : M₂) : M₃) : N)
    ((Q₁ : (a : M₁) → N) x : N)
have rw₁ : Eq.{u_7 + 1} (α := N) ((Q₃ : (a : M₃) → N) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x : M₂) : M₃) : N)
  ((Q₃ : (a : M₃) → N) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x : M₂) : M₃) : N)
Tactic: rw [← f.map_app, ← g.map_app]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv (goal)
Goal:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f g : Q₁.IsometryEquiv Q₂
⊢ Eq (α := M₁ → M₂) (⇑f.toLinearEquiv : (a : M₁) → M₂) (⇑g.toLinearEquiv : (a : M₁) → M₂) →
    Eq (α := M₂ → M₁) (⇑f.symm : (a : M₂) → M₁) (⇑g.symm : (a : M₂) → M₁) → f = g
have mk : ∀ (toLinearEquiv : M₁ ≃ₗ[R] M₂)
  (map_app' :
    ∀ (m : M₁),
      Eq.{u_9 + 1} (α := N) ((Q₂ : (a : M₂) → N) ((↑toLinearEquiv : M₁ →ₗ[R] M₂).toFun m) : N)
        ((Q₁ : (a : M₁) → N) m : N)),
  Eq (α := M₁ → M₂)
      (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ }.toLinearEquiv : (a : M₁) → M₂)
      (⇑g.toLinearEquiv : (a : M₁) → M₂) →
    Eq (α := M₂ → M₁)
        (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ }.symm : (a : M₂) → M₁)
        (⇑g.symm : (a : M₂) → M₁) →
      { toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ } = g
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv (goal)
Goal:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
g : Q₁.IsometryEquiv Q₂
toLinearEquiv : M₁ ≃ₗ[R] M₂
map_app' :
  ∀ (m : M₁),
    Eq.{u_9 + 1} (α := N) ((Q₂ : (a : M₂) → N) ((↑toLinearEquiv : M₁ →ₗ[R] M₂).toFun m) : N) ((Q₁ : (a : M₁) → N) m : N)
⊢ Eq (α := M₁ → M₂)
      (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ }.toLinearEquiv : (a : M₁) → M₂)
      (⇑g.toLinearEquiv : (a : M₁) → M₂) →
    Eq (α := M₂ → M₁)
        (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ }.symm : (a : M₂) → M₁)
        (⇑g.symm : (a : M₂) → M₁) →
      { toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ } = g
have mk : ∀ (toLinearEquiv_1 : M₁ ≃ₗ[R] M₂)
  (map_app'_1 :
    ∀ (m : M₁),
      Eq.{u_9 + 1} (α := N) ((Q₂ : (a : M₂) → N) ((↑toLinearEquiv_1 : M₁ →ₗ[R] M₂).toFun m) : N)
        ((Q₁ : (a : M₁) → N) m : N)),
  Eq (α := M₁ → M₂)
      (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ }.toLinearEquiv : (a : M₁) → M₂)
      (⇑{ toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 : Q₁.IsometryEquiv Q₂ }.toLinearEquiv :
        (a : M₁) → M₂) →
    Eq (α := M₂ → M₁)
        (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ }.symm : (a : M₂) → M₁)
        (⇑{ toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 : Q₁.IsometryEquiv Q₂ }.symm : (a : M₂) → M₁) →
      { toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ } =
        { toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 }
Tactic: cases g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv (goal)
Goal:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
⊢ Eq.{u_9 + 1} (α := N) ((Q₁ : (a : M₁) → N) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) : N) ((Q₂ : (a : M₂) → N) m : N)
have rw : Eq.{u_9 + 1} (α := N) ((Q₂ : (a : M₂) → N) ((f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) : M₂) : N)
  ((Q₂ : (a : M₂) → N) m : N)
Tactic: rw [← f.map_app]