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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ¬U ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
⊢ ∃ i, v b i ∈ U

Tactic:
suffices ∃ χ : H → K, χ ≠ 0 ∧ genWeightSpace U χ ≠ ⊥ by
    obtain ⟨χ, hχ₀, hχ⟩ := this
    obtain ⟨i, hi⟩ := instIsIrreducible_aux₀ χ hχ₀ hχ
    exact ⟨i, LieSubmodule.map_incl_le hi⟩

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ¬U ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
⊢ ∃ χ, χ ≠ 0 ∧ genWeightSpace (↥U) χ ≠ ⊥
Module: Mathlib.LinearAlgebra.SesquilinearForm.Star

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : StarRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
⊢ (∀ (i j : ι), star ((B (b i)) (b j)) = (B (b j)) (b i)) → B.IsSymm

Tactic:
refine fun h ↦ ⟨fun x y ↦ ?_⟩
    obtain ⟨fx, tx, ix, -, hx⟩ := Submodule.mem_span_iff_exists_finset_subset.1
      (by simp : x ∈ Submodule.span R (Set.range b))
    obtain ⟨fy, ty, iy, -, hy⟩ := Submodule.mem_span_iff_exists_finset_subset.1
      (by simp : y ∈ Submodule.span R (Set.range b))
    rw [← hx, ← hy]
    simp only [map_sum, LinearMap.map_smulₛₗ, starRingEnd_apply, map_smul, coe_sum,
      Finset.sum_apply, smul_apply, smul_eq_mul, Finset.mul_sum, map_mul, star_star]
    rw [Finset.sum_comm]
    refine Finset.sum_congr rfl (fun b₁ h₁ ↦ Finset.sum_congr rfl fun b₂ h₂ ↦ ?_)
    rw [mul_left_comm]
    obtain ⟨i, rfl⟩ := ix h₁
    obtain ⟨j, rfl⟩ := iy h₂
    rw [h]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
this✝ : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
him_mem : P.root i + P.root m ∈ range ⇑P.root
hik_mem : P.root k + P.root i ∈ range ⇑P.root
⊢ (chainBotCoeff i m + 1) * (chainBotCoeff j (-k) + 1) = (chainBotCoeff j (-l) + 1) * (chainBotCoeff i k + 1)

Tactic:
have hjk_mem : P.root j + P.root (-k) ∈ range P.root := by
    convert! mem_range_self (-m) using 1; simpa [sub_eq_add_neg] using congr(-$h₂)

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
this✝ : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
him_mem : P.root i + P.root m ∈ range ⇑P.root
hik_mem : P.root k + P.root i ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
⊢ (chainBotCoeff i m + 1) * (chainBotCoeff j (-k) + 1) = (chainBotCoeff j (-l) + 1) * (chainBotCoeff i k + 1)
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case trans
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) x✝ y✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • x✝) (r • y✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) (r • x✝) (r • z✝)

Tactic:
apply AddCon.trans

Goal state after:
case a
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) x✝ y✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • x✝) (r • y✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) (r • x✝) ?trans.y

case trans.a
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) x✝ y✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • x✝) (r • y✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) ?trans.y (r • z✝)

case trans.y
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) x✝ y✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • x✝) (r • y✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ ⨂[R] (x : ι), M
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
⊢ (↑s₁).pi t₁' ∩ (↑s₂).pi t₂ ∈ squareCylinders C

Tactic:
Set.pi_congr rfl h2,

Goal state after:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
⊢ (↑s₁).pi t₁' ∩ (↑s₂).pi t₂' ∈ squareCylinders C
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : f ∈ (↑s₁).pi t₁' ∩ (↑s₂).pi t₂
⊢ (t₁' i ∩ t₂' i).Nonempty

Tactic:
Set.pi_congr rfl h2,

Goal state after:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : f ∈ (↑s₁).pi t₁' ∩ (↑s₂).pi t₂'
⊢ (t₁' i ∩ t₂' i).Nonempty
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case pos
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : (∀ i ∈ ↑s₁, f i ∈ t₁' i) ∧ ∀ i ∈ ↑s₂, f i ∈ t₂' i
hi₂ : i ∈ s₂
⊢ f i ∈ t₂' i

pp: case neg
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : (∀ i ∈ ↑s₁, f i ∈ t₁' i) ∧ ∀ i ∈ ↑s₂, f i ∈ t₂' i
hi₂ : i ∉ s₂
⊢ f i ∈ t₂' i

Tactic:
· exact hf.2 i hi₂

Goal state after:
case neg
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : (∀ i ∈ ↑s₁, f i ∈ t₁' i) ∧ ∀ i ∈ ↑s₂, f i ∈ t₂' i
hi₂ : i ∉ s₂
⊢ f i ∈ t₂' i
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
f g : Dual K V
v : V
a b : K
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
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
x : V
⊢ g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v

Tactic:
have ha := ha x

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
f g : Dual K V
v : V
a b : K
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
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha✝ : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
x : V
ha : (auxTransvection hf * e) x - a • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
⊢ g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
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 : Finset ℕ
i : ℕ
left✝¹ : i ∈ ↑I
j : ℕ
left✝ : j ∈ ↑I
hst : f j ≠ f j
h_eq : i = j
⊢ False

Tactic:
exact hst rfl

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

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → (↑S).PairwiseDisjoint s → m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i)
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
hS : (↑S).PairwiseDisjoint s ∧ ∀ j ∈ ↑S, i ≠ j → Disjoint (s i) (s j)
⊢ m (s i ∪ ⋃ x ∈ ↑S, s x) = m (s i) + ∑ x ∈ S, m (s x)

Tactic:
rw [← h hs.2 hS.1]

Goal state after:
case insert
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → (↑S).PairwiseDisjoint s → m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i)
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
hS : (↑S).PairwiseDisjoint s ∧ ∀ j ∈ ↑S, i ≠ j → Disjoint (s i) (s j)
⊢ m (s i ∪ ⋃ x ∈ ↑S, s x) = m (s i) + m (⋃ i ∈ S, s i)
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
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
⊢ 1 < finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v)

Tactic:
rw [hrank]; omega

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M ↦ {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x ↦ ‖f x‖) μ
⊢ ∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε

Tactic:
have : Tendsto (fun n : ℕ ↦ ∫⁻ a, ENNReal.ofReal ‖{ x | n ≤ ‖f x‖₊ }.indicator f a - 0‖ ∂μ)
      atTop (𝓝 0) := by
    refine tendsto_lintegral_norm_of_dominated_convergence hmeas hbound ?_ htendsto
    refine fun n => univ_mem' (id fun x => ?_)
    by_cases hx : (n : ℝ) ≤ ‖f x‖
    · dsimp
      rwa [Set.indicator_of_mem]
    · dsimp
      rw [Set.indicator_of_notMem, norm_zero]
      · exact norm_nonneg _
      · assumption

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M ↦ {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x ↦ ‖f x‖) μ
this : Tendsto (fun n ↦ ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a - 0‖ ∂μ) atTop (𝓝 0)
⊢ ∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
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
inst✝ : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ HasSum (fun n ↦ v (t n)) (v (⋃ i, disjointed s i))

Tactic:
apply m_iUnion _ ht (disjoint_disjointed _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : MeasurableSpace β
x✝ : β
v✝ : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
⊢ HasSum (fun i ↦ if MeasurableSet (f i) ∧ x ∈ f i then v else 0)
    (if MeasurableSet (⋃ i, f i) ∧ x ∈ ⋃ i, f i then v else 0)

Tactic:
by
    by_cases hx : x ∈ ⋃ i, f i; swap
    · simp only [mem_iUnion, not_exists] at hx
      simp [hx, hasSum_zero]
    have : MeasurableSet (⋃ i, f i) := by
      apply MeasurableSet.iUnion f_meas
    simp only [f_meas, true_and, MeasurableSet.iUnion f_meas, hx, and_self, ↓reduceIte]
    obtain ⟨j, hj⟩ : ∃ j, x ∈ f j := by simpa using hx
    nth_rewrite 2 [show v = if x ∈ f j then v else 0 by simp [hj]]
    apply hasSum_single
    intro i hi
    have : Disjoint (f i) (f j) := f_disj hi
    grind

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

Goal state before:
pp: β : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : MeasurableSpace β
x : β
⊢ dirac x 0 = 0

Tactic:
ext s hs
  simp [dirac]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: α : 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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i ↦ p i ∧ 0 < r i
hq : ∀ {u : ℕ → Set α}, (∀ (i : ℕ), u i ≠ ∅ → 0 < r i) → blimsup u atTop p = blimsup u atTop q
⊢ blimsup (fun i ↦ thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ thickening (r i) (s i)) atTop p

Tactic:
hq fun i hi ↦ (thickening_nonempty_iff.1 <| nonempty_iff_ne_empty.2 hi).1,

Goal state after:
α : 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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i ↦ p i ∧ 0 < r i
hq : ∀ {u : ℕ → Set α}, (∀ (i : ℕ), u i ≠ ∅ → 0 < r i) → blimsup u atTop p = blimsup u atTop q
⊢ blimsup (fun i ↦ thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ thickening (r i) (s i)) atTop q
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
⊢ (v + w).map f = v.map f + w.map f

Tactic:
by
  by_cases hf : Measurable f
  · ext i hi
    simp [map_apply _ hf hi]
  · simp [map, dif_neg hf]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
⊢ -v ≪ᵥ w

Tactic:
intro s hs
  rw [neg_apply, h hs, neg_zero]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
hws : w (f ⁻¹' s) = 0
⊢ v (f ⁻¹' s) = 0

Tactic:
exact h hws

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

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

Tactic:
rintro ⟨u, hmeas, hu₁, hu₂⟩
    obtain ⟨i, hi₁, hi₂, hi₃, hipos, hineg⟩ := s.toJordanDecomposition_spec
    obtain ⟨j, hj₁, hj₂, hj₃, hjpos, hjneg⟩ := t.toJordanDecomposition_spec
    refine ⟨u, hmeas, ?_, ?_⟩
    · rw [totalVariation, Measure.add_apply, hipos, hineg, toMeasureOfZeroLE_apply _ _ _ hmeas,
        toMeasureOfLEZero_apply _ _ _ hmeas]
      simp [hu₁ _ Set.inter_subset_right]
    · rw [totalVariation, Measure.add_apply, hjpos, hjneg,
        toMeasureOfZeroLE_apply _ _ _ hmeas.compl,
        toMeasureOfLEZero_apply _ _ _ hmeas.compl]
      simp [hu₂ _ Set.inter_subset_right]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), s (B n) < -↑n
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
n : ℕ
⊢ s ((⋃ i, B i) \ B n) ≤ 0

Tactic:
have : s ≤[A] 0 := restrict_le_restrict_iUnion _ _ hmeas hr

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), s (B n) < -↑n
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
n : ℕ
this : s ≤[A] 0
⊢ s ((⋃ i, B i) \ B n) ≤ 0
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
⊢ μ.withDensityᵥ (-f) = -μ.withDensityᵥ f

Tactic:
ext1 i hi
    rw [_root_.neg_apply, withDensityᵥ_apply hf hi, ← integral_neg,
      withDensityᵥ_apply hf.neg hi]
    simp only [Pi.neg_apply]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
⊢ (μ.withDensityᵥ (f + g)) i = (μ.withDensityᵥ f + μ.withDensityᵥ g) i

Tactic:
rw [withDensityᵥ_apply (hf.add hg) hi, _root_.add_apply, withDensityᵥ_apply hf hi,
    withDensityᵥ_apply hg hi]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, (f + g) x ∂μ = ∫ (x : α) in i, f x ∂μ + ∫ (x : α) in i, g x ∂μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ s (i \ j ∪ j \ i) = 0

Tactic:
Set.sdiff_eq_compl_inter,

Goal state after:
case left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ s (jᶜ ∩ i ∪ j \ i) = 0