mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case e'_3
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
e : (ι → R) ≃+ M := ↑bM.equivFun.symm
he : e = ↑bM.equivFun.symm
e' : (ι → R) →+ M := ↑e
he' : Function.Surjective ⇑e'
e_2✝ : Pi.addCommGroup.toAddGroup = Pi.addGroup
⊢ N'.toAddSubgroup = AddSubgroup.map (↑(↑bM.equivFun.symm).symm) N.toAddSubgroup

Tactic:
hN',

Goal state after:
case e'_3
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
e : (ι → R) ≃+ M := ↑bM.equivFun.symm
he : e = ↑bM.equivFun.symm
e' : (ι → R) →+ M := ↑e
he' : Function.Surjective ⇑e'
e_2✝ : Pi.addCommGroup.toAddGroup = Pi.addGroup
⊢ (Submodule.map (↑bM.equivFun) N).toAddSubgroup = AddSubgroup.map (↑(↑bM.equivFun.symm).symm) N.toAddSubgroup
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: case refine_2
G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
⊢ Surjective ⇑(AddMonoidHom.toZModLinearMap n g.toAddMonoidHom)

Tactic:
· suffices mod ∘ b.repr = g ∘ nG.mkQ by
      exact (this ▸ (mapRange_surjective _ (map_zero _) ZMod.intCast_surjective).comp
        b.repr.surjective).of_comp
    ext x b
    simp [mod, g, f, H]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
⊢ ∀ (B : FixedDetMatrix (Fin 2) ℤ m) (n : ℤ), C (T ^ n • B) ↔ C B

Tactic:
intro B n
  induction n with
  | zero => simp only [zpow_zero, one_smul]
  | succ n hn =>
    simpa only [add_comm (n : ℤ), zpow_add _ 1, ← smul_eq_mul, zpow_one, smul_assoc,
      prop_red_T hS hT]
  | pred m hm =>
    rwa [sub_eq_neg_add, zpow_add, zpow_neg_one, ← prop_red_T hS hT, mul_smul, smul_inv_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Swap

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : Zero R
inst✝¹ : One R
inst✝ : DecidableEq n
i j : n
⊢ (swap R i j)ᵀ = swap R i j

Tactic:
simp [swap]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Swap

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
R : Type u_3
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
i j : n
⊢ (swap R i j)ᴴ = swap R i j

Tactic:
simp [swap]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Swap

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
S : Type u_4
inst✝ : NonAssocSemiring S
f : R →+* S
i j : n
⊢ (swap R i j).map ⇑f = swap S i j

Tactic:
simp [swap]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Swap

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
S : Type u_3
inst✝ : CommRing S
f : R →+* S
i j : n
⊢ ↑((map f) (swap R i j)) = ↑(swap S i j)

Tactic:
simp [swap]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a : R
⊢ ∀ (b : R), A.IsDetpBalanced a b → a = b

Tactic:
b

Goal state after:
R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
⊢ A.IsDetpBalanced a b → a = b
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
w : V
hw : w ≠ 0
h : LinearIndependent K ![v, w]
⊢ IsCollinear {mk K v hv, mk K w hw}

Tactic:
refine ⟨(Submodule.span K {v, w}).projectivization, ?_, ?_, fun s hs ↦ hs.casesOn ?_ ?_⟩

Goal state after:
case h.h.refine_1
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
w : V
hw : w ≠ 0
h : LinearIndependent K ![v, w]
⊢ Module.Finite K ↥(Subspace.submodule (Submodule.projectivization (Submodule.span K {v, w})))

case h.h.refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
w : V
hw : w ≠ 0
h : LinearIndependent K ![v, w]
⊢ Module.finrank K ↥(Subspace.submodule (Submodule.projectivization (Submodule.span K {v, w}))) ≤ 2

case h.h.refine_3
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
w : V
hw : w ≠ 0
h : LinearIndependent K ![v, w]
s : ℙ K V
hs : s ∈ {mk K v hv, mk K w hw}
⊢ s = mk K v hv → s ∈ ↑(Submodule.projectivization (Submodule.span K {v, w}))

case h.h.refine_4
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
w : V
hw : w ≠ 0
h : LinearIndependent K ![v, w]
s : ℙ K V
hs : s ∈ {mk K v hv, mk K w hw}
⊢ s ∈ {mk K w hw} → s ∈ ↑(Submodule.projectivization (Submodule.span K {v, w}))
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
i j : ι
⊢ ((Q.toBilin bm) (bm i)) (bm j) = if i = j then Q (bm i) else if i < j then polar (⇑Q) (bm i) (bm j) else 0

Tactic:
simp [toBilin]

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

Goal state before:
pp: case inl.inr
ι : 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✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
l : ι
⊢ (ω b * e i) (Sum.inl k) (Sum.inr l) = (f i * ω b) (Sum.inl k) (Sum.inr l)

pp: case inr.inl
ι : 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✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k : ι
l : ↥b.support
⊢ (ω b * e i) (Sum.inr k) (Sum.inl l) = (f i * ω b) (Sum.inr k) (Sum.inl l)

pp: case inr.inr
ι : 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✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k l : ι
⊢ (ω b * e i) (Sum.inr k) (Sum.inr l) = (f i * ω b) (Sum.inr k) (Sum.inr l)

Tactic:
· simp only [ω, e, f, mul_ite, mul_zero, Fintype.sum_sum_type, Matrix.mul_apply, Matrix.of_apply,
      Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Finset.sum_ite_eq']
    rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by simp_all)]
    simp [← ite_and, and_comm, -indexNeg_neg, neg_eq_iff_eq_neg]

