mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
⊢ kleinFour α = commutator ↥(alternatingGroup α)

Tactic:
have _ : (kleinFour α).Normal := normal_kleinFour hα4
  have : Nat.card (alternatingGroup α ⧸ kleinFour α) = 3 := by
    rw [← Nat.mul_left_inj (a := Nat.card (kleinFour α))]
    · rw [← Subgroup.card_eq_card_quotient_mul_card_subgroup]
      rw [card_of_card_eq_four hα4, kleinFour_card_of_card_eq_four hα4]
    rw [kleinFour_card_of_card_eq_four hα4]; simp
  have comm_le : commutator (alternatingGroup α) ≤ kleinFour α := by
    rw [← Subgroup.Normal.quotient_commutative_iff_commutator_le]
    exact (isCyclic_of_prime_card this).isMulCommutative
  have comm_ne_bot : commutator (alternatingGroup α) ≠ ⊥ := by
    rw [ne_eq, commutator_eq_bot_iff_center_eq_top,
      center_eq_bot (le_of_eq hα4.symm)]
    apply @bot_ne_top _ _ _ ?_
    rw [Subgroup.nontrivial_iff, ← Finite.one_lt_card_iff_nontrivial,
      card_of_card_eq_four hα4]
    simp
  obtain ⟨k, hk, hk'⟩ := Or.resolve_left (Subgroup.bot_or_exists_ne_one _) comm_ne_bot
  suffices hk22 : (k : Equiv.Perm α).cycleType = {2, 2} by
    refine le_antisymm ?_ comm_le
    intro g hg
    rw [← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hα4,
      Set.mem_union, Set.mem_singleton_iff, Set.mem_ofPred_eq] at hg
    rcases hg with ⟨rfl⟩ | hg
    · exact Subgroup.one_mem _
    · rw [← hg, ← Equiv.Perm.isConj_iff_cycleType_eq, isConj_iff] at hk22
      obtain ⟨c, hc⟩ := hk22
      rw [← MulAut.conjNormal_apply, Subtype.coe_inj] at hc
      simp only [commutator, ← hc]
      let fc : MulAut (alternatingGroup α) := MulAut.conjNormal c
      suffices (⊤ : Subgroup (alternatingGroup α)) =
        Subgroup.map fc.toMonoidHom (⊤ : Subgroup (alternatingGroup α)) by
        rw [this, ← Subgroup.map_commutator]
        refine Subgroup.mem_map_of_mem _ hk
      simp
  have hk2 := comm_le hk
  rw [← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hα4,
    Set.mem_union, Set.mem_singleton_iff, Set.mem_ofPred_eq] at hk2
  exact hk2.resolve_left hk'

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
⊢ ∀ ⦃x_1 : ι⦄, x_1 ∈ univ → ¬x x_1 ≠ x x_1

Tactic:
exact fun _ _ H => H rfl

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = hammingDist y x

Tactic:
simp_rw [hammingDist, ne_comm]

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → AddGroup (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = hammingNorm (-x + y)

Tactic:
simp_rw [hammingNorm, hammingDist, Pi.add_apply, Pi.neg_apply, ne_eq, neg_add_eq_zero]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsFiniteKernel κ
f : β → γ
a : α
hf : Measurable f
⊢ ((κ.map f) a) Set.univ ≤ κ.bound

Tactic:
rw [map_apply' κ hf a MeasurableSet.univ]

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsFiniteKernel κ
f : β → γ
a : α
hf : Measurable f
⊢ (κ a) (f ⁻¹' Set.univ) ≤ κ.bound
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
⊢ κ.swapRight.fst = κ.snd

Tactic:
by
  ext a s hs
  rw [fst_apply' _ _ hs, swapRight_apply', snd_apply' _ _ hs]
  · rfl
  · exact measurable_fst hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
h : IsSFiniteKernel (prodMkLeft γ κ)
⊢ IsSFiniteKernel κ

Tactic:
← sectR_prodMkLeft γ κ default

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
h : IsSFiniteKernel (prodMkLeft γ κ)
⊢ IsSFiniteKernel ((prodMkLeft γ κ).sectR default)
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
f : β → γ
hf : Measurable f
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (κ a) (f ⁻¹' s) ∂μ = ∫⁻ (a : α), ((κ.map f) a) s ∂μ

Tactic:
Kernel.map_apply' _ hf _ hs

Goal state after:
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 η
f : β × γ → E
h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ HasFiniteIntegral f ((κ ⊗ₖ η) a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y ↦ f (x, y)) (η (a, x))) ∧
      HasFiniteIntegral (fun x ↦ ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)

Tactic:
hasFiniteIntegral_congr h1f.ae_eq_mk,

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 η
f : β × γ → E
h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ HasFiniteIntegral (AEStronglyMeasurable.mk f h1f) ((κ ⊗ₖ η) a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y ↦ f (x, y)) (η (a, x))) ∧
      HasFiniteIntegral (fun x ↦ ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
⊢ μ.tilted f = 0

Tactic:
refine tilted_of_not_integrable ?_
  suffices ¬ AEMeasurable (fun x ↦ exp (f x)) μ by exact fun h ↦ this h.1.aemeasurable
  exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
h_ae1 : ∀ᵐ (a : 𝓧) ∂ν, μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a
h_compProd : (fun p ↦ μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p) =ᵐ[ν ⊗ₘ η] (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
⊢ ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)

Tactic:
Filter.EventuallyEq,

Goal state after:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
h_ae1 : ∀ᵐ (a : 𝓧) ∂ν, μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a
h_compProd : ∀ᵐ (x : 𝓧 × 𝓨) ∂ν ⊗ₘ η, μ.rnDeriv ν x.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) x = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x
⊢ ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ (klDiv μ ν).toReal = 0

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ ¬Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν

Tactic:
· rw [klDiv_of_not_integrable h_int, ENNReal.toReal_top]

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ ¬Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν
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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ klDiv (c • μ) (c • ν) = ↑c * klDiv μ ν

Tactic:
rw [klDiv_of_not_integrable h_int, klDiv_of_not_integrable, ENNReal.mul_top hc']
    refine fun h_contra ↦ h_int ?_
    rw [hμ_smul μ, hμ_smul ν]
    refine Integrable.smul_measure_nnreal ?_
    rw [integrable_congr (llr_smul_nnreal_same (hμν.smul c) c⁻¹ (by simpa))]
    fun_prop

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

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(Lp E 2 μ)
hg : AEStronglyMeasurable (↑↑g) μ
⊢ ⟪f, g⟫ = ⟪↑((condExpL2 E 𝕜 hm) f), g⟫

Tactic:
← sub_eq_zero,

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(Lp E 2 μ)
hg : AEStronglyMeasurable (↑↑g) μ
⊢ ⟪f, g⟫ - ⟪↑((condExpL2 E 𝕜 hm) f), g⟫ = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝⁴ : SigmaFinite (μ.trim hm)
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsOrderedModule ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
hx : 0 ≤ x
⊢ 0 ≤ (condExpInd E hm μ s) x

Tactic:
← coeFn_le

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝⁴ : SigmaFinite (μ.trim hm)
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsOrderedModule ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
hx : 0 ≤ x
⊢ ↑↑0 ≤ᵐ[μ] ↑↑((condExpInd E hm μ s) x)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ ∫ (x : α) in s, ↑↑↑((condExpL2 E' 𝕜 hm) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ

Tactic:
← sub_eq_zero,

Goal state after:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ ∫ (x : α) in s, ↑↑↑((condExpL2 E' 𝕜 hm) f) x ∂μ - ∫ (x : α) in s, ↑↑f x ∂μ = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E'
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ ∫⁻ (a : α) in t, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x‖₊ ∂μ =
    (∫⁻ (a : α) in t, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a‖₊ ∂μ) * ↑‖x‖₊

Tactic:
simp_rw [nnnorm_smul, ENNReal.coe_mul]
      rw [lintegral_mul_const]
      exact (Lp.stronglyMeasurable _).enorm (ε := ℝ)

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

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : G
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ ∫⁻ (a : α) in t, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x‖₊ ∂μ =
    (∫⁻ (a : α) in t, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a‖₊ ∂μ) * ↑‖x‖₊

Tactic:
simp_rw [nnnorm_smul, ENNReal.coe_mul]
      rw [lintegral_mul_const]
      exact (Lp.stronglyMeasurable _).enorm (ε := ℝ)

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

Goal state before:
pp: α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
f : α → F'
s : Set α
inst✝ : CompleteSpace F'
hf : Integrable f μ
hs : MeasurableSet s
⊢ ∫ (x : α) in s, ↑↑(condExpL1 hm μ f) x ∂μ = ∫ (x : α) in s, f x ∂μ

Tactic:
simp_rw [condExpL1_eq hf]

Goal state after:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
f : α → F'
s : Set α
inst✝ : CompleteSpace F'
hf : Integrable f μ
hs : MeasurableSet s
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (Integrable.toL1 f hf)) x ∂μ = ∫ (x : α) in s, f x ∂μ
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case pos
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 : w i = 1
j : Fin (n + 1)
hj : j = i
⊢ w j = Pi.single i 1 j

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 : ∑ 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 : w i = 1
j : Fin (n + 1)
hj : ¬j = i
⊢ w j = Pi.single i 1 j

Tactic:
· aesop

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 : ∑ 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 : w i = 1
j : Fin (n + 1)
hj : ¬j = i
⊢ w j = Pi.single i 1 j
Module: Mathlib.LinearAlgebra.Dual.BaseChange

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

Tactic:
by
  simp [toDual, linearMapLeftRightHom_comp_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case inr
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
hV : Nontrivial V
hcomm : ∀ (i j : ι) (r : R), i ≠ j → f * (b.coord i).transvection (r • b j) = (b.coord i).transvection (r • b j) * f
⊢ ∃ x, ∃ (h : ∀ (g : R), g * x = x * g), f = ⟨x, ⋯⟩ • 1

Tactic:
replace hcomm (i j : ι) (hij : i ≠ j) (r : R) :
      r • f (b j) = b.coord i (f (b i)) • r • b j := by
    have := hcomm i j r hij
    rw [LinearMap.ext_iff] at this
    simpa [LinearMap.transvection.apply] using this (b i)

Goal state after:
case inr
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
hV : Nontrivial V
hcomm : ∀ (i j : ι), i ≠ j → ∀ (r : R), r • f (b j) = (b.coord i) (f (b i)) • r • b j
⊢ ∃ x, ∃ (h : ∀ (g : R), g * x = x * g), f = ⟨x, ⋯⟩ • 1
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
e : V ≃ₗ[R] V
f : Dual R V
v : V
hv : f v = 0
⊢ (transvection hv).symm ∈ transvections R V

Tactic:
transvection.symm_eq

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e : V ≃ₗ[R] V
f : Dual R V
v : V
hv : f v = 0
⊢ transvection ⋯ ∈ transvections R V
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case h
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
⊢ ↑e = ↑(transvection hfv)

Tactic:
← sub_eq_zero,

Goal state after:
case h
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
⊢ ↑e - ↑(transvection hfv) = 0
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case refine_2
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 : e ∈ dilatransvections K V
he' : e.fixedReduce = 1
⊢ e ∈ transvections K V

Tactic:
by_cases he_one : e = 1
    · use 0, 0, by simp, by aesop
    have hefixed_ne_top : e.fixedSubmodule ≠ ⊤ := by
      rwa [ne_eq, LinearEquiv.fixedSubmodule_eq_top_iff]
    obtain ⟨w : V, hw : w ∉ e.fixedSubmodule⟩ :=
      SetLike.exists_not_mem_of_ne_top e.fixedSubmodule hefixed_ne_top rfl
    obtain ⟨f, hfw, hf⟩ := Submodule.exists_dual_map_eq_bot_of_notMem hw inferInstance
    rw [mem_dilatransvections_iff_finrank_quotient] at he
    have hf' : e.fixedSubmodule = LinearMap.ker f := by
      suffices finrank K (V ⧸ LinearMap.ker f) = 1 by
        apply Submodule.eq_of_le_of_finrank_le
        · intro x
          rw [mem_ker, ← Submodule.mem_bot K, ← hf]
          exact mem_map_of_mem
        rw [← Nat.add_le_add_iff_right, finrank_quotient_add_finrank] at he
        have := (LinearMap.ker f).finrank_quotient_add_finrank
        linarith
      rw [← Nat.add_left_inj, Submodule.finrank_quotient_add_finrank]
      rw [← f.finrank_ker_add_one_of_ne_zero, add_comm]
      aesop
    have eq_top : e.fixedSubmodule ⊔ Submodule.span K {w} = ⊤ := by
      rw [Submodule.sup_span_singleton_eq_top_iff hw]
      apply le_antisymm he
      apply Nat.one_le_of_lt
      rw [← Nat.ne_zero_iff_zero_lt]
      contrapose hefixed_ne_top
      apply eq_top_of_finrank_eq
      rw [← Nat.add_left_cancel_iff, finrank_quotient_add_finrank, hefixed_ne_top, zero_add]
    set v := (f w)⁻¹ • (e w - w)
    suffices hfv : f v = 0 by
      use f, v, hfv
      rw [← LinearEquiv.toLinearMap_inj,
        ← sub_eq_zero, ← LinearMap.ker_eq_top, eq_top_iff, ← eq_top]
      simp only [LinearEquiv.transvection.coe_toLinearMap,
        sup_le_iff, Submodule.span_singleton_le_iff_mem, LinearMap.mem_ker, LinearMap.sub_apply,
        LinearEquiv.coe_coe]
      constructor
      · intro x hx
        suffices f x = 0 by
          simpa [this, LinearMap.transvection.apply, sub_eq_zero] using hx
        rwa [hf', LinearMap.mem_ker] at hx
      · simp_all [v, LinearMap.transvection.apply]
    suffices e w - w ∈ LinearMap.ker f by
      simp only [LinearMap.mem_ker, map_sub] at this
      simp only [v, LinearMap.map_smul, map_sub, this, smul_zero]
    rw [← hf', ← Submodule.ker_mkQ e.fixedSubmodule, LinearMap.mem_ker]
    simp [Submodule.mkQ_apply, Submodule.Quotient.mk_sub, ← fixedReduce_mk, he']

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r₁ r₂ : R
⊢ (ι 0) (r₁ • 1) * (ι 0) (r₂ * 1) = 0

Tactic:
← smul_eq_mul r₂,

Goal state after:
R : Type u_1
inst✝ : CommRing R
r₁ r₂ : R
⊢ (ι 0) (r₁ • 1) * (ι 0) (r₂ • 1) = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ (DualNumber.lift ⟨(Algebra.ofId R (CliffordAlgebra 0), (ι 0) 1), ⋯⟩).comp ((CliffordAlgebra.lift 0) ⟨inrHom R R, ⋯⟩) =
    AlgHom.id R (CliffordAlgebra 0)

Tactic:
ext : 2; simp

Goal state after: