mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (μ.trim hm) t < ∞ →
    0 ≤ ∫ (x : α) in t, AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x ∂μ.trim hm

Tactic:
hμt

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 < ∞
⊢ 0 ≤ ∫ (x : α) in t, AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x ∂μ.trim hm
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_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (fun p ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
⊢ ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    ∫ (p : 𝓧 × 𝓨), ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal ∂ν ⊗ₘ η

Tactic:
integral_rnDeriv_mul_log h_ac

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 (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (fun p ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
⊢ ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ = ∫ (a : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) a ∂μ ⊗ₘ κ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

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

Tactic:
simp_rw [condExp_of_not_le hm, Set.indicator_zero']; rfl

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

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

Tactic:
simp_rw [condExp_of_not_le hm, Set.indicator_zero']; rfl

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]
⊢ s.indicator μ[s.indicator f | m] =ᵐ[μ] μ[s.indicator f | m]

Tactic:
by
      refine (condExp_indicator_aux hs ?_).symm.trans ?_
      · exact indicator_ae_eq_restrict_compl (hm _ hs)
      · rw [Set.indicator_indicator, Set.inter_self]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (ω : Ω) in s, P⁻[X | mΩ] ω ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P

Tactic:
setLIntegral_trim hm (measurable_condLExp _ _ _) hs,

Goal state after:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (x : Ω) in s, P⁻[X | mΩ] x ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ s φ
hφ_cont : UpperSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ μ[φ ∘ f | m] ≤ᵐ[μ] φ ∘ μ[f | m]

Tactic:
by
  filter_upwards [hφ_cvx.neg.map_condExp_le hm hφ_cont.neg hf hs hf_int hφ_int.neg,
    condExp_neg (φ ∘ f) m] with a h ha
  simp_all [Pi.neg_comp]

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

Goal state before:
pp: case mpr
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
s : AffineSubspace k P
p : ↥s
c : P
r : k
h : Nonempty ↥s
q x : P
hx : x ∈ s
heq : (1 - r) • (c -ᵥ ↑p) +ᵥ x = q
⊢ ∃ y ∈ s, (1 - r) • (c -ᵥ ↑⋯.some) +ᵥ y = (1 - r) • (c -ᵥ ↑p) +ᵥ x

Tactic:
refine ⟨(1 - r) • (h.some.val -ᵥ p.val) +ᵥ x, ?_, ?_⟩
    · exact vadd_mem_of_mem_direction (smul_mem _ _ (vsub_mem_direction h.some.prop p.prop)) hx
    · rw [vadd_vadd, ← smul_add, vsub_add_vsub_cancel]

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 : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
⊢ swap i j • σ = σ → (summand a b σ) v = 0

Tactic:
induction σ using Quotient.inductionOn' with | _ σ
   =>  _ 

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)
⊢ swap i j • Quotient.mk'' σ = Quotient.mk'' σ → (summand a b (Quotient.mk'' σ)) v = 0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case neg
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 : ∑ x ∈ univ.erase i, w x + 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 : w i = 1
j : Fin (n + 1)
hj : ¬j = i
⊢ w j = Pi.single i 1 j

Tactic:
hshift,

Goal state after:
case neg
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 : ∑ x ∈ univ.erase i, w x + 1 = 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 : w i = 1
j : Fin (n + 1)
hj : ¬j = i
⊢ w j = Pi.single i 1 j
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: case inr
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 : Nontrivial R
⊢ LinearMap.det (j.endHom f) = (algebraMap R S) (LinearMap.det f)

Tactic:
let b := Module.finBasis R M

Goal state after:
case inr
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 : Nontrivial R
b : Basis (Fin (finrank R M)) R M := finBasis R M
⊢ LinearMap.det (j.endHom f) = (algebraMap R S) (LinearMap.det f)
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
⊢ (LinearMap.transvection f (-h.unit⁻¹ • v)) ((LinearMap.transvection f v) x) = x

Tactic:
by
    nth_rewrite 3 [← one_smul R v]
    rw [← LinearMap.comp_apply, Units.smul_def, LinearMap.transvection.comp_smul_smul]
    simp only [Units.val_neg, one_mul, mul_neg, ← sub_eq_add_neg]
    suffices (-h.unit⁻¹) + 1 - f v * (h.unit⁻¹) = 0 by simp [this]
    rw [sub_eq_zero, neg_add_eq_iff_eq_add]
    nth_rewrite 1 [← one_mul (h.unit⁻¹), Units.val_mul, ← add_mul]
    simp

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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
x : V
this : ↑(u.rangeRestrict x) = u x
⊢ u x = (b.repr (u.rangeRestrict x)) default • ↑(b default)

Tactic:
rw [← this, ← Submodule.coe_smul, Subtype.coe_inj]

Goal state after:
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
x : V
this : ↑(u.rangeRestrict x) = u x
⊢ u.rangeRestrict x = (b.repr (u.rangeRestrict x)) default • b default
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
⊢ 0 + (contractLeft d) ((contractLeft d) y✝) = 0

Tactic:
hy,

Goal state after:
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
⊢ 0 + 0 = 0
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 d' : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
hy : (contractLeft d) ((contractLeft d') y✝) = -(contractLeft d') ((contractLeft d) y✝)
⊢ -(contractLeft d') ((contractLeft d) x✝) + (contractLeft d) ((contractLeft d') y✝) =
    -((contractLeft d') ((contractLeft d) x✝) + (contractLeft d') ((contractLeft d) y✝))

Tactic:
hy,

Goal state after:
case add
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
x✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
hy : (contractLeft d) ((contractLeft d') y✝) = -(contractLeft d') ((contractLeft d) y✝)
⊢ -(contractLeft d') ((contractLeft d) x✝) + -(contractLeft d') ((contractLeft d) y✝) =
    -((contractLeft d') ((contractLeft d) x✝) + (contractLeft d') ((contractLeft d) y✝))
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: 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))
⊢ ((toMatrix b b) (transvection f v)).det = 1 + f v

Tactic:
rw [this]
      simp only [Matrix.det_diagonal]
      rw [Finset.prod_eq_single i]
      · simp
      · intro j _ hj
        simp [Function.update_of_ne hj]
      · simp

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

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
⊢ ↥(even (Q' Q)) →ₐ[R] CliffordAlgebra Q

Tactic:
let f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
    ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap.comp <|
          (ι Q).comp (LinearMap.fst _ _ _) +
            (Algebra.linearMap R _).comp (LinearMap.snd _ _ _)).compl₂
      ((ι Q).comp (LinearMap.fst _ _ _) - (Algebra.linearMap R _).comp (LinearMap.snd _ _ _))

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
⊢ ↥(even (Q' Q)) →ₐ[R] CliffordAlgebra Q
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 ℬ
j₁ i₂ : ι
a₁ : ⨁ (i : ι), 𝒜 i
b₁ : ℬ j₁
a₂ : 𝒜 i₂
b₂ : ⨁ (i : ι), ℬ i
⊢ (map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i)))
      ((TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)).symm
        (a₁ ⊗ₜ[R]
          (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i))
            ((gradedComm R ℬ 𝒜) ((lof R ι ℬ j₁) b₁ ⊗ₜ[R] (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] b₂))) =
    (-1) ^ (j₁ * i₂) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * b₂)

Tactic:
rw [mul_comm j₁ i₂, gradedComm_of_tmul_of]

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 ℬ
j₁ i₂ : ι
a₁ : ⨁ (i : ι), 𝒜 i
b₁ : ℬ j₁
a₂ : 𝒜 i₂
b₂ : ⨁ (i : ι), ℬ i
⊢ (map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i)))
      ((TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)).symm
        (a₁ ⊗ₜ[R]
          (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i))
            (((-1) ^ (i₂ * j₁) • (lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₁) b₁) ⊗ₜ[R] b₂))) =
    (-1) ^ (i₂ * j₁) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * b₂)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₁ i₂ : ZMod 2
