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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd
he :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range =
    e.toAddMonoidHom.graph
r : R
x : M ⧸ L.goursatFst
l : M × N
hl : l ∈ L.toAddSubgroup
hl' :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype)
      ⟨l, hl⟩ =
    (x, e x)
⊢ r • (x, e x) ∈
    (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range

Tactic:
use ⟨r • l, L.smul_mem r hl⟩

Goal state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd
he :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range =
    e.toAddMonoidHom.graph
r : R
x : M ⧸ L.goursatFst
l : M × N
hl : l ∈ L.toAddSubgroup
hl' :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype)
      ⟨l, hl⟩ =
    (x, e x)
⊢ (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype)
      ⟨r • l, ⋯⟩ =
    r • (x, e x)
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
⊢ A.IsPivotedBy l ↔
    Monotone l ∧
      StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0

Tactic:
refine ⟨fun hA => ⟨hA.monotone, hA.strictMonoOn, hA.isPivotEntry⟩, ?_⟩

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
⊢ (Monotone l ∧
      StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0) →
    A.IsPivotedBy l
Module: Mathlib.LinearAlgebra.Matrix.Gershgorin

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ∑ i_1 ∈ Finset.univ.erase i, ‖A i i_1 * v i_1 * (v i)⁻¹‖ = ∑ j ∈ Finset.univ.erase i, ‖A i j‖ * ‖v j * (v i)⁻¹‖

Tactic:
simp_rw [mul_assoc, norm_mul]

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

Goal state before:
pp: n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
hexpand : ∀ (j : n), (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j
hdvd : ∀ (j : n), 4 ∣ (1 + A s j * A r j) * (1 + A t j * A r j)
hsum : ∑ j, (1 + A s j * A r j) * (1 + A t j * A r j) = ↑(Fintype.card n)
⊢ 4 ∣ Fintype.card n

Tactic:
← Int.ofNat_dvd,

Goal state after:
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
hexpand : ∀ (j : n), (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j
hdvd : ∀ (j : n), 4 ∣ (1 + A s j * A r j) * (1 + A t j * A r j)
hsum : ∑ j, (1 + A s j * A r j) * (1 + A t j * A r j) = ↑(Fintype.card n)
⊢ ↑4 ∣ ↑(Fintype.card n)
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
⊢ Finite V

Tactic:
let e := nonZeroEquivProjectivizationProdUnits k V

Goal state after:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
⊢ Finite V
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ iSupIndep fun i ↦ (f i).submodule

Tactic:
by
  refine ⟨?_, fun h => ?_⟩
  · rintro ⟨f, hf, hi⟩
    simp only [submodule_mk]
    exact (iSupIndep_iff_linearIndependent_of_ne_zero (R := K) hf).mpr hi
  · rw [independent_iff]
    refine h.linearIndependent (Projectivization.submodule ∘ f) (fun i => ?_) fun i => ?_
    · simpa only [Function.comp_apply, submodule_eq] using Submodule.mem_span_singleton_self _
    · exact rep_nonzero (f i)

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
a : ℙ K V
⊢ IsCollinear {a}

Tactic:
induction a using ind with

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : Field F
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
p : ℙ F (Fin 2 → F)
⊢ IsMulCommutative ↥(PSL.iwasawaT p)

Tactic:
have hSL : IsMulCommutative (lineStab (F := F) (ι := Fin 2) p.submodule) := by
      rw [← Projectivization.mk_rep p, Projectivization.submodule_mk]
      exact lineStab_isMulCommutative_of_span p.rep p.rep_nonzero

Goal state after:
ι : Type u_1
F : Type u_2
inst✝² : Field F
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
p : ℙ F (Fin 2 → F)
hSL : IsMulCommutative ↥(lineStab p.submodule)
⊢ IsMulCommutative ↥(PSL.iwasawaT p)
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
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
a✝ : Nontrivial R
x : V
hx : ¬x = 0
this : ∀ (u : SpecialLinearGroup R V) (x : V), ↑u x = x
⊢ (fun x ↦ ↑u x) x = (fun x ↦ ↑v x) x

Tactic:
simp [this u, this v]

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

Goal state before:
pp: case h
ι : 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
x : M
⊢ ∀ x_1 ∈ (bm.repr x).support.offDiag, ¬x_1.1 = x_1.2

Tactic:
intro x hx
    rw [Finset.mem_offDiag] at hx
    simpa using hx.2.2

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
d1 : Module.finrank R V ≤ 1
g : ↥(Subgroup.center (SpecialLinearGroup R V))
⊢ centerEquivRootsOfUnity g = 1

Tactic:
rw [← Subtype.coe_inj, OneMemClass.coe_one]

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
d1 : Module.finrank R V ≤ 1
g : ↥(Subgroup.center (SpecialLinearGroup R V))
⊢ ↑(centerEquivRootsOfUnity g) = 1
Module: Mathlib.LinearAlgebra.QuadraticForm.Real

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
w : ι → ℝ
u : ι → ℝˣ := fun i ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|↑(u i)| ≠ 0
hwu : ∀ (i : ι), w i / |↑(u i)| = ↑(sign (w i))
v : ι → ℝ
⊢ ∑ i, w i / |↑(u i)| * v i ^ 2 = ∑ i, w i * (v i ^ 2 * |↑(u i)|⁻¹)

Tactic:
exact sum_congr rfl fun j _ ↦ by ring

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X : QuadraticModuleCat R
⊢ ModuleCat.ofHom (Hom.toIsometry (ρ_ X).hom).toLinearMap =
    𝟙 (X.toModuleCat ⊗ (𝟙_ (QuadraticModuleCat R)).toModuleCat) ≫
      X.toModuleCat ◁ 𝟙 (𝟙_ (ModuleCat R)) ≫ (ρ_ X.toModuleCat).hom

Tactic:
erw [MonoidalCategory.whiskerLeft_id]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X : QuadraticModuleCat R
⊢ ModuleCat.ofHom (Hom.toIsometry (ρ_ X).hom).toLinearMap =
    𝟙 (X.toModuleCat ⊗ (𝟙_ (QuadraticModuleCat R)).toModuleCat) ≫
      𝟙 (X.toModuleCat ⊗ (𝟙_ (QuadraticModuleCat R)).toModuleCat) ≫ (ρ_ X.toModuleCat).hom
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case neg
ι : 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
hij : P.root j + (n + 1) • P.root ↑i ∉ range ⇑P.root
⊢ x • e i *ᵥ Pi.single (Sum.inr k) 1 = 0 ∨
    ∃ k_1 x_1,
      P.root k_1 = P.root j + (n + 1) • P.root ↑i ∧ x • e i *ᵥ Pi.single (Sum.inr k) 1 = x_1 • Pi.single (Sum.inr k_1) 1

Tactic:
left
      ext (l | l)
      · simp [e, -indexNeg_neg, hki]
      · replace hij : P.root l ≠ P.root i + P.root k :=
          fun contra ↦ hij ⟨l, by rw [contra, hk₁]; module⟩
        simp [e, -indexNeg_neg, hij]

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

Goal state before:
pp: case 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
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
j : ↥b.support
k : ι
⊢ (e i ^ 2).col (Sum.inl j) (Sum.inr k) = 0 (Sum.inr k)

Tactic:
have aux : ∀ x : ι, x ∈ Finset.univ → ¬ (x = i ∧ P.root k = P.root i + P.root x) := by
        suffices P.root k ≠ (2 : ℕ) • P.root i by simpa [two_smul]
        exact fun contra ↦ P.nsmul_notMem_range_root (n := 2) (i := i) ⟨k, contra⟩

Goal state after:
case 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
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
j : ↥b.support
k : ι
aux : ∀ x ∈ Finset.univ, ¬(x = ↑i ∧ P.root k = P.root ↑i + P.root x)
⊢ (e i ^ 2).col (Sum.inl j) (Sum.inr k) = 0 (Sum.inr k)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case calc_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
⊢ ω b * h j * f i - ω b * f i * h j = -(h j * e i - e i * h j) * ω b

Tactic:
ω_mul_h,

Goal state after:
case calc_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
⊢ -h j * ω b * f i - ω b * f i * h j = -(h j * e i - e i * h j) * ω b
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case calc_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
⊢ -h j * (e i * ω b) - e i * (ω b * h j) = -(h j * e i - e i * h j) * ω b

Tactic:
ω_mul_h,

Goal state after:
case calc_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
⊢ -h j * (e i * ω b) - e i * (-h j * ω b) = -(h j * e i - e i * h j) * ω b
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
r : R
a : M
⊢ Exists.choose ⋯ = (RingHom.id R) r • Exists.choose ⋯

Tactic:
by
    refine hx.1.1 ?_
    simp only [RingHom.id_apply]
    rw [← (hx.2 (r • a)).choose_spec, smul_eq_mul, mul_left_comm, ← (hx.2 a).choose_spec, map_smul,
      two_mul, smul_eq_mul, two_mul, mul_add]

Goal state after:
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}
z : M
⊢ 2 * (B ↑y) z - 2 * (B ↑y) ↑x * (IsReflective.coroot B ⋯) z = (B ↑y) ↑y * (IsReflective.coroot B ⋯) z

Tactic:
← isOrthogonal_reflection B x.2 hSB y y,

Goal state after:
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}
z : M
⊢ 2 * (B ↑y) z - 2 * (B ↑y) ↑x * (IsReflective.coroot B ⋯) z =
    (B ((Module.reflection ⋯) ↑y)) ((Module.reflection ⋯) ↑y) * (IsReflective.coroot B ⋯) z
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
m : ι
hm : P.root m = P.root l - P.root ↑j
l' : ι
hl' : P.root l' = P.root l + P.root ↑i
hk : P.root k = P.root l + P.root ↑i - P.root ↑j
aux₃ : ∀ (x : ι), x ≠ m → ¬(P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x)
aux₄ : ∀ (x : ι), x ≠ l' → ¬(P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j)
⊢ ∀ b_1 ∈ Finset.univ,
    b_1 ≠ m →
      (if P.root b_1 = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root b_1 then
          (↑(chainBotCoeff (↑i) b_1) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
        else 0) =
        0

Tactic:
rintro x - h; rw [if_neg (aux₃ _ h)]

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ ∃ i i_1, ∃ (_ : IsClosed i_1) (_ : IsCompact i_1), ∅ ∈ {cylinder i i_1}

Tactic:
mem_singleton_iff

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ ∃ i i_1, ∃ (_ : IsClosed i_1) (_ : IsCompact i_1), ∅ = cylinder i i_1
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case pos
ι : 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
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₁ : i ∈ s₁
⊢ t₁' i ∈ C i

pp: case neg
ι : 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
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₁ : i ∉ s₁
⊢ t₁' i ∈ C i

Tactic:
· rw [← h1 i hi₁]
        exact h₁ i (mem_univ _)

Goal state after:
case neg
ι : 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
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₁ : i ∉ s₁
⊢ t₁' i ∈ C i
Module: Mathlib.MeasureTheory.Constructions.Cylinders

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

Tactic:
← Finset.coe_singleton,

Goal state after:
case a
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ ((fun t ↦ (↑{i}).pi t) '' univ.pi fun i ↦ {s | MeasurableSet s}) ⊆ squareCylinders fun i ↦ {s | MeasurableSet s}
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
⊢ S = Finset.restrict₂ hJI ⁻¹' T

Tactic:
rw [Set.ext_iff] at h_eq

Goal state after:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
h_eq : ∀ (x : (i : ι) → α i), x ∈ cylinder I S ↔ x ∈ cylinder J T
hJI : J ⊆ I
⊢ S = Finset.restrict₂ hJI ⁻¹' T
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ ∃ i i_1, ∃ (_ : MeasurableSet i_1), ∅ ∈ {cylinder i i_1}

Tactic:
mem_singleton_iff

Goal state after:
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ ∃ i i_1, ∃ (_ : MeasurableSet i_1), ∅ = cylinder i i_1
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
t : Set ((i : ι) → α i)
⊢ (∃ i i_1, MeasurableSet i_1 ∧ t ∈ {cylinder i i_1}) ↔ ∃ s S, MeasurableSet S ∧ t = cylinder s S

Tactic:
mem_singleton_iff

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
⊢ MeasurableSet s

Tactic:
obtain ⟨I, t, mt, rfl⟩ := (mem_measurableCylinders s).1 hs
  exact mt.cylinder

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

Goal state before:
pp: case mk
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m' : AddContent G C
toFun✝ : Set α → G
empty'✝ : toFun✝ ∅ = 0
sUnion'✝ : ∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → toFun✝ (⋃₀ ↑I) = ∑ u ∈ I, toFun✝ u
x✝ : (fun m s ↦ m.toFun s) { toFun := toFun✝, empty' := empty'✝, sUnion' := sUnion'✝ } = (fun m s ↦ m.toFun s) m'
⊢ { toFun := toFun✝, empty' := empty'✝, sUnion' := sUnion'✝ } = m'

Tactic:
cases m'

Goal state after:
case mk.mk
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
toFun✝¹ : Set α → G
empty'✝¹ : toFun✝¹ ∅ = 0
sUnion'✝¹ : ∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → toFun✝¹ (⋃₀ ↑I) = ∑ u ∈ I, toFun✝¹ u
toFun✝ : Set α → G
empty'✝ : toFun✝ ∅ = 0
sUnion'✝ : ∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → toFun✝ (⋃₀ ↑I) = ∑ u ∈ I, toFun✝ u
x✝ :
  (fun m s ↦ m.toFun s) { toFun := toFun✝¹, empty' := empty'✝¹, sUnion' := sUnion'✝¹ } =
    (fun m s ↦ m.toFun s) { toFun := toFun✝, empty' := empty'✝, sUnion' := sUnion'✝ }
⊢ { toFun := toFun✝¹, empty' := empty'✝¹, sUnion' := sUnion'✝¹ } =
    { toFun := toFun✝, empty' := empty'✝, sUnion' := sUnion'✝ }