mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
mE : MeasurableSpace E
inst✝¹ : BorelSpace E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ s φ
hφ_cont : UpperSemicontinuousOn φ s
hφ_meas : StronglyMeasurable φ
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ μ[φ ∘ f | m] ≤ᵐ[μ] φ ∘ μ[f | m]

Tactic:
exact hφ_cvx.condExp_map_le hm hφ_cont hf hs hf_int hφ_int

Goal state after:
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 μ
⊢ (fun x ↦ ‖μ[f | m] x‖ ^ p) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ ^ p | m]

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)
hf_int : Integrable f μ
⊢ (fun x ↦ ‖μ[f | m] x‖ ^ p) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ ^ p | m]

Tactic:
· simp only [condExp_of_not_integrable hf_int, Pi.zero_apply, norm_zero,
      Real.zero_rpow hp'.ne.symm]
    apply condExp_nonneg
    filter_upwards with a; positivity

Goal state after:
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.LinearAlgebra.BilinearForm.Isometry

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₃
B₄ : LinearMap.BilinForm R M₄
inst✝ : Subsingleton M₁
x y : M₁
⊢ (B₂ ((toAddHom 0).toFun x)) ((toAddHom 0).toFun y) = (B₁ x) y

Tactic:
rw [Subsingleton.elim x 0, Subsingleton.elim y 0]

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₃
B₄ : LinearMap.BilinForm R M₄
inst✝ : Subsingleton M₁
x y : M₁
⊢ (B₂ ((toAddHom 0).toFun 0)) ((toAddHom 0).toFun 0) = (B₁ 0) 0
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_6
inst✝¹⁰ : CommRing R
S : Type u_7
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_8
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
P : Type u_9
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
hR : Subsingleton R
this : Subsingleton M
⊢ f = 1

Tactic:
exact Subsingleton.eq_one f

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case pos.hw
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hp : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
⊢ ∑ i_1, (lineMap (Pi.single i 1) w) x⁻¹ i_1 = 1

Tactic:
· simp [AffineMap.lineMap_apply, Finset.sum_add_distrib, ← Finset.mul_sum,
        Finset.sum_sub_distrib, hw]

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case neg
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
he : Nonempty (Basis Unit K ↥u.range)
⊢ ∃ f v, ↑e = LinearMap.transvection f v

Tactic:
obtain ⟨b⟩ := he

Goal state after:
case neg
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
⊢ ∃ f v, ↑e = LinearMap.transvection f v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
r : R
⊢ (ι (Q' Q)) (m, r) = (ι (Q' Q)) (m + 0, 0 + r)

Tactic:
zero_add,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
r : R
⊢ (ι (Q' Q)) (m, r) = (ι (Q' Q)) (m + 0, r)
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case neg
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : ¬f v = 0
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this : Fintype ↑ι
x y : ↑ι
hxy : ¬x = y
⊢ 0 + f v * (Finsupp.single y 1) i * (Finsupp.single i 1) x = 0

Tactic:
zero_add,

Goal state after:
case neg
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : ¬f v = 0
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this : Fintype ↑ι
x y : ↑ι
hxy : ¬x = y
⊢ f v * (Finsupp.single y 1) i * (Finsupp.single i 1) x = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (0 + 1) * (ι Q) m = (ι Q) m

Tactic:
zero_add,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ 1 * (ι Q) m = (ι Q) m
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ ((-1) ^ (j₁ * i₂) * (-1) ^ ((j₁ + j₂) * (i₁ + i₂))) •
      ((DirectSum.of ℬ j₁) b₁ * (DirectSum.of ℬ j₂) b₂) ⊗ₜ[R] ((DirectSum.of 𝒜 i₁) a₁ * (DirectSum.of 𝒜 i₂) a₂) =
    ((-1) ^ (j₂ * i₂) * ((-1) ^ (j₁ * i₁) * (-1) ^ (i₁ * j₂))) •
      ((DirectSum.of ℬ j₁) b₁ * (DirectSum.of ℬ j₂) b₂) ⊗ₜ[R] ((DirectSum.of 𝒜 i₁) a₁ * (DirectSum.of 𝒜 i₂) a₂)

Tactic:
← DirectSum.lof_eq_of R

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ ((-1) ^ (j₁ * i₂) * (-1) ^ ((j₁ + j₂) * (i₁ + i₂))) •
      ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂) ⊗ₜ[R] ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂) =
    ((-1) ^ (j₂ * i₂) * ((-1) ^ (j₁ * i₁) * (-1) ^ (i₁ * j₂))) •
      ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂) ⊗ₜ[R] ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
m : M₁ × M₂
⊢ ((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₁ 1).subtype ((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1)) +
        (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₂ 1).subtype ((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2))) *
      ((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₁ 1).subtype ((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1)) +
        (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₂ 1).subtype ((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2))) =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) ((QuadraticMap.prod Q₁ Q₂) m)

Tactic:
QuadraticMap.prod_apply,

Goal state after:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
m : M₁ × M₂
⊢ ((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₁ 1).subtype ((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1)) +
        (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₂ 1).subtype ((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2))) *
      ((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₁ 1).subtype ((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1)) +
        (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₂ 1).subtype ((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2))) =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₁ m.1 + Q₂ m.2)
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
⊢ Module R (⨁ (i : I), A i)

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
⊢ ringConGen (rel R A) = (ringConGen (rel R A on ⇑ofDirectSum)).comap (powerAlgebraEquivFreeTensorAlgebra R A).symm

Tactic:
RingCon.comap_ringConGen_ringEquiv

Goal state after:
I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
⊢ ringConGen (rel R A) =
    ringConGen (rel R A on ⇑ofDirectSum on ⇑(powerAlgebraEquivFreeTensorAlgebra R A).toRingEquiv.symm)
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
⊢ Semiring (FreeProduct R A)

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
⊢ Algebra R (FreeProduct R A)

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
⊢ LinearIndependent S (⇑(Pi.algebraMap ι' R S) ∘ v) ↔ LinearIndependent R v

Tactic:
refine ⟨fun h ↦ (h.restrict_scalars' R).of_comp, fun h ↦ ?_⟩

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
h : LinearIndependent R v
⊢ LinearIndependent S (⇑(Pi.algebraMap ι' R S) ∘ v)
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case top
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : LT m
l' : m → WithTop n
hl : A.IsPivotedBy l
hl' : A.IsPivotedBy l'
i : m
hc' : l' i = ⊤
⊢ l i = ⊤

Tactic:
rw [hl.eq_top_iff, ← hl'.eq_top_iff]

Goal state after:
case top
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : LT m
l' : m → WithTop n
hl : A.IsPivotedBy l
hl' : A.IsPivotedBy l'
i : m
hc' : l' i = ⊤
⊢ l' i = ⊤
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case pos
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : PartialOrder m
hA : A.IsPivotedBy l
i₁ i₂ : m
hlt : i₁ < i₂
h₁ : l i₁ = ⊤
⊢ l i₁ ≤ l i₂

Tactic:
simp [hA.eq_top_iff.mpr (hA.isRowEchelon.row_eq_zero_of_lt hlt (hA.eq_top_iff.mp h₁))]

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

Goal state before:
pp: n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
hexpand : ∀ (j : n), (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j
hdvd : ∀ (j : n), 4 ∣ (1 + A s j * A r j) * (1 + A t j * A r j)
hsum : ∑ j, (1 + A s j * A r j) * (1 + A t j * A r j) = ↑(Fintype.card n)
⊢ 4 ∣ Fintype.card n

Tactic:
rw [← Int.ofNat_dvd, ← hsum]

Goal state after:
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
hexpand : ∀ (j : n), (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j
hdvd : ∀ (j : n), 4 ∣ (1 + A s j * A r j) * (1 + A t j * A r j)
hsum : ∑ j, (1 + A s j * A r j) * (1 + A t j * A r j) = ↑(Fintype.card n)
⊢ ↑4 ∣ ∑ j, (1 + A s j * A r j) * (1 + A t j * A r j)
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
⊢ ?m.106

Tactic:
by simpa [Function.Surjective] using hg

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

Goal state before:
pp: R : Type u_1
m✝ : Type u_2
n✝ : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype m✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m✝
inst✝¹ : DecidableEq n✝
A✝ : Matrix n✝ n✝ R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Function.Injective ⇑f
g : (Fin m → R) →ₗ[R] Fin n → R := LinearMap.pi fun i ↦ if h : ↑i < m then LinearMap.proj ⟨↑i, h⟩ else 0
hnm : m < n
hg : Function.Injective ⇑g
A : Matrix (Fin n) (Fin n) R := LinearMap.toMatrix' (g ∘ₗ f)
x✝¹ : Fin n → R
x✝ : Fin n
⊢ (A *ᵥ x✝¹) x✝ = (⇑g ∘ ⇑f) x✝¹ x✝

Tactic:
simp [A, g]

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

Goal state before:
pp: R : Type u_1
m✝ : Type u_2
n✝ : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype m✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m✝
inst✝¹ : DecidableEq n✝
A✝ : Matrix n✝ n✝ R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Function.Injective ⇑f
g : (Fin m → R) →ₗ[R] Fin n → R := LinearMap.pi fun i ↦ if h : ↑i < m then LinearMap.proj ⟨↑i, h⟩ else 0
hnm : m < n
hg : Function.Injective ⇑g
A : Matrix (Fin n) (Fin n) R := LinearMap.toMatrix' (g ∘ₗ f)
hA : A.Nonsingular
x✝ : Fin n
⊢ A.row ⟨m, hnm⟩ x✝ = 0 x✝

Tactic:
simp [A, g]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: F : Type u_2
inst✝ : Field F
hF : 4 ≤ Nat.card F
this : Finite F
⊢ IsCyclic Fˣ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case inl
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : SpecialLinearGroup R V
hR : Subsingleton R
⊢ g ∈ Subgroup.center (SpecialLinearGroup R V) ↔ ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑g = r • LinearMap.id

Tactic:
have : Subsingleton (SpecialLinearGroup R V) := inferInstance

Goal state after:
case inl
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : SpecialLinearGroup R V
hR : Subsingleton R
this : Subsingleton (SpecialLinearGroup R V)
⊢ g ∈ Subgroup.center (SpecialLinearGroup R V) ↔ ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑g = r • LinearMap.id
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

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✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ (∑ p ∈ l.support.sym2, polarSym2 (⇑Q) (Sym2.map (fun i ↦ l i • g i) p) - l.sum fun i a ↦ a • a • Q (g i)) =
    ∑ x ∈ l.support.sym2, l.sym2Mul x • (polarSym2 ⇑Q ∘ Sym2.map g) x - ∑ x ∈ l.support, (l * l) x • (⇑Q ∘ g) x

Tactic:
simp [Finsupp.sum, ← polarSym2_map_smul, mul_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

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✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ (l.sum fun i r ↦ r • r • Q (g i)) +
      ∑ p ∈ l.support.sym2 with ¬p.IsDiag, polarSym2 (⇑Q) (Sym2.map (fun i ↦ l i • g i) p) =
    ∑ x ∈ l.support, (l * l) x • (⇑Q ∘ g) x +
      ∑ p ∈ l.support.sym2 with ¬p.IsDiag, (Sym2.map (⇑l) p).mul • polarSym2 (⇑Q) (Sym2.map g p)

Tactic:
simp [Finsupp.sum, ← polarSym2_map_smul, mul_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Real

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
w : ι → ℝ
u : ι → ℝˣ := fun i ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|↑(u i)| ≠ 0
hwu : ∀ (i : ι), w i / |↑(u i)| = ↑(sign (w i))
v : ι → ℝ
this : ∑ i, w i / |↑(u i)| * v i ^ 2 = ∑ i, w i * (v i ^ 2 * |↑(u i)|⁻¹)
⊢ (weightedSumSquares ℝ fun i ↦ ↑(sign (w i))) v =
    ((weightedSumSquares ℝ w).basisRepr ((Pi.basisFun ℝ ι).unitsSMul fun i ↦ Units.mk0 (1 / √|↑(u i)|) ⋯)) v

Tactic:
by
    simpa [basisRepr_apply, Basis.unitsSMul_apply, ← _root_.sq, mul_pow, ← hwu, Pi.single_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
V : Submodule R M
⊢ Module.finrank R ↥⊥ ≤ Module.finrank R M ∧
    ∃ V, Module.finrank R ↥V = Module.finrank R ↥⊥ ∧ (QuadraticMap.restrict Q V).PosDef

Tactic:
refine ⟨?_, ⟨⊥, rfl, fun x hx' ↦ (hx' <| Subsingleton.elim x 0).elim⟩⟩

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
V : Submodule R M
⊢ Module.finrank R ↥⊥ ≤ Module.finrank R M
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: case e'_2
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ -weightedSumSquares 𝕜 w = weightedSumSquares 𝕜 (-w)

pp: case e'_3
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ {i | w i < 0} = {i | 0 < (-w) i}

Tactic:
· ext; simp

Goal state after:
case e'_3
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ {i | w i < 0} = {i | 0 < (-w) i}
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra✝ : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
contra : P.root m = P.root i
⊢ False

Tactic:
replace h₂ : P.root k = P.root i + P.root j := by rwa [contra, sub_eq_iff_eq_add] at h₂

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra✝ : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
contra : P.root m = P.root i
h₂ : P.root k = P.root i + P.root j
⊢ False