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

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : ↑c ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
h_contra : μ ≪ c • ν
⊢ μ ≪ ν

Tactic:
hν_smul

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : ↑c ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
h_contra : μ ≪ c • ν
⊢ μ ≪ c⁻¹ • c • ν
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : ↑c ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
⊢ Integrable (llr μ ν) μ

Tactic:
hν_smul

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : ↑c ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
⊢ Integrable (llr μ (c⁻¹ • c • ν)) μ
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 α
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace F
hm : m ≤ m0
⊢ IsComplete {f | AEStronglyMeasurable (↑↑f) μ}

Tactic:
by
  rw [← completeSpace_coe_iff_isComplete]
  have : Fact (m ≤ m0) := ⟨hm⟩
  change CompleteSpace (lpMeasSubgroup F m p μ)
  infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: case inl
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hp : 1 ≤ ∞
h'f : ∑' (n : ι), eLpNorm (f n) ∞ μ ≠ ∞
this : ∀ᵐ (x : X) ∂μ, ∀ (n : ι), ‖f n x‖ₑ ≤ eLpNorm (f n) ∞ μ
⊢ ∀ᵐ (a : X) ∂μ, ∑' (n : ι), ‖f n a‖ₑ < ∞

Tactic:
filter_upwards [this] with x hx

Goal state after:
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hp : 1 ≤ ∞
h'f : ∑' (n : ι), eLpNorm (f n) ∞ μ ≠ ∞
this : ∀ᵐ (x : X) ∂μ, ∀ (n : ι), ‖f n x‖ₑ ≤ eLpNorm (f n) ∞ μ
x : X
hx : ∀ (n : ι), ‖f n x‖ₑ ≤ eLpNorm (f n) ∞ μ
⊢ ∑' (n : ι), ‖f n x‖ₑ < ∞
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: case inr
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : CompleteSpace E
f : ι → ↥(Lp E p μ)
hf : ∑' (n : ι), ‖f n‖ₑ ≠ ∞
hι : Infinite ι
e : ℕ ≃ ι
this : ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f (e n)) a) (↑↑(∑' (n : ℕ), f (e n)) a)
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ι), f n) a)

Tactic:
filter_upwards [this] with x hx

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)
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : CompleteSpace E
f : ι → ↥(Lp E p μ)
hf : ∑' (n : ι), ‖f n‖ₑ ≠ ∞
hι : Infinite ι
e : ℕ ≃ ι
this : ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f (e n)) a) (↑↑(∑' (n : ℕ), f (e n)) a)
x : X
hx : HasSum (fun n ↦ ↑↑(f (e n)) x) (↑↑(∑' (n : ℕ), f (e n)) x)
⊢ HasSum (fun n ↦ ↑↑(f n) x) (↑↑(∑' (n : ι), f n) x)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
F : Type u_4
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : 𝕜
x : F
⊢ condExpIndSMul hm hs hμs (c • x) = c • condExpIndSMul hm hs hμs x

Tactic:
by
  simp_rw [condExpIndSMul, toSpanSingleton_smul, smul_compLpL, smul_apply]

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

Goal state before:
pp: case empty
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
hf : ∀ i ∈ ∅, Integrable (f i) μ
⊢ μ[∑ i ∈ ∅, f i | m] =ᵐ[μ] ∑ i ∈ ∅, μ[f i | m]

Tactic:
| empty =>

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

Goal state before:
pp: case pos.refine_3
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
a✝ : (μ.restrict s) t < ∞
⊢ ∫ (x : α) in t, μ[f | m] x ∂μ.restrict s = ∫ (x : α) in t, 0 x ∂μ.restrict s

Tactic:
Measure.restrict_restrict (hm _ ht),

Goal state after:
case pos.refine_3
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
a✝ : (μ.restrict s) t < ∞
⊢ ∫ (x : α) in t ∩ s, μ[f | m] x ∂μ = ∫ (x : α) in t ∩ s, 0 x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict sᶜ] 0
hm : m ≤ m0
hsf_zero : ∀ (g : α → E), g =ᵐ[μ.restrict sᶜ] 0 → s.indicator g =ᵐ[μ] g
⊢ μ[s.indicator f | m] =ᵐ[μ] s.indicator μ[f | m]

Tactic:
refine ((hsf_zero (μ[f | m]) (condExp_ae_eq_restrict_zero hs.compl hf)).trans ?_).symm

Goal state after:
case pos
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict sᶜ] 0
hm : m ≤ m0
hsf_zero : ∀ (g : α → E), g =ᵐ[μ.restrict sᶜ] 0 → s.indicator g =ᵐ[μ] g
⊢ μ[f | m] =ᵐ[μ] μ[s.indicator f | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

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

Tactic:
rw [setIntegral_condExp (hm₁₂.trans hm₂) hf hs, setIntegral_condExp hm₂ hf (hm₁₂ s hs)]

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

Goal state before:
pp: α : 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]
this : sᶜ.indicator μ[sᶜ.indicator f | m] =ᵐ[μ] μ[sᶜ.indicator f | m]
⊢ s.indicator μ[sᶜ.indicator f | m] =ᵐ[μ] s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m])

Tactic:
filter_upwards [this] with x hx

Goal state after:
α : 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]
this : sᶜ.indicator μ[sᶜ.indicator f | m] =ᵐ[μ] μ[sᶜ.indicator f | m]
x : α
hx : sᶜ.indicator μ[sᶜ.indicator f | m] x = μ[sᶜ.indicator f | m] x
⊢ s.indicator μ[sᶜ.indicator f | m] x = s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) x
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ ∫ (x : α) in s ∩ t, (μ.restrict s)[f | m] x ∂μ = ∫ (x : α) in t, (μ.restrict s)[f | m] x ∂μ.restrict s

Tactic:
Measure.restrict_restrict (hm _ ht),

Goal state after:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ ∫ (x : α) in s ∩ t, (μ.restrict s)[f | m] x ∂μ = ∫ (x : α) in t ∩ s, (μ.restrict s)[f | m] x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ ∫ (x : α) in t, f x ∂μ.restrict s = ∫ (x : α) in s ∩ t, f x ∂μ

Tactic:
Measure.restrict_restrict (hm _ ht),

Goal state after:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ ∫ (x : α) in t ∩ s, f x ∂μ = ∫ (x : α) in s ∩ t, f 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
inst✝ : SigmaFinite (Measure.map g ν)
⊢ (fun a ↦ (Measure.map g μ).rnDeriv (Measure.map g ν) (g a)) =ᵐ[ν.trim ⋯] ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨]

Tactic:
by
  rw [StronglyMeasurable.ae_eq_trim_iff]
  · exact rnDeriv_map hμν hg
  · refine Measurable.stronglyMeasurable fun s hs ↦ ?_
    exact ⟨((μ.map g).rnDeriv (ν.map g)) ⁻¹' s, hs.preimage (by fun_prop), by grind⟩
  · fun_prop

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
⊢ affineSpan k (range p) = ⊤

Tactic:
cases nonempty_fintype ι
  suffices ∀ i, b i ∈ affineSpan k (range p) by
    rw [eq_top_iff, ← b.tot, affineSpan_le]
    rintro q ⟨i, rfl⟩
    exact this i
  intro i
  have hAi : ∑ j, A i j = 1 := by
    calc
      ∑ j, A i j = ∑ j, A i j * ∑ l, b.toMatrix p j l := by simp
      _ = ∑ j, ∑ l, A i j * b.toMatrix p j l := by simp_rw [Finset.mul_sum]
      _ = ∑ l, ∑ j, A i j * b.toMatrix p j l := by rw [Finset.sum_comm]
      _ = ∑ l, (A * b.toMatrix p) i l := rfl
      _ = 1 := by simp [hA, Matrix.one_apply]
  have hbi : b i = Finset.univ.affineCombination k p (A i) := by
    apply b.ext_elem
    intro j
    rw [b.coord_apply, Finset.univ.map_affineCombination _ _ hAi,
      Finset.univ.affineCombination_eq_linear_combination _ _ hAi]
    change _ = (A * b.toMatrix p) i j
    simp_rw [hA, Matrix.one_apply, @eq_comm _ i j]
  rw [hbi]
  exact affineCombination_mem_affineSpan hAi p

