mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ : P.root l = P.root j + P.root k
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ ↑b.support
h₃ : P.root j = ∑ m, P.root (f m)
h₄ : ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
h₅ : k ∈ b.support
m : Fin (n + 1)
hm : ↑m = n
a✝ : Fin (n + 1)
⊢ a✝ ∈ Finset.Iic m ↔ a✝ ∈ Finset.univ

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ : P.root l = P.root j + P.root k
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ ↑b.support
h₃ : P.root j = ∑ m, P.root (f m)
h₄ : ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
h₅ : k ∈ b.support
m : Fin (n + 1)
hm : ↑m = n
a✝ : Fin (n + 1)
⊢ a✝ ∈ Finset.Iic m ↔ a✝ ∈ Finset.univ
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j k : ι), P.root k = P.root i + P.root j → p i → j ∈ b.support → p k
this✝ : InvolutiveNeg ι := P.indexNeg
hi : b.IsPos (-i)
this : p (-i)
⊢ p (- -i)

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j k : ι), P.root k = P.root i + P.root j → p i → j ∈ b.support → p k
this✝ : InvolutiveNeg ι := P.indexNeg
hi : b.IsPos (-i)
this : p (-i)
⊢ p (- -i)
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case ind.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι}, b.IsPos i → (b.height i).natAbs = m → p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
hj : i ∈ b.support
hj' : 0 < P.pairingIn ℤ i i
⊢ p i

pp: case ind.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι}, b.IsPos i → (b.height i).natAbs = m → p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
⊢ p i

Tactic:
;

Goal state after:
case ind.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι}, b.IsPos i → (b.height i).natAbs = m → p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
hj : i ∈ b.support
hj' : 0 < P.pairingIn ℤ i i
⊢ p i

case ind.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι}, b.IsPos i → (b.height i).natAbs = m → p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
⊢ p i
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)
this✝ : InvolutiveNeg ι := P.indexNeg
hi : b.IsPos (-i)
this : p (-i)
⊢ p (- -i)

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)
this✝ : InvolutiveNeg ι := P.indexNeg
hi : b.IsPos (-i)
this : p (-i)
⊢ p (- -i)
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
q : Submodule R M
hq : ∀ i ∈ b.support, q ∈ invtSubmodule ↑(P.reflection i)
i : ι
this : InvolutiveNeg ι := P.indexNeg
j : ι
x : M
⊢ (P.reflection (-j)) x = (P.reflection j) x

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
q : Submodule R M
hq : ∀ i ∈ b.support, q ∈ invtSubmodule ↑(P.reflection i)
i : ι
this : InvolutiveNeg ι := P.indexNeg
j : ι
x : M
⊢ (P.reflection (-j)) x = (P.reflection j) x
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: a b : Cauchy abs
⊢ ({ cauchy := a } - { cauchy := b }).cauchy = { cauchy := a }.cauchy - { cauchy := b }.cauchy

Tactic:
by
    rw [sub_eq_add_neg, ← cauchy_neg, ← cauchy_add]
    rfl

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

Goal state before:
pp: x a b c : ℝ
⊢ (a + b + c).cauchy = (a + (b + c)).cauchy

Tactic:
;

Goal state after:
x a b c : ℝ
⊢ (a + b + c).cauchy = (a + (b + c)).cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ (0 + a).cauchy = a.cauchy

Tactic:
;

Goal state after:
x a : ℝ
⊢ (0 + a).cauchy = a.cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ (a + 0).cauchy = a.cauchy

Tactic:
;

Goal state after:
x a : ℝ
⊢ (a + 0).cauchy = a.cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ (a + b).cauchy = (b + a).cauchy

Tactic:
;

Goal state after:
x a b : ℝ
⊢ (a + b).cauchy = (b + a).cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ (a * b * c).cauchy = (a * (b * c)).cauchy

Tactic:
;

Goal state after:
x a b c : ℝ
⊢ (a * b * c).cauchy = (a * (b * c)).cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ (1 * a).cauchy = a.cauchy

Tactic:
;

Goal state after:
x a : ℝ
⊢ (1 * a).cauchy = a.cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ (a * 1).cauchy = a.cauchy

Tactic:
;

Goal state after:
x a : ℝ
⊢ (a * 1).cauchy = a.cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ (0 * a).cauchy = cauchy 0

Tactic:
;

Goal state after:
x a : ℝ
⊢ (0 * a).cauchy = cauchy 0
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ (a * 0).cauchy = cauchy 0

Tactic:
;

Goal state after:
x a : ℝ
⊢ (a * 0).cauchy = cauchy 0
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ (a * (b + c)).cauchy = (a * b + a * c).cauchy

Tactic:
;

Goal state after:
x a b c : ℝ
⊢ (a * (b + c)).cauchy = (a * b + a * c).cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ ((a + b) * c).cauchy = (a * c + b * c).cauchy

Tactic:
;

Goal state after:
x a b c : ℝ
⊢ ((a + b) * c).cauchy = (a * c + b * c).cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ { cauchy := ↑0 }.cauchy = cauchy 0

Tactic:
;

Goal state after:
x : ℝ
⊢ { cauchy := ↑0 }.cauchy = cauchy 0
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
n : ℕ
⊢ { cauchy := ↑(n + 1) }.cauchy = ({ cauchy := ↑n } + 1).cauchy

Tactic:
;

Goal state after:
x : ℝ
n : ℕ
⊢ { cauchy := ↑(n + 1) }.cauchy = ({ cauchy := ↑n } + 1).cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ (-a + a).cauchy = cauchy 0

Tactic:
;

Goal state after:
x a : ℝ
⊢ (-a + a).cauchy = cauchy 0
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
z : ℕ
⊢ { cauchy := ↑(Int.negSucc z) }.cauchy = (-↑(z + 1)).cauchy

Tactic:
;

Goal state after:
x : ℝ
z : ℕ
⊢ { cauchy := ↑(Int.negSucc z) }.cauchy = (-↑(z + 1)).cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ (a * b).cauchy = (b * a).cauchy

Tactic:
;

Goal state after:
x a b : ℝ
⊢ (a * b).cauchy = (b * a).cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f g : CauSeq ℚ abs
⊢ (match { cauchy := ⟦f⟧ }, { cauchy := ⟦g⟧ } with
    | { cauchy := x }, { cauchy := y } => Quotient.liftOn₂ x y (fun x1 x2 ↦ x1 < x2) definition._proof_1✝) ↔
    f < g

Tactic:
;

Goal state after:
f g : CauSeq ℚ abs
⊢ (match { cauchy := ⟦f⟧ }, { cauchy := ⟦g⟧ } with
    | { cauchy := x }, { cauchy := y } => Quotient.liftOn₂ x y (fun x1 x2 ↦ x1 < x2) definition._proof_1✝) ↔
    f < g
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: ⊢ mk 0 = { cauchy := 0 }

Tactic:
;

Goal state after:
⊢ mk 0 = { cauchy := 0 }
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: ⊢ mk 1 = { cauchy := 1 }

Tactic:
;

Goal state after:
⊢ mk 1 = { cauchy := 1 }
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
⊢ const x ≤ const y ↔ x < y ∨ x = y

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
⊢ const x ≤ const y ↔ x < y ∨ x = y
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f g : CauSeq ℚ abs
⊢ f < g ∨ f ≈ g ↔ f ≤ g

Tactic:
;

Goal state after:
f g : CauSeq ℚ abs
⊢ f < g ∨ f ≈ g ↔ f ≤ g
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
this : Fintype ι
⊢ LinearIndepOn R ⇑P.coroot ↑⋯.toFinset

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
this : Fintype ι
⊢ LinearIndepOn R ⇑P.coroot ↑⋯.toFinset
Module: Mathlib.Algebra.Star.Pi

Goal state before:
pp: I : Type u_1
J : Type u_2
α : Type u_3
x✝ : I → α
y : J → α
inst✝ : Star α
x : I ⊕ J
⊢ star (Sum.elim x✝ y) x = Sum.elim (star x✝) (star y) x

Tactic:
;

Goal state after:
I : Type u_1
J : Type u_2
α : Type u_3
x✝ : I → α
y : J → α
inst✝ : Star α
x : I ⊕ J
⊢ star (Sum.elim x✝ y) x = Sum.elim (star x✝) (star y) x
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
⊢ ∑ i, u i * w i ≤ ∑ i, v i * w i

Tactic:
;

Goal state after:
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
⊢ ∑ i, u i * w i ≤ ∑ i, v i * w i
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
⊢ ∑ i, w i * u i ≤ ∑ i, w i * v i

Tactic:
;

Goal state after:
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
⊢ ∑ i, w i * u i ≤ ∑ i, w i * v i
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)
h₆ : g - f * f.inv hf * g = g * (1 - f.inv hf * f)
⊢ (g * (1 - f.inv hf * f)).LimZero

Tactic:
;

Goal state after:
α : 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)
h₆ : g - f * f.inv hf * g = g * (1 - f.inv hf * f)
⊢ (g * (1 - f.inv hf * f)).LimZero
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).inv ⋯ * f.inv hf).LimZero

Tactic:
;

Goal state after:
α : 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).inv ⋯ * f.inv hf).LimZero
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:
;

Goal state after:
α : 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
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 α
i✝ : m
j✝ : n
⊢ (A ⊙ of 1) i✝ j✝ = A i✝ j✝

Tactic:
;

Goal state after:
α : Type u_1
m : Type u_2
n : Type u_3
inst✝ : MulOneClass α
A : Matrix m n α
i✝ : m
j✝ : n
⊢ (A ⊙ of 1) i✝ j✝ = A i✝ j✝
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 α
i✝ : m
j✝ : n
⊢ (of 1 ⊙ A) i✝ j✝ = A i✝ j✝

Tactic:
;

Goal state after:
α : Type u_1
m : Type u_2
n : Type u_3
inst✝ : MulOneClass α
A : Matrix m n α
i✝ : m
j✝ : n
⊢ (of 1 ⊙ A) i✝ j✝ = A i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: case inl
α : 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
a b : α
h✝ : ¬ia = ib
⊢ ((of fun i' j' ↦ if ia = i' ∧ ja = j' then a else 0) ⊙ of fun i' j' ↦ if ib = i' ∧ jb = j' then b else 0) = 0

Tactic:
;

Goal state after:
case inl
α : 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
a b : α
h✝ : ¬ia = ib
⊢ ((of fun i' j' ↦ if ia = i' ∧ ja = j' then a else 0) ⊙ of fun i' j' ↦ if ib = i' ∧ jb = j' then b else 0) = 0
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: case inr
α : 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
a b : α
h✝ : ¬ja = jb
⊢ ((of fun i' j' ↦ if ia = i' ∧ ja = j' then a else 0) ⊙ of fun i' j' ↦ if ib = i' ∧ jb = j' then b else 0) = 0

Tactic:
;

Goal state after:
case inr
α : 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
a b : α
h✝ : ¬ja = jb
⊢ ((of fun i' j' ↦ if ia = i' ∧ ja = j' then a else 0) ⊙ of fun i' j' ↦ if ib = i' ∧ jb = j' then b else 0) = 0
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

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

Tactic:
;

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
⊢ A.IsHermitian
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

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

Tactic:
;

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
i j : n
⊢ Aᴴ i j = A i j
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ᵀᵀ.map star = Aᵀ

Tactic:
transpose_map

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : A.IsHermitian
⊢ (Aᵀ.map star)ᵀ = Aᵀ
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:
;

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : Aᵀ.IsHermitian
⊢ A.IsHermitian
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:
;

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : Aᵀ.IsHermitian
⊢ Aᵀᵀ.IsHermitian
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case succ.succ.inl
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)

Tactic:
calc
        A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n := by
          simp only [pow_succ A⁻¹, pow_succ' A, Matrix.mul_assoc]
        _ = A ^ n * A⁻¹ ^ m := by simp only [h, Matrix.mul_one, IH m]
        _ = A ^ n * (A * A⁻¹) * A⁻¹ ^ m := by simp only [h', Matrix.mul_one]
        _ = A ^ (n + 1) * A⁻¹ ^ (m + 1) := by
          simp only [pow_succ A, pow_succ' A⁻¹, Matrix.mul_assoc]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
inst✝⁴ : CommRing α
inst✝³ : StarRing α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
inst✝ : Invertible A
h : A⁻¹.IsHermitian
⊢ A⁻¹⁻¹.IsHermitian

Tactic:
;

Goal state after:
α : Type u_1
m : Type u_3
inst✝⁴ : CommRing α
inst✝³ : StarRing α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
inst✝ : Invertible A
h : A⁻¹.IsHermitian
⊢ A⁻¹⁻¹.IsHermitian
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
⊢ A ^ (-1) = A⁻¹

Tactic:
by
  simpa using DivInvMonoid.zpow_neg' 0 A

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
h : IsUnit A.det
n : ℤ
⊢ A⁻¹ ^ n = A ^ (-n)

Tactic:
by
  rw [zpow_neg h, inv_zpow]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
b : Basis n R M
inst✝ : IsDomain R
x : M
hx : x ∈ maxGenEigenspace ((toLin b b) (diagonal d)) μ
k : ℕ
hk : (((toLin b b) (diagonal d) - μ • 1) ^ k) x = 0
j : n
⊢ (toLin b b) (diagonal d) - μ • 1 = (toLin b b) (diagonal d - diagonal (μ • 1))

Tactic:
;

Goal state after:
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
b : Basis n R M
inst✝ : IsDomain R
x : M
hx : x ∈ maxGenEigenspace ((toLin b b) (diagonal d)) μ
k : ℕ
hk : (((toLin b b) (diagonal d) - μ • 1) ^ k) x = 0
j : n
⊢ (toLin b b) (diagonal d) - μ • 1 = (toLin b b) (diagonal d - diagonal (μ • 1))
Module: Mathlib.LinearAlgebra.Matrix.ZMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
i j : ι
hμ : A i j ≤ if i = j then μ else 0
⊢ 0 ≤ N i j

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
i j : ι
hμ : A i j ≤ if i = j then μ else 0
⊢ 0 ≤ N i j