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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
f : A →ₐ[R] C
g : B →ₐ[R] C
h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)
⊢ ∀ (x y : 𝒜 ᵍ⊗[R] ℬ),
    (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) (x * y) =
      (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) x *
        (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) y

Tactic:
rw [LinearMap.map_mul_iff]

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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
f : A →ₐ[R] C
g : B →ₐ[R] C
h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)
⊢ (LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ)).compr₂
      (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) =
    (LinearMap.mul R C ∘ₗ
          LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm).compl₂
      (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm)
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

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

Tactic:
ihx,

Goal state after:
case add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x x✝ y✝ : ExteriorAlgebra R M
i✝ : ℕ
hx✝ : x✝ ∈ (ι R).range ^ i✝
hy✝ : y✝ ∈ (ι R).range ^ i✝
ihx : (liftι R M) x✝ = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩
ihy : (liftι R M) y✝ = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨y✝, hy✝⟩
⊢ (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩ + (liftι R M) y✝ =
    (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨x✝ + y✝, ⋯⟩
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
i : ℕ
x : ExteriorAlgebra R M
hx : x ∈ ⋀[R]^i M
⊢ (liftι R M) x = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i) ⟨x, hx⟩

Tactic:
induction hx using Submodule.pow_induction_on_left' with

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ toDirectSum ((tprod R M n) x) = (DirectSum.of (fun i ↦ ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)

Tactic:
rw [tprod_apply, map_list_prod, List.map_ofFn]
  simp_rw [Function.comp_def, toDirectSum_ι]
  rw [DirectSum.list_prod_ofFn_of_eq_dProd]
  apply DirectSum.of_eq_of_gradedMonoid_eq
  rw [GradedMonoid.mk_list_dProd]
  rw [TensorPower.list_prod_gradedMonoid_mk_single]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
⊢ N.toAddSubgroup.index = Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index

Tactic:
have snf' : ∀ i, (bN' i : ι → R) = Pi.single (f i) (a i) := by
    intro i
    simp only [map_apply, bN']
    rw [LinearEquiv.submoduleMap_apply]
    simp only [equivFun_apply, snf, map_smul, repr_self, Finsupp.single_eq_pi_single]
    ext j
    simp [Pi.single_apply]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
⊢ N.toAddSubgroup.index = Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps✝ : {i : I} → A i →ₐ[R] B
maps : FreeProduct R A →ₐ[R] B
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext i a

Goal state after:
I : Type u
inst✝⁵ : DecidableEq I
i✝ : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps✝ : {i : I} → A i →ₐ[R] B
maps : FreeProduct R A →ₐ[R] B
i : I
a : A i
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
f : FreeProduct R A →ₐ[R] B
h : ∀ (i : I), f ∘ₐ ι R A i = maps
⊢ f = (lift R A) fun {i} ↦ maps

Tactic:
ext i a

Goal state after:
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)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
f : FreeProduct R A →ₐ[R] B
h : ∀ (i : I), f ∘ₐ ι R A i = maps
i : I
a : A i
⊢ (((f ∘ₐ RingCon.mkₐ R (ringCon R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a =
    (((((lift R A) fun {i} ↦ maps) ∘ₐ RingCon.mkₐ R (ringCon R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ
        DirectSum.lof R I A i)
      a
Module: Mathlib.LinearAlgebra.Matrix.CharP

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : DecidableEq n
inst✝¹ : Nonempty n
p : ℕ
inst✝ : CharP R p
k : ℕ
⊢ ↑k = 0 ↔ p ∣ k

Tactic:
by simp_rw [← diagonal_natCast, ← diagonal_zero, diagonal_eq_diagonal_iff,
    CharP.cast_eq_zero_iff R p k, forall_const]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ detMonoidHom ((expand K (Fintype.card K)).mapMatrix (M ^ Fintype.card K).charmatrix) =
    detMonoidHom M.charmatrix ^ Fintype.card K

Tactic:
← (detMonoidHom : Matrix n n K[X] →* K[X]).map_pow

Goal state after:
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ detMonoidHom ((expand K (Fintype.card K)).mapMatrix (M ^ Fintype.card K).charmatrix) =
    detMonoidHom (M.charmatrix ^ Fintype.card K)
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case neg
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Sort u_3
base : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 = 0 → C A
step : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 ≠ 0 → C (reduceStep A) → C A
A : FixedDetMatrix (Fin 2) ℤ m
h : ¬↑A 1 0 = 0
⊢ C A

Tactic:
· exact step A h (reduce_rec base step (reduceStep A))

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

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ¬↑A 1 0 = 0
⊢ (↑(reduceStep A) 1 0).natAbs < (↑A 1 0).natAbs

Tactic:
decreasing_by
    zify
    exact reduce_aux h

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
⊢ A.den ≠ 0

Tactic:
simp [Matrix.den, Finset.lcm_eq_zero_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
A : Matrix n n R
inst✝ : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ j, 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ y, j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₁ : Path i v
p₂ : Path v j
_hp_eq : p = p₁.comp p₂
hp₁_len : p₁.length = 1
hlen_ne : p₁.length ≠ 0
⊢ False

Tactic:
obtain ⟨c, p', e, rfl⟩ := (Quiver.Path.length_ne_zero_iff_eq_cons (p := p₁)).1 (by lia)

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
A : Matrix n n R
inst✝ : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ j, 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ y, j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₂ : Path v j
c : n
p' : Path i c
e : c ⟶ v
_hp_eq : p = (p'.cons e).comp p₂
hp₁_len : (p'.cons e).length = 1
hlen_ne : (p'.cons e).length ≠ 0
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
⊢ A.IsIrreducible ↔ ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j

Tactic:
by
  let : Quiver n := toQuiver A
  constructor
  · intro h_irr i j
    obtain ⟨p, hp_len⟩ := h_irr.2 i j
    refine ⟨p.length, hp_len, ?_⟩
    have : Nonempty {q : Path i j // q.length = p.length} := ⟨⟨p, rfl⟩⟩
    have hpos :=
      (pow_apply_pos_iff_nonempty_path (A := A) hA p.length i j).2 this
    simpa using hpos
  · intro h_exists
    constructor
    · exact hA
    · intro i j
      obtain ⟨k, hk_pos, hk_entry⟩ := h_exists i j
      obtain ⟨⟨p, rfl⟩⟩ :=
        (pow_apply_pos_iff_nonempty_path (A := A) hA k i j).mp hk_entry
      exact ⟨p, hk_pos⟩

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

Goal state before:
pp: case pos
α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
g : i = j
⊢ Aᵀ i j = A i j

pp: case neg
α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
g : ¬i = j
⊢ Aᵀ i j = A i j

Tactic:
· rw [g, transpose_apply]

Goal state after:
case neg
α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
g : ¬i = j
⊢ Aᵀ i j = A i j
Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual

Goal state before:
pp: ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), Finite (κ i)
b : (i : ι) → Basis (κ i) R (M i)
this✝ : Fintype ι
this : (i : ι) → Fintype (κ i)
p : (i : ι) → κ i
⊢ (dualDistribInvOfBasis b ∘ₗ dualDistrib) ((Basis.piTensorProduct fun i ↦ (b i).dualBasis) p) =
    LinearMap.id ((Basis.piTensorProduct fun i ↦ (b i).dualBasis) p)

Tactic:
refine (Basis.piTensorProduct (fun i => (b i).dualBasis)).ext_elem (fun q ↦ ?_)

Goal state after:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), Finite (κ i)
b : (i : ι) → Basis (κ i) R (M i)
this✝ : Fintype ι
this : (i : ι) → Fintype (κ i)
p q : (i : ι) → κ i
⊢ ((Basis.piTensorProduct fun i ↦ (b i).dualBasis).repr
        ((dualDistribInvOfBasis b ∘ₗ dualDistrib) ((Basis.piTensorProduct fun i ↦ (b i).dualBasis) p)))
      q =
    ((Basis.piTensorProduct fun i ↦ (b i).dualBasis).repr
        (LinearMap.id ((Basis.piTensorProduct fun i ↦ (b i).dualBasis) p)))
      q
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → CommSemiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
x y : ⨂[R] (i : ι), A i
⊢ (mul x) y = (mul y) x

Tactic:
suffices mul (R := R) (A := A) = mul.flip from
    DFunLike.congr_fun (DFunLike.congr_fun this x) y

Goal state after:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → CommSemiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
x y : ⨂[R] (i : ι), A i
⊢ mul = mul.flip
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝³ : CommSemiring R
inst✝² : (i : ι) → CommSemiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : Fintype ι
toFun : (⨂[R] (i : ι), R) →ₗ[R] R := lift (MultilinearMap.mkPiAlgebra R ι R)
this✝ : IsScalarTower R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := IsScalarTower.right
this : SMulCommClass R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := Algebra.to_smulCommClass
⊢ ∀ (x y : ⨂[R] (x : ι), R), toFun (x * y) = toFun x * toFun y

Tactic:
rw [LinearMap.map_mul_iff]

Goal state after:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝³ : CommSemiring R
inst✝² : (i : ι) → CommSemiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : Fintype ι
toFun : (⨂[R] (i : ι), R) →ₗ[R] R := lift (MultilinearMap.mkPiAlgebra R ι R)
this✝ : IsScalarTower R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := IsScalarTower.right
this : SMulCommClass R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := Algebra.to_smulCommClass
⊢ (LinearMap.mul R (⨂[R] (x : ι), R)).compr₂ toFun = (LinearMap.mul R R ∘ₗ toFun).compl₂ toFun
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
f : ι → ℙ K V
⊢ Dependent f → ¬LinearIndependent K (Projectivization.rep ∘ f)

pp: case refine_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ Dependent f

Tactic:
· rintro ⟨ff, hff, hh1⟩
    contrapose hh1
    choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i)
    convert! hh1.units_smul a⁻¹
    ext i
    simp only [← ha, inv_smul_smul, Pi.smul_apply', Pi.inv_apply, Function.comp_apply]

Goal state after:
case refine_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ Dependent f
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
⊢ (fun s ↦
        { carrier := {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}, add_mem' := ⋯, zero_mem' := ⋯,
          smul_mem' := ⋯ })
      ((fun s ↦ { carrier := Set.ofPred (Projectivization.lift (fun x ↦ ↑x ∈ s) ⋯), mem_add' := ⋯ }) s) =
    s

Tactic:
ext x
    suffices x = 0 → x ∈ s by
      simpa [imp_iff_not_or]
    rintro rfl
    exact s.zero_mem

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
⊢ A * B = B * A

Tactic:
refine Subtype.ext <| ext_iff_smul.2 fun w ↦ ?_

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
⊢ ↑(A * B) • w = ↑(B * A) • w
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
i : ι
⊢ w i / |↑(u i)| = ↑(sign (w i))

Tactic:
by
    by_cases hi : w i = 0
    · simp [hi]
    · simp only [hi, ↓reduceDIte, Units.val_mk0, u]; field_simp; simp

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
⊢ (forget₂ (QuadraticModuleCat R) (ModuleCat R)).map (λ_ X).hom =
    (((Iso.refl
              ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj (𝟙_ (QuadraticModuleCat R)) ⊗
                (forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X)).symm ≪≫
          ((Iso.refl (𝟙_ (ModuleCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X))) ≪≫
        λ_ ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X)).hom

Tactic:
simp only [forget₂_obj, forget₂_map, Iso.refl_symm, Iso.trans_assoc, Iso.trans_hom,
          Iso.refl_hom, MonoidalCategory.tensorIso_hom, MonoidalCategory.tensorHom_id]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X : QuadraticModuleCat R
⊢ ModuleCat.ofHom (Hom.toIsometry (λ_ X).hom).toLinearMap =
    𝟙 (ModuleCat.of R ↑(𝟙_ (QuadraticModuleCat R)).toModuleCat ⊗ ModuleCat.of R ↑X.toModuleCat) ≫
      𝟙 (𝟙_ (ModuleCat R)) ▷ ModuleCat.of R ↑X.toModuleCat ≫ (λ_ (ModuleCat.of R ↑X.toModuleCat)).hom
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ ({i | w i < 0} ∪ {i | w i = 0}).ncard = {i | w i ≤ 0}.ncard

pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ Disjoint {i | w i < 0} {i | w i = 0}

Tactic:
· congr! 1
      ext
      grind

Goal state after:
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ Disjoint {i | w i < 0} {i | w i = 0}
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ { toSubmodule := span R (range h), lie_mem' := ⋯ } ≤ lieAlgebra b

Tactic:
lieAlgebra,

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✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ { toSubmodule := span R (range h), lie_mem' := ⋯ } ≤
    LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h ∪ range e ∪ range f)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : 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 ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
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)
hw₀ : genWeightSpace (↥b.support ⊕ ι → K) χ = ⊥
⊢ w = 0

Tactic:
LieSubmodule.eq_bot_iff

Goal state after:
ι : 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 ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
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)
hw₀ : ∀ m ∈ genWeightSpace (↥b.support ⊕ ι → K) χ, m = 0
⊢ w = 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : 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 ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
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)
l : ↥b.support
hl : χ (h' l) ≠ 0
hw₀ : ∀ (i : ι), w (Sum.inr i) = 0
this : ∀ (i : ↥b.support), w (Sum.inl i) = 0
⊢ w = 0

Tactic:
by ext (k | k) <;> simp [hw₀, this]

Goal state after:
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
hij' : ↑i ≠ ↑j
this✝ : InvolutiveNeg ι := P.indexNeg
k : ι
this :
  ((if k = ↑i then ↑|b.cartanMatrix i j| else 0) -
      ∑ x,
        if P.root x = P.root ↑i + P.root ↑j ∧ P.root k = P.root x - P.root ↑j then ↑(chainTopCoeff (↑j) x) + 1 else 0) =
    0
⊢ ⁅e i, f j⁆ᵀ (Sum.inr ↑j) (Sum.inr k) = 0 (Sum.inr k)

Tactic:
have hij : (j : ι) ≠ -i := by simpa using b.root_ne_neg_of_ne j.property i.property hij'.symm

Goal state after:
ι : 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
hij' : ↑i ≠ ↑j
this✝ : InvolutiveNeg ι := P.indexNeg
k : ι
this :
  ((if k = ↑i then ↑|b.cartanMatrix i j| else 0) -
      ∑ x,
        if P.root x = P.root ↑i + P.root ↑j ∧ P.root k = P.root x - P.root ↑j then ↑(chainTopCoeff (↑j) x) + 1 else 0) =
    0
hij : ↑j ≠ -↑i
⊢ ⁅e i, f j⁆ᵀ (Sum.inr ↑j) (Sum.inr k) = 0 (Sum.inr k)