mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ⇑κ =ᵐ[μ] ⇑η
⊢ μ ⊗ₘ κ = μ ⊗ₘ η

Tactic:
rw [compProd, compProd]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ⇑κ =ᵐ[μ] ⇑η
⊢ (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) () = (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η) ()
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ℕ), (((κ.seq i).comap g hg) a) s = ∑' (i : ℕ), ((κ.seq i) (g a)) s

Tactic:
comap_apply' _ hg _ s

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : ¬Measurable g
⊢ (κ.map fun x ↦ (f x, g x)).snd = κ.map g

Tactic:
have : ¬ Measurable (fun x ↦ (f x, g x)) := by
      contrapose hg; exact hg.snd

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : ¬Measurable g
this : ¬Measurable fun x ↦ (f x, g x)
⊢ (κ.map fun x ↦ (f x, g x)).snd = κ.map g
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
hs : MeasurableSet s
⊢ κ.restrict hs ⊗ₖ η = (κ ⊗ₖ η).restrict ⋯

Tactic:
rw [← compProd_restrict hs MeasurableSet.univ]
  congr; exact Kernel.restrict_univ.symm

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
ht₂ : MeasurableSet t₂
⊢ (μ ⊗ₘ κ) (t₁ ×ˢ t₂) = ∫⁻ (a : α) in t₁, μ.rnDeriv ν a * (κ a) t₂ ∂ν

Tactic:
setLIntegral_rnDeriv_mul hμν (κ.measurable_coe ht₂).aemeasurable ht₁,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
ht₂ : MeasurableSet t₂
⊢ (μ ⊗ₘ κ) (t₁ ×ˢ t₂) = ∫⁻ (x : α) in t₁, (κ x) t₂ ∂μ
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:

Tactic:
∫⁻ b, ENNReal.ofReal (η (a, b) (Prod.mk b ⁻¹' s)).toReal ∂κ a
    _ ≤ ∫⁻ b, η (a, b) (Prod.mk b ⁻¹' t) ∂κ a := by
      refine lintegral_mono_ae ?_
      filter_upwards [ae_kernel_lt_top a h2s] with b hb
      rw [ofReal_toReal hb.ne]
      exact measure_mono (preimage_mono (subset_toMeasurable _ _))
    _ ≤ (κ ⊗ₖ η) a t := le_compProd_apply _ _ _ _
    _ = (κ ⊗ₖ η) a s := measure_toMeasurable s
    _ < ⊤ := h2s.lt_top

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ llr μ (c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log c.toReal

Tactic:
simp only [llr, llr_def]
  have h := Measure.rnDeriv_smul_right_of_ne_top μ ν hc hc_ne_top
  filter_upwards [hμν.ae_le h, Measure.rnDeriv_pos hμν, hμν.ae_le (Measure.rnDeriv_lt_top μ ν)]
    with x hx_eq hx_pos hx_ne_top
  rw [hx_eq]
  simp only [Pi.smul_apply, smul_eq_mul, ENNReal.toReal_mul]
  rw [log_mul]
  rotate_left
  · rw [ENNReal.toReal_ne_zero]
    simp [hc, hc_ne_top]
  · rw [ENNReal.toReal_ne_zero]
    simp [hx_pos.ne', hx_ne_top.ne]
  rw [ENNReal.toReal_inv, log_inv]
  ring

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ c⁻¹ ≠ 0

Tactic:
simp [hc_ne_top]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ klDiv μ μ = 0

Tactic:
have h := llr_self μ

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᵐ[μ] 0
⊢ klDiv μ μ = 0
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
hf : AEFinStronglyMeasurable f μ
h'f : ¬f =ᵐ[μ] 0
⊢ ∃ s, MeasurableSet s ∧ 0 < μ s ∧ μ s < ∞

Tactic:
apply hf.finStronglyMeasurable_mk.exists_measurableSet_measure_pos_lt_top

Goal state after:
α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
hf : AEFinStronglyMeasurable f μ
h'f : ¬f =ᵐ[μ] 0
⊢ ¬AEFinStronglyMeasurable.mk f hf =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) x).toReal = (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ llr μ (ν.tilted f) x = -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x

Tactic:
rw [llr, hx, log_mul, log_mul (exp_pos _).ne', log_exp, llr]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) x).toReal = (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ ∫ (x : α), rexp (f x) ∂ν ≠ 0

case hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) x).toReal = (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν ≠ 0

case hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) x).toReal = (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg.refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := (ν univ)⁻¹ • ν
hμν' : μ ≪ ν'
h : 0 ≤ ∫ (a : α), llr μ ν a - log (ν univ)⁻¹.toReal ∂μ + ν'.real univ - μ.real univ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ

Tactic:
integral_sub h_int (integrable_const _),

Goal state after:
case neg.refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := (ν univ)⁻¹ • ν
hμν' : μ ≪ ν'
h : 0 ≤ ∫ (a : α), llr μ ν a ∂μ - ∫ (a : α), log (ν univ)⁻¹.toReal ∂μ + ν'.real univ - μ.real univ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace E
f : ℕ → ↥(Lp E p μ)
hf : ∑' (n : ℕ), ‖f n‖ₑ ≠ ∞
A : ∀ᵐ (a : X) ∂μ, Summable fun n ↦ ‖↑↑(f n) a‖
⊢ ∀ᵐ (x : X) ∂μ, ∀ (n : ℕ), ↑↑(∑ i ∈ range n, f i) x = ∑ i ∈ range n, ↑↑(f i) x

Tactic:
ae_all_iff

Goal state after:
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace E
f : ℕ → ↥(Lp E p μ)
hf : ∑' (n : ℕ), ‖f n‖ₑ ≠ ∞
A : ∀ᵐ (a : X) ∂μ, Summable fun n ↦ ‖↑↑(f n) a‖
⊢ ∀ (i : ℕ), ∀ᵐ (a : X) ∂μ, ↑↑(∑ i ∈ range i, f i) a = ∑ i ∈ range i, ↑↑(f i) a
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
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ (if hm : m ≤ m₀ then
      if h : SigmaFinite (μ.trim hm) ∧ Integrable f μ then
        if StronglyMeasurable f then f
        else
          have this := ⋯;
          AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯
      else 0
    else 0) =
    if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯ else 0

Tactic:
dif_pos hm

Goal state after:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ (if h : SigmaFinite (μ.trim hm) ∧ Integrable f μ then
      if StronglyMeasurable f then f
      else
        have this := ⋯;
        AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯
    else 0) =
    if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯ else 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

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

Tactic:
setIntegral_congr_ae (hm s hs) ((condExp_ae_eq_condExpL1 hm f).mono fun x hx _ => hx)

Goal state after:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
s : Set α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
hm : m ≤ m₀
inst✝ : SigmaFinite (μ.trim hm)
hf : Integrable f μ
hs : MeasurableSet s
⊢ ∫ (x : α) in s, ↑↑(condExpL1 hm μ f) x ∂μ = ∫ (x : α) in s, f x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable μ[f | ⊥]
⊢ μ[f | ⊥] = fun x ↦ (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
obtain ⟨c, h_eq⟩ := stronglyMeasurable_bot_iff.mp h_meas

Goal state after:
case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable μ[f | ⊥]
c : E
h_eq : μ[f | ⊥] = fun x ↦ c
⊢ μ[f | ⊥] = fun x ↦ (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X =ᵐ[P] Y
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ ∀ᵐ (x : Ω) ∂P, x ∈ s → X x = Y x

Tactic:
filter_upwards [hXY] with _ h _ using h

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (Measure.map g ν)
this✝ : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
ht : MeasurableSet t
a✝ : ν (g ⁻¹' t) < ∞
⊢ ((Measure.map g μ) t).toReal = μ.real (g ⁻¹' t)

Tactic:
Measure.map_apply hg ht,

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (Measure.map g ν)
this✝ : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
ht : MeasurableSet t
a✝ : ν (g ⁻¹' t) < ∞
⊢ (μ (g ⁻¹' t)).toReal = μ.real (g ⁻¹' t)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case inr.mpr.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p x : P
hmem : x ∈ s
heq : r • (x -ᵥ c) +ᵥ c = p
⊢ (1 - r) • (c -ᵥ ↑h.some) +ᵥ r • (x -ᵥ ↑h.some) +ᵥ ↑h.some = r • (x -ᵥ c) +ᵥ c

Tactic:
· rw [sub_eq_add_neg, add_smul, one_smul, neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev,
        ← vadd_vadd, vadd_vadd _ _ h.some.val, ← smul_add, add_comm, vsub_add_vsub_cancel,
        vadd_vadd, add_comm, ← vadd_vadd, vsub_vadd]

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
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
α : M →ₗ[R] P
j : IsBaseChange S α
⊢ IsBaseChange S j.endHom

Tactic:
apply of_equiv <|
      (j.linearMapRight M).equiv ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft P S j.equiv
  intro f
  ext p
  simp [equiv_tmul, LinearEquiv.congrLeft, endHom_apply]

Goal state after:
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
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
⊢ ∃ a, f = a • 1

Tactic:
replace feq (i j) : f (b j) = b.coord i (f (b i)) • b j := by
    by_cases hij : i = j
    · rw [← hij, ← feq]
    · have := h' i j hij 1
      simp only [mul_one, one_mul] at this
      rw [feq, ← this]

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
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
feq : ∀ (i j : ι), f (b j) = (b.coord i) (f (b i)) • b j
⊢ ∃ a, f = a • 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) ((ι Q) m✝ * x✝) = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) ((ι Q) m✝ * x✝)

Tactic:
rw [foldr'_ι_mul, foldr'_ι_mul, hx]

Goal state after:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝
⊢ ((contractLeftAux Q (c • d)) m✝) (x✝, c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝) =
    c • ((contractLeftAux Q d) m✝) (x✝, (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝)
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 g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
⊢ f = g

Tactic:
ext ⟨x, hx⟩

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 g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x : CliffordAlgebra Q
hx : x ∈ even Q
⊢ f ⟨x, hx⟩ = g ⟨x, hx⟩
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
hxi : ¬x = i
⊢ (Finsupp.single y 1) x + f v * (Finsupp.single y 1) i * (Finsupp.single i 1) x = 1

Tactic:
rw [Finsupp.single_eq_of_ne hxi]; simp [hxy]

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)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
⊢ ((gradedMul R 𝒜 ℬ) x) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) = r • x

Tactic:
suffices (gradedMul R 𝒜 ℬ).flip (algebraMap R _ r ⊗ₜ 1) = DistribSMul.toLinearMap R _ r by
    exact DFunLike.congr_fun this x

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 : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
⊢ (gradedMul R 𝒜 ℬ).flip ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) =
    DistribSMul.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r
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)ˣ
inst✝ : Invertible 2
y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (m : M), ↑y * (ι Q) m * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (m : M), ↑z * (ι Q) m * ↑z⁻¹ ∈ (ι Q).range
m : M
this : ↑y * (↑z * (ι Q) m * ↑z⁻¹) * ↑y⁻¹ ∈ ?m.199
⊢ ↑y * ↑z * (ι Q) m * (↑z⁻¹ * ↑y⁻¹) ∈ (ι Q).range

Tactic:
by
      simpa only [mul_assoc] using this

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
inst✝ : Invertible 2
x y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (b : M), involute ↑y * (ι Q) b * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (b : M), involute ↑z * (ι Q) b * ↑z⁻¹ ∈ (ι Q).range
b : M
this : involute ↑y * (involute ↑z * (ι Q) b * ↑z⁻¹) * ↑y⁻¹ ∈ ?m.248
⊢ involute ↑y * involute ↑z * (ι Q) b * (↑z⁻¹ * ↑y⁻¹) ∈ (ι Q).range

Tactic:
by
      simpa only [mul_assoc] using this

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 ℤˣ)
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)
⊢ f 1 * g 1 = 1

Tactic:
simp only [map_one, mul_one]

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
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
⊢ ((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra) a) b =
    (((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra) a) b

Tactic:
refine LinearMap.congr_fun (LinearMap.congr_fun ?_ a) b

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
⊢ ((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra =
    (LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra
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
i j : ℕ
a : Fin i → M
b : Fin j → M
⊢ List.map (⇑(TensorAlgebra.ι R)) (List.ofFn (Fin.append a b)) =
    List.map (⇑(TensorAlgebra.ι R)) (List.ofFn a) ++ List.map (⇑(TensorAlgebra.ι R)) (List.ofFn b)

Tactic:
← List.map_append,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : Fin i → M
b : Fin j → M
⊢ List.map (⇑(TensorAlgebra.ι R)) (List.ofFn (Fin.append a b)) =
    List.map (⇑(TensorAlgebra.ι R)) (List.ofFn a ++ List.ofFn b)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ matPolyEquiv ((expand K (p ^ k)).mapMatrix (M ^ p ^ k).charmatrix) = X ^ p ^ k - C (M ^ p ^ k)

pp: case inl.h
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ Commute X (C M)

Tactic:
· exact (id (matPolyEquiv_eq_X_pow_sub_C (p ^ k) M) :)

Goal state after:
case inl.h
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ Commute X (C M)
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ ∑ j_1, v (i - j_1) * w (j_1 - j) = ∑ i_1, v (i - j - i_1) * w i_1

Tactic:
refine Fintype.sum_equiv (Equiv.subRight j) _ _ ?_

Goal state after:
α : Type u_1
n : Type u_3
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ ∀ (x : n), v (i - x) * w (x - j) = v (i - j - (Equiv.subRight j) x) * w ((Equiv.subRight j) x)