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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁵ : Finite ι
M : ι → Type u_3
N : Type u_4
γ : ι → Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N
h : ∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))
⊢ φ = φ'

Tactic:
obtain ⟨n, hι⟩ : ∃ (n : ℕ), Nat.card ι = n := ⟨_, rfl⟩
  induction n generalizing ι with
  | zero =>
    ext x
    have : IsEmpty ι := (Nat.card_eq_zero.1 hι).resolve_right <| Finite.not_infinite ‹_›
    obtain rfl : x = fun i ↦ @g i (isEmptyElim i) := Subsingleton.elim _ _
    apply h
  | succ n hn =>
    classical
    have : Nonempty ι := ((Nat.card_pos_iff (α := ι)).1 (by omega)).1
    have i₀ : ι := Classical.arbitrary _
    let e := (equivPiTensorComplSingletonTensor R M i₀).trans (TensorProduct.comm _ _ _)
    obtain ⟨ψ, rfl⟩ : ∃ ψ, φ = LinearMap.comp ψ e.toLinearMap :=
      ⟨φ.comp e.symm.toLinearMap, by ext; simp⟩
    obtain ⟨ψ', rfl⟩ : ∃ ψ', φ' = LinearMap.comp ψ' e.toLinearMap :=
      ⟨φ'.comp e.symm.toLinearMap, by ext; simp⟩
    dsimp [e] at h
    congr 1
    apply (TensorProduct.lift.equiv _ _ _ _).symm.injective
    rw [Submodule.linearMap_eq_iff_of_span_eq_top _ _ (hg i₀)]
    rintro ⟨_, ⟨g₀, rfl⟩⟩
    apply hn (g := fun i (j : γ i.1) ↦ by exact g j)
    · intro
      exact hg _
    · intro j
      have : (g g₀ ⊗ₜ[R] (tprod R) fun i ↦ g (j i)) =
          TensorProduct.comm R _ _ ((equivPiTensorComplSingletonTensor R M i₀)
            (⨂ₜ[R] (i : ι), g (Function.subtypeNeLift i₀ j g₀ i))) := by
        simp only [equivPiTensorComplSingletonTensor_tprod, Function.subtypeNeLift_self]
        congr
        ext ⟨x, hx⟩
        congr
        rw [Function.subtypeNeLift_of_neq _ _ _ _ (by assumption)]
        rfl
      simpa only [lift.equiv_symm_apply, this] using h (Function.subtypeNeLift i₀ j g₀)
    · exact Set.ncard_compl_of_ncard_eq_add _ (by simpa)

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
w : ι → ℝ
⊢ (weightedSumSquares ℝ w).IsometryEquiv (weightedSumSquares ℝ fun i ↦ ↑(sign (w i)))

Tactic:
let u i := if h : w i = 0 then (1 : ℝˣ) else Units.mk0 (w i) h

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
w : ι → ℝ
u : ι → ℝˣ := fun i ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
⊢ (weightedSumSquares ℝ w).IsometryEquiv (weightedSumSquares ℝ fun i ↦ ↑(sign (w i)))
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

Goal state before:
pp: R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ (associatedHom R) (comp (Q₂.tmul Q₁) ↑(TensorProduct.comm R M₁ M₂)) = (associatedHom R) (Q₁.tmul Q₂)

Tactic:
ext m₁ m₂ m₁' m₂'

Goal state after:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
m₁' : M₁
m₂' : M₂
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry
                ((associatedHom R) (comp (Q₂.tmul Q₁) ↑(TensorProduct.comm R M₁ M₂))))
              m₁)
            m₂))
        m₁')
      m₂' =
    ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (Q₁.tmul Q₂))) m₁) m₂))
        m₁')
      m₂'
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
⊢ LinearMap.Nondegenerate Q.polarBilin ↔ Nondegenerate

Tactic:
rw [nondegenerate_iff_radical_eq_bot, radical_eq_ker_polarBilin,
    LinearMap.IsRefl.nondegenerate_iff_separatingLeft, LinearMap.separatingLeft_iff_ker_eq_bot]
  exact fun x y ↦ (polar_comm Q y x).trans

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

Goal state before:
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 * 0 ≤ 0

Tactic:
mul_zero

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
⊢ 0 ≤ 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case inl.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✝¹ : CharZero R
inst✝ : Fintype ι
i k l : ↥b.support
⊢ (ω b * h i) (Sum.inl k) (Sum.inl l) = (-h i * ω b) (Sum.inl k) (Sum.inl l)

Tactic:
simp [ω, h]

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✝¹ : CharZero R
inst✝ : Fintype ι
i k : ↥b.support
l : ι
⊢ (ω b * h i) (Sum.inl k) (Sum.inr l) = (-h i * ω b) (Sum.inl k) (Sum.inr l)

Tactic:
simp [ω, h]

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

Goal state before:
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✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k : ι
l : ↥b.support
⊢ (ω b * h i) (Sum.inr k) (Sum.inl l) = (-h i * ω b) (Sum.inr k) (Sum.inl l)

Tactic:
simp [ω, h]

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, x • P.root i + y • P.root j = P.root k

Tactic:
← Submodule.mem_span_pair,

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
⊢ P.root k ∈ Submodule.span ℤ {P.root i, P.root j}
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:

Tactic:
⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b := by rw [Ring.lie_def, sub_mul]
                      _ = e i * (f j * ω b) - f j * (e i * ω b) := by rw [mul_assoc, mul_assoc]
                      _ = e i * (ω b * e j) - f j * (ω b * f i) := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = (e i * ω b) * e j - (f j * ω b) * f i := by rw [← mul_assoc, ← mul_assoc]
                      _ = (ω b * f i) * e j - (ω b * e j) * f i := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = ω b * (f i * e j) - ω b * (e j * f i) := by rw [mul_assoc, mul_assoc]
                      _ = -ω b * ⁅e j, f i⁆ := ?_

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.IsCrystallographic
b : P.Base
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : Fintype ι
i j : ↥b.support
⊢ ω b * (f i * e j) - ω b * (e j * f i) = -ω b * ⁅e j, f i⁆
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.EmbeddedG2
⊢ threeShortAddLongRoot P = 3 • shortRoot P + longRoot P

Tactic:
by
  simp [threeShortAddLongRoot, threeShortAddLong, reflection_apply_root]
  module

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

Goal state before:
pp: case calc_2
ι : 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 * (B.form (P.root i)) (threeShortAddLongRoot P) =
    3 * (2 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P)

pp: case calc_3
ι : 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
⊢ 3 * (2 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P) =
    P.pairing i (short P) * (B.form (longRoot P)) (longRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P)

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
⊢ P.pairing i (short P) * (B.form (longRoot P)) (longRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P) =
    (P.pairing i (short P) + P.pairing i (long P)) * (B.form (threeShortAddLongRoot P)) (threeShortAddLongRoot P)

Tactic:
· rw [threeShortAddLongRoot_eq, map_add, mul_add, map_smul, smul_eq_mul]; ring

Goal state after:
case calc_3
ι : 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
⊢ 3 * (2 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P) =
    P.pairing i (short P) * (B.form (longRoot P)) (longRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P)

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
⊢ P.pairing i (short P) * (B.form (longRoot P)) (longRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P) =
    (P.pairing i (short P) + P.pairing i (long P)) * (B.form (threeShortAddLongRoot P)) (threeShortAddLongRoot P)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case smul
ι : 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
inst✝ : P.IsIrreducible
i : ι
hi : P.root i ∉ allRoots P
this✝ : Fintype ι
B : P.InvariantForm
h₂ : (B.form (P.root i)) (P.root (long P)) = 0
h₁ : (B.form (P.root i)) (P.root (short P)) = 0
this : Module.IsReflexive R M
x : M
a✝¹ : R
x✝ : M
hx✝ : x✝ ∈ Submodule.span R {longRoot P, shortRoot P}
a✝ : (B.form (P.root i)) x✝ = 0
⊢ (B.form (P.root i)) (a✝¹ • x✝) = 0

Tactic:
| smul =>

Goal state after:
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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
h_ne : i ≠ j
this : {i, j} ⊆ b.support
⊢ Submodule.span ℤ {P.root i, P.root j} = P.rootSpan ℤ

Tactic:
← image_pair,

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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
h_ne : i ≠ j
this : {i, j} ⊆ b.support
⊢ Submodule.span ℤ (⇑P.root '' {i, j}) = P.rootSpan ℤ
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
h2x : ∀ (z : M), 2 * (B ↑x) z = (B ↑x) ↑x * (IsReflective.coroot B ⋯) z
h2y : ∀ (z : M), (B ↑y) ↑y * (IsReflective.coroot B ⋯) z = 2 * (B ↑y) z
⊢ 2 * (B ↑x) ↑x = 2 * (B ↑y) ↑y

Tactic:
specialize h2x 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}
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 : ∀ (z : M), (IsReflective.coroot B ⋯) z = (IsReflective.coroot B ⋯) z
h2x : 2 * (B ↑x) ↑y = (B ↑x) ↑x * (IsReflective.coroot B ⋯) ↑y
h2y : ∀ (z : M), (B ↑y) ↑y * (IsReflective.coroot B ⋯) z = 2 * (B ↑y) z
⊢ 2 * (B ↑x) ↑x = 2 * (B ↑y) ↑y
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
h2x : ∀ (z : M), 2 * (B ↑x) z = (B ↑x) ↑x * (IsReflective.coroot B ⋯) z
h2y : ∀ (z : M), (B ↑y) ↑y * (IsReflective.coroot B ⋯) z = 2 * (B ↑y) z
h2xy : (B ↑x) ↑x = (B ↑y) ↑y
⊢ x = y

Tactic:
Subtype.ext_iff,

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), 2 * (B ↑x) z = (B ↑x) ↑x * (IsReflective.coroot B ⋯) z
h2y : ∀ (z : M), (B ↑y) ↑y * (IsReflective.coroot B ⋯) z = 2 * (B ↑y) z
h2xy : (B ↑x) ↑x = (B ↑y) ↑y
⊢ ↑x = ↑y
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
h2x : ∀ (z : M), 2 * (B ↑x) z = (B ↑x) ↑x * (IsReflective.coroot B ⋯) z
h2y : ∀ (z : M), (B ↑y) ↑y * (IsReflective.coroot B ⋯) z = 2 * (B ↑y) z
h2xy : (B ↑x) ↑x = (B ↑y) ↑y
z : M
⊢ (B (↑x - ↑y)) z = 0

Tactic:
map_sub,

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), 2 * (B ↑x) z = (B ↑x) ↑x * (IsReflective.coroot B ⋯) z
h2y : ∀ (z : M), (B ↑y) ↑y * (IsReflective.coroot B ⋯) z = 2 * (B ↑y) z
h2xy : (B ↑x) ↑x = (B ↑y) ↑y
z : M
⊢ (B ↑x - B ↑y) z = 0
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 z) ↑y - 2 * (B ↑y) ↑x * (IsReflective.coroot B ⋯) z = 2 * (B z) (↑y - (IsReflective.coroot B ⋯) ↑y • ↑x)

Tactic:
map_sub,

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 z) ↑y - 2 * (B ↑y) ↑x * (IsReflective.coroot B ⋯) z =
    2 * ((B z) ↑y - (B z) ((IsReflective.coroot B ⋯) ↑y • ↑x))
Module: Mathlib.LinearAlgebra.SModEq.Pow

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

Tactic:
simp only [← Ideal.Quotient.eq_zero_iff_mem, map_sum, map_mul, map_pow, h₁, ← pow_add]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
h₂ : ↑p = 0
⊢ ∑ x ∈ Finset.range p, (Ideal.Quotient.mk I) y ^ (x + (p - 1 - x)) = 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

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

Tactic:
have aux₃ (x) (hx : x ≠ m) :
      ¬ (P.root x = P.root l - P.root j ∧ P.root k = P.root i + P.root x) := by
        grind [EmbeddingLike.apply_eq_iff_eq]

Goal state after:
case pos
ι : 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)
⊢ (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0
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
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
this✝ : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
him_mem : P.root i + P.root m ∈ range ⇑P.root
hik_mem : P.root i + P.root k ∈ range ⇑P.root
hjk_mem : P.root (-k) + P.root j ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
h₁' : P.root (-k) - P.root i = P.root (-l)
h₂' : P.root (-k) + P.root j = P.root (-m)
h₃' : P.root (-k) + P.root j - P.root i ∈ range ⇑P.root
hki : P.pairingIn ℤ k i < 0
hik : chainBotCoeff i k = 0
hkj : P.pairingIn ℤ (-k) j < 0
hjk : chainBotCoeff j (-k) = 0
⊢ P.root j + P.root (-k) ∈ range ⇑P.root

Tactic:
by rwa [add_comm]

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

Goal state before:
pp: case mul
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_mul

Goal state after:
case mul
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.Logic.Godel.GodelBetaFunction

Goal state before:
pp: m : ℕ
l : List ℕ
⊢ ∀ i ∈ Finset.univ, coprimes (fun x ↦ l[x]) i ≠ 0

Tactic:
by simp [coprimes]

Goal state after:
Module: Mathlib.Logic.Godel.GodelBetaFunction

Goal state before:
pp: l : List ℕ
i : Fin l.length
⊢ ∀ i ∈ Finset.univ, coprimes (fun x ↦ l[x]) i ≠ 0

Tactic:
by simp [coprimes]

Goal state after: