mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ (auxEquiv R 𝒜 ℬ).symm
      (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((algebraMap R (⨁ (i : ι), ↥(𝒜 i))) r ⊗ₜ[R] (decompose ℬ) 1))
        ((auxEquiv R 𝒜 ℬ) x)) =
    (auxEquiv R 𝒜 ℬ).symm
      (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((auxEquiv R 𝒜 ℬ) x))
        ((algebraMap R (⨁ (i : ι), ↥(𝒜 i))) r ⊗ₜ[R] (decompose ℬ) 1))

Tactic:
DirectSum.decompose_one,

Goal state after:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ (auxEquiv R 𝒜 ℬ).symm
      (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((algebraMap R (⨁ (i : ι), ↥(𝒜 i))) r ⊗ₜ[R] 1))
        ((auxEquiv R 𝒜 ℬ) x)) =
    (auxEquiv R 𝒜 ℬ).symm
      (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((auxEquiv R 𝒜 ℬ) x))
        ((algebraMap R (⨁ (i : ι), ↥(𝒜 i))) r ⊗ₜ[R] 1))
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ r • x =
    (auxEquiv R 𝒜 ℬ).symm
      (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((algebraMap R (⨁ (i : ι), ↥(𝒜 i))) r ⊗ₜ[R] (decompose ℬ) 1))
        ((auxEquiv R 𝒜 ℬ) x))

Tactic:
DirectSum.decompose_one,

Goal state after:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ r • x =
    (auxEquiv R 𝒜 ℬ).symm
      (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((algebraMap R (⨁ (i : ι), ↥(𝒜 i))) r ⊗ₜ[R] 1))
        ((auxEquiv R 𝒜 ℬ) x))
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
⊢ ∀ (x y : B), 1 ᵍ⊗ₜ[R] (x + y) = 1 ᵍ⊗ₜ[R] x + 1 ᵍ⊗ₜ[R] y

Tactic:
by simp [tmul, TensorProduct.tmul_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Torsion.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Module.rank R M = 0 ↔ IsTorsion R M

Tactic:
simp [IsTorsion, rank_eq_zero_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : Ring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Module ι (Additive ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
⊢ (fun fg ↦ lift 𝒜 ℬ (↑fg).1 (↑fg).2 ⋯) ((fun F ↦ ⟨(F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)), ⋯⟩) F) = F

Tactic:
by
    apply AlgHom.toLinearMap_injective
    ext
    dsimp
    rw [← map_mul, tmul_one_mul_one_tmul]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ M →ₗ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M)

Tactic:
apply GradedAlgebra.ι R M

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

Goal state before:
pp: I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
i : I
⊢ (ι' R A) ((lof R I A i) 1) = 1

Tactic:
suffices ι' R A (DirectSum.lof R I A i 1) = mkAlgHom R A 1 by simpa [← ι_apply]
  exact Quotient.sound <| RingCon.le_ringConGen _ _ <| rel_id R A (i := i)

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

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v : n → α
⊢ (fun i ↦ v (-i)) = v ↔ ∀ (i : n), v (-i) = v i

Tactic:
funext_iff

Goal state after:
α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v : n → α
⊢ (∀ (x : n), v (-x) = v x) ↔ ∀ (i : n), v (-i) = v i
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
let H' : Subgroup (Multiplicative (ι → ℤ)) := H.comap em

Goal state after:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em) H
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
h : H'.index = H.index
⊢ H'.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
← Subgroup.index_toAddSubgroup,

Goal state after:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
h : H'.index = H.index
⊢ (Subgroup.toAddSubgroup H').index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case «0».«1»
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
h2 : 0 < |↑A 0 0|
⊢ |↑A ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)| ≤ |m|

Tactic:
simpa only [← abs_mul, A_c_eq_zero h10] using! h11.le.trans (le_mul_of_one_le_left h1.le h2)

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
s : R
hA : A.IsHadamard
hcard : IsRegular ↑(Fintype.card n)
hcol : ∀ (j : n), ∑ i, A i j = s
hvcol : 1 ᵥ* A = s • 1
hconjcol : Aᴴ *ᵥ 1 = star s • 1
hleft : 1 ᵥ* (A * Aᴴ) ⬝ᵥ 1 = ↑(Fintype.card n) ^ 2
⊢ s • 1 ⬝ᵥ star s • 1 = ↑(Fintype.card n) * (s * star s)

Tactic:
simp [dotProduct]

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

Goal state before:
pp: n : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix n n R
⊢ A.det ∈ nonZeroDivisors R ↔ A.det ≠ 0

Tactic:
mem_nonZeroDivisors_iff_ne_zero

Goal state after:
n : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix n n R
⊢ A.det ≠ 0 ↔ A.det ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: case neg
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
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
⊢ (A.submatrix f g).IsDetpBalanced a b

Tactic:
let D := A.submatrix f g

Goal state after:
case neg
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
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
⊢ (A.submatrix f g).IsDetpBalanced a b
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: case refine_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i ↦ mk K (ff i) ⋯)
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = (mk K (ff i) ⋯).rep
⊢ LinearIndependent K ff

Tactic:
convert! hh1.units_smul a⁻¹

Goal state after:
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i ↦ mk K (ff i) ⋯)
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = (mk K (ff i) ⋯).rep
⊢ ff = a⁻¹ • Projectivization.rep ∘ fun i ↦ mk K (ff i) ⋯
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case h
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:
let ⟨r, hr⟩ := r

Goal state after:
case h
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 : Rˣ
hr : r ∈ rootsOfUnity (max (Module.finrank R V) 1) R
⊢ ↑↑⟨r, hr⟩ ^ Module.finrank R V = 1
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]
  apply rootsOfUnity.eq_one
  rw [Nat.max_eq_right d1]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
⊢ False

Tactic:
have hli : P.root l ≠ P.root i := fun contra ↦ by
    replace h₁ : P.root k = 0 := by rwa [contra, add_eq_right] at h₁
    exact P.ne_zero _ h₁

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : 2 * (x + 1) + A * y ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
⊢ 2 * (x + 1) + A * (y - 1) ∈ s

Tactic:
convert! IsG2.pairingIn_mem_zero_one_three P n i hni hni'

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : 2 * (x + 1) + A * y ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
⊢ 2 * (x + 1) + A * (y - 1) = P.pairingIn ℤ n i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
hki : P.pairingIn ℤ k i = 0
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hnk_notMem : P.root n - P.root k ∉ range ⇑P.root
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
⊢ P.pairingIn ℤ i k = 0

Tactic:
rwa [pairingIn_eq_zero_iff]

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}
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 : ∀ (z : M), (IsReflective.coroot B ⋯) z = (IsReflective.coroot B ⋯) z
⊢ x = y

Tactic:
have h2x : ∀ z, B x x * IsReflective.coroot B x.2 z =
            B x x * IsReflective.coroot B y.2 z :=
          fun z => congrArg (HMul.hMul ((B x) x)) (h1 z)

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}
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 : ∀ (z : M), (IsReflective.coroot B ⋯) z = (IsReflective.coroot B ⋯) z
h2x : ∀ (z : M), (B ↑x) ↑x * (IsReflective.coroot B ⋯) z = (B ↑x) ↑x * (IsReflective.coroot B ⋯) z
⊢ x = y
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case refine_1
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : ↑I ⊆ C
hI : (↑I).PairwiseDisjoint id
hst : s \ t = ⋃₀ ↑I
⊢ I.sup id = s \ t

Tactic:
sup_id_eq_sSup,

Goal state after:
case refine_1
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : ↑I ⊆ C
hI : (↑I).PairwiseDisjoint id
hst : s \ t = ⋃₀ ↑I
⊢ sSup ↑I = s \ t
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case compl
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s t : Set α
hs✝ : generateSetAlgebra 𝒜 t
t_mem : t ∈ ℬ
⊢ tᶜ ∈ ℬ

Tactic:
exact hℬ.compl_mem t_mem

Goal state after:
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' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : ↑I ⊆ _root_.supClosure C
h'I : (↑I).PairwiseDisjoint id
hh'I : ⋃₀ ↑I ∈ _root_.supClosure C
J : (s : Set α) → Finpartition s
hJC : ∀ s ∈ I, ↑(J s).parts ⊆ C
K : Finpartition (I.sup id) := Finpartition.combine J ⋯
⊢ m.supClosureFun (K.parts.sup id) = ∑ u ∈ I, m.supClosureFun u

Tactic:
sup_id_eq_sSup,

Goal state after:
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : ↑I ⊆ _root_.supClosure C
h'I : (↑I).PairwiseDisjoint id
hh'I : ⋃₀ ↑I ∈ _root_.supClosure C
J : (s : Set α) → Finpartition s
hJC : ∀ s ∈ I, ↑(J s).parts ⊆ C
K : Finpartition (I.sup id) := Finpartition.combine J ⋯
⊢ m.supClosureFun (sSup ↑K.parts) = ∑ u ∈ I, m.supClosureFun u
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun i ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun i ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun i ↦ ⋃ j, ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬μ W = 0
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (fun j ↦ μ (W ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : ℕ → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun j ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun j ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
j : ℕ
hj : i ≤ j
hj' : M * r₁ (f j) ≤ r₂ (f j)
⊢ Disjoint (b j) (Z i)ᶜ

Tactic:
rw [disjoint_compl_right_iff_subset]

Goal state after:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun i ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun i ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun i ↦ ⋃ j, ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬μ W = 0
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (fun j ↦ μ (W ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : ℕ → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun j ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun j ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
j : ℕ
hj : i ≤ j
hj' : M * r₁ (f j) ≤ r₂ (f j)
⊢ b j ⊆ Z i
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
⊢ m (s ∪ ⋃₀ ↑I) = ∑ u ∈ insert s I, m u

Tactic:
m_add h_ss.1 h_sUnion_mem (Set.disjoint_sUnion_right.mpr h_dis.2),

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 : ⋃₀ insert s ↑I ∈ C
h_sUnion_mem : ⋃₀ ↑I ∈ C
⊢ m s + m (⋃₀ ↑I) = ∑ u ∈ insert s I, m u