Goal state after:
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
σ : Perm (ιa ⊕ ιb)
hσ : swap i j • Quotient.mk'' σ = Quotient.mk'' σ
⊢ (Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v = 0

Tactic:
obtain ⟨⟨sl, sr⟩, hσ⟩ := QuotientGroup.leftRel_apply.mp (Quotient.exact' hσ)

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
σ : Perm (ιa ⊕ ιb)
hσ✝ : swap i j • Quotient.mk'' σ = Quotient.mk'' σ
sl : Perm ιa
sr : Perm ιb
hσ : (Perm.sumCongrHom ιa ιb) (sl, sr) = ((fun x ↦ swap i j • x) σ)⁻¹ * σ
⊢ (Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v = 0
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
α : M →ₗ[R] P
j : IsBaseChange S α
⊢ j.endHom 1 = 1

Tactic:
by
  ext p
  induction p using j.inductionOn with
  | zero => simp
  | add x y hx hy => simp [hx, hy]
  | smul _ _ h => simp [h]
  | tmul m => simp [endHom_comp_apply]

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
⊢ ∑ x ∈ Finset.image (⇑(sumCongrHom ιa ιb)) Finset.univ, sign (σ * x) • domDomCongr (σ * x) (a.domCoprod b) =
    ∑ x, sign (σ * (sumCongrHom ιa ιb) x) • domDomCongr (σ * (sumCongrHom ιa ιb) x) (a.domCoprod b)

Tactic:
Finset.sum_image sumCongrHom_injective.injOn

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
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
h : ¬LinearIndependent R ![x, f x]
⊢ (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))

Tactic:
simp only [Nat.succ_eq_add_one, Nat.reduceAdd,
      LinearIndependent.pair_iff, not_forall, not_and] at h

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
h : ∃ x_1 x_2, ∃ (_ : x_1 • x + x_2 • f x = 0), x_1 = 0 → ¬x_2 = 0
⊢ (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
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⁻¹) + (f x + f ((f x * ↑(-h.unit⁻¹)) • v)) = 0

Tactic:
LinearMap.map_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⁻¹)) • f v) = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ associated (QuadraticForm.baseChange A Q) = BilinForm.baseChange A (associated Q)

Tactic:
by
  dsimp only [QuadraticForm.baseChange, LinearMap.baseChange]
  rw [associated_tmul (QuadraticMap.sq (R := A)) Q, associated_sq]
  exact rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ op (1 ⊗ₜ[R] (ι Q) v) = op (unop (↑(AlgEquiv.toOpposite A A) 1) ⊗ₜ[R] unop (reverseOp ((ι Q) v)))

Tactic:
reverseOp_ι

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ op (1 ⊗ₜ[R] (ι Q) v) = op (unop (↑(AlgEquiv.toOpposite A A) 1) ⊗ₜ[R] unop (op ((ι Q) v)))
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
A : Type u_5
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
W : Type u_6
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module A W
inst✝ : IsScalarTower R A W
ε : V →ₗ[R] W
ibc : IsBaseChange A ε
f : Dual R V
v : V
⊢ ibc.endHom (LinearMap.transvection f v) = LinearMap.transvection (ibc.toDual f) (ε v)

Tactic:
ext w
  induction w using ibc.inductionOn with
  | zero => simp
  | add x y hx hy => simp [hx, hy]
  | smul a w hw => simp [hw]
  | tmul x => simp [LinearMap.transvection.apply, endHom_comp_apply, toDual_comp_apply]

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 ↑ι
x y : ↑ι
hxy : ¬x = y
⊢ f v * (Finsupp.single y 1) i * (Finsupp.single i 1) x = 0

Tactic:
mul_assoc

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 ↑ι
x y : ↑ι
hxy : ¬x = y
⊢ f v * ((Finsupp.single y 1) i * (Finsupp.single i 1) x) = 0
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 y z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ ↑↑((-1) ^ (ixb * iya)) •
      (-1) ^ ((ixb + iyb) * iza) •
        ((lof R ι 𝒜 ixa) xa * (lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za) ⊗ₜ[R]
          ((lof R ι ℬ ixb) xb * (lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb) =
    ↑↑((-1) ^ (iyb * iza)) •
      (-1) ^ (ixb * (iya + iza)) •
        ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
          ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb))

Tactic:
mul_assoc

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 y z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ ↑↑((-1) ^ (ixb * iya)) •
      (-1) ^ ((ixb + iyb) * iza) •
        ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
          ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb)) =
    ↑↑((-1) ^ (iyb * iza)) •
      (-1) ^ (ixb * (iya + iza)) •
        ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
          ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb))
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)ˣ
⊢ (∃ x_1 ∈ lipschitzGroup Q, x_1 = x) ↔ x ∈ lipschitzGroup Q

Tactic:
exact exists_eq_right

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsTorsion R M
⊢ Module.rank R M = 0

Tactic:
by_contra! h'
  obtain ⟨f, hf⟩ := by rwa [← Cardinal.one_le_iff_ne_zero, one_le_rank_iff] at h'
  simpa [← map_smul, zero_notMem_nonZeroDivisors, hf] using @h (f 1)

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
x : CliffordAlgebra Q
hx : x ∈ spinGroup Q
⊢ star x ∈ spinGroup Q

Tactic:
by
  rw [mem_iff] at hx ⊢
  obtain ⟨hx₁, hx₂⟩ := hx
  refine ⟨pinGroup.star_mem hx₁, ?_⟩
  dsimp only [CliffordAlgebra.even] at hx₂ ⊢
  simp only [Submodule.mem_toSubalgebra] at hx₂ ⊢
  simp only [star_def, reverse_mem_evenOdd_iff, involute_mem_evenOdd_iff, hx₂]

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

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

Tactic:
simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl

Goal state after: