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

Goal state before:
pp: case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s,
      (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) + ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp))) x ∂μ =
    ∫ (x : α) in s, (↑↑(MemLp.toLp f hf_Lp) + ↑↑(MemLp.toLp g hg_Lp)) x ∂μ

Tactic:
Pi.add_apply

Goal state after:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s,
      ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x + ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x + ↑↑(MemLp.toLp g hg_Lp) x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
this : ∫ (x : α) in Set.univ, μ[f | m] x ∂μ = ∫ (x : α) in Set.univ, f x ∂μ
⊢ ∫ (x : α), μ[f | m] x ∂μ = ∫ (x : α), f x ∂μ

Tactic:
setIntegral_univ

Goal state after:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
this : ∫ (x : α), μ[f | m] x ∂μ = ∫ (x : α), f x ∂μ
⊢ ∫ (x : α), μ[f | m] x ∂μ = ∫ (x : α), f x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case pos.refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
⊢ ∀ (s_1 : Set α), MeasurableSet s_1 → (μ.restrict s) s_1 < ∞ → IntegrableOn 0 s_1 (μ.restrict s)

Tactic:
exact fun t _ _ => (integrable_zero _ _ _).integrableOn

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✝⁵ : 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 : ι
⊢ ∑ j, ∑ l, A i j * b.toMatrix p j l = ∑ l, ∑ j, A i j * b.toMatrix p j l

Tactic:
rw [Finset.sum_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case e'_6.e'_3.e'_9
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
a✝ : Perm (ιa ⊕ ιb)
k : ιa
⊢ v ((swap i j) (a✝ (Sum.inl k))) = v (a✝ (Sum.inl k))

Tactic:
rw [Equiv.apply_swap_eq_self hv]

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case e'_6.e'_3.e'_10
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
a✝ : Perm (ιa ⊕ ιb)
k : ιb
⊢ v ((swap i j) (a✝ (Sum.inr k))) = v (a✝ (Sum.inr k))

Tactic:
rw [Equiv.apply_swap_eq_self hv]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝¹² : CommSemiring R
S : Type u_2
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
M : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this✝ : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ (Finsupp.llift N R R ι).symm
f : (M →ₗ[R] P) ≃ₗ[S] ι → P := LinearEquiv.congrLeft P S b.repr ≪≫ₗ (Finsupp.llift P R S ι).symm
h : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P := linearMapRightBaseChangeHom S M ε
e' : S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] S ⊗[R] (ι → N) := LinearEquiv.baseChange R S (M →ₗ[R] N) (ι → N) e
h' : S ⊗[R] (ι → N) →ₗ[S] ι → P := (↑f ∘ₗ linearMapRightBaseChangeHom S M ε) ∘ₗ ↑e'.symm
this : Function.Bijective ⇑h'
⊢ Function.Bijective ⇑(linearMapRightBaseChangeHom S M ε)

Tactic:
by simpa [h'] using this

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
⊢ alternatization (a.domCoprod b) = (alternatization a).domCoprod (alternatization b)

Tactic:
apply coe_multilinearMap_injective
  rw [domCoprod_coe, MultilinearMap.alternatization_coe,
    Finset.sum_partition (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)]
  congr 1
  ext1 σ
  induction σ using Quotient.inductionOn' with
  | h σ =>
  set f := sumCongrHom ιa ιb
  calc
    ∑ τ ∈ _, sign τ • domDomCongr τ (a.domCoprod b) =
        ∑ τ ∈ {τ | τ⁻¹ * σ ∈ f.range}, sign τ • domDomCongr τ (a.domCoprod b) := by
      simp [QuotientGroup.leftRel_apply, f, Quotient.eq]
    _ = ∑ τ ∈ {τ | τ⁻¹ ∈ f.range}, sign (σ * τ) • domDomCongr (σ * τ) (a.domCoprod b) := by
      conv_lhs => rw [← Finset.map_univ_equiv (Equiv.mulLeft σ), Finset.filter_map, Finset.sum_map]
      simp [-MonoidHom.mem_range]
    _ = ∑ τ, sign (σ * f τ) • domDomCongr (σ * f τ) (a.domCoprod b) := by
      simp_rw [f, Subgroup.inv_mem_iff, MonoidHom.mem_range, Finset.univ_filter_exists,
        Finset.sum_image sumCongrHom_injective.injOn]
    _ = ∑ τ : Perm ιa × Perm ιb,
         sign σ • (domDomCongrEquiv σ) (sign τ.1 • sign τ.2 •
           (domDomCongr τ.1 a).domCoprod (domDomCongr τ.2 b)) := by
      simp [f, domDomCongr_mul, domCoprod_domDomCongr_sumCongr, mul_smul]
    _ = domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ) := by
      simp [domCoprod.summand_mk'', domCoprod_alternization_coe, ← domDomCongrEquiv_apply,
        Finset.smul_sum, ← Finset.sum_product']

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

Goal state before:
pp: case «1»
R : Type u_3
V : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid V
inst✝³ : Module R V
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : StrongRankCondition R
f : Dual R V
v : V
hfv : f v = 0
h : finrank R V = 1
h1 : 1 ≤ 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
⊢ f x • v = 0

Tactic:
suffices ∀ x, x = b.repr x i • (b i) by
      rw [this v, map_smul, smul_eq_mul, mul_comm] at hfv
      rw [this x, this v, map_smul, smul_eq_mul, ← mul_smul, mul_assoc, hfv, mul_zero, zero_smul]

Goal state after:
case «1»
R : Type u_3
V : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid V
inst✝³ : Module R V
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : StrongRankCondition R
f : Dual R V
v : V
hfv : f v = 0
h : finrank R V = 1
h1 : 1 ≤ 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
⊢ ∀ (x : V), x = (b.repr x) i • b i
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
x y : A ⊗[R] M₂
hx : Q₁ x = Q₂ x
hy : Q₁ y = Q₂ y
x✝¹ x✝ : M₂
⊢ Q₁ (1 ⊗ₜ[R] x✝¹ + 1 ⊗ₜ[R] x✝) - Q₁ (1 ⊗ₜ[R] x✝¹) - Q₁ (1 ⊗ₜ[R] x✝) =
    Q₂ (1 ⊗ₜ[R] x✝¹ + 1 ⊗ₜ[R] x✝) - Q₂ (1 ⊗ₜ[R] x✝¹) - Q₂ (1 ⊗ₜ[R] x✝)

Tactic:
rw [← TensorProduct.tmul_add, h, h, h]

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 Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q
⊢ (changeForm ⋯) x = x

Tactic:
simp_rw [(add_neg_cancel B), changeForm_self_apply]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ star y ∈ lipschitzGroup Q

Tactic:
rw [← hy₂] at hx₃

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : ↑y * star ↑y = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ star y ∈ lipschitzGroup Q
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ toTensorAlgebra (DirectSum.GAlgebra.toFun r) = (algebraMap R (TensorAlgebra R M)) r

Tactic:
rw [TensorPower.galgebra_toFun_def, TensorPower.algebraMap₀_eq_smul_one, map_smul,
    TensorPower.toTensorAlgebra_gOne, Algebra.algebraMap_eq_smul_one]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : CommRing S
inst✝³ : LinearOrder S
inst✝² : IsStrictOrderedRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), abv (A i j) ≤ x
⊢ ∑ _σ, ∏ _i, x = (Fintype.card n)! • x ^ Fintype.card n

Tactic:
by simp [Fintype.card_perm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ A.IsTotallyUnimodular → ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
intro hA

Goal state after:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
⊢ ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast) → A.IsTotallyUnimodular

Tactic:
intro hA

Goal state after:
case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ A.IsTotallyUnimodular
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ A.IsTotallyUnimodular

Tactic:
intro _ _ _ _ _

Goal state after:
case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
f✝ : Fin k✝ → m
g✝ : Fin k✝ → n
a✝¹ : Function.Injective f✝
a✝ : Function.Injective g✝
⊢ (A.submatrix f✝ g✝).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast) →
    ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
      (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
intro hA

Goal state after:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
    (A.submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
      (A.submatrix f g).det ∈ Set.range SignType.cast) →
    ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
intro hA

Goal state after:
case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA :
  ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
    (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
ih : C (T • B)
⊢ C (S • S • S • T • S • T • S • T • B)

Tactic:
solve_by_elim (maxDepth := 10)

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
e₁ e₂ : m ≃ n
h : (A.submatrix ⇑e₁ ⇑e₂).IsHadamard
⊢ A.IsHadamard

Tactic:
simpa using h.reindex e₁ e₂

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
i : m
i' : n
j : m
j' : n
⊢ ∑ x₁, ∑ x₂, Bᴴ i' x₂ * (Aᴴ i x₁ * A x₁ j) * B x₂ j' = if i = j then ∑ x, Bᴴ i' x * (Fintype.card m • B) x j' else 0

Tactic:
rw [Finset.sum_comm]

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
i : m
i' : n
j : m
j' : n
⊢ ∑ y, ∑ x, Bᴴ i' y * (Aᴴ i x * A x j) * B y j' = if i = j then ∑ x, Bᴴ i' x * (Fintype.card m • B) x j' else 0
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: case inr.inr
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
i j : n
hij : Sum.inr i ≠ Sum.inr j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inr i) (Sum.inr j) = 0

Tactic:
· exact hd (ne_of_apply_ne _ hij)

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
N₁ N₂ : Matrix ι ι R
v : ι → M
i : ι
⊢ ∑ x, ∑ x_1, N₁ i x_1 • N₂ x_1 x • v x = ∑ x, ∑ x_1, N₁ i x • N₂ x x_1 • v x_1

Tactic:
rw [Finset.sum_comm]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
a : n → R
⊢ swap R i j *ᵥ a = a ∘ ⇑(Equiv.swap i j)

Tactic:
by
  simp [swap, PEquiv.toMatrix_toPEquiv_mulVec]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
a : n → R
⊢ (swap R i j *ᵥ a) i = a j

Tactic:
by
  simp [swap, PEquiv.toMatrix_toPEquiv_mulVec]

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

Goal state before:
pp: R : Type u_2
inst✝³ : CommSemiring R
n : Type u_3
inst✝² : Unique n
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
⊢ A.permanent = A default default

Tactic:
by simp [permanent, univ_unique]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
⊢ Finite V

Tactic:
let eq : { v : V // v ≠ 0 } ⊕ Unit ≃ V :=
    ⟨(Sum.elim Subtype.val (fun _ ↦ 0)), fun v ↦ if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩,
      by intro x; aesop, by intro x; aesop⟩

Goal state after:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
eq : { v // v ≠ 0 } ⊕ Unit ≃ V :=
  { toFun := Sum.elim Subtype.val fun x ↦ 0, invFun := fun v ↦ if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩,
    left_inv := ⋯, right_inv := ⋯ }
⊢ Finite V
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: k✝ : Type u_1
V✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : AddCommGroup V✝
inst✝⁴ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
⊢ Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i

Tactic:
refine Nat.mul_right_cancel (m := Nat.card k - 1) (by lia) ?_

Goal state after:
k✝ : Type u_1
V✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : AddCommGroup V✝
inst✝⁴ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
⊢ Nat.card (ℙ k V) * (Nat.card k - 1) = (∑ i ∈ Finset.range n, Nat.card k ^ i) * (Nat.card k - 1)
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: k✝ : Type u_1
V✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : AddCommGroup V✝
inst✝⁴ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
hc : Nat.card V = Nat.card k ^ n
| (∑ x ∈ Finset.range n, ↑(Nat.card k) ^ x) * ↑(Nat.card k - 1)

Tactic:
rw [Int.natCast_sub this.le, Int.natCast_one, geom_sum_mul]

Goal state after:
k✝ : Type u_1
V✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : AddCommGroup V✝
inst✝⁴ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
hc : Nat.card V = Nat.card k ^ n
| ↑(Nat.card k) ^ n - 1
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ IsCollinear ∅

Tactic:
by
  rw [IsCollinear_iff_rank]
  use ⊥
  rw [map_bot]
  simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
m : M
h : Q (m + m) - Q m - Q m = 0
⊢ Q m = 0

Tactic:
← two_smul R,

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
m : M
h : Q (2 • m) - Q m - Q m = 0
⊢ Q m = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
m : M
h : (2 * 2) • Q m - (Q m + Q m) = 0
⊢ Q m = 0

Tactic:
← two_smul R,

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
m : M
h : (2 * 2) • Q m - 2 • Q m = 0
⊢ Q m = 0
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
j k : ι
hj : j ∈ b.support
hkj : k ≠ j
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hij : l ≠ j
hi : l ∈ b.support
hk' : P.root k + P.root l ∈ range ⇑P.root
hl : P.root k = P.root j
⊢ False

Tactic:
P.root.injective.eq_iff

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
j k : ι
hj : j ∈ b.support
hkj : k ≠ j
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hij : l ≠ j
hi : l ∈ b.support
hk' : P.root k + P.root l ∈ range ⇑P.root
hl : k = j
⊢ False