hm₁ : m₁ ∈ evenOdd Q₁ i₁
hm₂ : m₂ ∈ evenOdd Q₂ i₂
⊢ (map f₁) m₁ * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) m₁)

Tactic:
induction hm₁ using Submodule.iSup_induction' with

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)ˣ
⊢ ↑x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ↔ x ∈ lipschitzGroup Q

Tactic:
by
  simp only [Submonoid.mem_map, Subgroup.mem_toSubmonoid, Units.coeHom_apply]
  norm_cast
  exact exists_eq_right

Goal state after:
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✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
this : ⇑mod ∘ ⇑b.repr = ⇑g ∘ ⇑nG.mkQ
⊢ Surjective ⇑(AddMonoidHom.toZModLinearMap n g.toAddMonoidHom)

Tactic:
by
      exact (this ▸ (mapRange_surjective _ (map_zero _) ZMod.intCast_surjective).comp
        b.repr.surjective).of_comp

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
⊢ LinearIndependent L fun i ↦ ⇑(algebraMap K L) ∘ v i

Tactic:
classical
  let : Fintype ι' := .ofFinite ι'
  let I : Set (ι' → K) := hv.linearIndepOn_id.extend (subset_univ _)
  let b : Module.Basis I K (ι' → K) := .extend hv.linearIndepOn_id
  let b' : Module.Basis I L (ι' → L) := (b.baseChange L).map (TensorProduct.piScalarRight K L L ι')
  let v' (i : ι) : I := ⟨v i, hv.linearIndepOn_id.subset_extend _ <| mem_range_self i⟩
  have hv' : b' ∘ v' = fun i ↦ algebraMap K L ∘ v i := by
    ext; simp [b', b, v', Module.Basis.extend, Algebra.algebraMap_eq_smul_one]
  have h_inj : Injective v' := fun i j hij ↦ by have : Injective v := hv.injective; aesop
  rw [← hv']
  exact b'.linearIndependent.comp _ h_inj

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : CommRing S
inst✝³ : LinearOrder S
inst✝² : IsStrictOrderedRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), abv (A i j) ≤ x
⊢ ∑ σ, ∏ i, abv (A (σ i) i) ≤ ∑ _σ, ∏ _i, x

Tactic:
gcongr; simp [hx]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
⊢ ⋯.choose * a hj.choose = g i

Tactic:
rw [mul_comm]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
⊢ a hj.choose * ⋯.choose = g i
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
⊢ (∏ x ∈ {x | ∃ j, f j = x}.attach, (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index) *
      Nat.card R ^ {x | ¬∃ j, f j = x}.card =
    Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index

Tactic:
rw [mul_comm]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
⊢ Nat.card R ^ {x | ¬∃ j, f j = x}.card *
      ∏ x ∈ {x | ∃ j, f j = x}.attach, (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index =
    Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
⊢ (M.submatrix i.succ.succAbove id).det = -((↑↑i).negOnePow • (M.submatrix (Fin.succAbove 0) id).det)

Tactic:
← neg_eq_iff_eq_neg,

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
⊢ -(M.submatrix i.succ.succAbove id).det = (↑↑i).negOnePow • (M.submatrix (Fin.succAbove 0) id).det