mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
K : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : DecidableEq K
w : ι → K
i : ι
h : ¬w i = 0
⊢ ⋯.choose ≠ 0

Tactic:
rw [← mul_self_eq_zero.ne, ← (IsAlgClosed.exists_eq_mul_self (w i)).choose_spec]
      simpa using h

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
b : Module.Basis n R V
A : SpecialLinearGroup n R
⊢ (fun a ↦ ↑a) ((fun u ↦ ⟨LinearMap.toMatrix' ↑↑u, ⋯⟩) ((fun A ↦ ⟨toLin' A, ⋯⟩) A)) = (fun a ↦ ↑a) A

Tactic:
by
    rw [← LinearEquiv.eq_symm_apply, LinearMap.toMatrix'_symm,
      Matrix.SpecialLinearGroup.toLin'_to_linearMap]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ Function.Injective ⇑PSLAction.toPermHom

Tactic:
by
  rw [injective_iff_map_eq_one]
  intro g hg
  rwa [← MonoidHom.mem_ker, PSLAction.toPermHom,
    QuotientGroup.ker_lift, SL_mulAction_ker, QuotientGroup.map_mk'_self,
    Subgroup.mem_bot] at hg

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

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module ℝ M
inst✝ : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
hQ : LinearMap.SeparatingLeft (associated Q)
w : Fin (finrank ℝ M) → SignType
hw₀ : ∀ (i : Fin (finrank ℝ M)), w i ≠ 0
hw : Equivalent Q (weightedSumSquares ℝ fun i ↦ ↑(w i))
i : Fin (finrank ℝ M)
⊢ (fun x ↦ ↑(w x)) i = -1 ∨ (fun x ↦ ↑(w x)) i = 1

Tactic:
cases hi : w i <;> simp_all

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing 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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
property✝ : x ∈ lieAlgebra b
hx : x ∈ span R (range h)
g : ↥(cartanSubalgebra' b) →ₗ[R] Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  (lieAlgebra b).subtype ∘ₗ (cartanSubalgebra' b).subtype
this : x ∈ map g (span R (range h'))
⊢ ⟨⟨x, property✝⟩, hx⟩ ∈ ↑(span R (range h'))

Tactic:
← (injective_subtype _).mem_set_image,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing 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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
property✝ : x ∈ lieAlgebra b
hx : x ∈ span R (range h)
g : ↥(cartanSubalgebra' b) →ₗ[R] Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  (lieAlgebra b).subtype ∘ₗ (cartanSubalgebra' b).subtype
this : x ∈ map g (span R (range h'))
⊢ (cartanSubalgebra' b).subtype ⟨⟨x, property✝⟩, hx⟩ ∈ ⇑(cartanSubalgebra' b).subtype '' ↑(span R (range h'))
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing 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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
property✝ : x ∈ lieAlgebra b
hx : x ∈ span R (range h)
g : ↥(cartanSubalgebra' b) →ₗ[R] Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  (lieAlgebra b).subtype ∘ₗ (cartanSubalgebra' b).subtype
this : x ∈ map g (span R (range h'))
⊢ (cartanSubalgebra' b).subtype ⟨⟨x, property✝⟩, hx⟩ ∈ ⇑(cartanSubalgebra' b).subtype '' ↑(span R (range h'))

Tactic:
← (injective_subtype _).mem_set_image,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing 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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
property✝ : x ∈ lieAlgebra b
hx : x ∈ span R (range h)
g : ↥(cartanSubalgebra' b) →ₗ[R] Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  (lieAlgebra b).subtype ∘ₗ (cartanSubalgebra' b).subtype
this : x ∈ map g (span R (range h'))
⊢ (lieAlgebra b).subtype ((cartanSubalgebra' b).subtype ⟨⟨x, property✝⟩, hx⟩) ∈
    ⇑(lieAlgebra b).subtype '' ⇑(cartanSubalgebra' b).subtype '' ↑(span R (range h'))
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P)

Tactic:
apply mul_right_cancel₀ (B.ne_zero (shortAddLong P))

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ P.pairing i (shortAddLong P) * (B.form (P.root (shortAddLong P))) (P.root (shortAddLong P)) =
    (P.pairing i (short P) + 3 * P.pairing i (long P)) * (B.form (P.root (shortAddLong P))) (P.root (shortAddLong P))
Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear

Goal state before:
pp: case dvd_two_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
⊢ ∀ (y_1 : M), (B ((reflection ⋯) y)) ((reflection ⋯) y) ∣ 2 * (B ((reflection ⋯) y)) y_1

Tactic:
intro z
    have hz : Module.reflection (coroot_apply_self B hx)
        (Module.reflection (coroot_apply_self B hx) z) = z := by
      exact (LinearEquiv.eq_symm_apply (Module.reflection (coroot_apply_self B hx))).mp rfl
    rw [← hz, isOrthogonal_reflection B hx hSB,
      isOrthogonal_reflection B hx hSB]
    exact hy.2 _

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
x : R
⊢ algebraMapInv ((algebraMap R (SymmetricAlgebra R M)) x) = x

Tactic:
by
  simp [algebraMapInv]

Goal state after:
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
s : Multiset α
ihs : (∀ a ∈ s, Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : ∀ a_1 ∈ a ::ₘ s, Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) (a ::ₘ s)

Tactic:
← s.singleton_add a

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
s : Multiset α
ihs : (∀ a ∈ s, Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : ∀ a_1 ∈ a ::ₘ s, Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) ({a} + s)
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
⊢ (P I) S = (P J) T

Tactic:
let U := Finset.restrict₂ Finset.subset_union_left ⁻¹' S ∩
      Finset.restrict₂ Finset.subset_union_right ⁻¹' T

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : ↥(I ∪ J)) → α ↑i) := Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T
⊢ (P I) S = (P J) T
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
a✝ : t ∉ T
ih : ∀ ⦃s : Set α⦄, s ∈ supClosure C → ↑T ⊆ C → s \ T.sup id ∈ supClosure C
s : Set α
hs : s ∈ supClosure C
hTC : ↑(insert t T) ⊆ C
⊢ (s \ t) \ T.sup id ∈ supClosure C

Tactic:
rw [coe_insert, insert_subset_iff] at hTC

Goal state after:
case insert
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
a✝ : t ∉ T
ih : ∀ ⦃s : Set α⦄, s ∈ supClosure C → ↑T ⊆ C → s \ T.sup id ∈ supClosure C
s : Set α
hs : s ∈ supClosure C
hTC : t ∈ C ∧ ↑T ⊆ C
⊢ (s \ t) \ T.sup id ∈ supClosure C
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
t : Finset ℕ
S : Set ((i : ↥t) → X ↑i)
mS : MeasurableSet S
⊢ t.restrict ⁻¹' S ∈ {(Finset.Iic (t.sup id)).restrict ⁻¹' Finset.restrict₂ ⋯ ⁻¹' S}

Tactic:
← preimage_comp,

Goal state after:
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
t : Finset ℕ
S : Set ((i : ↥t) → X ↑i)
mS : MeasurableSet S
⊢ t.restrict ⁻¹' S ∈ {Finset.restrict₂ ⋯ ∘ (Finset.Iic (t.sup id)).restrict ⁻¹' S}
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case h_ss
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ⊆ C

pp: case h_dis
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑(I ∪ hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

pp: case h_mem
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ∈ C

Tactic:
· rw [coe_union]
    exact Set.union_subset hI (hC.disjointOfDiffUnion_subset hs hI)

Goal state after:
case h_dis
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑(I ∪ hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

case h_mem
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ∈ C
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case h_dis
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (↑(insert s (hC.disjointOfDiff ht hs))).PairwiseDisjoint id

pp: case h_mem
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ⋃₀ ↑(insert s (hC.disjointOfDiff ht hs)) ∈ C

Tactic:
· rw [coe_insert]
    exact hC.pairwiseDisjoint_insert_disjointOfDiff ht hs

Goal state after:
case h_mem
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ⋃₀ ↑(insert s (hC.disjointOfDiff ht hs)) ∈ C
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
⊢ ∑ t ∈ J', ∑ s ∈ J, m (s ∩ t) = ∑ t ∈ J', m t

Tactic:
apply Finset.sum_congr rfl (fun t ht ↦ ?_)

Goal state after:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
t : Set α
ht : t ∈ J'
⊢ ∑ s ∈ J, m (s ∩ t) = m t
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case h
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
⊢ ∅ ∈ C

Tactic:
exact hC.empty_mem

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
⊢ extend (fun x x_1 ↦ m x) (⋃₀ ↑I) = ∑ u ∈ I, extend (fun x x_1 ↦ m x) u

Tactic:
rw [extend_eq]

Goal state after:
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
⊢ m (⋃₀ ↑I) = ∑ u ∈ I, extend (fun x x_1 ↦ m x) u

case h
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
⊢ ⋃₀ ↑I ∈ C
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s✝ t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
s : Set α
hs : s ∈ I
⊢ m s = extend (fun x x_1 ↦ m x) s

Tactic:
rw [extend_eq]

Goal state after:
case h
α : Type u_1
C : Set (Set α)
s✝ t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
s : Set α
hs : s ∈ I
⊢ s ∈ C
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
he : ¬e.IsExceptional
⊢ e ∈ transvections K V ^ (finrank K (V ⧸ (↑e).fixedSubmodule) - 1) * dilatransvections K V

Tactic:
by
  simp only [not_and_or] at he
  push Not at he
  rcases he with he | he | he
  · simpa [Nat.sub_eq_zero_of_le he, mem_dilatransvections_iff_finrank_quotient] using he
  · exact mem_transvections_pow_mul_dilatransvections_of_fixedReduce_eq_one he
  · exact mem_transvections_pow_mul_dilatransvections_of_fixedReduce_ne_smul_id he

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hf : MemLp f ∞ μ
hp_ne_zero : ¬∞ = 0
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) ∞ μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨M, hM⟩ := hf.eLpNormEssSup_indicator_norm_ge_eq_zero hmeas

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hf : MemLp f ∞ μ
hp_ne_zero : ¬∞ = 0
M : ℝ
hM : eLpNormEssSup ({x | M ≤ ↑‖f x‖₊}.indicator f) μ = 0
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) ∞ μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ s.someExistsOneDivLT i ⊆ i

Tactic:
rw [someExistsOneDivLT, dif_neg hi]

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ ∅ ⊆ i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasurableSet (s.someExistsOneDivLT i)

Tactic:
rw [someExistsOneDivLT, dif_neg hi]

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasurableSet ∅
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
hij : j ⊆ i
⊢ (v.restrict i) j = v j

Tactic:
by
  rw [restrict_apply v hi hj, Set.inter_eq_left.2 hij]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ (v + w).restrict i = v.restrict i + w.restrict i

Tactic:
· simp [restrict_not_measurable _ hi]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ (-v).restrict i = -v.restrict i

Tactic:
· simp [restrict_not_measurable _ hi]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
⊢ (c • v).map f = c • v.map f

Tactic:
simp only [map, dif_neg hf]
    -- `smul_zero` does not work since we do not require `ContinuousAdd`
    ext i
    simp

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s t : SignedMeasure α
⊢ s.totalVariation ⟂ₘ t.totalVariation → s ⟂ᵥ t

Tactic:
· rintro ⟨u, hmeas, hu₁, hu₂⟩
    exact
      ⟨u, hmeas, fun t htu => null_of_totalVariation_zero _ (measure_mono_null htu hu₁),
        fun t htv => null_of_totalVariation_zero _ (measure_mono_null htv hu₂)⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : Module ℚ≥0 E
inst✝ : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
hs : s.Nonempty
⊢ lpNorm (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, (fun i ↦ lpNorm (f i) p μ) i

Tactic:
exact lpNorm_sum_le hf hp

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

Goal state before:
pp: case refine_2
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i ↦ (fs i) ω) L (𝓝 (f ω))
⊢ ∀ᵐ (a : Ω) ∂μ, Tendsto (fun n ↦ ↑((fs n) a)) L (𝓝 ↑(f a))

Tactic:
simpa only [Function.comp_apply, ENNReal.tendsto_coe] using fs_lim

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝² : s.HaveLebesgueDecomposition μ
inst✝¹ : t.HaveLebesgueDecomposition μ
inst✝ : (s + t).HaveLebesgueDecomposition μ
⊢ (s + t).rnDeriv μ =ᵐ[μ] s.rnDeriv μ + t.rnDeriv μ

Tactic:
by
  refine
    Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _)
      ((integrable_rnDeriv _ _).add (integrable_rnDeriv _ _)) ?_
  rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
    withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add,
    add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set (α × β)
u : Set α
⊢ MeasurableSet u → ∀ (x : Set β), MeasurableSet x → u ×ˢ x = s✝ → Measurable fun a ↦ ((↑a.1).prod ↑a.2) s✝

Tactic:
Hu

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set (α × β)
u : Set α
Hu : MeasurableSet u
⊢ ∀ (x : Set β), MeasurableSet x → u ×ˢ x = s✝ → Measurable fun a ↦ ((↑a.1).prod ↑a.2) s✝
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ ‖{x | max C 1 ≤ ‖Exists.choose ⋯ x‖₊}.indicator (Exists.choose ⋯) x‖ ≤ ‖{x | C ≤ ‖g i x‖₊}.indicator (g i) x‖

Tactic:
rw [norm_indicator_eq_indicator_norm, norm_indicator_eq_indicator_norm]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ {x | max C 1 ≤ ‖Exists.choose ⋯ x‖₊}.indicator (fun a ↦ ‖Exists.choose ⋯ a‖) x ≤
    {x | C ≤ ‖g i x‖₊}.indicator (fun a ↦ ‖g i a‖) x
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
Heval : ∀ {u : Set α} {v : Set β}, MeasurableSet u → MeasurableSet v → Measurable fun a ↦ ↑a.1 u * ↑a.2 v
s✝ : Set (α × β)
x✝ : Set α
⊢ MeasurableSet x✝ → ∀ (x : Set β), MeasurableSet x → x✝ ×ˢ x = s✝ → Measurable fun a ↦ ((↑a.1).prod ↑a.2) s✝

Tactic:
Hu

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
Heval : ∀ {u : Set α} {v : Set β}, MeasurableSet u → MeasurableSet v → Measurable fun a ↦ ↑a.1 u * ↑a.2 v
s✝ : Set (α × β)
x✝ : Set α
Hu : MeasurableSet x✝
⊢ ∀ (x : Set β), MeasurableSet x → x✝ ×ˢ x = s✝ → Measurable fun a ↦ ((↑a.1).prod ↑a.2) s✝
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
⊢ testAgainstNN 0 = 0

Tactic:
funext
  simp only [zero_testAgainstNN_apply, Pi.zero_apply]

Goal state after: