mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
rw [klDiv_of_not_ac h_ac]
    rw [Measure.absolutelyContinuous_compProd_iff] at h_ac
    simp only [not_and_or] at h_ac
    cases h_ac with
    | inl h => simp [h]
    | inr h => simp [h]

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
simp_rw [klDiv_of_ac_of_integrable h_ac h_int, klDiv_of_ac_of_integrable h_ac_μν h_int_μν,
    klDiv_of_ac_of_integrable h_ac_κη h_int_κη,
    ← ENNReal.ofReal_add (integral_llr_add_sub_measure_univ_nonneg h_ac_μν h_int_μν)
    (integral_llr_add_sub_measure_univ_nonneg h_ac_κη h_int_κη), measureReal_def,
    Measure.compProd_apply_univ, add_sub_cancel_right]

Goal state after:
case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ ENNReal.ofReal (∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) x ∂μ ⊗ₘ κ + (ν univ).toReal - (μ univ).toReal) =
    ENNReal.ofReal
      (∫ (x : 𝓧), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal + ∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) x ∂μ ⊗ₘ κ)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
A : μ[fun x ↦ (ENNReal.ofReal (f x)).toReal | m] =ᵐ[μ] μ[f | m]
B : 0 ≤ᵐ[μ] μ[f | m]
g : 𝓧 → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (f x)
this : ∫⁻ (x : 𝓧), g x ∂μ = ∫⁻ (x : 𝓧), ‖f x‖ₑ ∂μ
⊢ ∫⁻ (x : 𝓧), ‖f x‖ₑ ∂μ ≠ ∞

Tactic:
exact hf.2.ne

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case pos.h12
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
a✝ : (P.trim hm) s < ∞
⊢ ∫⁻ (x : Ω) in s, P⁻[X | mΩ] x + P⁻[Y | mΩ] x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[X + Y | mΩ] x ∂P.trim hm

Tactic:
rw [lintegral_add_left (by fun_prop)]

Goal state after:
case pos.h12
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
a✝ : (P.trim hm) s < ∞
⊢ ∫⁻ (a : Ω) in s, P⁻[X | mΩ] a ∂P.trim hm + ∫⁻ (a : Ω) in s, P⁻[Y | mΩ] a ∂P.trim hm ≤
    ∫⁻ (x : Ω) in s, P⁻[X + Y | mΩ] x ∂P.trim hm
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case e'_4
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
s : Finset ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ ∑ i ∈ s, X i = ∑' (i : ↥s), X ↑i

Tactic:
simp [Finset.sum_attach]

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✝⁵ : PartialOrder k
inst✝⁴ : IsOrderedAddMonoid k
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Module k V
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x < 0 ∨ 1 < x
⊢ Disjoint s.closedInterior ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) x)

Tactic:
refine Set.disjoint_left.mpr fun p hleft hright ↦ ?_
  obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype <|
    s.closedInterior_subset_affineSpan hleft
  rw [SetLike.mem_coe, s.independent.affineCombination_mem_shift_iff i hw] at hright
  rw [affineCombination_mem_closedInterior_iff hw] at hleft
  grind

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

Goal state before:
pp: case h
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e✝ e : V ≃ₗ[R] V
f : Dual R V
v : V
he : ↑e = LinearMap.transvection f v
x : V
⊢ e x = x + f x • v

Tactic:
← coe_coe,

Goal state after:
case h
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e✝ e : V ≃ₗ[R] V
f : Dual R V
v : V
he : ↑e = LinearMap.transvection f v
x : V
⊢ ↑e x = x + f x • v
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
hx : x = b i + r • b j
h1 : s + t * (b.coord i) (f (b i)) = 0
⊢ s * r + t * r * (b.coord j) (f (b j)) = 0

Tactic:
suffices s * r + t * ((b.repr (f (b i))) j + r * (b.repr (f (b j))) j) = 0 by
        rw [mul_add, ← add_assoc, add_right_comm, add_eq_zero_iff_eq_neg, ← mul_assoc] at this
        rw [Basis.coord_apply, this, feq]
        simp [single_eq_of_ne' hij]

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
hx : x = b i + r • b j
h1 : s + t * (b.coord i) (f (b i)) = 0
⊢ s * r + t * ((b.repr (f (b i))) j + r * (b.repr (f (b j))) j) = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Star

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
m : M
⊢ star ((ι Q) m) = -(ι Q) m

Tactic:
rw [star_def, involute_ι, map_neg, reverse_ι]

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
x : M
⊢ d x • 1 = (algebraMap R (CliffordAlgebra Q)) (d x)

Tactic:
Algebra.algebraMap_eq_smul_one

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

Goal state before:
pp: ⊢ (ι Q) 1 * (ι Q) 1 = -1

Tactic:
by
      rw [CliffordAlgebra.ι_sq_scalar, Q_apply, one_mul, map_neg, map_one]

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

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
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m₁ m₂ : M
⊢ (((foldr Q (fFold f) ⋯) (((foldr Q (fFold f) ⋯) (1, 0)) ((CliffordAlgebra.ι Q) m₂))) ((CliffordAlgebra.ι Q) m₁)).1 =
    (f.bilin m₁) m₂

Tactic:
foldr_ι,

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
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m₁ m₂ : M
⊢ (((fFold f) m₁) (((foldr Q (fFold f) ⋯) (1, 0)) ((CliffordAlgebra.ι Q) m₂))).1 = (f.bilin m₁) 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)
⊢ gradedCommAux R 𝒜 ℬ ∘ₗ gradedCommAux R ℬ 𝒜 = LinearMap.id

Tactic:
by
  ext i a b
  dsimp
  rw [gradedCommAux_lof_tmul, LinearMap.map_smul_of_tower, gradedCommAux_lof_tmul, smul_smul,
    mul_comm i.2 i.1, Int.units_mul_self, one_smul]

Goal state after:
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)
i j : ι
a : 𝒜 i
b : ℬ j
⊢ (gradedComm R 𝒜 ℬ) ((lof R ι 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ j) b) = (-1) ^ (j * i) • (lof R ι ℬ j) b ⊗ₜ[R] (lof R ι 𝒜 i) a

Tactic:
rw [gradedComm]
  dsimp only [LinearEquiv.trans_apply, LinearEquiv.coe_ofLinearMap]
  rw [TensorProduct.directSum_lof_tmul_lof, gradedCommAux_lof_tmul, Units.smul_def,
    -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 specialized `map_smul` to `LinearEquiv.map_smul` to avoid timeouts.
    ← Int.cast_smul_eq_zsmul R, LinearEquiv.map_smul, TensorProduct.directSum_symm_lof_tmul,
    Int.cast_smul_eq_zsmul, ← Units.smul_def]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: case e_a.e_a
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 z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ ixb * iya + (ixb * iza + iyb * iza) = iyb * iza + (ixb * iya + ixb * iza)

Tactic:
abel

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
⊢ ∀ (x y : B),
    { toFun := fun b ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } (x * y) =
      { toFun := fun b ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } x *
        { toFun := fun b ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } y

Tactic:
LinearMap.map_mul_iff

Goal state after:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
⊢ (LinearMap.mul R B).compr₂ { toFun := fun b ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } =
    (LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ) ∘ₗ { toFun := fun b ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ }).compl₂
      { toFun := fun b ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ }
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : Ring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Module ι (Additive ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
f : A →ₐ[R] C
g : B →ₐ[R] C
h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)
⊢ ∀ (x y : 𝒜 ᵍ⊗[R] ℬ),
    (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) (x * y) =
      (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) x *
        (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) y

Tactic:
LinearMap.map_mul_iff

Goal state after:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : Ring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Module ι (Additive ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
f : A →ₐ[R] C
g : B →ₐ[R] C
h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)
⊢ (LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ)).compr₂
      (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) =
    (LinearMap.mul R C ∘ₗ
          LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm).compl₂
      (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm)
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₂
⊢ (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₁ m.1) + (ι Q₁) m.1 ᵍ⊗ₜ[R] (ι Q₂) m.2 +
      (-(ι Q₁) m.1 ᵍ⊗ₜ[R] (ι Q₂) m.2 + (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₂ m.2)) =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₁ m.1) + (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₂ m.2)

Tactic:
abel

Goal state after:
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
⊢ r • 1 = (algebraMap R (TensorAlgebra R M)) r

Tactic:
Algebra.algebraMap_eq_smul_one

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ r • 1 = r • 1
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: case e_a
α : Type u_1
n : Type u_3
inst✝³ : CommMagma α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ x - j = i - (i - x + j)

Tactic:
abel

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

Goal state before:
pp: α : Type u_1
n : Type u_5
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : AddGroup n
inst✝ : Fintype n
a : α
⊢ circulant (Pi.single 0 a) = (scalar n) a

Tactic:
ext i j
  simp [Pi.single_apply, diagonal_apply, sub_eq_zero]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type v
A : Matrix m n R
inst✝³ : Zero R
inst✝² : LinearOrder m
inst✝¹ : LT n
inst✝ : One R
i₁ i₂ : m
c : n
hA : A.IsReducedRowEchelon
hne : i₁ ≠ i₂
hlead : A.IsLeadingEntry i₂ c
⊢ A i₁ c = 0

Tactic:
by
  rcases hne.lt_or_gt with hlt | hlt
  · exact hA.eq_zero hlt hlead
  · exact hA.isRowEchelon hlt hlead.1

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case e_a
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
⊢ ∏ x, (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index =
    ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index

Tactic:
congr! with i

Goal state after:
case e_a.a
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
i : Fin n
a✝ : i ∈ Finset.univ
⊢ ⋯.choose = i
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (i : Fin (n + 1)), i ≠ i₀ → ∑ j, M i j = 0
⊢ ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, Mᵀ i i₀) * (M.submatrix i₀.succAbove j₀.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ j, M i₀ j) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
simp_rw [transpose_apply]

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
μ : 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
j : n
⊢ ‖v j‖ * ‖v i‖⁻¹ ≤ 1

Tactic:
mul_inv_le_iff₀ (norm_pos_iff.mpr h_nz),

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
j : n
⊢ ‖v j‖ ≤ 1 * ‖v i‖
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 B

Tactic:
rw [show B = T⁻¹ • T • B by simp, ← T_S_rel_smul]

Goal state after:
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)
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case succ
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
n : ℕ
hn : C (T ^ ↑n • B) ↔ C B
⊢ C (T ^ (↑n + 1) • B) ↔ C B

Tactic:
| succ n hn =>

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'
i : ι
inst✝ : DecidableEq ι
⊢ Pi.mulSingle i ((algebraMap R' (A i)) r) = update (fun i ↦ 1) i (r • 1)

Tactic:
Algebra.algebraMap_eq_smul_one

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'
i : ι
inst✝ : DecidableEq ι
⊢ Pi.mulSingle i (r • 1) = update (fun i ↦ 1) i (r • 1)
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: case succ
R : Type u_1
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
n : ℕ
hn :
  ∀ {ι : Type u_2} [Finite ι] {M : ι → Type u_3} {γ : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (M i)]
    [inst_1 : (i : ι) → Module R (M i)] {g : ⦃i : ι⦄ → γ i → M i},
    (∀ (i : ι), Submodule.span R (Set.range g) = ⊤) →
      ∀ {φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N},
        (∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))) → Nat.card ι = n → φ = φ'
ι : Type u_2
inst✝² : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N
h : ∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))
hι : Nat.card ι = n + 1
⊢ φ = φ'

Tactic:
| succ n hn =>

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✝² : (i : ι) → CommSemiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : Fintype ι
toFun : (⨂[R] (i : ι), R) →ₗ[R] R := lift (MultilinearMap.mkPiAlgebra R ι R)
this✝ : IsScalarTower R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := IsScalarTower.right
this : SMulCommClass R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := Algebra.to_smulCommClass
⊢ ∀ (x y : ⨂[R] (x : ι), R), toFun (x * y) = toFun x * toFun y

Tactic:
LinearMap.map_mul_iff

Goal state after:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝³ : CommSemiring R
inst✝² : (i : ι) → CommSemiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : Fintype ι
toFun : (⨂[R] (i : ι), R) →ₗ[R] R := lift (MultilinearMap.mkPiAlgebra R ι R)
this✝ : IsScalarTower R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := IsScalarTower.right
this : SMulCommClass R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := Algebra.to_smulCommClass
⊢ (LinearMap.mul R (⨂[R] (x : ι), R)).compr₂ toFun = (LinearMap.mul R R ∘ₗ toFun).compl₂ toFun
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: case inl.inl
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Finite V
this✝¹ : Fintype V
this✝ : Fintype (ℙ k V)
this : Fintype k
hV : Fintype.card { v // v ≠ 0 } = Fintype.card V - 1
⊢ Fintype.card { v // v ≠ 0 } = Fintype.card (ℙ k V) * Fintype.card kˣ

Tactic:
rw [Fintype.card_congr (nonZeroEquivProjectivizationProdUnits k V), Fintype.card_prod]

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

Goal state before:
pp: G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
e : V ≃ₗ[K] V
D : ℙ K V
⊢ e • D = LinearMap.GeneralLinearGroup.ofLinearEquiv e • D

Tactic:
rw [← mk_rep D, smul_mk, smul_mk]

Goal state after:
G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
e : V ≃ₗ[K] V
D : ℙ K V
⊢ mk K (e • D.rep) ⋯ = mk K (LinearMap.GeneralLinearGroup.ofLinearEquiv e • D.rep) ⋯