mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
hij : i ≠ j
this : InvolutiveNeg ι := P.indexNeg
k : ι
aux : ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-↑i)) = (⁅e i, f j⁆ * ω b) (Sum.inr k) (Sum.inr ↑i)
⊢ (⁅e j, f i⁆ᵀ (Sum.inr ↑i) ⬝ᵥ fun j ↦ (-ω b)ᵀ j (Sum.inr k)) = 0 (Sum.inr k)

Tactic:
lie_e_f_ne_aux₁ hij.symm

Goal state after:
case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
hij : i ≠ j
this : InvolutiveNeg ι := P.indexNeg
k : ι
aux : ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-↑i)) = (⁅e i, f j⁆ * ω b) (Sum.inr k) (Sum.inr ↑i)
⊢ (0 ⬝ᵥ fun j ↦ (-ω b)ᵀ j (Sum.inr k)) = 0 (Sum.inr k)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
i j : ↥b.support
⊢ ⁅⟨h i, ⋯⟩, ⟨h j, ⋯⟩⁆ = 0

Tactic:
by simp [Subtype.ext_iff, lie_h_h]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear

Goal state before:
pp: 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
hx : B.IsReflective x
a b : M
⊢ (B x) x * Exists.choose ⋯ = (B x) x * (Exists.choose ⋯ + Exists.choose ⋯)

Tactic:
← (hx.2 (a + b)).choose_spec,

Goal state after:
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
hx : B.IsReflective x
a b : M
⊢ 2 * (B x) (a + b) = (B x) x * (Exists.choose ⋯ + Exists.choose ⋯)
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s' s : Multiset α
⊢ CutExpand r s' s ↔ ∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t

Tactic:
simp_rw [CutExpand, add_singleton_eq_iff]

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s' s : Multiset α
⊢ (∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a) ↔
    ∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s' s : Multiset α
⊢ CutExpand r s' s → (∀ a ∈ s, p a) → ∀ a ∈ s', p a

Tactic:
classical
  rw [cutExpand_iff]
  rintro ⟨t, a, hr, ha, rfl⟩ hsp a' h'
  obtain (h' | h') := mem_add.1 h'
  exacts [hsp a' (mem_of_mem_erase h'), h (hr a' h') (hsp a ha)]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: case right
ι : 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) := ⋯
⊢ (P (I ∪ J)) U = (P J) T

Tactic:
· have h_eq_union : cylinder J T = cylinder (I ∪ J) U := by
      rw [← inter_cylinder, h_eq, inter_self]
    exact hP.congr_cylinder_of_subset hT h_eq_union.symm Finset.subset_union_right

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetRing C
⊢ ∀ s ∈ C, ∀ t ∈ C, ∃ I, ↑I ⊆ C ∧ (↑I).PairwiseDisjoint id ∧ s \ t = ⋃₀ ↑I

Tactic:
by
    refine fun s hs t ht => ⟨{s \ t}, ?_, ?_, ?_⟩
    · simp only [coe_singleton, Set.singleton_subset_iff]
      exact hC.sdiff_mem hs ht
    · simp only [coe_singleton, pairwiseDisjoint_singleton]
    · simp only [coe_singleton, sUnion_singleton]

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case empty
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
hSC : ↑∅ ⊆ C
⊢ ∃ P, ↑P.parts ⊆ C

Tactic:
exact ⟨.empty _, hSC⟩

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case insert.inr
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
a✝ : s ∉ S
ih : ↑S ⊆ C → ∃ P, ↑P.parts ⊆ C
hsC : s ∈ C
hSC : ↑S ⊆ C
P : Finpartition (S.sup id)
hP : ↑P.parts ⊆ C
hs : s ≠ ⊥
Q : (t : Set α) → t ∈ (P.avoid s).parts → Finpartition t
hQ : ∀ (t : Set α) (a : t ∈ (P.avoid s).parts), ↑(Q t a).parts ⊆ C
⊢ ↑(((P.avoid s).bind Q).extend hs ⋯ ⋯).parts ⊆ C

Tactic:
Finpartition.extend_parts,

Goal state after:
case insert.inr
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
a✝ : s ∉ S
ih : ↑S ⊆ C → ∃ P, ↑P.parts ⊆ C
hsC : s ∈ C
hSC : ↑S ⊆ C
P : Finpartition (S.sup id)
hP : ↑P.parts ⊆ C
hs : s ≠ ⊥
Q : (t : Set α) → t ∈ (P.avoid s).parts → Finpartition t
hQ : ∀ (t : Set α) (a : t ∈ (P.avoid s).parts), ↑(Q t a).parts ⊆ C
⊢ ↑(insert s ((P.avoid s).bind Q).parts) ⊆ C
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ generateFrom (measurableCylinders α) ≤ MeasurableSpace.pi

Tactic:
refine MeasurableSpace.generateFrom_le (fun S hS ↦ ?_)

Goal state after:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
S : Set ((i : ι) → α i)
hS : S ∈ measurableCylinders α
⊢ MeasurableSet S
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ generateFrom (measurableCylinders α) = MeasurableSpace.pi

Tactic:
by
  apply le_antisymm
  · refine MeasurableSpace.generateFrom_le (fun S hS ↦ ?_)
    obtain ⟨s, S, hSm, rfl⟩ := (mem_measurableCylinders _).mp hS
    exact hSm.cylinder
  · refine iSup_le fun i ↦ ?_
    refine (comap_eval_le_generateFrom_squareCylinders_singleton α i).trans ?_
    refine MeasurableSpace.generateFrom_mono (fun x ↦ ?_)
    simp only [singleton_pi, mem_image, mem_pi, mem_univ, mem_ofPred_eq,
      forall_true_left, mem_measurableCylinders, forall_exists_index, and_imp]
    rintro t ht rfl
    refine ⟨{i}, {f | f ⟨i, Finset.mem_singleton_self i⟩ ∈ t i}, measurable_pi_apply _ (ht i), ?_⟩
    ext1 x
    simp only [mem_preimage, Function.eval, mem_cylinder, mem_ofPred_eq, Finset.restrict]

Goal state after:
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
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
u : V
hu : LinearIndependent K ![(↑e).fixedSubmodule.mkQ u, e.fixedReduce ((↑e).fixedSubmodule.mkQ u)]
f : Dual K V
hfu : f u ≠ 0
v : V := (f u)⁻¹ • u
hf : map f ((↑e).fixedSubmodule ⊔ K ∙ (e v - v)) = ⊥
v_def : v = (f u)⁻¹ • u
hspan : K ∙ (e v - v) = K ∙ (e u - u)
⊢ ∃ f v,
    LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)] ∧
      (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f ∧ f v = 1

Tactic:
← le_ker_iff_map

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
u : V
hu : LinearIndependent K ![(↑e).fixedSubmodule.mkQ u, e.fixedReduce ((↑e).fixedSubmodule.mkQ u)]
f : Dual K V
hfu : f u ≠ 0
v : V := (f u)⁻¹ • u
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
v_def : v = (f u)⁻¹ • u
hspan : K ∙ (e v - v) = K ∙ (e u - u)
⊢ ∃ f v,
    LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)] ∧
      (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f ∧ f v = 1
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) = ⋃₀ ↑I ∪ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)

Tactic:
simp_rw [coe_union]

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
⊢ ⋃₀ (↑I ∪ ↑(hC.disjointOfDiffUnion hs hI)) = ⋃₀ ↑I ∪ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)
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
x✝ : (fun m s ↦ m.toFun s) m = (fun m s ↦ m.toFun s) m'
⊢ m = m'

Tactic:
cases m

Goal state after:
case mk
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m' : AddContent G C
toFun✝ : Set α → G
empty'✝ : toFun✝ ∅ = 0
sUnion'✝ : ∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → toFun✝ (⋃₀ ↑I) = ∑ u ∈ I, toFun✝ u
x✝ : (fun m s ↦ m.toFun s) { toFun := toFun✝, empty' := empty'✝, sUnion' := sUnion'✝ } = (fun m s ↦ m.toFun s) m'
⊢ { toFun := toFun✝, empty' := empty'✝, sUnion' := sUnion'✝ } = m'
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'
s : Set α
hs : s ∈ J
⊢ s = ⋃ t ∈ J', s ∩ t

Tactic:
simp_rw [← Finset.set_biUnion_coe, ← inter_iUnion, left_eq_inter, ← sUnion_eq_biUnion, ← h]

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'
s : Set α
hs : s ∈ J
⊢ s ⊆ ⋃₀ ↑J
Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' T
hS' : MeasurableSet S'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (I ∪ J) S'
⊢ projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t

Tactic:
have h_eq2 : t = cylinder (I ∪ J) T' := by rw [ht_eq]; exact cylinder_eq_cylinder_union J T I

Goal state after:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' T
hS' : MeasurableSet S'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (I ∪ J) S'
h_eq2 : t = cylinder (I ∪ J) T'
⊢ projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t
Module: Mathlib.MeasureTheory.Constructions.SimpleGraph

Goal state before:
pp: V : Type u_1
⊢ Measurable fromEdgeSet

Tactic:
by
  simp only [measurable_iff_adj, fromEdgeSet_adj, ne_eq]; fun_prop

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
⊢ ∑' (i : ℕ), m (f i) ≤ m (⋃ i, f i)

Tactic:
refine ENNReal.summable.tsum_le_of_sum_le fun I ↦ ?_

Goal state after:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
⊢ ∑ i ∈ I, m (f i) ≤ m (⋃ i, f i)
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 : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : m (accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)
⊢ accumulate s n ∈ C

Tactic:
· exact hC.accumulate_mem hsC n

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case neg
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn_pos : n > 0
he' : auxTransvection hf * e ∉ transvections K V ^ n * dilatransvections K V
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
g : Dual K V
hg0 : g ≠ 0
hg2 : map g ((↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v) = ⊥
⊢ ∃ x ∈ transvections K V, ∃ y ∈ transvections K V ^ n * dilatransvections K V, x * y = e

Tactic:
← le_ker_iff_map

Goal state after:
case neg
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn_pos : n > 0
he' : auxTransvection hf * e ∉ transvections K V ^ n * dilatransvections K V
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
g : Dual K V
hg0 : g ≠ 0
hg2 : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v ≤ ker g
⊢ ∃ x ∈ transvections K V, ∃ y ∈ transvections K V ^ n * dilatransvections K V, x * y = e
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
m : AddContent G C
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ m s + m (t \ s) ≤ m s + m t

Tactic:
exact add_le_add_right (addContent_mono hC.isSetSemiring (hC.sdiff_mem ht hs) ht sdiff_subset) _

Goal state after:
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:
simp only [not_and_or] at he

Goal state after:
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 :
  ¬1 < finrank K (V ⧸ (↑e).fixedSubmodule) ∨
    ¬e.fixedReduce ≠ 1 ∨ ¬∃ a, ∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • x
⊢ e ∈ transvections K V ^ (finrank K (V ⧸ (↑e).fixedSubmodule) - 1) * dilatransvections K V
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: case inl
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := ⋯
R₂ : ℕ → ℝ := ⋯
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : 1 ≤ M
⊢ blimsup (fun i ↦ cthickening (max 0 (r₁ i)) (s i)) atTop p ⊆
    blimsup (fun i ↦ cthickening (max 0 (r₂ i)) (s i)) atTop p

Tactic:
refine mono_blimsup' (hMr.mono fun i hi _ => cthickening_mono ?_ (s i))

Goal state after:
case inl
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := fun i ↦ max 0 (r₁ i)
R₂ : ℕ → ℝ := fun i ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : 1 ≤ M
i : ℕ
hi : M * R₁ i ≤ R₂ i
x✝ : p i
⊢ max 0 (r₁ i) ≤ max 0 (r₂ i)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
this : {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
⊢ μ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} = 0

Tactic:
← nonpos_iff_eq_zero

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
this : {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
⊢ μ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ≤ 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0
⊢ 0 < s (s.restrictNonposSeq i 0)

Tactic:
rw [restrictNonposSeq]; rw [← @Set.sdiff_empty _ i] at hi₂
    rcases someExistsOneDivLT_spec hi₂ with ⟨_, _, h⟩
    exact lt_trans Nat.one_div_pos_of_nat h

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n < m
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
hx₂ : x ∈ s.restrictNonposSeq i m
⊢ False

Tactic:
cases m

Goal state after:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
h : n < 0
hx₂ : x ∈ s.restrictNonposSeq i 0
⊢ False

case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
n✝ : ℕ
h : n < n✝ + 1
hx₂ : x ∈ s.restrictNonposSeq i (n✝ + 1)
⊢ False
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ ∃ i,
    ∃ (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0),
      s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧
        s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃

Tactic:
by
  set i := s.exists_compl_positive_negative.choose
  obtain ⟨hi₁, hi₂, hi₃⟩ := s.exists_compl_positive_negative.choose_spec
  exact ⟨i, hi₁, hi₂, hi₃, rfl, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : s ≤[i] 0
hi₁ : MeasurableSet i
⊢ (s.toMeasureOfLEZero i hi₁ hi) univ < ∞

Tactic:
by
    rw [toMeasureOfLEZero_apply s hi hi₁ MeasurableSet.univ]
    exact ENNReal.coe_lt_top

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ μ.toSignedMeasure ≤ ν.toSignedMeasure ↔ ∀ (s : Set α), MeasurableSet s → μ s ≤ ν s

Tactic:
VectorMeasure.le_iff

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ (∀ (i : Set α), MeasurableSet i → μ.toSignedMeasure i ≤ ν.toSignedMeasure i) ↔
    ∀ (s : Set α), MeasurableSet s → μ s ≤ ν s
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : SignedMeasure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ (t.toJordanDecomposition.posPart + μ.withDensity fun x ↦ ENNReal.ofReal (f x)) ⟂ₘ
    t.toJordanDecomposition.negPart + μ.withDensity fun x ↦ ENNReal.ofReal (-f x)

Tactic:
rw [mutuallySingular_ennreal_iff, totalVariation_mutuallySingular_iff,
    VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure] at htμ
  exact
    ((JordanDecomposition.mutuallySingular _).add_right
          (htμ.1.mono_ac (refl _) (withDensity_absolutelyContinuous _ _))).add_left
      ((htμ.2.symm.mono_ac (withDensity_absolutelyContinuous _ _) (refl _)).add_right
        (withDensity_ofReal_mutuallySingular hf))

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
⊢ lpNorm ((starRingEnd (α → K)) f) p μ = 0

Tactic:
lpNorm_of_not_aestronglyMeasurable fun h ↦ hf ?_

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
⊢ 0 = 0

α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
h : AEStronglyMeasurable ((starRingEnd (α → K)) f) μ
⊢ AEStronglyMeasurable f μ
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 μ
⊢ (s + t).singularPart μ = s.singularPart μ + t.singularPart μ

Tactic:
by
  refine
    (eq_singularPart _ (s.rnDeriv μ + t.rnDeriv μ)
        ((mutuallySingular_singularPart s μ).add_left (mutuallySingular_singularPart t μ))
        ?_).symm
  rw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ), 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.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
⊢ μ (s₁ ∪ s₂) ≤ μ s₁ + μ s₂

Tactic:
by
  have := measure_union_le (μ := (μ : Measure Ω)) s₁ s₂
  apply (ENNReal.toNNReal_mono (by finiteness) this).trans_eq
  rw [ENNReal.toNNReal_add (by finiteness) (by finiteness), coeFn_def]

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s
⊢ μ = ν

Tactic:
by
  apply Subtype.ext
  ext1 s s_mble
  exact h s s_mble

Goal state after: