mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (allRoots P).Nodup

Tactic:
have hli : Injective (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) := by
    rw [← linearIndependent_iff_injective_fintypeLinearCombination]
    exact (linearIndependent_short_long P).restrict_scalars' ℤ

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
hli : Injective ⇑(Fintype.linearCombination ℤ ![shortRoot P, longRoot P])
⊢ (allRoots P).Nodup
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
inst✝ : P.IsIrreducible
this : P.pairing (long P) (short P) = -3
⊢ LinearIndependent R ![shortRoot P, longRoot P]

Tactic:
refine (IsReduced.linearIndependent_iff P).mpr ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
ι : 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
inst✝ : P.IsIrreducible
this : P.pairing (long P) (short P) = -3
h : short P = long P
⊢ False

case refine_2
ι : 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
inst✝ : P.IsIrreducible
this : P.pairing (long P) (short P) = -3
h : P.root (short P) = -P.root (long P)
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : 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 k : ↥b.support
l : ι
this : InvolutiveNeg ι := P.indexNeg
hl : P.root ↑j = P.root ↑i + P.root l
⊢ P.root (-l) = P.root ↑i - P.root ↑j

Tactic:
simp [hl]

Goal state after:
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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
hw : w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
⊢ ∃ d,
    (∀ (i : ι), d i ≠ 0) ∧
      Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d) ∧ diagonal (0 ⊕ᵥ d) ∈ { toSubmodule := span K (range h), lie_mem' := ⋯ }

Tactic:
LieSubalgebra.mem_mk_iff',

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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
hw : w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
⊢ ∃ d, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d) ∧ diagonal (0 ⊕ᵥ d) ∈ span K (range h)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : 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 k : ↥b.support
l : ι
this : InvolutiveNeg ι := P.indexNeg
aux₁ : ∀ x ∈ Finset.univ, ¬(P.root x = P.root ↑i + P.root l ∧ k = j ∧ x = ↑j)
hl : P.root ↑i = P.root ↑j - P.root l
⊢ P.root (-l) = P.root ↑i - P.root ↑j

Tactic:
simp [hl]

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

Goal state before:
pp: case regular
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
⊢ IsRegular ((B ((reflection ⋯) y)) ((reflection ⋯) y))

Tactic:
isOrthogonal_reflection B hx hSB

Goal state after:
case regular
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
⊢ IsRegular ((B y) y)
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
z : M
hz : (reflection ⋯) ((reflection ⋯) z) = z
⊢ (B y) y ∣ 2 * (B ((reflection ⋯) y)) ((reflection ⋯) ((reflection ⋯) z))

Tactic:
isOrthogonal_reflection B hx hSB

Goal state after:
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
z : M
hz : (reflection ⋯) ((reflection ⋯) z) = z
⊢ (B y) y ∣ 2 * (B y) ((reflection ⋯) z)
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.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
aux : ∀ (k : ↥b.support), u k ∈ U
this : ∀ (j : ι), v b j ∈ U
⊢ ∀ (y : ↥b.support ⊕ ι), (Pi.basisFun K (↥b.support ⊕ ι)) y ∈ ↑↑U

Tactic:
Pi.basisFun_apply

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.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
aux : ∀ (k : ↥b.support), u k ∈ U
this : ∀ (j : ι), v b j ∈ U
⊢ ∀ (y : ↥b.support ⊕ ι), Pi.single y 1 ∈ ↑↑U
Module: Mathlib.LinearAlgebra.SesquilinearForm.Star

Goal state before:
pp: R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Fintype n
inst✝ : DecidableEq n
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
⊢ (∀ (i j : n), star ((B (b i)) (b j)) = (B (b j)) (b i)) ↔ ((toMatrix₂ b b) B).IsHermitian

Tactic:
Matrix.IsHermitian.ext_iff,

Goal state after:
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Fintype n
inst✝ : DecidableEq n
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
⊢ (∀ (i j : n), star ((B (b i)) (b j)) = (B (b j)) (b i)) ↔
    ∀ (i j : n), star ((toMatrix₂ b b) B j i) = (toMatrix₂ b b) B i j
Module: Mathlib.MeasureTheory.Category.MeasCat

Goal state before:
pp: μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ ∫⁻ (x : ℝ≥0∞), x ∂μ.join = ∫⁻ (x : ℝ≥0∞), x ∂Measure.map (fun m ↦ ∫⁻ (x : ℝ≥0∞), x ∂m) μ

Tactic:
rw [Measure.lintegral_join, lintegral_map]

Goal state after:
case hf
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ Measurable fun x ↦ x

case hg
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ Measurable fun m ↦ ∫⁻ (x : ℝ≥0∞), x ∂m

μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ AEMeasurable (fun x ↦ x) μ.join
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
W : Submodule K V
v : V
hv : v ∉ W
⊢ finrank K (V ⧸ W ⊔ K ∙ v) + 1 = finrank K (V ⧸ W)

Tactic:
have h1 := finrank_quotient_add_finrank (W ⊔ K ∙ v)

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
W : Submodule K V
v : V
hv : v ∉ W
h1 : finrank K (V ⧸ W ⊔ K ∙ v) + finrank K ↥(W ⊔ K ∙ v) = finrank K V
⊢ finrank K (V ⧸ W ⊔ K ∙ v) + 1 = finrank K (V ⧸ W)
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 : e.fixedReduce = 1
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
f : Dual K V
v : V
hf : (↑e).fixedSubmodule ≤ ker f
hv : f v = 1
hv' : v ∈ (↑e).fixedSubmodule
⊢ 1 = 0

Tactic:
rw [← hv, ← LinearMap.mem_ker]

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
n✝ : ℕ
e : V ≃ₗ[K] V
he : e.fixedReduce = 1
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
f : Dual K V
v : V
hf : (↑e).fixedSubmodule ≤ ker f
hv : f v = 1
hv' : v ∈ (↑e).fixedSubmodule
⊢ v ∈ ker f
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)
μ ν : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
this : IsFiniteMeasure μ
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders α
⊢ (P I) S = ν (cylinder I S)

Tactic:
hν.measure_cylinder _ hS

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ ν : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
this : IsFiniteMeasure μ
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders α
⊢ (P I) S = (P I) S
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case refine_2.he
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 : e.fixedReduce = 1
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
f : Dual K V
v : V
hf : (↑e).fixedSubmodule ≤ ker f
hv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hv' : v - e v ∈ (↑e).fixedSubmodule
t : V ≃ₗ[K] V := ⋯
ht : t = auxTransvection ⋯
⊢ (t * e).fixedReduce = 1

Tactic:
simp only [ht, one_eq_refl, fixedReduce_eq_one, auxTransvection_mul_fixed hv] at he ⊢
        intro w
        simp only [auxTransvection, LinearEquiv.mul_apply, transvection.apply,
          add_sub_right_comm]
        apply mem_sup_left
        apply Submodule.add_mem _ (he w)
        exact smul_mem _ _ hv'

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : j = i
⊢ Set (α j)

Tactic:
by convert! t

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case refine_2
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : ↑I ⊆ C
hI : (↑I).PairwiseDisjoint id
hst : s \ t = ⋃₀ ↑I
⊢ ↑(Finpartition.ofErase I ⋯ ⋯).parts ⊆ C

Tactic:
grw [Finpartition.ofErase_parts, Finset.erase_subset, hIC]

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ MeasurableSet (Finset.restrict₂ ⋯ ⁻¹' S₁ ∩ {f | Finset.restrict₂ ⋯ f ∈ S₂})

pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ cylinder s₁ S₁ ∩ cylinder s₂ S₂ = cylinder (s₁ ∪ s₂) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∩ {f | Finset.restrict₂ ⋯ f ∈ S₂})

Tactic:
· refine MeasurableSet.inter ?_ ?_
    · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _) hS₁
    · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _) hS₂

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ cylinder s₁ S₁ ∩ cylinder s₂ S₂ = cylinder (s₁ ∪ s₂) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∩ {f | Finset.restrict₂ ⋯ f ∈ S₂})
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)
⊢ ∃ 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:
have : ∃ v, LinearIndependent K ![v, e.fixedReduce v] := by
    contrapose! he
    obtain ⟨a, ha⟩ :=
      LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent h.ne' he
    refine ⟨a, fun x ↦ by
      simp only [← coe_toLinearMap, ha, LinearMap.smul_apply, one_apply, Subring.smul_def]⟩
  obtain ⟨v, hu⟩ := this
  -- We lift `v` to `u : V`.
  obtain ⟨u, rfl⟩ := e.fixedSubmodule.mkQ_surjective v
  -- We can take `f : Dual K V` which vanishes on `e.fixedSubmodule ⊔ K ∙ (e u - u)`
  -- and satisfies `f u ≠ 0`, and we rescale `u` to `v` so that `f v = 1`.
  obtain ⟨f, hfu, hf⟩ :=
    exists_dual_map_eq_bot_of_notMem (apply_notMem_sup_of_linearIndependent hu) inferInstance
  replace hfu : f u ≠ 0 := by
    contrapose hfu
    rw [← hfu, ← sub_eq_zero, ← map_sub, ← Submodule.mem_bot K, ← hf]
    exact mem_map_of_mem (mem_sup_right (mem_span_singleton_self _))
  set v := (f u)⁻¹ • u with v_def
  have hspan : K ∙ (e v - v) = K ∙ (e u - u) := by
    simp only [Submodule.span_singleton_eq_span_singleton]
    use (Ne.isUnit hfu).unit
    simp [v_def, _root_.map_smul, Units.smul_isUnit, smul_sub,
      ← mul_smul, mul_inv_cancel₀ hfu]
  rw [← hspan, ← le_ker_iff_map] at hf
  refine ⟨f, v, ?_, hf,
    by simp only [_root_.map_smul, smul_eq_mul, v_def, inv_mul_cancel₀ hfu]⟩
  rw [← LinearIndependent.pair_smul_smul_iff (Ne.isUnit hfu).inv (Ne.isUnit hfu).inv] at hu
  simpa only [← LinearMap.map_smul, ← LinearEquiv.map_smul, ← v_def] using hu

Goal state after:
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
⊢ generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} ≤ instWithTopOfOrderTopology

Tactic:
let basis : Set (Set ι) := {s | ∃ (f g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite
      ∧ s = (⋂ a ∈ f, Ioi a) ∩ (⋂ a ∈ g, Iio a)}

Goal state after:
case a
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
⊢ generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} ≤ instWithTopOfOrderTopology
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inl.coe.top.inr.refine_1
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a : ι
hb✝ : ⊤ ∈ Ioi ↑a
ha : (Ioi a).Nonempty
b : ι
bc' : b ∈ c'
hb : b ∈ Ioi a
⊢ ↑a ≤ ↑b

Tactic:
simpa using hb.le

Goal state after:
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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
| m t

Tactic:
rw [← hC.sUnion_insert_disjointOfDiff ht hs hst]

Goal state after:
α : 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
| m (⋃₀ insert s ↑(hC.disjointOfDiff ht hs))
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case inr
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
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c ≠ 0
x : V
a✝ : x ∈ ⊤
h1 : g (e x) • (v - e v) ∈ K ∙ (e v - v)
hle : (↑e).fixedSubmodule ⊔ K ∙ v ≤ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v
⊢ x ∈ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v

Tactic:
have h2 : c • x ∈ e.fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v := by
      rw [show c • x = g (e x) • (v - e v) - (g (e x) • (v - e v) - c • x) by abel]
      exact Submodule.sub_mem _ (mem_sup_left (mem_sup_right h1)) (hle (key x))

Goal state after:
case inr
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
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c ≠ 0
x : V
a✝ : x ∈ ⊤
h1 : g (e x) • (v - e v) ∈ K ∙ (e v - v)
hle : (↑e).fixedSubmodule ⊔ K ∙ v ≤ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v
h2 : c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v
⊢ x ∈ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x ↦ ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
⊢ M ^ (1 / p.toReal) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ p.toReal‖₊

Tactic:
rw [coe_nnnorm, coe_nnnorm, Real.norm_rpow_of_nonneg (norm_nonneg _), norm_norm,
      ← Real.rpow_le_rpow_iff hM' (by positivity)
        (one_div_pos.2 <| ENNReal.toReal_pos hp_ne_zero hp_ne_top), ← Real.rpow_mul (norm_nonneg _),
      mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm, Real.rpow_one]

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

Goal state before:
pp: case mpr
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : μ i = 0
⊢ ↑(c i).re + ↑(c i).im * Complex.I = 0

Tactic:
(_ : (c i).re = 0),

Goal state after:
case mpr
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : μ i = 0
⊢ ↑0 + ↑(c i).im * Complex.I = 0

α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : μ i = 0
⊢ (c i).re = 0
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
v : VectorMeasure α M
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (v.map f) s = v (f ⁻¹' s)

Tactic:
by
  rw [map, dif_pos hf]
  exact if_pos hs

Goal state after:
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
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (v.restrict t).restrict s = v.restrict (s ∩ t)

Tactic:
ext u hu

Goal state after:
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
hu : MeasurableSet u
⊢ ((v.restrict t).restrict s) u = (v.restrict (s ∩ t)) u