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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
⊢ Measurable fun a ↦ ∫⁻ (b : β), f a b ∂κ a

Tactic:
let F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
  have h : ∀ a, ⨆ n, F n a = uncurry f a := SimpleFunc.iSup_eapprox_apply hf
  simp only [Prod.forall, uncurry_apply_pair] at h
  simp_rw [← h]
  have : ∀ a, (∫⁻ b, ⨆ n, F n (a, b) ∂κ a) = ⨆ n, ∫⁻ b, F n (a, b) ∂κ a := by
    intro a
    rw [lintegral_iSup]
    · exact fun n => (F n).measurable.comp measurable_prodMk_left
    · exact fun i j hij b => SimpleFunc.monotone_eapprox (uncurry f) hij _
  simp_rw [this]
  refine .iSup fun n => ?_
  refine SimpleFunc.induction
    (motive := fun f => Measurable (fun (a : α) => ∫⁻ (b : β), f (a, b) ∂κ a)) ?_ ?_ (F n)
  · intro c t ht
    simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
      SimpleFunc.coe_zero, Set.piecewise_eq_indicator]
    exact Kernel.measurable_lintegral_indicator_const (κ := κ) ht c
  · intro g₁ g₂ _ hm₁ hm₂
    simp only [SimpleFunc.coe_add, Pi.add_apply]
    have h_add :
      (fun a => ∫⁻ b, g₁ (a, b) + g₂ (a, b) ∂κ a) =
        (fun a => ∫⁻ b, g₁ (a, b) ∂κ a) + fun a => ∫⁻ b, g₂ (a, b) ∂κ a := by
      ext1 a
      rw [Pi.add_apply, lintegral_add_left (by fun_prop)]
    rw [h_add]
    exact Measurable.add hm₁ hm₂

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
h : IsSFiniteKernel η
a✝¹ : α × γ
s✝ : Set (β × δ)
a✝ : MeasurableSet s✝
⊢ ((0 ∥ₖ η) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
simp [parallelComp_apply]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : IsSFiniteKernel κ
a✝¹ : α × γ
s✝ : Set (β × δ)
a✝ : MeasurableSet s✝
⊢ ((κ ∥ₖ 0) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
simp [parallelComp_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ ⊗ₘ κ) s = ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' s) ∂μ

Tactic:
simp_rw [compProd, Kernel.compProd_apply hs, Kernel.const_apply, Kernel.prodMkLeft_apply']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst✝ : Countable ι
κ : ι → Kernel α β
⊢ (Kernel.sum fun i ↦ prodMkLeft γ (κ i)) = prodMkLeft γ (Kernel.sum κ)

Tactic:
by
  ext
  simp_rw [sum_apply, prodMkLeft_apply, sum_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a : α
⊢ ∫⁻ (p : α × β), f p ∂(Kernel.id ×ₖ κ) a = ∫⁻ (b : β), f (a, b) ∂κ a

Tactic:
by
  rw [Kernel.id, lintegral_deterministic_prod _ _ _ hf, id_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
⊢ ((κ + η) ∘ₖ Kernel.const Unit μ) () = (κ ∘ₖ Kernel.const Unit μ) () + (η ∘ₖ Kernel.const Unit μ) ()

Tactic:
Kernel.comp_add_left,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
⊢ (κ ∘ₖ Kernel.const Unit μ + η ∘ₖ Kernel.const Unit μ) () =
    (κ ∘ₖ Kernel.const Unit μ) () + (η ∘ₖ Kernel.const Unit μ) ()
Module: Mathlib.Probability.Kernel.Composition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
h2 : (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η] 0
x : α × β
hx :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x =
    ((μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)) x
⊢ (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x = 0 x →
    (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x =
      (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x

Tactic:
hx2

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
h2 : (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η] 0
x : α × β
hx :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x =
    ((μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)) x
hx2 : (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x = 0 x
⊢ (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x =
    (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: case neg
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
have h_eq : ∫ x, f (μ'.rnDeriv ν' x).toReal ∂ν'
      = (ν.real univ)⁻¹ * ∫ x, f ((μ.rnDeriv ν x).toReal) ∂ν := by
    rw [integral_smul_measure, smul_eq_mul, ENNReal.toReal_inv]
    congr 1
    refine integral_congr_ae ?_
    filter_upwards [h_rnDeriv_eq] with x hx
    rw [hx]

Goal state after:
case neg
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:

Tactic:
∫⁻ a in s, ∫⁻ b, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η a) ∂μ
  _ = ∫⁻ a in s, ∫⁻ b in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η a) ∂μ := by simp
  _ = ∫⁻ a in s, (κ a) univ ∂μ := by
    rw [← Measure.setLIntegral_compProd (by fun_prop) hs .univ, Measure.setLIntegral_rnDeriv hκη,
      Measure.compProd_apply_prod hs .univ]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h_ac : μ ≪ ν
⊢ klDiv μ ν = ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν

Tactic:
simp [klDiv_eq_lintegral_klFun, h_ac]

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

Goal state before:
pp: α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
⊢ MemLp.toLp ↑↑f ⋯ ∈ lpMeasSubgroup F m p μ

Tactic:
let hf_mem_ℒp := memLp_of_memLp_trim hm (Lp.memLp f)
  rw [mem_lpMeasSubgroup_iff_aestronglyMeasurable]
  refine AEStronglyMeasurable.congr ?_ (MemLp.coeFn_toLp hf_mem_ℒp).symm
  exact (Lp.aestronglyMeasurable f).of_trim hm

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

Goal state before:
pp: α : 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
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ i, S i ∩ s
hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ∞
i j : ℕ
⊢ i ≤ j → (fun i ↦ S i ∩ s) i ⊆ (fun i ↦ S i ∩ s) j

Tactic:
hij

Goal state after:
α : 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
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ i, S i ∩ s
hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ∞
i j : ℕ
hij : i ≤ j
⊢ (fun i ↦ S i ∩ s) i ⊆ (fun i ↦ S i ∩ s) j
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
G' : Type u_6
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : CompleteSpace G'
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
x : G'
⊢ (∫ (a : α) in s, ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ht hμt 1)) a ∂μ) • x = μ.real (t ∩ s) • x

Tactic:
by rw [setIntegral_condExpL2_indicator hs ht hμs hμt]

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

Goal state before:
pp: case pos.refine_2
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
⊢ AEStronglyMeasurable μ[s.indicator f | m] μ

Tactic:
have : StronglyMeasurable[m] (μ[s.indicator f | m]) := stronglyMeasurable_condExp
    refine this.aestronglyMeasurable.of_measurableSpace_le_on hm hs_m (fun t => (hs t).mp) ?_
    exact condExp_ae_eq_restrict_zero hs_m.compl (indicator_ae_eq_restrict_compl (hm _ hs_m))

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

Goal state before:
pp: case inr
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
i : ι
w : ι → k
hw : ∑ i, w i = 1
h✝ : Nontrivial k
j : ι
hj : j ≠ i
⊢ -(w i • ((affineCombination k univ p) (Pi.single i 1) -ᵥ (affineCombination k univ p) (Pi.single j 1))) +ᵥ
      (affineCombination k univ p) w ∈
    affineSpan k (p '' {i}ᶜ)

Tactic:
affineCombination_vsub,

Goal state after:
case inr
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
i : ι
w : ι → k
hw : ∑ i, w i = 1
h✝ : Nontrivial k
j : ι
hj : j ≠ i
⊢ -(w i • (univ.weightedVSub p) (Pi.single i 1 - Pi.single j 1)) +ᵥ (affineCombination k univ p) w ∈
    affineSpan k (p '' {i}ᶜ)
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
t : Finset ι
w' : ι → k
ht✝ : ↑t ⊆ {i}ᶜ
hw' : ∑ i ∈ t, w' i = 1
hqmem : (affineCombination k t p) w' ∈ affineSpan k (p '' {i}ᶜ)
heq :
  (1 - c) • ((affineCombination k univ p) (Pi.single i 1) -ᵥ (affineCombination k univ p) (Pi.single j 1)) +ᵥ
      (affineCombination k univ p) ((↑t).indicator w') =
    (affineCombination k univ p) w
ht : (↑t).indicator w' i = 0
⊢ w i = 1 - c

Tactic:
affineCombination_vsub,

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
t : Finset ι
w' : ι → k
ht✝ : ↑t ⊆ {i}ᶜ
hw' : ∑ i ∈ t, w' i = 1
hqmem : (affineCombination k t p) w' ∈ affineSpan k (p '' {i}ᶜ)
heq :
  (1 - c) • (univ.weightedVSub p) (Pi.single i 1 - Pi.single j 1) +ᵥ (affineCombination k univ p) ((↑t).indicator w') =
    (affineCombination k univ p) w
ht : (↑t).indicator w' i = 0
⊢ w i = 1 - c
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case h
ι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)
⊢ (Perm.sign a✝ • MultilinearMap.domDomCongr a✝ ((↑a).domCoprod ↑b)) v +
      ((-1 * Perm.sign a✝) • MultilinearMap.domDomCongr (swap i j * a✝) ((↑a).domCoprod ↑b)) v =
    0

Tactic:
simp only [one_mul, neg_mul, Function.comp_apply, Units.neg_smul, Perm.coe_mul,
    _root_.smul_apply, _root_.neg_apply, MultilinearMap.domDomCongr_apply,
    MultilinearMap.domCoprod_apply]

Goal state after:
case h
ι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)
⊢ (Perm.sign a✝ • (↑a fun i₁ ↦ v (a✝ (Sum.inl i₁))) ⊗ₜ[R'] ↑b fun i₂ ↦ v (a✝ (Sum.inr i₂))) +
      -(Perm.sign a✝ •
          (↑a fun i₁ ↦ v ((swap i j) (a✝ (Sum.inl i₁)))) ⊗ₜ[R'] ↑b fun i₂ ↦ v ((swap i j) (a✝ (Sum.inr i₂)))) =
    0
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: case mpr
R : Type u_4
V : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e : V ≃ₗ[R] V
a : R
H : ∀ (v : V), e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = (↑e).fixedSubmodule.mkQ (a • v)
x : V ⧸ (↑e).fixedSubmodule
⊢ e.fixedReduce x = a • x

Tactic:
have ⟨y, hy⟩ := e.fixedSubmodule.mkQ_surjective x

Goal state after:
case mpr
R : Type u_4
V : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e : V ≃ₗ[R] V
a : R
H : ∀ (v : V), e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = (↑e).fixedSubmodule.mkQ (a • v)
x : V ⧸ (↑e).fixedSubmodule
y : V
hy : (↑e).fixedSubmodule.mkQ y = x
⊢ e.fixedReduce x = a • x
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case neg
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))
i j : ι
hij : ¬i = j
⊢ f (b j) = (b.coord i) (f (b i)) • b j

Tactic:
have := h' i j hij 1
      simp only [mul_one, one_mul] at this
      rw [feq, ← this]

Goal state after:
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
⊢ e ∈ transvections K V ↔ e ∈ dilatransvections K V ∧ e.fixedReduce = 1

Tactic:
refine ⟨fun ⟨f, v, hfv, he⟩ ↦ ?_, fun ⟨he, he'⟩ ↦ ?_⟩

Goal state after:
case refine_1
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 ∈ transvections K V
f : Dual K V
v : V
hfv : f v = 0
he : e = transvection hfv
⊢ e ∈ dilatransvections K V ∧ e.fixedReduce = 1

case refine_2
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 : e ∈ dilatransvections K V
he' : e.fixedReduce = 1
⊢ e ∈ transvections K V
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 = ⊥
this : finrank K (V ⧸ ker f) = 1
⊢ (↑e).fixedSubmodule = ker f

Tactic:
apply Submodule.eq_of_le_of_finrank_le
        · intro x
          rw [mem_ker, ← Submodule.mem_bot K, ← hf]
          exact mem_map_of_mem
        rw [← Nat.add_le_add_iff_right, finrank_quotient_add_finrank] at he
        have := (LinearMap.ker f).finrank_quotient_add_finrank
        linarith

Goal state after:
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 Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
d : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h) ((contractLeft d) x✝) = (contractLeft d) ((changeForm h) x✝)
⊢ (changeForm h) ((contractLeft d) ((ι Q) m✝ * x✝)) = (contractLeft d) ((changeForm h) ((ι Q) m✝ * x✝))

Tactic:
simp only [contractLeft_ι_mul, changeForm_ι_mul, map_sub, map_smul]
    rw [← hx, contractLeft_comm, ← sub_add, sub_neg_eq_add, ← hx]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Torsion.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ finrank R M = 0 ↔ IsTorsion R M

Tactic:
by
  simp [← rank_eq_zero_iff_isTorsion (R := R), ← finrank_eq_rank]

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

Goal state before:
pp: case fst
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
fg : { fg // ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), fg.1 ↑a * fg.2 ↑b = (-1) ^ (j * i) • (fg.2 ↑b * fg.1 ↑a) }
x✝ : A
⊢ (↑((fun F ↦ ⟨(F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)), ⋯⟩) ((fun fg ↦ lift 𝒜 ℬ (↑fg).1 (↑fg).2 ⋯) fg))).1
      x✝ =
    (↑fg).1 x✝

Tactic:
(dsimp; simp only [map_one, mul_one, one_mul])

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

Goal state before:
pp: case snd
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
fg : { fg // ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), fg.1 ↑a * fg.2 ↑b = (-1) ^ (j * i) • (fg.2 ↑b * fg.1 ↑a) }
x✝ : B
⊢ (↑((fun F ↦ ⟨(F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)), ⋯⟩) ((fun fg ↦ lift 𝒜 ℬ (↑fg).1 (↑fg).2 ⋯) fg))).2
      x✝ =
    (↑fg).2 x✝

Tactic:
(dsimp; simp only [map_one, mul_one, one_mul])

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
hx : x ∈ ⋀[R]^i M
⊢ (liftι R M) x = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i) ⟨x, hx⟩

Tactic:
induction hx using Submodule.pow_induction_on_left' with
  | algebraMap => simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
  | add _ _ _ _ _ ihx ihy => simp_rw [map_add, ihx, ihy, ← map_add]; rfl
  | mem_mul _ hm _ _ _ ih =>
      obtain ⟨_, rfl⟩ := hm
      simp_rw [map_mul, ih, GradedAlgebra.liftι, lift_ι_apply, GradedAlgebra.ι_apply R M,
        DirectSum.of_mul_of]
      exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)

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

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Fintype ι
inst✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
h : ¬n = Fintype.card ι
⊢ Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index = 0

Tactic:
· have hlt : n < Fintype.card ι :=
      Ne.lt_of_le h (by simpa using Fintype.card_le_of_embedding snf.f)
    simp [hlt]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : LinearOrder m
inst✝² : LinearOrder n
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
l : m → WithTop n
hA : A.IsPivotedBy l
g : { i // l i ≠ ⊤ } → n := fun i ↦ (l ↑i).untop ⋯
hlead : ∀ (i : { i // l i ≠ ⊤ }), A.IsLeadingEntry (↑i) (g i)
i j : { i // l i ≠ ⊤ }
⊢ id j < id i → A.submatrix Subtype.val g i j = 0

Tactic:
hij

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : LinearOrder m
inst✝² : LinearOrder n
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
l : m → WithTop n
hA : A.IsPivotedBy l
g : { i // l i ≠ ⊤ } → n := fun i ↦ (l ↑i).untop ⋯
hlead : ∀ (i : { i // l i ≠ ⊤ }), A.IsLeadingEntry (↑i) (g i)
i j : { i // l i ≠ ⊤ }
hij : id j < id i
⊢ A.submatrix Subtype.val g i j = 0
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
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

Tactic:
have h4 := Int.ediv_mul_le (A.1 0 1) hd

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)
h4 : ↑A 0 1 / ↑A 1 1 * ↑A 1 1 ≤ ↑A 0 1
⊢ T ^ (-(↑A 0 1 / ↑A 1 1)) • A ∈ reps m
Module: Mathlib.LinearAlgebra.Matrix.Gershgorin

Goal state before:
pp: case inl
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✝ : IsEmpty n
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)

Tactic:
exfalso
    exact hμ Submodule.eq_bot_of_subsingleton

Goal state after: