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

Goal state before:
pp: case inr
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 : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R :=
  (Matrix.SpecialLinearGroup.toLin_equiv b).symm
⊢ g ∈ Subgroup.center (SpecialLinearGroup R V) ↔
    ∃ r, r ^ Fintype.card (Module.Free.ChooseBasisIndex R V) = 1 ∧ ↑↑g = r • LinearMap.id

Tactic:
← show e g ∈ Subgroup.center _ ↔ g ∈ Subgroup.center _ from
    MulEquivClass.apply_mem_center_iff e

Goal state after:
case inr
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 : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R :=
  (Matrix.SpecialLinearGroup.toLin_equiv b).symm
⊢ e g ∈ Subgroup.center (Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R) ↔
    ∃ r, r ^ Fintype.card (Module.Free.ChooseBasisIndex R V) = 1 ∧ ↑↑g = r • LinearMap.id
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ ↑↑r ^ Module.finrank R V = 1

Tactic:
have := (mem_rootsOfUnity' _ _).mp r.prop

Goal state after:
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
⊢ ↑↑r ^ Module.finrank R V = 1
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case inl
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
h : max (Module.finrank R V) 1 = Module.finrank R V
h' : 1 ≤ Module.finrank R V
this : ↑↑r ^ Module.finrank R V = 1
⊢ ↑↑r ^ Module.finrank R V = 1

Tactic:
exact this

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: case inl
ι : 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
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i j : ι
h : i < j
⊢ (((s • Q).toBilin bm) (bm i)) (bm j) = ((s • Q.toBilin bm) (bm i)) (bm j)

Tactic:
simp [h.ne, h, toBilin_apply, polar_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X Y Z : QuadraticModuleCat R
⊢ (forget₂ (QuadraticModuleCat R) (ModuleCat R)).map (α_ X Y Z).hom =
    (((Iso.refl
              ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj (X ⊗ Y) ⊗
                (forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj Z)).symm ≪≫
          ((Iso.refl
                ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X ⊗
                  (forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj Y)).symm ⊗ᵢ
            Iso.refl ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj Z))) ≪≫
        α_ ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X) ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj Y)
            ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj Z) ≪≫
          (Iso.refl ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X) ⊗ᵢ
              Iso.refl
                ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj Y ⊗
                  (forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj Z)) ≪≫
            Iso.refl
              ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X ⊗
                (forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj (Y ⊗ Z))).hom

Tactic:
dsimp only [forget₂_obj, forget₂_map_associator_hom]
        simp only [Iso.refl_symm, Iso.trans_hom,
          MonoidalCategory.tensorIso_hom, Iso.refl_hom, MonoidalCategory.id_tensorHom_id]
        dsimp only [toModuleCat_tensor, ModuleCat.of_coe]
        rw [Category.id_comp, Category.id_comp, Category.comp_id, MonoidalCategory.id_tensorHom_id,
          Category.id_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

Goal state before:
pp: R : Type uR
M₁ : Type uM₁
inst✝³ : CommRing R
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
m₁ m₁' : M₁
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (comp Q₁ ↑(TensorProduct.rid R M₁)))) m₁) 1))
        m₁')
      1 =
    ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (Q₁.tmul QuadraticMap.sq))) m₁) 1))
        m₁')
      1

Tactic:
simp [associated_tmul, QuadraticMap.associated_comp, one_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
V : Submodule R M
e : IsometryEquiv Q Q'
⊢ (restrict Q' (Submodule.map (↑e.toLinearEquiv) V)).PosDef ↔ (restrict Q V).PosDef

Tactic:
simp [PosDef, -Submodule.mem_map_equiv]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
V : Submodule R M
e : IsometryEquiv Q Q'
⊢ (restrict (-Q') (Submodule.map (↑e.toLinearEquiv) V)).PosDef ↔ (restrict (-Q) V).PosDef

Tactic:
simp [PosDef, -Submodule.mem_map_equiv]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: case pos
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : x ∈ Pi.spanSubset 𝕜 s
i : ι
a✝ : i ∈ univ
hi : i ∈ s
⊢ w i * (x i * x i) ≤ 0

pp: case neg
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : x ∈ Pi.spanSubset 𝕜 s
i : ι
a✝ : i ∈ univ
hi : i ∉ s
⊢ w i * (x i * x i) ≤ 0

Tactic:
· exact mul_nonpos_of_nonpos_of_nonneg (hs i hi) (mul_self_nonneg _)

Goal state after:
case neg
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : x ∈ Pi.spanSubset 𝕜 s
i : ι
a✝ : i ∈ univ
hi : i ∉ s
⊢ w i * (x i * x i) ≤ 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case pos.inr.inr
ι : 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
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
l : ι
hl : P.root l = P.root j + (n + 1) • P.root ↑i
m : ι
hml : m ≠ l
⊢ (x • e i *ᵥ Pi.single (Sum.inr k) 1) (Sum.inr m) =
    ((x * (chainBotCoeff (↑i) k + 1)) • Pi.single (Sum.inr l) 1) (Sum.inr m)

Tactic:
· replace hl : P.root m ≠ P.root i + P.root k :=
            fun contra ↦ hml (P.root.injective <| by rw [hl, contra, hk₁]; module)
          simp [e, -indexNeg_neg, hml, hl]

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

Goal state before:
pp: case inl.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
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
y : ι
hy : P.root k = P.root y - 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) -
      ∑ x,
        if P.root k = P.root x - P.root ↑i then (↑(chainTopCoeff (↑i) x) + 1) * (↑(chainBotCoeff (↑i) k) + 1) else 0) =
    ↑(chainBotCoeff (↑i) k) - ↑(chainTopCoeff (↑i) k)

Tactic:
have h_lin_ind_x : LinearIndependent R ![P.root i, P.root x] := by simpa [hx] using h_lin_ind
    have h_lin_ind_y : LinearIndependent R ![P.root i, P.root y] := by
      rw [← add_eq_of_eq_sub hy, add_comm]; simpa
    have hx' : P.chainBotCoeff i k = P.chainBotCoeff i x + 1 :=
      chainBotCoeff_of_add h_lin_ind_x (add_comm (P.root i) _ ▸ hx)
    have hy' : P.chainTopCoeff i k = P.chainTopCoeff i y + 1 := chainTopCoeff_of_sub h_lin_ind_y hy
    rw [Finset.sum_eq_single_of_mem x (Finset.mem_univ _) (by aesop),
      Finset.sum_eq_single_of_mem y (Finset.mem_univ _) (by aesop)]
    simp only [hx, hy.symm, hx', hy', reduceIte, Nat.cast_add]
    ring

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

Goal state before:
pp: case inr.inr
ι : 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
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 : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)
hd₂ : diagonal (0 ⊕ᵥ d) ∈ cartanSubalgebra b
x : ↥H := ⟨⟨diagonal (0 ⊕ᵥ d), ⋯⟩, hd₂⟩
k : ℕ
hk : diagonal ((0 ⊕ᵥ d - χ x • 1) ^ k) *ᵥ w = 0
hχx : d i = χ x
hk₀ : k ≠ 0
j : ι
hij : i ≠ j
⊢ ((w (Sum.inr i))⁻¹ • w) (Sum.inr j) = v b i (Sum.inr j)

Tactic:
suffices d j ≠ χ x by
          simpa [mulVec_eq_sum, diagonal_apply, sub_eq_zero, this, hij, hi] using!
            congr_fun hk (Sum.inr j)
        rw [← hχx]
        exact hd₁ <| by simp [hij.symm]

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

Goal state before:
pp: case add
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 + y))

Tactic:
map_add

Goal state after:
case add
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)
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Goal state before:
pp: 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)
a : TensorAlgebra R M
⊢ motive ((algHom R M) a)

Tactic:
induction a using TensorAlgebra.induction with
  | algebraMap r => rw [AlgHom.commutes]; exact algebraMap r
  | ι x => exact ι x
  | mul x y hx hy => rw [map_mul]; exact mul _ _ hx hy
  | add x y hx hy => rw [map_add]; exact add _ _ hx hy

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

Goal state before:
pp: 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
e : SymmetricAlgebra R M ≃ₐ[R] A
he : ↑↑e ∘ₗ SymmetricAlgebra.ι R M = f
⊢ IsSymmetricAlgebra f

Tactic:
by
  suffices h : e = SymmetricAlgebra.lift f by
    change Function.Bijective _
    exact h ▸ e.bijective
  ext x
  simpa using congr($he x)

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

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ℕ
x✝ x y : TensorAlgebra R M
i : ℕ
hx : x ∈ (ι R).range ^ i
hy : y ∈ (ι R).range ^ i
ihx : ((lift R) (GradedAlgebra.ι R M)) x = (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨x, hx⟩
ihy : ((lift R) (GradedAlgebra.ι R M)) y = (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨y, hy⟩
⊢ ((lift R) (GradedAlgebra.ι R M)) (x + y) = (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨x + y, ⋯⟩

Tactic:
rw [map_add, ihx, ihy, ← map_add]
      rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst✝¹⁴ : DecidableEq ι
inst✝¹³ : DecidableEq κ
inst✝¹² : Fintype ι
inst✝¹¹ : Fintype κ
inst✝¹⁰ : Finite ι'
inst✝⁹ : Finite κ'
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
i : ι'
j : κ'
i' : ι
j' : κ
⊢ ((bM'.tensorProduct bN').repr ((map f g) (bM i' ⊗ₜ[R] bN j'))) (i, j) =
    (bM'.repr (f (bM i'))) i * (bN'.repr (g (bN j'))) j

Tactic:
TensorProduct.map_tmul,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst✝¹⁴ : DecidableEq ι
inst✝¹³ : DecidableEq κ
inst✝¹² : Fintype ι
inst✝¹¹ : Fintype κ
inst✝¹⁰ : Finite ι'
inst✝⁹ : Finite κ'
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
i : ι'
j : κ'
i' : ι
j' : κ
⊢ ((bM'.tensorProduct bN').repr (f (bM i') ⊗ₜ[R] g (bN j'))) (i, j) =
    (bM'.repr (f (bM i'))) i * (bN'.repr (g (bN j'))) j
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
b : α
h : (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) b a
⊢ count b s = count b t

pp: case refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
⊢ count a s < count a t

Tactic:
· apply_fun count b at he
    simpa only [count_add, count_singleton, if_neg h.2, add_zero, count_eq_zero.2 (hr b h.1)]
      using he

Goal state after:
case refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
⊢ count a s < count a t
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)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
⊢ (P I) S = (P J) T

Tactic:
by
  cases isEmpty_or_nonempty (∀ i, α i) with
  | inl h =>
    suffices ∀ I, P I univ = 0 by
      simp only [Measure.measure_univ_eq_zero] at this
      simp [this]
    simpa using eq_zero_of_isEmpty hP
  | inr h =>
    have : S = Finset.restrict₂ hJI ⁻¹' T :=
      eq_of_cylinder_eq_of_subset h_eq hJI
    rw [hP I J hJI, Measure.map_apply _ hT, this]
    exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

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
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
⊢ v - e v ∈ (↑e).fixedSubmodule

Tactic:
← e.fixedSubmodule.ker_mkQ,

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_notMem : v ∉ (↑e).fixedSubmodule
⊢ v - e v ∈ (↑e).fixedSubmodule.mkQ.ker
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f g : Dual K V
v : V
a b : K
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha✝ : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb✝ : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
x : V
ha : e x + f (e x) • (v - e v) - a • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : e x + f (e x) • (v - e v) + g (e x) • (v - e v) - b • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
⊢ g (e x) • (v - e v) + -(c • x) =
    g (e x) • (v - e v) + e x + f (e x) • (v - e v) - b • x - (e x + f (e x) • (v - e v) - a • x)

Tactic:
simp only [add_sub_assoc, add_assoc, add_right_inj, sub_smul, smul_sub, hc]

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f g : Dual K V
v : V
a b : K
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha✝ : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb✝ : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
x : V
ha : e x + f (e x) • (v - e v) - a • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : e x + f (e x) • (v - e v) + g (e x) • (v - e v) - b • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
⊢ -(b • x - a • x) = e x + (f (e x) • v - f (e x) • e v - b • x - (e x + (f (e x) • v - f (e x) • e v - a • x)))
Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
⊢ projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t

Tactic:
by
  obtain ⟨I, S, hS, hs_eq⟩ := (mem_measurableCylinders _).1 hs
  obtain ⟨J, T, hT, ht_eq⟩ := (mem_measurableCylinders _).1 ht
  classical
  let S' := restrict₂ (subset_union_left (s₂ := J)) ⁻¹' S
  let T' := restrict₂ (subset_union_right (s₁ := I)) ⁻¹' T
  have hS' : MeasurableSet S' := measurable_restrict₂ _ hS
  have hT' : MeasurableSet T' := measurable_restrict₂ _ hT
  have h_eq1 : s = cylinder (I ∪ J) S' := by rw [hs_eq]; exact cylinder_eq_cylinder_union I S J
  have h_eq2 : t = cylinder (I ∪ J) T' := by rw [ht_eq]; exact cylinder_eq_cylinder_union J T I
  have h_eq3 : s ∪ t = cylinder (I ∪ J) (S' ∪ T') := by
    rw [hs_eq, ht_eq]; exact union_cylinder _ _ _ _
  rw [projectiveFamilyFun_congr hP hs h_eq1 hS', projectiveFamilyFun_congr hP ht h_eq2 hT',
    projectiveFamilyFun_congr hP (union_mem_measurableCylinders hs ht) h_eq3 (hS'.union hT')]
  cases isEmpty_or_nonempty (Π i, α i) with
  | inl h => simp [hP.eq_zero_of_isEmpty]
  | inr h =>
    rw [measure_union _ hT']
    rwa [hs_eq, ht_eq, disjoint_cylinder_iff] at hst

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

Goal state before:
pp: case refine_3
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
⊢ ∀ a ∈ I, f a ⊆ ⋃ i, f i

Tactic:
exact fun i _ ↦ subset_iUnion _ i

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

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
s✝ t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α}, s ∈ C → t ∈ C → Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h : ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → m (⋃₀ ↑I) = ∑ u ∈ I, m u
h_ss : s ∈ C ∧ ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id ∧ ∀ j ∈ ↑I, Disjoint (id s) (id j)
h_mem : ⋃₀ insert s ↑I ∈ C
h_sUnion_mem : ⋃₀ ↑I ∈ C
⊢ ⋃₀ ↑I ∈ C

Tactic:
Set.sUnion_insert

Goal state after:
case insert
α : Type u_1
C : Set (Set α)
s✝ t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α}, s ∈ C → t ∈ C → Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h : ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → m (⋃₀ ↑I) = ∑ u ∈ I, m u
h_ss : s ∈ C ∧ ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id ∧ ∀ j ∈ ↑I, Disjoint (id s) (id j)
h_mem : s ∪ ⋃₀ ↑I ∈ C
h_sUnion_mem : ⋃₀ ↑I ∈ C
⊢ ⋃₀ ↑I ∈ C