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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ Integrable (fun x ↦ (∫ (a : α), rexp (f a) ∂μ)⁻¹ • rexp (f x) • g x) μ ↔ Integrable (fun x ↦ rexp (f x) • g x) μ

Tactic:
integrable_fun_smul_iff

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ Integrable (fun x ↦ rexp (f x) • g x) μ ↔ Integrable (fun x ↦ rexp (f x) • g x) μ

case hc
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ (∫ (a : α), rexp (f a) ∂μ)⁻¹ ≠ 0
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⁻¹ • μ) ν) (c⁻¹ • μ)
⊢ Integrable (llr (c • c⁻¹ • μ) ν) (c⁻¹ • μ)

Tactic:
integrable_congr (llr_smul_nnreal_left (hμν.smul_left _) c hc)

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⁻¹ • μ) ν) (c⁻¹ • μ)
⊢ Integrable (fun x ↦ llr (c⁻¹ • μ) ν x + log ↑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 α
hm : m ≤ m0
f : ↥(Lp F p μ)
hf_meas : f ∈ lpMeasSubgroup F m p μ
⊢ MemLp (Exists.choose ⋯) p (μ.trim hm)

Tactic:
by
  have hf : AEStronglyMeasurable[m] f μ :=
    mem_lpMeasSubgroup_iff_aestronglyMeasurable.mp hf_meas
  change MemLp (hf.mk f) p (μ.trim hm)
  refine ⟨hf.stronglyMeasurable_mk.aestronglyMeasurable, ?_⟩
  rw [eLpNorm_trim hm hf.stronglyMeasurable_mk, eLpNorm_congr_ae hf.ae_eq_mk.symm]
  exact Lp.eLpNorm_lt_top f

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᵐ[μ.restrict s] 0
⊢ ↑↑↑((condExpL2 ℝ ℝ hm) f) =ᵐ[μ.restrict s] 0

Tactic:
by
  suffices h_nnnorm_eq_zero : ∫⁻ x in s, ‖(condExpL2 ℝ ℝ hm f : α → ℝ) x‖₊ ∂μ = 0 by
    rw [lintegral_eq_zero_iff] at h_nnnorm_eq_zero
    · refine h_nnnorm_eq_zero.mono fun x hx => ?_
      dsimp only at hx
      rw [Pi.zero_apply] at hx ⊢
      · rwa [ENNReal.coe_eq_zero, nnnorm_eq_zero] at hx
    · refine Measurable.coe_nnreal_ennreal (Measurable.nnnorm ?_)
      exact (Lp.stronglyMeasurable _).measurable
  rw [← nonpos_iff_eq_zero]
  refine (lintegral_nnnorm_condExpL2_le hs hμs f).trans (le_of_eq ?_)
  rw [lintegral_eq_zero_iff]
  · refine hf.mono fun x hx => ?_
    dsimp only
    rw [hx]
    simp
  · exact (Lp.stronglyMeasurable _).enorm (ε := ℝ)

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_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)

Tactic:
rw [integrable_add_iff_integrable_right'] 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_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (fun x ↦ log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)

𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal) (μ ⊗ₘ κ)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
⊢ μ[f + g | m] =ᵐ[μ] μ[f | m] + μ[g | m]

Tactic:
by_cases hm : m ≤ m₀
  swap; · simp_rw [condExp_of_not_le hm]; simp
  by_cases hμm : SigmaFinite (μ.trim hm)
  swap; · simp_rw [condExp_of_not_sigmaFinite hm hμm]; simp
  refine (condExp_ae_eq_condExpL1 hm _).trans ?_
  rw [condExpL1_add hf hg]
  exact (coeFn_add _ _).trans
    ((condExp_ae_eq_condExpL1 hm _).symm.add (condExp_ae_eq_condExpL1 hm _).symm)

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

Goal state before:
pp: case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
inst✝ : SigmaFinite (μ.trim hm)
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
t : Set α
ht : MeasurableSet t
hμt : (μ.trim hm) t < ∞
h_ae :
  ∀ᵐ (x : α) ∂μ,
    x ∈ t →
      AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x =
        ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) x
⊢ 0 ≤ ∫ (x : α) in t, ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) x ∂μ

Tactic:
setIntegral_condExpL2_indicator ht hs ((le_trim hm).trans_lt hμt).ne hμs

Goal state after:
case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
inst✝ : SigmaFinite (μ.trim hm)
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
t : Set α
ht : MeasurableSet t
hμt : (μ.trim hm) t < ∞
h_ae :
  ∀ᵐ (x : α) ∂μ,
    x ∈ t →
      AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x =
        ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) x
⊢ 0 ≤ μ.real (s ∩ t)
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 α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm this : SigmaFinite (μ.trim hm)
⊢ SigmaFinite ((μ.restrict s).trim hm)

Tactic:
← restrict_trim hm _ hs

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 α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm this : SigmaFinite (μ.trim hm)
⊢ SigmaFinite ((μ.trim hm).restrict s)
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: 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✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
i : ι
hAi : ∑ j, A i j = 1
hbi : b i = (Finset.affineCombination k Finset.univ p) (A i)
⊢ b i ∈ affineSpan k (range p)

Tactic:
hbi

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✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
i : ι
hAi : ∑ j, A i j = 1
hbi : b i = (Finset.affineCombination k Finset.univ p) (A i)
⊢ (Finset.affineCombination k Finset.univ p) (A i) ∈ affineSpan k (range p)
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case inl
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hcomm : ∀ (i j : ι) (r : R), i ≠ j → Commute f ((b.coord i).transvection (r • b j))
hV : Subsingleton V
x : V
⊢ f x = (⟨1, ⋯⟩ • 1) x

Tactic:
simp [Subring.smul_def, hV.allEq (f x) x]

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
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 = ⊥
hf' : (↑e).fixedSubmodule = ker f
eq_top : (↑e).fixedSubmodule ⊔ K ∙ w = ⊤
v : V := (f w)⁻¹ • (e w - w)
hfv : f v = 0
x : V
hx : x ∈ (↑e).fixedSubmodule
this : f x = 0
⊢ x ∈ (↑e - LinearMap.transvection f v).ker

Tactic:
by
          simpa [this, LinearMap.transvection.apply, sub_eq_zero] using hx

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
h : IsUnit (Q m)
⊢ IsUnit ((ι Q) m)

Tactic:
cases h.nonempty_invertible
  let := invertibleιOfInvertible Q m
  exact isUnit_of_invertible (ι Q m)

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
this :
  (gradedMul R 𝒜 ℬ) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) =
    DistribSMul.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r
⊢ ((gradedMul R 𝒜 ℬ) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1)) x = r • x

Tactic:
exact DFunLike.congr_fun this x

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
this :
  (gradedMul R 𝒜 ℬ).flip ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) =
    DistribSMul.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r
⊢ ((gradedMul R 𝒜 ℬ) x) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) = r • x

Tactic:
exact DFunLike.congr_fun this x

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
⊢ (ofProd Q₁ Q₂) ((ι (QuadraticMap.prod Q₁ Q₂)) (m₁, m₂)) = (ι Q₁) m₁ ᵍ⊗ₜ[R] 1 + 1 ᵍ⊗ₜ[R] (ι Q₂) m₂

Tactic:
ofProd,

Goal state after:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
⊢ ((lift (QuadraticMap.prod Q₁ Q₂))
        ⟨((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ
                (evenOdd Q₁ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯).coprod
            ((GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ
              (evenOdd Q₂ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯),
          ⋯⟩)
      ((ι (QuadraticMap.prod Q₁ Q₂)) (m₁, m₂)) =
    (ι Q₁) m₁ ᵍ⊗ₜ[R] 1 + 1 ᵍ⊗ₜ[R] (ι Q₂) m₂
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : AddMonoid M
φ : { φ // ∀ (g : G), n • φ g = 0 }
⊢ ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup ≤ (↑φ).ker

Tactic:
rintro - ⟨g, rfl⟩; simpa using φ.property g

Goal state after:
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
n : ℤ := ↑A 0 1 / ↑A 1 1
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * n
h4 : n * ↑A 1 1 ≤ ↑A 0 1
h3 : |↑A 0 1 % ↑A 1 1| < |↑A 1 1|
⊢ ↑A 1 0 = 0 ∧ n * ↑A 1 0 < ↑A 0 0 ∧ n * ↑A 1 1 ≤ ↑A 0 1 ∧ |↑A 0 1 + -(n * ↑A 1 1)| < |↑A 1 1|

Tactic:
simp_all only [mul_comm n, zero_mul, ← sub_eq_add_neg, ← h2,
        Fin.isValue, and_true]

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp

Goal state before:
pp: R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝³ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (κ i)
x : (i : ι) → Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ (ofDFinsuppEquiv ((tprod R) x)) p = (tprod R) fun i ↦ (x i) (p i)

Tactic:
simpa [ofDFinsuppEquiv, MultilinearMap.fromDFinsuppEquiv_apply] using fun i hi ↦
    ((tprod R).map_coord_zero (m := fun i ↦ x i (p i)) i hi).symm

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual

Goal state before:
pp: ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), Finite (κ i)
b : (i : ι) → Basis (κ i) R (M i)
this✝ : Fintype ι
this : (i : ι) → Fintype (κ i)
⊢ dualDistrib ∘ₗ dualDistribInvOfBasis b = LinearMap.id

Tactic:
refine (Basis.piTensorProduct b).dualBasis.ext (fun p ↦ ?_)
  refine (Basis.piTensorProduct b).ext (fun q ↦ ?_)
  simp [Finsupp.single_apply, Fintype.prod_ite_zero, ← funext_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁵ : Finite ι
M : ι → Type u_3
N : Type u_4
γ : ι → Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N
h : ∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))
n : ℕ
hι : Nat.card ι = n
⊢ φ = φ'

Tactic:
induction n generalizing ι with

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.DirectSum

Goal state before:
pp: R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst✝³ : CommSemiring R
inst✝² : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝¹ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝ : Finite ι
x : (i : ι) → ⨁ (j : κ i), M i j
p : (i : ι) → κ i
⊢ (ofDirectSumEquiv ((tprod R) x)) p = (tprod R) fun i ↦ (x i) (p i)

Tactic:
by
  have : Fintype ι := Fintype.ofFinite ι
  convert! ofDFinsuppEquiv_tprod_apply _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: F : Type u_2
inst✝ : Field F
hF : ∃ a, a ≠ 0 ∧ a ^ 2 ≠ 1
⊢ commutator PSL(2, F) = ⊤

Tactic:
by
  obtain ⟨a, ha, hasq⟩ := hF
  have : Group.IsPerfect SL(2, F) := ⟨SL2.commutator_eq_top ha hasq⟩
  have : Group.IsPerfect (Matrix.ProjectiveSpecialLinearGroup (Fin 2) F) := inferInstance
  exact this.commutator_eq_top

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
⊢ Q.radical ≤ LinearMap.ker Q.polarBilin

Tactic:
by
  intro m
  simp +contextual [mem_radical_iff', LinearMap.ext_iff, QuadraticMap.polar]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ {i | 0 < w i}.ncard + {i | w i < 0}.ncard + {i | w i = 0}.ncard = {i | 0 < w i}.ncard + {i | w i ≤ 0}.ncard

Tactic:
add_assoc,

Goal state after:
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ {i | 0 < w i}.ncard + ({i | w i < 0}.ncard + {i | w i = 0}.ncard) = {i | 0 < w i}.ncard + {i | w i ≤ 0}.ncard
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
ha : (a, a') ∈ S
hb : (b, b') ∈ S
hc : (c, c') ∈ S
hd : (d, d') ∈ S
he : (e, e') ∈ S
hf : (f, f') ∈ S
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
⊢ a = 0 ∧ b = 0

Tactic:
simp [S_def] at ha hb hc hd he hf

Goal state after:
a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
ha :
  a = 0 ∧ a' = 0 ∨
    a = 1 ∧ a' = 1 ∨
      a = -1 ∧ a' = -1 ∨
        a = 1 ∧ a' = 2 ∨
          a = 2 ∧ a' = 1 ∨
            a = -1 ∧ a' = -2 ∨ a = -2 ∧ a' = -1 ∨ a = 1 ∧ a' = 3 ∨ a = 3 ∧ a' = 1 ∨ a = -1 ∧ a' = -3 ∨ a = -3 ∧ a' = -1
hb :
  b = 0 ∧ b' = 0 ∨
    b = 1 ∧ b' = 1 ∨
      b = -1 ∧ b' = -1 ∨
        b = 1 ∧ b' = 2 ∨
          b = 2 ∧ b' = 1 ∨
            b = -1 ∧ b' = -2 ∨ b = -2 ∧ b' = -1 ∨ b = 1 ∧ b' = 3 ∨ b = 3 ∧ b' = 1 ∨ b = -1 ∧ b' = -3 ∨ b = -3 ∧ b' = -1
hc :
  c = 0 ∧ c' = 0 ∨
    c = 1 ∧ c' = 1 ∨
      c = -1 ∧ c' = -1 ∨
        c = 1 ∧ c' = 2 ∨
          c = 2 ∧ c' = 1 ∨
            c = -1 ∧ c' = -2 ∨ c = -2 ∧ c' = -1 ∨ c = 1 ∧ c' = 3 ∨ c = 3 ∧ c' = 1 ∨ c = -1 ∧ c' = -3 ∨ c = -3 ∧ c' = -1
hd :
  d = 0 ∧ d' = 0 ∨
    d = 1 ∧ d' = 1 ∨
      d = -1 ∧ d' = -1 ∨
        d = 1 ∧ d' = 2 ∨
          d = 2 ∧ d' = 1 ∨
            d = -1 ∧ d' = -2 ∨ d = -2 ∧ d' = -1 ∨ d = 1 ∧ d' = 3 ∨ d = 3 ∧ d' = 1 ∨ d = -1 ∧ d' = -3 ∨ d = -3 ∧ d' = -1
he :
  e = 0 ∧ e' = 0 ∨
    e = 1 ∧ e' = 1 ∨
      e = -1 ∧ e' = -1 ∨
        e = 1 ∧ e' = 2 ∨
          e = 2 ∧ e' = 1 ∨
            e = -1 ∧ e' = -2 ∨ e = -2 ∧ e' = -1 ∨ e = 1 ∧ e' = 3 ∨ e = 3 ∧ e' = 1 ∨ e = -1 ∧ e' = -3 ∨ e = -3 ∧ e' = -1
hf :
  f = 0 ∧ f' = 0 ∨
    f = 1 ∧ f' = 1 ∨
      f = -1 ∧ f' = -1 ∨
        f = 1 ∧ f' = 2 ∨
          f = 2 ∧ f' = 1 ∨
            f = -1 ∧ f' = -2 ∨ f = -2 ∧ f' = -1 ∨ f = 1 ∧ f' = 3 ∨ f = 3 ∧ f' = 1 ∨ f = -1 ∧ f' = -3 ∨ f = -3 ∧ f' = -1
⊢ a = 0 ∧ b = 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i : ↥b.support
inst✝¹ : P.IsReduced
inst✝ : DecidableEq ι
⊢ ⁅h i, f i⁆ = -(2 • f i)

Tactic:
rw [lie_h_f]; simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
h : TensorAlgebra R M →ₐ[R] A
x✝¹ x✝ : TensorAlgebra R M
h' : (symRingCon R M) x✝¹ x✝
⊢ (RingCon.ker h.toRingHom) x✝¹ x✝

Tactic:
refine RingCon.ringConGen_le.2 (fun x y h' => ?_) h'

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
h : TensorAlgebra R M →ₐ[R] A
x✝¹ x✝ : TensorAlgebra R M
h'✝ : (symRingCon R M) x✝¹ x✝
x y : TensorAlgebra R M
h' : SymRel R M x y
⊢ (RingCon.ker h.toRingHom) x y
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
a : M
⊢ (lift f) ((ι R M) a) = f a

Tactic:
simp [lift, ι, algHom, RingCon.liftₐEquiv]

Goal state after:
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
t u s x✝¹ : Multiset α
x✝ : α
⊢ s + t + {x✝} = s + u + x✝¹ ↔ t + {x✝} = u + x✝¹

Tactic:
add_assoc,

Goal state after:
α : Type u_1
r : α → α → Prop
t u s x✝¹ : Multiset α
x✝ : α
⊢ s + (t + {x✝}) = s + u + x✝¹ ↔ t + {x✝} = u + x✝¹
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
t u s x✝¹ : Multiset α
x✝ : α
⊢ s + (t + {x✝}) = s + u + x✝¹ ↔ t + {x✝} = u + x✝¹

Tactic:
add_assoc,

Goal state after:
α : Type u_1
r : α → α → Prop
t u s x✝¹ : Multiset α
x✝ : α
⊢ s + (t + {x✝}) = s + (u + x✝¹) ↔ t + {x✝} = u + x✝¹
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s₁ + s₂ + t
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a

Tactic:
add_assoc,

Goal state after:
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s₁ + (s₂ + t)
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a