mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.LimZero
⊢ f.lim = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ f.lim ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬f✝.LimZero
hl : f✝.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
⊢ g - f * f.inv hf * g = 1 * g - f * f.inv hf * g

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ ∀ (a b : ℝ), a ⊓ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
⊢ v = w

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬f✝.LimZero
hl : f✝.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
⊢ f * f.inv hf * g = f * f.inv hf * g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Fintype n
u v w : n → R
huv : u ≤ v
hw : 0 ≤ w
⊢ u ⬝ᵥ w ≤ v ⬝ᵥ w

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ ∀ (a b : ℝ), a ⊓ b ≤ b

Tactic:
intro a b
    induction a using Real.ind_mk
    induction b using Real.ind_mk
    rw [← mk_inf, mk_le]
    exact CauSeq.inf_le_right

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ ∀ (a b : ℝ), a ⊓ b ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Fintype n
u v w : n → R
huv : u ≤ v
hw : 0 ≤ w
⊢ w ⬝ᵥ u ≤ w ⬝ᵥ v

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ ∀ (a b c : ℝ), a ≤ b → a ≤ c → a ≤ b ⊓ c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬f✝.LimZero
hl : f✝.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
⊢ g - f * f.inv hf * g = (1 - f * f.inv hf) * g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝³ : Fintype n
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : n → R
⊢ (∀ i ∈ Finset.univ, v i * v i = 0) ↔ v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
⊢ (fun x ↦ star (v x) * v x) = 0 ↔ v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
⊢ (fun x ↦ v x * star (v x)) = 0 ↔ v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix n p R
h : A * B = 0
⊢ Aᴴ * A * B = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬f✝.LimZero
hl : f✝.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
⊢ g - f * f.inv hf * g = g * (1 - f * f.inv hf)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ ∀ (x y z : ℝ), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix n p R
⊢ Aᴴ * A * B = 0 ↔ A * B = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix m p R
⊢ A * Aᴴ * B = 0 ↔ Aᴴ * B = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ ∀ (a b : ℝ), a ≤ b ∨ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f g : Cauchy abs
⊢ { cauchy := f / g } = { cauchy := f } / { cauchy := g }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
h : a ≤ b
⊢ a ⊔ b ≈ b

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix p m R
⊢ B * (A * Aᴴ) = 0 ↔ B * A = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix p n R
⊢ B * (Aᴴ * A) = 0 ↔ B * Aᴴ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ ∀ (a : ℝ), a ≠ 0 → a * a⁻¹ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ 0⁻¹ = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
v : n → R
⊢ (Aᴴ * A) *ᵥ v = 0 ↔ A *ᵥ v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
v : m → R
⊢ (A * Aᴴ) *ᵥ v = 0 ↔ Aᴴ *ᵥ v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
v : n → R
⊢ v ᵥ* (Aᴴ * A) = 0 ↔ v ᵥ* Aᴴ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
v : m → R
⊢ v ᵥ* (A * Aᴴ) = 0 ↔ v ᵥ* A = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ DivisionRing ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ Decidable (a < b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ Decidable (a ≤ b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ Decidable (a = b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬f✝.LimZero
hl : f✝.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)
⊢ g - f * f.inv hf * g = g * (1 - f.inv hf * f)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
⊢ 0 < star v ⬝ᵥ v ↔ v ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
⊢ 0 < v ⬝ᵥ star v ↔ v ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
f : CauSeq ℚ abs
⊢ (∃ i, ∀ j ≥ i, x ≤ ↑(↑f j)) → x ≤ mk f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬f✝.LimZero
hl : f✝.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
⊢ (g - f * f.inv hf * g).LimZero

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
h : b ≤ a
⊢ a ⊓ b ≈ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ j ≥ i, ↑(↑f j) ≤ x
j : ℕ
ij : j ≥ i
⊢ -x ≤ ↑(↑(-f) j)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f : CauSeq ℚ abs
x : ℝ
h : ∃ i, ∀ j ≥ i, ↑(↑f j) ≤ x
⊢ mk f ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
h : b ≤ a
⊢ a ⊔ b ≈ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: b : ℕ
hb : ∀ {a : ℝ}, 0 < a → a * ↑b + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ a * ↑(b + 1) + 1 = (0 + 1) ^ b * a + (a * ↑b + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
h : a ≤ b
⊢ a ⊓ b ≈ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: b : ℕ
hb : ∀ {a : ℝ}, 0 < a → a * ↑b + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ (0 + 1) ^ b * a + (a * ↑b + 1) ≤ (a + 1) ^ b * a + (a + 1) ^ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: b : ℕ
hb : ∀ {a : ℝ}, 0 < a → a * ↑b + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ (a + 1) ^ b * a + (a + 1) ^ b = (a + 1) ^ (b + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
b : ℕ
⊢ a * ↑b + 1 ≤ (a + 1) ^ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
f : R → ℝ
hf : IsPowMul f
⊢ f 1 ^ 2 = f 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
ha : a ≤ c
hb : b ≤ c
⊢ a ⊔ b ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : a < b
hc : a ≈ c
⊢ a ≤ b ⊓ c

Tactic:
replace hb := le_of_eq_of_le (Setoid.symm hc) hb.le

Goal state after:
case inl.inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
⊢ a ≤ b ⊓ c
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
f : R → ℝ
hf : IsPowMul f
⊢ f 1 ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : a ≤ b
hc : a ≤ c
⊢ a ≤ b ⊓ c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (f.inv hf - const abv f.lim * (f.inv hf * const abv f.lim⁻¹)).LimZero

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (const abv f.lim⁻¹ - f * (f.inv hf * const abv f.lim⁻¹)).LimZero

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (f.inv hf - const abv f.lim⁻¹ - (const abv f.lim - f) * (f.inv hf * const abv f.lim⁻¹)).LimZero

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
M : Matrix n n α
w : n → α
⊢ M ⊙ diagonal w = diagonal (M.diag * w)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
M : Matrix n n α
w : n → α
⊢ diagonal w ⊙ M = diagonal (w * M.diag)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
v w : n → α
⊢ diagonal v ⊙ diagonal w = diagonal (v * w)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
A : Matrix n n α
d e : n → α
⊢ diagonal d ⊙ A = diagonal e ↔ d * A.diag = e

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
A : Matrix n n α
d e : n → α
⊢ A ⊙ diagonal d = diagonal e ↔ A.diag * d = e

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
A : Matrix n n α
d : n → α
⊢ 1 ⊙ A = diagonal d ↔ A.diag = d

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
A : Matrix n n α
d : n → α
⊢ A ⊙ 1 = diagonal d ↔ A.diag = d

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
A : Matrix n n α
⊢ 1 ⊙ A = 0 ↔ A.diag = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
A : Matrix n n α
⊢ A ⊙ 1 = 0 ↔ A.diag = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
m : Type u_2
n : Type u_3
inst✝ : MulOneClass α
A : Matrix m n α
⊢ A ⊙ of 1 = A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
m : Type u_2
n : Type u_3
inst✝ : MulOneClass α
A : Matrix m n α
⊢ of 1 ⊙ A = A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
m : Type u_2
n : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
h : ¬(ia = ib ∧ ja = jb)
a b : α
⊢ single ia ja a ⊙ single ib jb b = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
m : Type u_2
n : Type u_3
A B : Matrix m n α
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalSemiring α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
v : m → α
w : n → α
⊢ v ᵥ* A ⊙ B ⬝ᵥ w = (diagonal v * A * (B * diagonal w)ᵀ).trace

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
A B : Matrix m n R
⊢ A.vec = B.vec ↔ A = B

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: ι : Type u_2
m : Type u_3
n : Type u_4
R : Type u_1
inst✝ : AddCommMonoid R
s : Finset ι
A : ι → Matrix m n R
⊢ (∑ i ∈ s, A i).vec = ∑ i ∈ s, (A i).vec

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_1
inst✝³ : AddCommMonoid R
inst✝² : Mul R
inst✝¹ : Fintype m
inst✝ : Fintype n
A B : Matrix m n R
⊢ A.vec ⬝ᵥ B.vec = (Aᵀ * B).trace

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
⊢ (∀ (i j : n), star (A j i) = A i j) → A.IsHermitian

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝¹ : Star α
inst✝ : TrivialStar α
A : Matrix n n α
⊢ A.IsHermitian ↔ A.IsSymm

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : Mul R
inst✝² : Star R
inst✝¹ : Fintype m
inst✝ : Fintype n
A B : Matrix m n R
⊢ star A.vec ⬝ᵥ B.vec = (Aᴴ * B).trace

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : A.IsHermitian
f : α → β
hf : Function.Semiconj f star star
⊢ (A.map f).IsHermitian

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero R
i : m
j : n
r : R
⊢ (single i j r).vec = Pi.single (j, i) r

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
f : α → β
hf : Function.Semiconj f star star
hinj : Function.Injective f
⊢ (A.map f).IsHermitian ↔ A.IsHermitian

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : A.IsHermitian
⊢ Aᵀ.IsHermitian

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
⊢ Aᵀ.IsHermitian → A.IsHermitian

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix n n α
e : m ≃ n
h : (A.submatrix ⇑e ⇑e).IsHermitian
⊢ A.IsHermitian

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : A.IsHermitian
f : n ≃ m
⊢ ((Matrix.reindex f f) A).IsHermitian

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix n n α
f : n ≃ m
⊢ ((reindex f f) A).IsHermitian ↔ A.IsHermitian

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix m m (Matrix n n α)
⊢ ((comp m m n n α) A).IsHermitian ↔ A.IsHermitian

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix m m (Matrix n n α)
⊢ ((comp m m n n α) A).IsHermitian ↔ ∀ (i j : m) (i' j' : n), star (A j i j' i') = A i j i' j'

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
⊢ Cᴴ = B

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix l m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) B A *ᵥ X.vec = (A * X * Bᵀ).vec

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ A⁻¹ ^ n = (A ^ n)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
⊢ (Matrix.fromBlocks A B C D).IsHermitian

Tactic:
by

Goal state after: