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

Goal state before:
pp: α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ∞ → IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
hg_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ∞ → IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, AEStronglyMeasurable.mk f hfm x ∂μ = ∫ (x : α) in s, AEStronglyMeasurable.mk g hgm x ∂μ

Tactic:
integral_congr_ae (ae_restrict_of_ae hfm.ae_eq_mk.symm),

Goal state after:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ∞ → IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
hg_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ∞ → IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (a : α) in s, f a ∂μ = ∫ (x : α) in s, AEStronglyMeasurable.mk g hgm x ∂μ
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ klDiv μ ν ≠ ∞

Tactic:
klDiv_ne_top_iff

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ μ ≪ ν ∧ Integrable (llr μ ν) μ
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : klDiv μ ν = 0
h_ne : klDiv μ ν ≠ ∞
⊢ μ = ν

Tactic:
klDiv_ne_top_iff

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : klDiv μ ν = 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ μ = ν
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ μ[f | m] = f

Tactic:
by
  rw [condExp_of_sigmaFinite hm, if_pos hfi, if_pos hf]

Goal state after:
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 | ⊥]
c : E
h_eq : μ[f | ⊥] = fun x ↦ c
h_integral : μ.real Set.univ • c = ∫ (x : α), f x ∂μ
⊢ (fun x ↦ c) = fun x ↦ (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
← h_integral,

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
h_integral : μ.real Set.univ • c = ∫ (x : α), f x ∂μ
⊢ (fun x ↦ c) = fun x ↦ (μ.real Set.univ)⁻¹ • μ.real Set.univ • c
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

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

Tactic:
by_cases h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η

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 : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

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 (μ ⊗ₘ κ) (μ ⊗ₘ η)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case 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 α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ μ[(sᶜ ∩ sᶜ).indicator f | m] =ᵐ[μ] μ[sᶜ.indicator f | m]

Tactic:
Set.inter_self

Goal state after:
case 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 α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ μ[sᶜ.indicator f | m] =ᵐ[μ] μ[sᶜ.indicator f | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case 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 α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ μ[(s ∩ s).indicator f | m] =ᵐ[μ] μ[s.indicator f | m]

Tactic:
Set.inter_self

Goal state after:
case 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 α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ μ[s.indicator f | m] =ᵐ[μ] μ[s.indicator f | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case pos.refine_1
α : 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 μ
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
this : ∫ (x : α) in t, μ[s.indicator f | m] x ∂μ = ∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ
hst_m : MeasurableSet (s ∩ t)
⊢ ∫ (x : α) in s ∩ s ∩ t, f x ∂μ = ∫ (x : α) in s ∩ t, f x ∂μ

Tactic:
Set.inter_self

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

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
⊢ (fun x ↦ (μ⁻[f | m] x).toReal) =ᵐ[μ] μ[fun x ↦ (f x).toReal | m]

Tactic:
by_cases hm : m ≤ m𝓧

Goal state after:
case pos
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
⊢ (fun x ↦ (μ⁻[f | m] x).toReal) =ᵐ[μ] μ[fun x ↦ (f x).toReal | m]

case neg
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : ¬m ≤ m𝓧
⊢ (fun x ↦ (μ⁻[f | m] x).toReal) =ᵐ[μ] μ[fun x ↦ (f x).toReal | m]
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
⊢ μ⁻[fun x ↦ ENNReal.ofReal (f x) | m] =ᵐ[μ] fun x ↦ ENNReal.ofReal (μ[f | m] x)

Tactic:
by_cases hm : m ≤ m𝓧

Goal state after:
case pos
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
hm : m ≤ m𝓧
⊢ μ⁻[fun x ↦ ENNReal.ofReal (f x) | m] =ᵐ[μ] fun x ↦ ENNReal.ofReal (μ[f | m] x)

case neg
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
hm : ¬m ≤ m𝓧
⊢ μ⁻[fun x ↦ ENNReal.ofReal (f x) | m] =ᵐ[μ] fun x ↦ ENNReal.ofReal (μ[f | m] x)
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 ν
h_ne_top1 : ∀ᵐ (x : 𝓧) ∂ν, (Measure.map g μ).rnDeriv (Measure.map g ν) (g x) ≠ ∞
h_ne_top2 : ∀ᵐ (x : 𝓧) ∂ν, ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x ≠ ∞
h_condExp✝ :
  (fun x ↦ (ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x).toReal) =ᵐ[ν]
    ν[fun x ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨]
x : 𝓧
hx :
  ((Measure.map g μ).rnDeriv (Measure.map g ν) (g x)).toReal =
    ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨] x
h_condExp :
  (ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x).toReal =
    ν[fun x ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨] x
⊢ (Measure.map g μ).rnDeriv (Measure.map g ν) (g x) ≠ ∞ →
    ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x ≠ ∞ →
      (Measure.map g μ).rnDeriv (Measure.map g ν) (g x) = ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x

Tactic:
h_ne_top1

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 ν
h_ne_top1✝ : ∀ᵐ (x : 𝓧) ∂ν, (Measure.map g μ).rnDeriv (Measure.map g ν) (g x) ≠ ∞
h_ne_top2 : ∀ᵐ (x : 𝓧) ∂ν, ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x ≠ ∞
h_condExp✝ :
  (fun x ↦ (ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x).toReal) =ᵐ[ν]
    ν[fun x ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨]
x : 𝓧
hx :
  ((Measure.map g μ).rnDeriv (Measure.map g ν) (g x)).toReal =
    ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨] x
h_condExp :
  (ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x).toReal =
    ν[fun x ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨] x
h_ne_top1 : (Measure.map g μ).rnDeriv (Measure.map g ν) (g x) ≠ ∞
⊢ ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x ≠ ∞ →
    (Measure.map g μ).rnDeriv (Measure.map g ν) (g x) = ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x
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✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
⊢ AffineIndependent k p

Tactic:
cases nonempty_fintype ι'

Goal state after:
case intro
ι : 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✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val✝ : Fintype ι'
⊢ AffineIndependent k p
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 ι
this : ∀ (i : ι), b i ∈ affineSpan k (range p)
⊢ ⊤ ≤ affineSpan k (range p)

Tactic:
← b.tot,

Goal state after:
ι : 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 ι
this : ∀ (i : ι), b i ∈ affineSpan k (range p)
⊢ affineSpan k (range ⇑b) ≤ affineSpan k (range p)
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)
inst✝ : ZeroLEOneClass k
w : Fin (n + 1) → k
hw : ∀ i_1 ∈ univ.erase i, w i_1 = 0
x✝ :
  (affineCombination k univ s.points) w ∈ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0)
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hshift : w i = 1
j : Fin (n + 1)
hj : ¬j = i
⊢ j ∈ univ.erase i

Tactic:
simpa using hj

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

Goal state before:
pp: case inl
R : Type u_6
inst✝¹⁰ : CommRing R
S : Type u_7
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_8
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
P : Type u_9
inst✝⁵ : AddCommGroup 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 α
f : M →ₗ[R] M
hR : Subsingleton R
⊢ LinearMap.det (j.endHom f) = (algebraMap R S) (LinearMap.det f)

Tactic:
have : f = 1 := by
      have : Subsingleton M := Module.subsingleton R M
      exact Subsingleton.eq_one f
    simp [this, endHom_one]

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₂
σ : Perm (ιa ⊕ ιb)
f : Perm ιa × Perm ιb →* Perm (ιa ⊕ ιb) := sumCongrHom ιa ιb
| ∑ τ ∈ Finset.map (Equiv.toEmbedding (Equiv.mulLeft σ)) Finset.univ with τ⁻¹ * σ ∈ f.range,
    sign τ • domDomCongr τ (a.domCoprod b)

Tactic:
Finset.filter_map,

Goal state after:
ι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₂
σ : Perm (ιa ⊕ ιb)
f : Perm ιa × Perm ιb →* Perm (ιa ⊕ ιb) := sumCongrHom ιa ιb
| ∑
    τ ∈
      Finset.map (Equiv.toEmbedding (Equiv.mulLeft σ))
        (Finset.filter ((fun τ ↦ τ⁻¹ * σ ∈ f.range) ∘ ⇑(Equiv.toEmbedding (Equiv.mulLeft σ))) Finset.univ),
    sign τ • domDomCongr τ (a.domCoprod b)
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₂
σ : Perm (ιa ⊕ ιb)
f : Perm ιa × Perm ιb →* Perm (ιa ⊕ ιb) := sumCongrHom ιa ιb
⊢ ∑ τ with τ⁻¹ * σ ∈ f.range, sign τ • domDomCongr τ (a.domCoprod b) =
    ∑ τ with τ⁻¹ ∈ f.range, sign (σ * τ) • domDomCongr (σ * τ) (a.domCoprod b)

Tactic:
conv_lhs => rw [← Finset.map_univ_equiv (Equiv.mulLeft σ), Finset.filter_map, Finset.sum_map]
      simp [-MonoidHom.mem_range]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
⊢ (f x * ↑(-h.unit⁻¹)) • v + f (x + (f x * ↑(-h.unit⁻¹)) • v) • v = 0

Tactic:
← add_smul

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
⊢ (f x * ↑(-h.unit⁻¹) + f (x + (f x * ↑(-h.unit⁻¹)) • v)) • v = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Opposite

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
⊢ AlgHom.op.symm
      ((algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯).comp (AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯))) =
    AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ)

Tactic:
ext <;> rfl

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Opposite

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
⊢ (AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯)).comp (algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯) =
    AlgHom.id S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)

Tactic:
ext <;> rfl

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

Goal state before:
pp: case add
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ reverse (x₁ + x₂) = x₁ + x₂

Tactic:
reverse.map_add,

Goal state after:
case add
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ reverse x₁ + reverse x₂ = x₁ + x₂
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case add
x₁ x₂ : CliffordAlgebra Q
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ reverse (x₁ + x₂) = x₁ + x₂

Tactic:
reverse.map_add,

Goal state after:
case add
x₁ x₂ : CliffordAlgebra Q
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ reverse x₁ + reverse x₂ = x₁ + x₂
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case h₀
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 ↑ι
this : (toMatrix b b) (transvection f v) = Matrix.diagonal (Function.update 1 i (1 + f v))
⊢ ∀ b ∈ Finset.univ, b ≠ i → Function.update 1 i (1 + f v) b = 1

pp: case h₁
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 ↑ι
this : (toMatrix b b) (transvection f v) = Matrix.diagonal (Function.update 1 i (1 + f v))
⊢ i ∉ Finset.univ → Function.update 1 i (1 + f v) i = 1

Tactic:
· intro j _ hj
        simp [Function.update_of_ne hj]

Goal state after:
case h₁
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 ↑ι
this : (toMatrix b b) (transvection f v) = Matrix.diagonal (Function.update 1 i (1 + f v))
⊢ i ∉ Finset.univ → Function.update 1 i (1 + f v) i = 1
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case e'_2.e'_6
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
⊢ (Finsupp.single y 1) i * (Finsupp.single i 1) x = 0

Tactic:
by_cases hxi : x = i

Goal state after:
case pos
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) i * (Finsupp.single i 1) x = 0

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) i * (Finsupp.single i 1) x = 0
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
i : Fin n
⊢ (ibc.toDual fM) (b i) = f (b i)

Tactic:
← hε,

Goal state after:
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
i : Fin n
⊢ (ibc.toDual fM) (ε (Pi.single i 1)) = f (ε (Pi.single i 1))