mathlib-initiative/mathlib-tactics huggingface dataset:
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
hSB : B.IsSymm
y : M
⊢ ∀ (y_1 : M), (B ((reflection ⋯) y)) ((reflection ⋯) y_1) = (B y) y_1

Tactic:
z

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
hSB : B.IsSymm
y z : M
⊢ (B ((reflection ⋯) y)) ((reflection ⋯) z) = (B y) 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 : ι
⊢ (∀ {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:
h

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)},
    (∀ (k : ↥b.support), u k ∈ U) → v b ((P.reflectionPerm j) j) ∈ U
Module: Mathlib.LinearAlgebra.SModEq.Pow

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
⊢ x ^ p - y ^ p ∈ J * I

Tactic:
rw [← Commute.mul_neg_geom_sum₂ (.all _ _)]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
⊢ (x - y) * ∑ i ∈ Finset.range p, y ^ i * x ^ (p - 1 - i) ∈ J * I
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
h : ∀ (i j : ι), star ((B (b i)) (b j)) = (B (b j)) (b i)
x y : M
fx : M → R
tx : Finset M
ix : ↑tx ⊆ Set.range ⇑b
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : ↑ty ⊆ Set.range ⇑b
hy : ∑ a ∈ ty, fy a • a = y
i : ι
h₁ : b i ∈ tx
j : ι
h₂ : b j ∈ ty
⊢ fx (b i) * (star (fy (b j)) * star ((B (b i)) (b j))) = fx (b i) * (star (fy (b j)) * (B (b j)) (b i))

Tactic:
h

Goal state after:
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
h : ∀ (i j : ι), star ((B (b i)) (b j)) = (B (b j)) (b i)
x y : M
fx : M → R
tx : Finset M
ix : ↑tx ⊆ Set.range ⇑b
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : ↑ty ⊆ Set.range ⇑b
hy : ∑ a ∈ ty, fy a • a = y
i : ι
h₁ : b i ∈ tx
j : ι
h₂ : b j ∈ ty
⊢ fx (b i) * (star (fy (b j)) * (B (b j)) (b i)) = fx (b i) * (star (fy (b j)) * (B (b j)) (b i))
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Goal state before:
pp: case algebraMap
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)
r : R
⊢ motive ((algHom R M) ((Algebra.algebraMap R (TensorAlgebra R M)) r))

Tactic:
| algebraMap r =>

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

Goal state before:
pp: case algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : SymmetricAlgebra R M
r : R
⊢ Commute a ((algebraMap R (SymmetricAlgebra R M)) r)

Tactic:
| algebraMap r =>

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

Goal state before:
pp: case ι.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
⊢ Commute ((algebraMap R (SymmetricAlgebra R M)) r) ((ι R M) x)

Tactic:
| algebraMap r =>

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

Goal state before:
pp: case algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
x : TensorAlgebra R M
r : R
⊢ ((lift R) (GradedAlgebra.ι R M)) ((algebraMap R (TensorAlgebra R M)) r) =
    (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) 0) ⟨(algebraMap R (TensorAlgebra R M)) r, ⋯⟩

Tactic:
| algebraMap r =>

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

Goal state before:
pp: case algebraMap
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
h : IsSymmetricAlgebra f
motive : A → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A) r)
ι : ∀ (x : M), motive (f x)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
add : ∀ (a b : A), motive a → motive b → motive (a + b)
a : A
r : R
⊢ motive ((SymmetricAlgebra.lift f) ((Algebra.algebraMap R (SymmetricAlgebra R M)) r))

Tactic:
| algebraMap r =>

Goal state after:
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y : ⨂[R] (x : ι), M
h : (addConGen (Rel R ι M)) x y
⊢ (addConGen (Rel R ι M)) (r • x) (r • y)

Tactic:
induction h with

Goal state after:
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:
by
  simp_rw [CutExpand, add_singleton_eq_iff]
  refine exists₂_congr fun t a ↦ ⟨?_, ?_⟩
  · rintro ⟨ht, ha, rfl⟩
    obtain h | h := mem_add.1 ha
    exacts [⟨ht, h, erase_add_left_pos t h⟩, (@irrefl α r _ a (ht a h)).elim]
  · rintro ⟨ht, h, rfl⟩
    exact ⟨ht, mem_add.2 (Or.inl h), (erase_add_left_pos t h).symm⟩

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 f : V ≃ₗ[K] V
hf : f ∈ dilatransvections K V
⊢ finrank K ↥(↑e).fixedSubmodule ≤ 1 + finrank K ↥(↑(f * e)).fixedSubmodule

Tactic:
by
  have := finrank_fixedSubmodule_add_le f e
  have := finrank_le_one_add_finrank_fixedSubmodule_dilatransvection f hf
  have : finrank K ↥(f.fixedSubmodule ⊔ e.fixedSubmodule) ≤ finrank K V :=
    finrank_le _
  linarith

Goal state after:
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case inr
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a

Tactic:
refine ⟨(s₁, (s₂ + t).erase a), GameAdd.snd ⟨t, a, hr, ?_⟩, ?_⟩
    · rw [add_comm, singleton_add, cons_erase h]
    · rw [add_assoc, erase_add_right_pos _ h]

Goal state after:
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
⊢ (↑s₁).pi t₁ ∩ (↑s₂).pi t₂ ∈ squareCylinders C

Tactic:
have h1' : ∀ i ∉ (s₁ : Set ι), t₁' i = univ :=
    fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi

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
⊢ (↑s₁).pi t₁ ∩ (↑s₂).pi t₂ ∈ squareCylinders C
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
⊢ eval i ⁻¹' t = S → ∃ x, (∀ (i : ι), MeasurableSet (x i)) ∧ eval i ⁻¹' x i = S

Tactic:
h

Goal state after:
ι : 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
⊢ ∃ x, (∀ (i : ι), MeasurableSet (x i)) ∧ eval i ⁻¹' x i = S
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case refine_2.h
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 := auxTransvection ⋯
ht : t = auxTransvection ⋯
⊢ finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 + 1

Tactic:
h

Goal state after:
case refine_2.h
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 := auxTransvection ⋯
ht : t = auxTransvection ⋯
⊢ n + 2 = n + 1 + 1
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
h : S = ∅
⊢ cylinder s S = ∅

Tactic:
h

Goal state after:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
h : S = ∅
⊢ cylinder s ∅ = ∅
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α ↑i := hS.some
hf : f ∈ S
f' : (i : ι) → α i := fun i ↦ if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
hf' : f' ∈ cylinder s S
⊢ False

Tactic:
h

Goal state after:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α ↑i := hS.some
hf : f ∈ S
f' : (i : ι) → α i := fun i ↦ if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
hf' : f' ∈ ∅
⊢ False
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
⊢ (∃ 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

Tactic:
refine ⟨fun ⟨i, hi⟩ ↦ ⟨i, x, hi, rfl⟩, fun ⟨n, x', hn, hx⟩ ↦ ⟨n, ?_⟩⟩

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
x✝ : ∃ i x_1, (I i).domRestrict x_1 ∈ t i ∧ (⋃ n, I n).domRestrict x_1 = (⋃ n, I n).domRestrict x
n : ℕ
x' : (a : ι) → α a
hn : (I n).domRestrict x' ∈ t n
hx : (⋃ n, I n).domRestrict x' = (⋃ n, I n).domRestrict x
⊢ (I n).domRestrict x ∈ t n
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
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
⊢ m (⋃ i ∈ a, f i) = ∑ i ∈ a, m (f i)

Tactic:
have A : ⋃ i ∈ a, f i = ⋃₀ (a.image f) := by simp
  rw [A, addContent_sUnion]; rotate_left
  · grind
  · simpa using! h_dis.image
  · rwa [← A]
  rw [sum_image_of_pairwise_eq_zero]
  refine h_dis.imp ?_
  grind [Set.bot_eq_empty (α := α), addContent_empty]

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

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

Tactic:
· rwa [hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]

Goal state after:
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case union.refine_2.inl
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Au
t : Set α
ht : t ∈ a
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

pp: case union.refine_2.inr
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Av
t : Set α
ht : t ∈ a
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

Tactic:
· exact hAu a ha t ht

Goal state after:
case union.refine_2.inr
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Av
t : Set α
ht : t ∈ a
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
Module: Mathlib.MeasureTheory.Measure.AddContent

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

Tactic:
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'
t : Set α
ht : t ∈ J'
⊢ t ⊆ ⋃₀ ↑J'
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
⊢ extend (fun x x_1 ↦ m x) ∅ = 0

Tactic:
rw [extend_eq, addContent_empty]

Goal state after:
case h
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
⊢ ∅ ∈ C
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case pos
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
⊢ ∃ x ∈ transvections K V, ∃ y ∈ transvections K V ^ n * dilatransvections K V, x * y = e

Tactic:
refine ⟨(auxTransvection hf)⁻¹, ?_, auxTransvection hf * e, he', by simp⟩

Goal state after:
case pos
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
⊢ (auxTransvection hf)⁻¹ ∈ transvections K V
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, m s ≠ ∞
hm_tendsto : ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n ↦ m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n ↦ (⋃ i, f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
⊢ Tendsto (fun n ↦ m (s n)) atTop (𝓝 0)

Tactic:
refine hm_tendsto hCs ?_ ?_

Goal state after:
case refine_1
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, m s ≠ ∞
hm_tendsto : ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n ↦ m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n ↦ (⋃ i, f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
⊢ Antitone s

case refine_2
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, m s ≠ ∞
hm_tendsto : ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n ↦ m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n ↦ (⋃ i, f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
⊢ ⋂ n, s n = ∅
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_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h : ∀ (n : ℕ), m (f n) = ∑ i ∈ Finset.range (n + 1), m (disjointed f i)
⊢ Tendsto (fun n ↦ m (f n)) atTop (𝓝 (∑' (i : ℕ), m (disjointed f i)))

Tactic:
h

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_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h : ∀ (n : ℕ), m (f n) = ∑ i ∈ Finset.range (n + 1), m (disjointed f i)
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range (n + 1), m (disjointed f i)) atTop (𝓝 (∑' (i : ℕ), m (disjointed f i)))
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
⊢ μ.toSignedMeasure i = ν.toSignedMeasure i

Tactic:
h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
⊢ ν.toSignedMeasure i = ν.toSignedMeasure i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
⊢ n ≠ m → (Disjoint on s.restrictNonposSeq i) n m

Tactic:
h

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n ≠ m
⊢ (Disjoint on s.restrictNonposSeq i) n m
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case posPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.posPart = j₂.posPart

Tactic:
exact hj

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : j₁.posPart.real i = j₁.toSignedMeasure (i ∩ Sᶜ)
⊢ j₂.posPart.real i = j₂.posPart.real (i ∩ Tᶜ) - (j₂.negPart (i ∩ Tᶜ)).toReal

Tactic:
show j₂.negPart (i ∩ Tᶜ) = 0 from
        nonpos_iff_eq_zero.1 (hT₅ ▸ measure_mono Set.inter_subset_right),

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : j₁.posPart.real i = j₁.toSignedMeasure (i ∩ Sᶜ)
⊢ j₂.posPart.real i = j₂.posPart.real (i ∩ Tᶜ) - ENNReal.toReal 0