mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

Tactic:
by_cases hf : Integrable (fun x ↦ exp (f x)) μ

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
hf : ¬Integrable (fun x ↦ rexp (f x)) μ
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
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 γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = ∑' (n : ℕ) (m : ℕ), ((κ.seq n ⊗ₖ η.seq m) a) s

Tactic:
compProd_eq_sum_compProd

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ ((Kernel.sum fun n ↦ Kernel.sum fun m ↦ κ.seq n ⊗ₖ η.seq m) a) s = ∑' (n : ℕ) (m : ℕ), ((κ.seq n ⊗ₖ η.seq m) a) s
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (rexp (f a)) / ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ∂μ = 1

Tactic:
div_eq_mul_inv

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (rexp (f a)) * (ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ))⁻¹ ∂μ = 1
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
⊢ IsZeroOrProbabilityMeasure (μ.tilted f)

Tactic:
by_cases hf : Integrable (fun x ↦ exp (f x)) μ

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ IsZeroOrProbabilityMeasure (μ.tilted f)

case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : ¬Integrable (fun x ↦ rexp (f x)) μ
⊢ IsZeroOrProbabilityMeasure (μ.tilted f)
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)
⊢ ∫ (x : β), ∫ (y : γ), f (x, y) ∂(η.restrict ht) (a, x) ∂(κ.restrict hs) a =
    ∫ (x : β) in s, ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a

pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)
⊢ Integrable f ((κ.restrict hs ⊗ₖ η.restrict ht) a)

Tactic:
· simp_rw [Kernel.restrict_apply]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)
⊢ Integrable f ((κ.restrict hs ⊗ₖ η.restrict ht) a)
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
⊢ (fun x ↦ rexp (llr μ ν x)) =ᵐ[ν] fun x ↦ if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [Measure.rnDeriv_lt_top μ ν] with x hx
  by_cases h_zero : μ.rnDeriv ν x = 0
  · simp only [llr, h_zero, ENNReal.toReal_zero, log_zero, exp_zero, ite_true]
  · rw [llr, exp_log, if_neg h_zero]
    exact ENNReal.toReal_pos h_zero hx.ne

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

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
this : ∀ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ
⊢ ∫ (x : α), rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ ∂μ =
    (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
div_eq_mul_inv

Goal state after:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
this : ∀ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ
⊢ ∫ (x : α), rexp ((f + g) x) * (∫ (x : α), rexp (f x) ∂μ)⁻¹ ∂μ =
    (∫ (x : α), rexp ((f + g) x) ∂μ) * (∫ (x : α), rexp (f x) ∂μ)⁻¹
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ AEMeasurable g ν

Tactic:
exact ((measurable_exp.comp_aemeasurable hfν).div_const _).ennreal_ofReal

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

Goal state before:
pp: α : Type u_5
β : Type u_6
E : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
hf : AEStronglyMeasurable f (⇑κ ∘ₘ μ)
⊢ AEStronglyMeasurable f (map Prod.snd (μ ⊗ₘ κ))

Tactic:
← Measure.snd,

Goal state after:
α : Type u_5
β : Type u_6
E : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
hf : AEStronglyMeasurable f (⇑κ ∘ₘ μ)
⊢ AEStronglyMeasurable f (μ ⊗ₘ κ).snd
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
⊢ (klDiv (c • μ) (c • ν)).toReal = ↑c * (klDiv μ ν).toReal

Tactic:
by_cases hc : c = 0
  · simp [hc]
  rw [toReal_klDiv_smul_right_eq_smul_left, smul_smul, inv_mul_cancel₀ hc, one_smul]
  · exact hμν.smul_left c
  · refine Integrable.smul_measure_nnreal ?_
    rw [integrable_congr (llr_smul_nnreal_left hμν c (by simpa))]
    fun_prop

Goal state after:
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_not : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] = 0

Tactic:
rw [condExp, dif_pos hm, dif_neg]; push Not; exact fun h => absurd h hμm_not

Goal state after:
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:
rw [condExp_of_sigmaFinite hm, if_pos hfi, if_pos hf]

Goal state after:
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 η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
hμν_ac : μ ≪ ν
hκη_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ Integrable (llr μ ν) μ

Tactic:
rw [← integrable_rnDeriv_mul_log_iff h_ac] at h_int

Goal state after:
𝓧 : 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 (fun a ↦ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) a).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) a).toReal) (ν ⊗ₘ η)
hμν_ac : μ ≪ ν
hκη_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ Integrable (llr μ ν) μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᵐ[μ] g
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ ↑↑(condExpL1 hm μ f) =ᵐ[μ] ↑↑(condExpL1 hm μ g)

Tactic:
by rw [condExpL1_congr_ae hm h]

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

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

Tactic:
by
      simp_rw [setIntegral_univ] at this; exact this

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

Goal state before:
pp: case neg
α : 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 : ¬SigmaFinite (μ.trim ⋯)
⊢ μ[f | ⊥] = fun x ↦ (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
rw [not_isFiniteMeasure_iff] at hμ_finite

Goal state after:
case neg
α : 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 : μ Set.univ = ∞
h : ¬SigmaFinite (μ.trim ⋯)
⊢ μ[f | ⊥] = fun x ↦ (μ.real Set.univ)⁻¹ • ∫ (x : α), 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 | ⊥]
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:
rw [← h_integral, ← smul_assoc, smul_eq_mul, inv_mul_cancel₀, one_smul]

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 ∂μ
⊢ μ.real Set.univ ≠ 0
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_assoc,

Goal state after:
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 ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

Goal state before:
pp: case hf
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
⊢ StronglyMeasurable fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal

Tactic:
refine Measurable.stronglyMeasurable fun s hs ↦ ?_
    refine ⟨(fun a ↦ ((μ.map g).rnDeriv (ν.map g) a).toReal) ⁻¹' s, hs.preimage (by fun_prop), ?_⟩
    rw [← Set.preimage_comp]
    rfl

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

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
i : ι
⊢ ∑ j, A i j * ∑ l, b.toMatrix p j l = ∑ j, ∑ l, A i j * b.toMatrix p j l

Tactic:
simp_rw [Finset.mul_sum]

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
⊢ (affineCombination k univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) (1 - w i)

Tactic:
rw [shift_eq ⟨p j, mem_affineSpan k <| Set.mem_image_of_mem _ hj⟩]

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
⊢ (affineCombination k univ p) w ∈
    map (↑(AffineEquiv.constVAdd k P ((1 - (1 - w i)) • (p i -ᵥ ↑⟨p j, ⋯⟩)))) (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
⊢ (affineCombination k univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) c → w i = 1 - c

Tactic:
rw [shift_eq ⟨p j, mem_affineSpan k <| Set.mem_image_of_mem _ hj⟩]

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
⊢ (affineCombination k univ p) w ∈
      map (↑(AffineEquiv.constVAdd k P ((1 - c) • (p i -ᵥ ↑⟨p j, ⋯⟩)))) (affineSpan k (p '' {i}ᶜ)) →
    w i = 1 - c
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
q : P
hqmem : q ∈ affineSpan k (p '' {i}ᶜ)
heq : (1 - c) • (p i -ᵥ p j) +ᵥ q = (affineCombination k univ p) w
⊢ w i = 1 - c

Tactic:
obtain ⟨t, w', ht, hw', rfl⟩ := eq_affineCombination_of_mem_affineSpan_image hqmem

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) • (p i -ᵥ p j) +ᵥ (affineCombination k t p) w' = (affineCombination k univ p) w
⊢ w i = 1 - c
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, w i = 1
x✝ :
  (affineCombination k univ s.points) w ∈ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0)
hp : (affineCombination k univ s.points) w ∈ s.closedInterior
hshift : (affineCombination k univ s.points) w ∈ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0)
⊢ w = Pi.single i 1

Tactic:
rw [affineCombination_mem_closedInterior_iff hw] at hp

Goal state after:
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, w i = 1
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 : (affineCombination k univ s.points) w ∈ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0)
⊢ w = Pi.single i 1
Module: Mathlib.LinearAlgebra.FixedSubmodule

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

Tactic:
intro H x

Goal state after:
case mp
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 : ∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • x
x : V
⊢ e.fixedReduce ((↑e).fixedSubmodule.mkQ x) = (↑e).fixedSubmodule.mkQ (a • x)
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
⊢ (∀ (v : V), e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = (↑e).fixedSubmodule.mkQ (a • v)) →
    ∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • x

Tactic:
intro H 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
⊢ e.fixedReduce x = a • x
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 * (1 + (↑(-h.unit⁻¹) + ↑(-h.unit⁻¹) * f v)) = 0

Tactic:
← mul_one (-h.unit⁻¹),

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 * (1 + (↑(-h.unit⁻¹ * 1) + ↑(-h.unit⁻¹) * f v)) = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case algebraMap
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
r✝ : R
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) ((algebraMap R (CliffordAlgebra Q)) r✝) =
    c • (foldr' Q (contractLeftAux Q d) ⋯ 0) ((algebraMap R (CliffordAlgebra Q)) r✝)

Tactic:
simp_rw [foldr'_algebraMap, smul_zero]

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
⊢ (contractLeft d) 1 = 0

Tactic:
simpa only [map_one] using contractLeft_algebraMap Q d 1

Goal state after:
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
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
⊢ LinearMap.det (transvection f v) = 1 + f v

Tactic:
rw [← det_toMatrix b]

Goal state after:
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
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
⊢ ((toMatrix b b) (transvection f v)).det = 1 + f v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
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✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d) x✝) = 0
hy : (contractLeft d) ((contractLeft d) y✝) = 0
⊢ (contractLeft d) ((contractLeft d) (x✝ + y✝)) = 0

Tactic:
rw [map_add, map_add, hx, hy, add_zero]

Goal state after:
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 ↑ι
⊢ LinearMap.det (transvection f v) = 1 + f v

Tactic:
rw [← det_toMatrix b]

Goal state after:
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 ↑ι
⊢ ((toMatrix b b) (transvection f v)).det = 1 + f v
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
B : BilinForm R M
v : M
x : CliffordAlgebra Q
⊢ (algebraMap R (CliffordAlgebra Q)) (Q v) * x - (ι Q) v * (contractLeft (B v)) x -
        ((B v) v • x - (ι Q) v * (contractLeft (B v)) x) +
      (contractLeft (B v)) ((contractLeft (B v)) x) =
    (Q v - (B v) v) • x

Tactic:
sub_sub_sub_comm,

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
B : BilinForm R M
v : M
x : CliffordAlgebra Q
⊢ (algebraMap R (CliffordAlgebra Q)) (Q v) * x - (B v) v • x -
        ((ι Q) v * (contractLeft (B v)) x - (ι Q) v * (contractLeft (B v)) x) +
      (contractLeft (B v)) ((contractLeft (B v)) x) =
    (Q v - (B v) v) • x