Goal state after:
case inr.inl
ι : 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✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k : ι
l : ↥b.support
⊢ (ω b * e i) (Sum.inr k) (Sum.inl l) = (f i * ω b) (Sum.inr k) (Sum.inl l)

case inr.inr
ι : 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✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k l : ι
⊢ (ω b * e i) (Sum.inr k) (Sum.inr l) = (f i * ω b) (Sum.inr k) (Sum.inr l)
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 ι
i j : ↥b.support
⊢ ⁅e i, u j⁆ = |b.cartanMatrix i j| • v b ↑i

Tactic:
by
  ext (k | k) <;> simp [e, Pi.single_apply]

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

Goal state before:
pp: case mem
ι : 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 u : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hu : u ∈ range h ∪ range e ∪ range f
⊢ (ωConj b) u ∈ lieAlgebra b

Tactic:
obtain (⟨i, rfl⟩ | ⟨i, rfl⟩ | ⟨i, rfl⟩) : (∃ j, h j = u) ∨ (∃ j, e j = u) ∨ (∃ j, f j = u) := by
      simpa only [mem_union, mem_range, or_assoc] using hu
    · rw [← neg_mem_iff]
      exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_h, mul_assoc]
    · exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_e, mul_assoc]
    · exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_f, mul_assoc]

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

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ↥b.support
⊢ ∃ n, (e i ^ n).col (Sum.inl j) = 0

Tactic:
exact ⟨2, case_inl j⟩

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_4
ι : 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
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P) =
    (2 * P.pairing i (short P) + 3 * P.pairing i (long P)) * (B.form (twoShortAddLongRoot P)) (twoShortAddLongRoot P)

Tactic:
rw [long_eq_three_mul_short, twoShortAddLongRoot_shortRoot]

Goal state after:
case calc_4
ι : 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
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (3 * (B.form (shortRoot P)) (shortRoot P)) =
    (2 * P.pairing i (short P) + 3 * P.pairing i (long P)) * (B.form (shortRoot P)) (shortRoot P)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inl.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
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
x : ι
hx : P.root k = P.root ↑i + P.root x
h₂ : ∀ (a : ι), ¬P.root k = P.root a - P.root ↑i
⊢ (∑ x, if P.root k = P.root ↑i + P.root x then (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑i) k) + 1) else 0) =
    ↑(chainBotCoeff (↑i) k) - ↑(chainTopCoeff (↑i) k)

Tactic:
replace h₂ : P.chainTopCoeff i k = 0 :=
      P.chainTopCoeff_eq_zero_iff.mpr <| Or.inr fun ⟨x, hx⟩ ↦ h₂ x <| by simp [hx]

Goal state after:
case inl.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
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
x : ι
hx : P.root k = P.root ↑i + P.root x
h₂ : chainTopCoeff (↑i) k = 0
⊢ (∑ x, if P.root k = P.root ↑i + P.root x then (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑i) k) + 1) else 0) =
    ↑(chainBotCoeff (↑i) k) - ↑(chainTopCoeff (↑i) k)
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.IsG2
b : P.Base
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
_i✝ : P.EmbeddedG2
_i : Nonempty ι
⊢ b.support.card = Module.finrank R M

Tactic:
Module.finrank_eq_card_basis b.toWeightBasis,

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.IsG2
b : P.Base
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
_i✝ : P.EmbeddedG2
_i : Nonempty ι
⊢ b.support.card = Fintype.card ↥b.support
Module: Mathlib.Logic.Hydra

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

Tactic:
classical
  obtain ⟨ha, rfl⟩ := add_singleton_eq_iff.1 he
  rw [add_assoc, mem_add] at ha
  obtain h | h := ha
  · refine ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, ?_⟩, ?_⟩
    · rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
    · rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]
  · 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.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ (insert t ↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id

Tactic:
by
  have h := hC.pairwiseDisjoint_disjointOfDiff hs ht
  refine PairwiseDisjoint.insert_of_notMem h (hC.notMem_disjointOfDiff hs ht) fun u hu ↦ ?_
  simp_rw [id]
  refine Disjoint.mono_right ?_ (hC.disjoint_sUnion_disjointOfDiff hs ht)
  exact subset_sUnion_of_mem hu

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
a : Set α
ha : a ∈ ↑{Set.Ioc u u', Set.Ioc v' v}
⊢ ∀ ⦃y : Set α⦄, y ∈ ↑{Set.Ioc u u', Set.Ioc v' v} → a ≠ y → Function.onFun Disjoint id a y

Tactic:
b

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
a : Set α
ha : a ∈ ↑{Set.Ioc u u', Set.Ioc v' v}
b : Set α
⊢ b ∈ ↑{Set.Ioc u u', Set.Ioc v' v} → a ≠ b → Function.onFun Disjoint id a b
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
h : ∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s = ⋃₀ ↑J
⊢ ∑ s ∈ ⋯.choose, m s = ∑ s ∈ J, m s

Tactic:
apply sum_addContent_eq_of_sUnion_eq hC _ _ h.choose_spec.1 h.choose_spec.2.1 hJ h'J

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
⊢ ⋃₀ ↑h.choose = ⋃₀ ↑J
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
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
⊢ g (e x) • (v - e v) - (g (e x) • (v - e v) - c • x) ∈ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v

Tactic:
exact Submodule.sub_mem _ (mem_sup_left (mem_sup_right h1)) (hle (key x))

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ s A
hB₂ : 0 ≤ s B
hAB : s (A ∪ B) = 0
⊢ s A = 0

Tactic:
rw [of_union h hA₁ hB₁] at hAB
  linarith

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : s A ≤ 0
hB₂ : s B ≤ 0
hAB : s (A ∪ B) = 0
⊢ s A = 0

Tactic:
rw [of_union h hA₁ hB₁] at hAB
  linarith

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: case neg.refine_9.hf
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝¹ : CompleteSpace E
hm : m ≤ mΩ
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun x ↦ (fs x) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), ‖(fs n) ω‖ ≤ c
this : μ[fun ω ↦ (B (f ω)) (μ[g | m] ω) | m] = fun ω ↦ (B (f ω)) (μ[g | m] ω)
n : ℕ
⊢ StronglyMeasurable fun ω ↦ (B ((fs n) ω)) (μ[g | m] ω)

pp: case neg.refine_9.hfi
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝¹ : CompleteSpace E
hm : m ≤ mΩ
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun x ↦ (fs x) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), ‖(fs n) ω‖ ≤ c
this : μ[fun ω ↦ (B (f ω)) (μ[g | m] ω) | m] = fun ω ↦ (B (f ω)) (μ[g | m] ω)
n : ℕ
⊢ Integrable (fun ω ↦ (B ((fs n) ω)) (μ[g | m] ω)) μ

Tactic:
· exact Continuous.comp_stronglyMeasurable (g := (fun z : F × E ↦ B z.1 z.2)) (by fun_prop)
        ((fs n).stronglyMeasurable.prodMk stronglyMeasurable_condExp)

Goal state after:
case neg.refine_9.hfi
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝¹ : CompleteSpace E
hm : m ≤ mΩ
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun x ↦ (fs x) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), ‖(fs n) ω‖ ≤ c
this : μ[fun ω ↦ (B (f ω)) (μ[g | m] ω) | m] = fun ω ↦ (B (f ω)) (μ[g | m] ω)
n : ℕ
⊢ Integrable (fun ω ↦ (B ((fs n) ω)) (μ[g | m] ω)) μ
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)
⊢ 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:
simp only [f_meas, true_and, MeasurableSet.iUnion f_meas, hx, and_self, ↓reduceIte]

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)
⊢ HasSum (fun i ↦ if x ∈ f i then v else 0) v
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ (μ + ν).toENNRealVectorMeasure = μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure

Tactic:
by
  refine MeasureTheory.VectorMeasure.ext fun i hi => ?_
  rw [toENNRealVectorMeasure_apply_measurable hi, add_apply, _root_.add_apply,
    toENNRealVectorMeasure_apply_measurable hi, toENNRealVectorMeasure_apply_measurable hi]

Goal state after: