mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: case inl
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h : Finite k
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
cases finite_or_infinite V with
  | inr h =>
    have := not_iff_not.mpr (finite_iff_of_finite k V)
    push Not at this
    have : Infinite (ℙ k V) := by rwa [this]
    simp
  | inl h =>
  classical
  have : Fintype V := Fintype.ofFinite V
  have : Fintype (ℙ k V) := Fintype.ofFinite (ℙ k V)
  have : Fintype k := Fintype.ofFinite k
  have hV : Fintype.card { v : V // v ≠ 0 } = Fintype.card V - 1 := by simp
  simp_rw [← Fintype.card_eq_nat_card, ← Fintype.card_units (α := k), ← hV]
  rw [Fintype.card_congr (nonZeroEquivProjectivizationProdUnits k V), Fintype.card_prod]

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
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
A : SpecialLinearGroup R V
⊢ LinearEquiv.det (↑A).dualMap = 1

Tactic:
by
    simp only [← Units.val_inj, LinearEquiv.coe_det, Units.val_one,
      LinearEquiv.dualMap, LinearMap.det_dualMap]
    simp [← LinearEquiv.coe_det, A.prop]

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
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
⊢ centerEquivRootsOfUnity_invFun
      ((fun g ↦
          ⋯.by_cases (fun x ↦ 1) fun hR ↦
            ⋯.by_cases (fun x ↦ 1) fun hV ↦
              have hV := ⋯;
              have hr := ⋯;
              let r := ⋯.choose;
              have this := ⋯;
              ⟨this.unit, ⋯⟩)
        g) =
    g

Tactic:
by
    simp only [centerEquivRootsOfUnity_invFun, ← Subtype.val_inj,
      ← LinearEquiv.toLinearMap_inj, LinearMap.coe_equivOfIsUnitDet]
    simp only [Or.by_cases]
    split_ifs with hR hV
    · simp [Subsingleton.eq_one g]
    · simp [Subsingleton.eq_one g]
    · simp only [IsUnit.unit_spec, ← (mem_center_iff.mp g.prop).choose_spec.2]

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
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
⊢ False

Tactic:
have hki' : P.root k ≠ -P.root i := fun contra ↦ by
    replace h₁ : P.root l = 0 := by rwa [contra, neg_add_cancel, eq_comm] at h₁
    exact P.ne_zero _ 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
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
⊢ False
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✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ LieModule.IsTriangularizable R (↥(cartanSubalgebra' b)) (↥b.support ⊕ ι → R)

Tactic:
refine ⟨fun ⟨⟨x, hx'⟩, hx⟩ ↦ ?_⟩

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✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : ↥(cartanSubalgebra' b)
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx' : x ∈ lieAlgebra b
hx : ⟨x, hx'⟩ ∈ cartanSubalgebra' b
⊢ ⨆ φ, ((LieModule.toEnd R (↥(cartanSubalgebra' b)) (↥b.support ⊕ ι → R)) ⟨⟨x, hx'⟩, hx⟩).maxGenEigenspace φ = ⊤
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
ha : (a, a') ∈ S
hb : (b, b') ∈ S
hc : (c, c') ∈ S
hd : (d, d') ∈ S
he : (e, e') ∈ S
hf : (f, f') ∈ S
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
⊢ a = 0 ∧ b = 0

Tactic:
simp [S_def] at ha hb hc hd he hf
  omega

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

Goal state before:
pp: case inr.inr.inr.inl
ι : 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 : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
l : ι
hki : -↑i ≠ ↑i
⊢ ⁅e i, f i⁆ (Sum.inr (-↑i)) (Sum.inr l) = h i (Sum.inr (-↑i)) (Sum.inr l)

pp: case inr.inr.inr.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 : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k l : ι
hki : k ≠ ↑i
hki' : k ≠ -↑i
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)

Tactic:
· have hx (x : ι) : ¬ (P.root x = P.root l - P.root i ∧ P.root (-i) = P.root i + P.root x) := by
        rintro ⟨-, contra⟩
        refine P.nsmul_notMem_range_root (n := 2) (i := -i) ⟨x, ?_⟩
        replace contra : P.root x = -(P.root i + P.root i) := by
          simpa [neg_eq_iff_add_eq_zero, ← add_assoc, add_eq_zero_iff_eq_neg'] using contra
        simp [contra, two_smul]
      have aux (x : ι) : ¬ P.root (-i) = P.root x - P.root i := by
        simp [P.ne_zero x, eq_comm]
      simp only [e, f, h, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply, Fintype.sum_sum_type,
        Matrix.fromBlocks_apply₂₁, Matrix.of_apply, hki, reduceIte, zero_mul, Finset.sum_const_zero,
        Matrix.fromBlocks_apply₂₂, mul_ite, ite_mul, mul_zero, ← ite_and, if_neg (hx _), add_zero,
        aux, zero_sub, Matrix.diagonal_apply]
      rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by aesop)]
      simp [eq_comm, apply_ite ((-·) : R → R)]

Goal state after:
case inr.inr.inr.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 : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k l : ι
hki : k ≠ ↑i
hki' : k ≠ -↑i
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)
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 ((reflection ⋯) y)) ((reflection ⋯) y) ∣ 2 * (B ((reflection ⋯) y)) z

Tactic:
← hz,

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 ((reflection ⋯) y)) ((reflection ⋯) y) ∣ 2 * (B ((reflection ⋯) y)) ((reflection ⋯) ((reflection ⋯) z))
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case h₀
ι : 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
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j✝ j : ι
h : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, (∀ (k : ↥b.support), u k ∈ U) → v b j ∈ U
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
⊢ (∀ (k : ↥b.support), u k ∈ U) → v b ((P.reflectionPerm j) j) ∈ U

Tactic:
hU

Goal state after:
case h₀
ι : 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
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j✝ j : ι
h : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, (∀ (k : ↥b.support), u k ∈ U) → v b j ∈ U
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hU : ∀ (k : ↥b.support), u k ∈ U
⊢ v b ((P.reflectionPerm j) j) ∈ U
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
inst✝ : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular 2
x y : ↑{x | B.IsReflective x}
⊢ { toFun := fun x ↦ IsReflective.coroot B ⋯, inj' := ⋯ } y -
      ((Dual.eval R M) ((Embedding.subtype fun x ↦ B.IsReflective x) x))
          ({ toFun := fun x ↦ IsReflective.coroot B ⋯, inj' := ⋯ } y) •
        { toFun := fun x ↦ IsReflective.coroot B ⋯, inj' := ⋯ } x =
    { toFun := fun x ↦ IsReflective.coroot B ⋯, inj' := ⋯ }
      ({ toFun := fun y ↦ ⟨(Module.reflection ⋯) ↑y, ⋯⟩, invFun := fun y ↦ ⟨(Module.reflection ⋯) ↑y, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        y)

Tactic:
by
    simp only [coe_ofPred, mem_ofPred_eq, Embedding.coeFn_mk, Embedding.subtype_apply,
      Dual.eval_apply, Equiv.coe_fn_mk]
    ext z
    simp only [sub_apply, smul_apply, smul_eq_mul]
    refine y.2.1.1 ?_
    simp only [mem_ofPred_eq, mul_sub, apply_self_mul_coroot_apply B y.2, ← mul_assoc]
    rw [← isOrthogonal_reflection B x.2 hSB y y, apply_self_mul_coroot_apply, ← hSB.eq z,
      ← hSB.eq z, RingHom.id_apply, RingHom.id_apply, Module.reflection_apply, map_sub,
      mul_sub, sub_eq_sub_iff_comm, sub_left_inj]
    refine x.2.1.1 ?_
    simp only [mem_ofPred_eq, map_smul, smul_eq_mul]
    rw [← mul_assoc _ _ (B z x), ← mul_assoc _ _ (B z x), mul_left_comm,
      apply_self_mul_coroot_apply B x.2, mul_left_comm (B x x), apply_self_mul_coroot_apply B x.2,
      ← hSB.eq x y, RingHom.id_apply, ← hSB.eq x z, RingHom.id_apply]
    ring

Goal state after:
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Goal state before:
pp: case mul
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : SymmetricAlgebra R M → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (SymmetricAlgebra R M)) r)
ι : ∀ (x : M), motive ((SymmetricAlgebra.ι R M) x)
mul : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a * b)
add : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a + b)
x y : TensorAlgebra R M
hx : motive ((algHom R M) x)
hy : motive ((algHom R M) y)
⊢ motive ((algHom R M) x * (algHom R M) y)

Tactic:
exact mul _ _ hx hy

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
x : ↥((ι R).range ^ i)
⊢ ((lift R) (GradedAlgebra.ι R M)) ↑x = (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) x

Tactic:
obtain ⟨x, hx⟩ := x
    dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]
    induction hx using Submodule.pow_induction_on_left' with
    | algebraMap r =>
      rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
    | add x y i hx hy ihx ihy =>
      rw [map_add, ihx, ihy, ← map_add]
      rfl
    | mem_mul m hm i x hx ih =>
      obtain ⟨_, rfl⟩ := hm
      rw [map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.of_mul_of]
      exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)

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

Goal state before:
pp: case refine_2
ι : 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
⊢ f i ∈ t₂' i

Tactic:
by_cases hi₂ : i ∈ s₂
        · exact hf.2 i hi₂
        · rw [h2' i hi₂]
          exact mem_univ _

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

Goal state before:
pp: case a
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ (squareCylinders fun i ↦ {s | MeasurableSet s}) ⊆ {t | MeasurableSet t}

Tactic:
rintro S ⟨s, t, h, rfl⟩

Goal state after:
case a
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
t : (i : ι) → Set (α i)
h : t ∈ univ.pi fun i ↦ {s | MeasurableSet s}
⊢ (↑s).pi t ∈ {t | MeasurableSet t}
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.fixedReduce = 1
x✝ : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = x✝
⊢ e ∈ transvections K V ^ (x✝ - 1) * dilatransvections K V

Tactic:
induction h : finrank K (V ⧸ e.fixedSubmodule) generalizing e he with

Goal state after:
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
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion hs hI
h_disj : u = ∅
⊢ False

Tactic:
refine hC.empty_notMem_disjointOfDiffUnion hs hI ?_

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion hs hI
h_disj : u = ∅
⊢ ∅ ∈ hC.disjointOfDiffUnion hs hI
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case refine_3
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : ℕ → Set ι
t : (i : ℕ) → Set ((a : ↑(I i)) → α ↑a)
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).domRestrict ⁻¹' t i
x : (a : ι) → α a
⊢ x ∈ ⋃ i, f i ↔ x ∈ (⋃ n, I n).domRestrict ⁻¹' ⋃ n, (⋃ k, I k).domRestrict '' f n

Tactic:
simp only [hf, mem_iUnion, mem_preimage, preimage_iUnion, mem_image]

Goal state after:
case refine_3
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : ℕ → Set ι
t : (i : ℕ) → Set ((a : ↑(I i)) → α ↑a)
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).domRestrict ⁻¹' t i
x : (a : ι) → α a
⊢ (∃ i, (I i).domRestrict x ∈ t i) ↔
    ∃ i x_1, (I i).domRestrict x_1 ∈ t i ∧ (⋃ n, I n).domRestrict x_1 = (⋃ n, I n).domRestrict x
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
⊢ generateSetAlgebra 𝒜 ⊆ generateSetAlgebra ℬ

Tactic:
intro s hs

Goal state after:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s : Set α
hs : s ∈ generateSetAlgebra 𝒜
⊢ s ∈ generateSetAlgebra ℬ
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
⊢ generateSetAlgebra 𝒜 ⊆ ℬ

Tactic:
intro s hs

Goal state after:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s : Set α
hs : s ∈ generateSetAlgebra 𝒜
⊢ s ∈ ℬ
Module: Mathlib.MeasureTheory.Measure.AddContent

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

Tactic:
have h : ∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J :=
    ⟨J, hJ, h'J, hs⟩

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (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
⊢ Tendsto (fun n ↦ m ((partialSups f) n)) atTop (𝓝 (m (⨆ i, f i)))

Tactic:
← iSup_partialSups_eq

Goal state after:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (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
⊢ Tendsto (fun n ↦ m ((partialSups f) n)) atTop (𝓝 (m (⨆ i, (partialSups f) i)))
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (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
h_tendsto : Tendsto (fun n ↦ m ((partialSups f) n)) atTop (𝓝 (m (⋃ i, f i)))
h_tendsto' : Tendsto (fun n ↦ ∑ i ∈ Finset.range (n + 1), m (f i)) atTop (𝓝 (∑' (i : ℕ), m (f i)))
⊢ m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)

Tactic:
refine le_of_tendsto_of_tendsto' h_tendsto h_tendsto' fun _ ↦ ?_

Goal state after:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (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
h_tendsto : Tendsto (fun n ↦ m ((partialSups f) n)) atTop (𝓝 (m (⋃ i, f i)))
h_tendsto' : Tendsto (fun n ↦ ∑ i ∈ Finset.range (n + 1), m (f i)) atTop (𝓝 (∑' (i : ℕ), m (f i)))
x✝ : ℕ
⊢ m ((partialSups f) x✝) ≤ ∑ i ∈ Finset.range (x✝ + 1), m (f 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
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
x✝ : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = x✝
⊢ e ∈ transvections K V ^ (x✝ - 1) * dilatransvections K V

Tactic:
induction h : finrank K (V ⧸ e.fixedSubmodule) generalizing e he with

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_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)
hx : x ∈ ⋃ i, f i
this : MeasurableSet (⋃ i, f i)
j : ℕ
hj : x ∈ f j
i : ℕ
hi : i ≠ j
⊢ (if x ∈ f i then v else 0) = 0

Tactic:
have : Disjoint (f i) (f j) := f_disj hi

Goal state after:
case pos
α : 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)
hx : x ∈ ⋃ i, f i
this✝ : MeasurableSet (⋃ i, f i)
j : ℕ
hj : x ∈ f j
i : ℕ
hi : i ≠ j
this : Disjoint (f i) (f j)
⊢ (if x ∈ f i then v else 0) = 0
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:
restrict_apply v hi hj,

Goal state after:
α : 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 (j ∩ i) = v j
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ ENNReal.ofReal M ≠ 0

Tactic:
· simpa only [ENNReal.ofReal_eq_zero, not_le, Ne]

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
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : ¬Measurable f
⊢ (v + w).map f = v.map f + w.map f

Tactic:
simp [map, dif_neg hf]

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : ¬MeasurableSet i
⊢ v i ≤ w i

Tactic:
rw [v.not_measurable hi, w.not_measurable hi]

Goal state after: