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
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s

Tactic:
let Y := (Submodule.span ℝ t).topologicalClosure

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
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
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
this✝¹ : CompleteSpace ↥Y
this✝ : SecondCountableTopology ↥Y
fY : α → ↥Y := fun a ↦ if h : f a ∈ Y then ⟨f a, h⟩ else 0
fX : α → E := ⇑Y.subtypeL ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᵐ[μ] fX
lem2 : ∀ᵐ (a : α) ∂μ, fY a ∈ ⇑Y.subtypeL ⁻¹' s
g : α → E
hg1 : StronglyMeasurable g
hg2 : ∀ (x : α), g x ∈ ↑(Submodule.span ℝ t).topologicalClosure
hg3 : f =ᵐ[μ] g
a : α
ha : f a = g a
this : g a ∈ Y
⊢ fY a = codRestrict g (↑Y) hg2 a

Tactic:
simp_all [fY, codRestrict]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: case ht
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᵐ[μ.restrict (spanningSets (μ.trim hm) n)] μ[f | m]
⊢ (μ.restrict (spanningSets (μ.trim hm) n)) {x | (fun a ↦ μ[f | m] a ∈ s) x}ᶜ = 0

Tactic:
have : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n)) := isFiniteMeasure_restrict.2
    ((le_trim hm).trans_lt (measure_spanningSets_lt_top (μ.trim hm) n)).ne

Goal state after:
case ht
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᵐ[μ.restrict (spanningSets (μ.trim hm) n)] μ[f | m]
this : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n))
⊢ (μ.restrict (spanningSets (μ.trim hm) n)) {x | (fun a ↦ μ[f | m] a ∈ s) x}ᶜ = 0
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
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]

Tactic:
let Y := (Submodule.span ℝ t).topologicalClosure

Goal state after:
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
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
⊢ φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]
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
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
this✝¹ : CompleteSpace ↥Y
this✝ : SecondCountableTopology ↥Y
φY : ↥Y → ℝ := φ ∘ ⇑Y.subtypeL
fY : α → ↥Y := fun a ↦ if h : f a ∈ Y then ⟨f a, h⟩ else 0
fX : α → E := ⇑Y.subtypeL ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᵐ[μ] fX
g : α → E
hg1 : StronglyMeasurable g
hg2 : ∀ (x : α), g x ∈ ↑(Submodule.span ℝ t).topologicalClosure
hg3 : f =ᵐ[μ] g
a : α
ha : f a = g a
this : g a ∈ Y
⊢ fY a = codRestrict g (↑Y) hg2 a

Tactic:
simp_all [fY, codRestrict]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: case ht
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
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᵐ[μ.restrict (spanningSets (μ.trim hm) n)] μ[f | m]
h2 : (μ.restrict (spanningSets (μ.trim hm) n))[φ ∘ f | m] =ᵐ[μ.restrict (spanningSets (μ.trim hm) n)] μ[φ ∘ f | m]
⊢ (μ.restrict (spanningSets (μ.trim hm) n)) {x | (fun x ↦ (φ ∘ μ[f | m]) x ≤ μ[φ ∘ f | m] x) x}ᶜ = 0

Tactic:
have : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n)) := isFiniteMeasure_restrict.2
    ((le_trim hm).trans_lt (measure_spanningSets_lt_top (μ.trim hm) n)).ne

Goal state after:
case ht
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
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᵐ[μ.restrict (spanningSets (μ.trim hm) n)] μ[f | m]
h2 : (μ.restrict (spanningSets (μ.trim hm) n))[φ ∘ f | m] =ᵐ[μ.restrict (spanningSets (μ.trim hm) n)] μ[φ ∘ f | m]
this : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n))
⊢ (μ.restrict (spanningSets (μ.trim hm) n)) {x | (fun x ↦ (φ ∘ μ[f | m]) x ≤ μ[φ ∘ f | m] x) x}ᶜ = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
i : ι
⊢ ∑ l, (A * b.toMatrix p) i l = 1

Tactic:
simp [hA, Matrix.one_apply]

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

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ (b.toMatrix ⇑b₂).det • b₂.coords x = (b.toMatrix ⇑b₂)ᵀ.cramer (b.coords x)

Tactic:
← b.toMatrix_inv_vecMul_toMatrix,

Goal state after:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ (b.toMatrix ⇑b₂).det • b.coords x ᵥ* (b.toMatrix ⇑b₂)⁻¹ = (b.toMatrix ⇑b₂)ᵀ.cramer (b.coords x)
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
V : Type u_2
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : Algebra A R
inst✝¹ : Module A V
inst✝ : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
j : R ⊗[A] (ι →₀ A) ≃ₗ[R] ι →₀ R := finsuppScalarRight A R R ι
x : ι →₀ A
this : j (1 ⊗ₜ[A] x) = Finsupp.mapRange ⇑(algebraMap A R) ⋯ x
⊢ (LinearEquiv.ofBijective (Finsupp.linearCombination R ⇑b ∘ₗ ↑j) ⋯) (1 ⊗ₜ[A] x) = (Finsupp.linearCombination A ⇑b) x

Tactic:
by
      simp [this, Finsupp.linearCombination_apply, Finsupp.sum_mapRange_index]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
h : AffineIndependent k p
i : ι
w : ι → k
hw : ∑ i, w i = 1
c : k
j : ι
hj : j ≠ i
q : P
⊢ q ∈ affineSpan k (p '' {i}ᶜ) → (1 - c) • (p i -ᵥ p j) +ᵥ q = (affineCombination k univ p) w → w i = 1 - c

Tactic:
hqmem

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
h : AffineIndependent k p
i : ι
w : ι → k
hw : ∑ i, w i = 1
c : k
j : ι
hj : j ≠ i
q : P
hqmem : q ∈ affineSpan k (p '' {i}ᶜ)
⊢ (1 - c) • (p i -ᵥ p j) +ᵥ q = (affineCombination k univ p) w → w i = 1 - c
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: R : Type u_4
inst✝² : Ring R
V : Type u_5
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : V →ₗ[R] V
⊢ f.fixedSubmodule = (f - id).ker

Tactic:
ext; simp [sub_eq_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e).fixedSubmodule
x : V
hx : x ∈ W
this : e x = x
⊢ (DistribSMul.toLinearMap R V e) x ∈ W

Tactic:
by simpa [this, coe_coe]

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case h
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Free R V
f : V →ₗ[R] V
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
hV1 : Nonempty (Basis Unit R V)
b : Basis Unit R V := Classical.ofNonempty
i : Unit
⊢ f (b i) = ((b.coord ()) (f (b ())) • 1) (b i)

Tactic:
← b.linearCombination_repr (f (b i))

Goal state after:
case h
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Free R V
f : V →ₗ[R] V
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
hV1 : Nonempty (Basis Unit R V)
b : Basis Unit R V := Classical.ofNonempty
i : Unit
⊢ (linearCombination R ⇑b) (b.repr (f (b i))) = ((b.coord ()) (f (b ())) • 1) (b i)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
hy :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ +
      ((foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝)

Tactic:
add_add_add_comm,

Goal state after:
case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
hy :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝ +
      ((foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝)
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
eq_top : (↑e).fixedSubmodule ⊔ K ∙ w = ⊤
v : V := (f w)⁻¹ • (e w - w)
this : f (e w) - f w = 0
⊢ f v = 0

Tactic:
simp only [v, LinearMap.map_smul, map_sub, this, smul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
r : R
b : CliffordAlgebra Q
⊢ (contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r * b) =
    (algebraMap R (CliffordAlgebra Q)) r * (contractLeft d) b

Tactic:
rw [← Algebra.smul_def, map_smul, Algebra.smul_def]

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

Goal state before:
pp: I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
i : I
⊢ (lof R A i) 1 = 1

Tactic:
by
  rw [lof]; dsimp [mkAlgHom]; exact identify_one R A i

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

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq 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
f : FreeProduct R A →ₐ[R] B
i : I
a : A i
h : ∀ (i : I) (x : A i), (f ∘ₐ ι R A i) x = maps x
⊢ (((f ∘ₐ RingCon.mkₐ R (ringCon R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a =
    (((((lift R A) fun {i} ↦ maps) ∘ₐ RingCon.mkₐ R (ringCon R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ
        DirectSum.lof R I A i)
      a

Tactic:
specialize h i a

Goal state after:
I : Type u
inst✝⁵ : DecidableEq 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
f : FreeProduct R A →ₐ[R] B
i : I
a : A i
h : (f ∘ₐ ι R A i) a = maps a
⊢ (((f ∘ₐ RingCon.mkₐ R (ringCon R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a =
    (((((lift R A) fun {i} ↦ maps) ∘ₐ RingCon.mkₐ R (ringCon R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ
        DirectSum.lof R I A i)
      a
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
h : Nonempty n
i j : n
⊢ 1 i j = Pi.single i (↑1) j

Tactic:
simp [one_apply, Pi.single_apply, eq_comm]

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

Goal state before:
pp: case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
⊢ T ^ (-(↑A 0 1 / ↑A 1 1)) • A ∈ reps m

Tactic:
have h2 := Int.emod_def (A.1 0 1) (A.1 1 1)

Goal state after:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * (↑A 0 1 / ↑A 1 1)
⊢ T ^ (-(↑A 0 1 / ↑A 1 1)) • A ∈ reps m
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
A : Matrix n n R
inst✝ : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ j, 0 < A i j
⊢ False

Tactic:
have no_out : ∀ j : n, IsEmpty (i ⟶ j) :=
    fun j => ⟨fun e => h_row ⟨j, e.down⟩⟩

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
A : Matrix n n R
inst✝ : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ j, 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case succ
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
⊢ 0 < (A ^ m * A) i j ↔ Nonempty { p // p.length = m + 1 }

Tactic:
mul_apply

Goal state after:
case succ
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
⊢ 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j ↔ Nonempty { p // p.length = m + 1 }
Module: Mathlib.LinearAlgebra.Matrix.Gershgorin

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖(∑ j ∈ Finset.univ.erase i, A i j * v j) * (v i)⁻¹‖ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖ * ‖v j * (v i)⁻¹‖

Tactic:
Finset.sum_mul

Goal state after:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖∑ i_1 ∈ Finset.univ.erase i, A i i_1 * v i_1 * (v i)⁻¹‖ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖ * ‖v j * (v i)⁻¹‖
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ Aᵀ * Aᵀᴴ = ↑(Fintype.card n) • 1

Tactic:
rw [conjTranspose_transpose_eq_transpose_conjTranspose, ← transpose_mul, hA.conjTranspose_mul,
      transpose_smul, transpose_one]

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

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖
⊢ A.det ≠ 0

Tactic:
by
  rw [← Matrix.det_transpose]
  exact det_ne_zero_of_sum_row_lt_diag (by simp_rw [Matrix.transpose_apply]; exact h)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case neg
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
this : ¬Aᵀ.IsIrreducible
⊢ Aᵀ.IsIrreducible ↔ A.IsIrreducible

Tactic:
have : ¬ A.IsIrreducible := by
      rw [isIrreducible_iff]; simp_all only [not_forall, not_le, isSStronglyConnected_iff,
      not_and, not_exists, not_lt, nonpos_iff_eq_zero, isEmpty_Prop, IsEmpty.forall_iff]

Goal state after:
case neg
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
this✝ : ¬Aᵀ.IsIrreducible
this : ¬A.IsIrreducible
⊢ Aᵀ.IsIrreducible ↔ A.IsIrreducible
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
inst✝ : IsCancelAdd R
⊢ IsRightRegular A ↔ A.Nonsingular

Tactic:
by
  rw [isRightRegular_iff_vecMul_injective, vecMul_injective_iff, linearIndependent_row_iff]

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁶ : CommSemiring R'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ { toFun := fun x ↦ x • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x =
    x * { toFun := fun x ↦ x • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r

Tactic:
simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]

Goal state after:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁶ : CommSemiring R'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • 1 * x = x * r • 1
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁶ : CommSemiring R'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • x = { toFun := fun x ↦ x • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x

Tactic:
simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]

Goal state after:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁶ : CommSemiring R'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • x = r • 1 * x
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: 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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ LinearEquiv.det (LinearMap.equivOfIsUnitDet ⋯) = 1

Tactic:
simp only [← Units.val_inj, LinearEquiv.coe_det, LinearMap.coe_equivOfIsUnitDet,
      LinearMap.det_smul, LinearMap.det_id, mul_one, Units.val_one]

Goal state after:
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ ↑↑r ^ Module.finrank R V = 1