mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
⊢ ∃ a, S'.inl a = (f (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * e'

Tactic:
rw [← MonoidHom.mem_range, S'.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv,
      ← MonoidHom.comp_apply, rightHom_comp]

Goal state after:
N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
⊢ (S.rightHom (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * S'.rightHom e' = 1
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
this : ∀ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ, ∃ k, x = k • a
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)

Tactic:
rw [isPretransitive_iff]
    rintro ⟨x, hx⟩ ⟨y, hy⟩
    obtain ⟨k, hk⟩ := this x hx
    obtain ⟨k', hk'⟩ := this y hy
    use k' * k⁻¹
    rw [← SetLike.coe_eq_coe]
    simp only [SetLike.mk_smul_mk]
    rw [hk, hk', smul_smul, inv_mul_cancel_right]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: case f
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
b : Localization s
a✝ : α
b✝ : ↥s
⊢ mk a✝ b✝ ≤ b → b ≤ mk a✝ b✝ → mk a✝ b✝ = b

Tactic:
induction b using Localization.rec
      · simp_rw [mk_le_mk, mk_eq_mk_iff, r_iff_exists]
        exact fun hab hba => ⟨1, by rw [hab.antisymm hba]⟩

Goal state after:
case f.H
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
b : Localization s
a✝¹ : α
b✝¹ : ↥s
a✝ c✝ : α
b✝ d✝ : ↥s
h✝ : (r s) (a✝, b✝) (c✝, d✝)
⊢ ⋯ = ⋯
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
⊢ f (mk.symm (mk (stabilizerEquiv_invFun_aux g)) • a) = f a

Tactic:
symm_apply_apply,

Goal state after:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
⊢ f (stabilizerEquiv_invFun_aux g • a) = f a
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
⊢ m.sum ≤ Fintype.card α

Tactic:
← hg,

Goal state after:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
⊢ g.cycleType.sum ≤ Fintype.card α
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) → ∃ g, g.cycleType = m

Tactic:
rintro ⟨hc, h2c⟩

Goal state after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ ∃ g, g.cycleType = m
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
k_mem : k ∈ centralizer {g}
c_mem : c ∈ g.cycleFactorsFinset
this : ↑g.cycleFactorsFinset = ConjAct.toConjAct k • ↑g.cycleFactorsFinset
⊢ ConjAct.toConjAct k • c ∈ g.cycleFactorsFinset

Tactic:
rw [← Finset.mem_coe, this]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
k_mem : k ∈ centralizer {g}
c_mem : c ∈ g.cycleFactorsFinset
this : ↑g.cycleFactorsFinset = ConjAct.toConjAct k • ↑g.cycleFactorsFinset
⊢ ConjAct.toConjAct k • c ∈ ConjAct.toConjAct k • ↑g.cycleFactorsFinset
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
⊢ Function.Injective ⇑a

Tactic:
intro c d h
  rw [← Subtype.coe_inj]
  apply g.cycleFactorsFinset_pairwise_disjoint.eq c.prop d.prop
  simp only [Disjoint, not_forall, not_or]
  use a c
  conv_rhs => rw [h]
  simp only [← Perm.mem_support, a.mem_support_self c, a.mem_support_self d, and_self]

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case H
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
motive : (con φ).Quotient → Prop
of : ∀ (i : ι) (g : G i), motive (((con φ).mk'.comp (inl.comp CoprodI.of)) g)
base : ∀ (h : H), motive (((con φ).mk'.comp inr) h)
mul : ∀ (x y : (con φ).Quotient), motive x → motive y → motive (x * y)
x : CoprodI G ∗ H
⊢ motive ↑x

Tactic:
induction x using Coprod.induction_on with
    | inl g =>
      induction g using CoprodI.induction_on with
      | of i g => exact of i g
      | mul x y ihx ihy =>
        rw [map_mul]
        exact mul _ _ ihx ihy
      | one => simpa using base 1
    | inr h => exact base h
    | mul x y ihx ihy => exact mul _ _ ihx ihy

Goal state after:
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
⊢ #{g | g.cycleType = {n}} = (n - 1)! * (card α).choose n

Tactic:
(Tactic.tacticSeq
 (Tactic.tacticSeq1Indented
  [(Tactic.tacticHave__
    "have"
    (Term.letConfig [])
    (Term.letDecl
     (Term.letIdDecl
      (Term.letId `hn₀)
      []
      [(Term.typeSpec ":" («term_≠_» `n "≠" (num "0")))]
      ":="
      (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.lia "lia" (Tactic.optConfig []))]))))))
   []
   (Tactic.tacticHave__
    "have"
    (Term.letConfig [])
    (Term.letDecl
     (Term.letIdDecl
      (Term.letId `aux)
      []
      [(Term.typeSpec
        ":"
        («term_=_»
         (Nat.term_! `n "!")
         "="
         («term_*_»
          (Nat.term_!
           (Term.paren (Term.hygienicLParen "(" (hygieneInfo `[anonymous])) («term_-_» `n "-" (num "1")) ")")
           "!")
          "*"
          `n)))]
      ":="
      (Term.byTactic
       "by"
       (Tactic.tacticSeq
        (Tactic.tacticSeq1Indented
         [(Tactic.rwSeq
           "rw"
           (Tactic.optConfig [])
           (Tactic.rwRuleSeq
            "["
            [(Tactic.rwRule [] `mul_comm) "," (Tactic.rwRule [] (Term.app `mul_factorial_pred [`hn₀]))]
            "]")
           [])]))))))
   []
   (Tactic.rwSeq
    "rw"
    (Tactic.optConfig [])
    (Tactic.rwRuleSeq
     "["
     [(Tactic.rwRule [] `mul_comm)
      ","
      (Tactic.rwRule ["←"] (Term.app `Nat.mul_left_inj [`hn₀]))
      ","
      (Tactic.rwRule [] `mul_assoc)
      ","
      (Tactic.rwRule ["←"] `aux)
      ","
      (Tactic.rwRule
       ["←"]
       (Term.app
        `Nat.mul_left_inj
        [(Term.paren
          (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
          (Term.app `factorial_ne_zero [(Term.hole "_")])
          ")")]))
      ","
      (Tactic.rwRule [] (Term.app `Nat.choose_mul_factorial_mul_factorial [`hα]))
      ","
      (Tactic.rwRule [] `mul_assoc)]
     "]")
    [])
   []
   (Tactic.simpa
    "simpa"
    []
    []
    (Tactic.simpaArgsRest
     (Tactic.optConfig [])
     []
     []
     [(Tactic.simpArgs
       "["
       [(Tactic.simpLemma [] [] `ite_and)
        ","
        (Tactic.simpLemma [] [] (Term.app `if_pos [`hα]))
        ","
        (Tactic.simpLemma [] [] (Term.app `if_pos [`hn']))
        ","
        (Tactic.simpLemma [] [] (Term.app `mul_comm [(Term.hole "_") `n]))
        ","
        (Tactic.simpLemma [] [] `mul_assoc)]
       "]")]
     ["using"
      (Term.app
       `card_of_cycleType_mul_eq
       [`α
        (choice
         («term{_}» "{" [`n] "}")
         (Term.structInst
          "{"
          []
          (Term.structInstFields [(Term.structInstField (Term.structInstLVal `n []) [])])
          (Term.optEllipsis [])
          []
          "}"))])]))]))

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : (↑k).cycleType = {2, 2}
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
⊢ g ∈ commutator ↥(alternatingGroup α)

Tactic:
← hg,

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
g : ↥(alternatingGroup α)
hk22 : (↑k).cycleType = (↑g).cycleType
hg : (↑g).cycleType = {2, 2}
⊢ g ∈ commutator ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : Group G''
f : G →* G'
f' : G' →* G''
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : Nontrivial ↥H
⊢ Subgroup.map H.subtype ⁅⊤, ⊤⁆ < Subgroup.map H.subtype ⊤

Tactic:
Subgroup.map_subtype_lt_map_subtype

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : Group G''
f : G →* G'
f' : G' →* G''
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : Nontrivial ↥H
⊢ ⁅⊤, ⊤⁆ < ⊤
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
⊢ ∀ {m₁ m₂ : G i}, (∀ (a : NormalWord d), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
by simp [summand_smul_def']

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
hH : ∀ y < H, IsCyclic ↥⁅y, y⁆
h : H ≠ ⊥
⊢ IsCyclic ↥⁅H, H⁆

Tactic:
· specialize hH ⁅H, H⁆ (Group.IsSolvable.commutator_lt_of_ne_bot h)
    replace hH : IsCyclic (⁅commutator H, commutator H⁆ : Subgroup H) := by
      let f := Subgroup.equivMapOfInjective ⁅commutator H, commutator H⁆ _ H.subtype_injective
      rw [Subgroup.map_commutator, Subgroup.map_subtype_commutator] at f
      exact isCyclic_of_surjective f.symm f.symm.surjective
    suffices IsCyclic (commutator H) by
      let f := Subgroup.equivMapOfInjective (commutator H) _ H.subtype_injective
      rw [Subgroup.map_subtype_commutator] at f
      exact isCyclic_of_surjective f f.surjective
    suffices h : commutator (commutator H) ≤ Subgroup.center (commutator H) by
      rw [← Abelianization.ker_of (commutator H)] at h
      let _ := commGroupOfCyclicCenterQuotient Abelianization.of h
      infer_instance
    suffices h : (commutator (commutator H)).map (commutator H).subtype ≤
        Subgroup.centralizer (commutator H) by
      simpa [SetLike.le_def, Subgroup.mem_center_iff, Subgroup.mem_centralizer_iff] using h
    rw [Subgroup.map_subtype_commutator, Subgroup.le_centralizer_iff]
    let _ := (hH.mulAutMulEquiv _).toMonoidHom.commGroupOfInjective (hH.mulAutMulEquiv _).injective
    have h := Abelianization.commutator_subset_ker ⁅commutator H, commutator H⁆.normalizerMonoidHom
    rwa [Subgroup.normalizerMonoidHom_ker, Subgroup.normalizer_eq_top,
      ← Subgroup.map_subtype_le_map_subtype, Subgroup.map_subtype_commutator,
        Subgroup.map_subgroupOf_eq_of_le le_top] at h

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_2
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : ↑Q ≤ commutator ↥(Subgroup.normalizer ↑P)
⊢ ↑P ≤ commutator G

Tactic:
rw [P.coe_subtype, ← Subgroup.map_subtype_le_map_subtype, ← P.coe_coe,
      Subgroup.map_subgroupOf_eq_of_le P.le_normalizer, Subgroup.map_subtype_commutator] at h
    exact h.trans (Subgroup.commutator_mono le_top le_top)

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
hG : IsZGroup G
⊢ ∃ N H φ x, IsCyclic ↥H ∧ IsCyclic ↥N ∧ (Nat.card ↥N).Coprime (Nat.card ↥H)

Tactic:
obtain ⟨H, hH⟩ := Subgroup.exists_right_complement'_of_coprime hG.coprime_commutator_index

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
hG : IsZGroup G
H : Subgroup G
hH : (commutator G).IsComplement' H
⊢ ∃ N H φ x, IsCyclic ↥H ∧ IsCyclic ↥N ∧ (Nat.card ↥N).Coprime (Nat.card ↥H)
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
a : α
f : δ → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : β), ∫⁻ (b : γ), ∫⁻ (b : δ), f b ∂ξ b ∂η b ∂κ a = ∫⁻ (b : γ), ∫⁻ (b : δ), f b ∂ξ b ∂(η ∘ₖ κ) a

Tactic:
lintegral_comp _ _ _ hf.lintegral_kernel

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ℕ), (((κ.seq i).comap g hg) a) s = ∑' (i : ℕ), ((κ.seq i) (g a)) s

Tactic:
simp_rw [comap_apply' _ hg _ s]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : ¬IsSFiniteKernel κ
⊢ 0 ⊗ₖ κ = 0

Tactic:
rw [Kernel.compProd_of_not_isSFiniteKernel_right _ _ h]

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 : StronglyMeasurable f
this : ∀ (x : β), ∀ᵐ (y : γ) ∂η (a, x), 0 ≤ ‖f (x, y)‖
p q r : Prop
h1 : r → p
⊢ (r ↔ p ∧ q) ↔ (p ∧ r ↔ p ∧ q)

Tactic:
and_iff_right_of_imp h1

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 : StronglyMeasurable f
this : ∀ (x : β), ∀ᵐ (y : γ) ∂η (a, x), 0 ≤ ‖f (x, y)‖
p q r : Prop
h1 : r → p
⊢ (r ↔ p ∧ q) ↔ (r ↔ p ∧ q)
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: case neg.refine_2
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : ν.real univ * f (μ'.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

pp: case neg.refine_2
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : f (μ'.real univ) ≤ (∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν) * (ν.real univ)⁻¹
⊢ 0 < (ν.real univ)⁻¹

Tactic:
· convert! h
    · simp only [div_eq_inv_mul, Measure.smul_apply, smul_eq_mul, ENNReal.toReal_mul,
      ENNReal.toReal_inv, μ', measureReal_def]

Goal state after:
case neg.refine_2
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : f (μ'.real univ) ≤ (∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν) * (ν.real univ)⁻¹
⊢ 0 < (ν.real univ)⁻¹
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
hfg : f =ᵐ[(κ ⊗ₖ η) a] g
a✝ : Integrable f ((κ ⊗ₖ η) a)
hf : ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
⊢ ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a

Tactic:
apply integral_congr_ae
      filter_upwards [ae_ae_of_ae_compProd hfg] with x hfgx using
        integral_congr_ae (ae_eq_symm hfgx)

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ ∫ (x : α), f x - log (∫ (x : α), rexp (f x) ∂μ) + llr μ ν x ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ

Tactic:
rw [integral_add ?_ h_int]
        swap; · exact hf.sub (integrable_const _)
        rw [integral_sub hf (integrable_const _)]
        simp only [integral_const, probReal_univ, smul_eq_mul, one_mul]

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

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

Tactic:
by_cases hc : c = 0
  · simp [hc, measureReal_def]
  have h_llr := llr_smul_nnreal_left hμν c (by simpa)
  rw [toReal_klDiv hμν h_int, toReal_klDiv (hμν.smul_left c)]
  swap
  · refine Integrable.smul_measure_nnreal ?_
    rw [integrable_congr h_llr]
    fun_prop
  simp only [integral_smul_nnreal_measure, measureReal_nnreal_smul_apply]
  rw [integral_congr_ae h_llr, integral_add h_int (integrable_const _)]
  have h_smul (a : ℝ) : c • a = c * a := rfl
  simp [h_smul]
  ring

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

Goal state before:
pp: case h
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
s : Set X
hs : MeasurableSet s
h's : μ s ≠ ∞
this : ∑' (n : ι), eLpNorm (f n) p (μ.restrict s) * (μ.restrict s) Set.univ ^ (1 / ENNReal.toReal 1 - 1 / p.toReal) < ∞
i : ι
⊢ ∫⁻ (a : X) in s, ‖f i a‖ₑ ∂μ ≤
    eLpNorm (f i) p (μ.restrict s) * (μ.restrict s) Set.univ ^ (1 / ENNReal.toReal 1 - 1 / p.toReal)

Tactic:
rw [← eLpNorm_one_eq_lintegral_enorm]

Goal state after:
case h
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
s : Set X
hs : MeasurableSet s
h's : μ s ≠ ∞
this : ∑' (n : ι), eLpNorm (f n) p (μ.restrict s) * (μ.restrict s) Set.univ ^ (1 / ENNReal.toReal 1 - 1 / p.toReal) < ∞
i : ι
⊢ eLpNorm (f i) 1 (μ.restrict s) ≤
    eLpNorm (f i) p (μ.restrict s) * (μ.restrict s) Set.univ ^ (1 / ENNReal.toReal 1 - 1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : G
⊢ ↑↑((condExpInd G hm μ s) x) =ᵐ[μ] ↑↑(condExpIndSMul hm hs hμs x)

Tactic:
← condExpIndL1Fin_ae_eq_condExpIndSMul

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : G
⊢ ↑↑((condExpInd G hm μ s) x) =ᵐ[μ] ↑↑(condExpIndL1Fin hm hs hμs x)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_3
α : 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 : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
⊢ AEStronglyMeasurable (↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯))) μ

Tactic:
exact lpMeas.aestronglyMeasurable _

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

Goal state before:
pp: 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) (↑↑(∑' (b : ι), f b) x)
⊢ HasSum (fun n ↦ ↑↑(f n) x) (↑↑(∑' (n : ι), f n) x)

Tactic:
exact e.hasSum_iff.1 hx

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

Goal state before:
pp: case refine_2
α : 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 α
E'' : Type u_8
𝕜' : Type u_9
inst✝⁴ : RCLike 𝕜'
inst✝³ : NormedAddCommGroup E''
inst✝² : InnerProductSpace 𝕜' E''
inst✝¹ : CompleteSpace E''
inst✝ : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ AEStronglyMeasurable (↑↑↑((condExpL2 E'' 𝕜' hm) (T.compLp f))) μ

Tactic:
exact lpMeas.aestronglyMeasurable _

Goal state after: