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

Goal state before:
pp: 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
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
s : ℤˣ
⊢ detp s Ai = ∑ x, A.col (g x) i * detp (-s) (Aj x) + A.col j₀ i * detp s D

Tactic:
detp_option_expand_row_none,

Goal state after:
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
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
s : ℤˣ
⊢ Ai none none * detp s (Ai.submatrix some some) +
      ∑ k, Ai none (some k) * detp (-s) (Ai.submatrix some (Function.update some k none)) =
    ∑ x, A.col (g x) i * detp (-s) (Aj x) + A.col j₀ i * detp s D
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : ∀ (i : ι), Finite (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) = g.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this✝ : (i : ι) → Fintype (κ i)
this : DecidableEq ι
⊢ (f fun i ↦ ∑ i_1, Pi.single i_1 (x i i_1)) = g fun i ↦ ∑ i_1, Pi.single i_1 (x i i_1)

Tactic:
[

Goal state after:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : ∀ (i : ι), Finite (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) = g.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this✝ : (i : ι) → Fintype (κ i)
this : DecidableEq ι
⊢ (f fun i ↦ ∑ i_1, Pi.single i_1 (x i i_1)) = g fun i ↦ ∑ i_1, Pi.single i_1 (x i i_1)
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: case a
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : ∀ (i : ι), Finite (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) = g.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this✝ : (i : ι) → Fintype (κ i)
this : DecidableEq ι
p : (a : ι) → κ a
a✝ : p ∈ Fintype.piFinset fun i ↦ Finset.univ
⊢ (f fun i ↦ Pi.single (p i) (x i (p i))) = g fun i ↦ Pi.single (p i) (x i (p i))

Tactic:
[

Goal state after:
case a
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : ∀ (i : ι), Finite (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) = g.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this✝ : (i : ι) → Fintype (κ i)
this : DecidableEq ι
p : (a : ι) → κ a
a✝ : p ∈ Fintype.piFinset fun i ↦ Finset.univ
⊢ (f fun i ↦ Pi.single (p i) (x i (p i))) = g fun i ↦ Pi.single (p i) (x i (p i))
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
x y : (j : κ i) → M i j
p : (i : ι) → κ i
⊢ ((f p) fun i_1 ↦ Function.update m i (x + y) i_1 (p i_1)) =
    ((f p) fun i_1 ↦ Function.update m i x i_1 (p i_1)) + (f p) fun i_1 ↦ Function.update m i y i_1 (p i_1)

Tactic:
[

Goal state after:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
x y : (j : κ i) → M i j
p : (i : ι) → κ i
⊢ ((f p) fun i_1 ↦ Function.update m i (x + y) i_1 (p i_1)) =
    ((f p) fun i_1 ↦ Function.update m i x i_1 (p i_1)) + (f p) fun i_1 ↦ Function.update m i y i_1 (p i_1)
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
c : R
x : (j : κ i) → M i j
p : (i : ι) → κ i
⊢ ((f p) fun i_1 ↦ Function.update m i (c • x) i_1 (p i_1)) = c • (f p) fun i_1 ↦ Function.update m i x i_1 (p i_1)

Tactic:
[

Goal state after:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
c : R
x : (j : κ i) → M i j
p : (i : ι) → κ i
⊢ ((f p) fun i_1 ↦ Function.update m i (c • x) i_1 (p i_1)) = c • (f p) fun i_1 ↦ Function.update m i x i_1 (p i_1)
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: case inr
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
i : ι
hpqi : p i ≠ q i
⊢ Pi.single (p i) (m i) (q i) = 0

Tactic:
[

Goal state after:
case inr
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
i : ι
hpqi : p i ≠ q i
⊢ Pi.single (p i) (m i) (q i) = 0
Module: Mathlib.LinearAlgebra.Matrix.WithConv

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : IsIdempotentElem f
⊢ IsSelfAdjoint f

Tactic:
[

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : IsIdempotentElem f
⊢ IsSelfAdjoint f
Module: Mathlib.LinearAlgebra.Multilinear.DirectSum

Goal state before:
pp: R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝⁵ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : MultilinearMap R (fun i ↦ ⨁ (j : κ i), M i j) M'
p : (i : ι) → κ i
this : Fintype ι
⊢ fromDirectSumEquiv.symm f p = f.compLinearMap fun i ↦ lof R (κ i) (M i) (p i)

Tactic:
[

Goal state after:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝⁵ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : MultilinearMap R (fun i ↦ ⨁ (j : κ i), M i j) M'
p : (i : ι) → κ i
this : Fintype ι
⊢ fromDirectSumEquiv.symm f p = f.compLinearMap fun i ↦ lof R (κ i) (M i) (p i)
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝³ : DecidableEq ι
M : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i₀ : ι
m : (i : ι) → M i
⊢ (reindex R M (Equiv.subtypeNeSumPUnit i₀).symm) (⨂ₜ[R] (i : ι), m i) =
    (tprod R) fun j ↦ m ((Equiv.subtypeNeSumPUnit i₀) j)

Tactic:
[

Goal state after:
R : Type u_1
ι : Type u_2
inst✝³ : DecidableEq ι
M : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i₀ : ι
m : (i : ι) → M i
⊢ (reindex R M (Equiv.subtypeNeSumPUnit i₀).symm) (⨂ₜ[R] (i : ι), m i) =
    (tprod R) fun j ↦ m ((Equiv.subtypeNeSumPUnit i₀) j)
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
⊢ toFun (((tprod R) fun x ↦ 1) * (tprod R) fun x ↦ 1) = toFun ((tprod R) fun x ↦ 1) * toFun ((tprod R) fun x ↦ 1)

Tactic:
[

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
⊢ toFun (((tprod R) fun x ↦ 1) * (tprod R) fun x ↦ 1) = toFun ((tprod R) fun x ↦ 1) * toFun ((tprod R) fun x ↦ 1)
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
a✝ : Nontrivial V
h✝ : Finite k
h : Infinite V
this : Infinite (ℙ k V) ↔ Infinite V
⊢ Infinite (ℙ k V)

Tactic:
this

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Infinite V
this : Infinite (ℙ k V) ↔ Infinite V
⊢ Infinite V
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: case inl.inl
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Finite V
this✝¹ : Fintype V
this✝ : Fintype (ℙ k V)
this : Fintype k
hV : Fintype.card { v // v ≠ 0 } = Fintype.card V - 1
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
[

Goal state after:
case inl.inl
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Finite V
this✝¹ : Fintype V
this✝ : Fintype (ℙ k V)
this : Fintype k
hV : Fintype.card { v // v ≠ 0 } = Fintype.card V - 1
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
g g' : G
x : ℙ K V
⊢ map ((DistribMulAction.toModuleEnd K V) (g * g')) ⋯ x =
    map ((DistribMulAction.toModuleEnd K V) g) ⋯ (map ((DistribMulAction.toModuleEnd K V) g') ⋯ x)

Tactic:
[

Goal state after:
G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
g g' : G
x : ℙ K V
⊢ map ((DistribMulAction.toModuleEnd K V) (g * g')) ⋯ x =
    map ((DistribMulAction.toModuleEnd K V) g) ⋯ (map ((DistribMulAction.toModuleEnd K V) g') ⋯ x)
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 : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), S ⊆ ↑W → u ∈ W

Tactic:
[

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), S ⊆ ↑W → u ∈ W
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 : Set (ℙ K V)
x : ℙ K V
⊢ x ∈ (span S).carrier ↔ x ∈ (sInf {W | S ⊆ ↑W}).carrier

Tactic:
[

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
⊢ x ∈ (span S).carrier ↔ x ∈ (sInf {W | S ⊆ ↑W}).carrier
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case h.right
G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 0 1)) = D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 1 1)) = D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) := ⋯
this : FiniteDimensional K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg : ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))), ↑(f x) = g ↑x
⊢ g • D' = E'

Tactic:
· rw [← mk_rep D', ← mk_rep E', smul_mk, mk_eq_mk_iff]
    use 1
    simp only [one_smul, LinearEquiv.smul_def, ← qD' hD, ← hg, ← qD' hE]
    simp [f]

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

Goal state before:
pp: case pos
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
⊢ ∃ h, LinearEquiv.det h = a ∧ h • D = D ∧ h • D' = D'

Tactic:
rw [← mk_rep D, ← mk_rep D']

Goal state after:
case pos
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
⊢ ∃ h, LinearEquiv.det h = a ∧ h • mk K D.rep ⋯ = mk K D.rep ⋯ ∧ h • mk K D'.rep ⋯ = mk K D'.rep ⋯
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: case «0»
F : Type u_2
inst✝ : Field F
j : Fin 2
c : F
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

Tactic:
fin_cases j

Goal state after:
case «0».«0»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

case «0».«1»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: case «1»
F : Type u_2
inst✝ : Field F
j : Fin 2
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

Tactic:
fin_cases j

Goal state after:
case «1».«0»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

case «1».«1»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)
Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
K : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : DecidableEq K
w : ι → K
i : ι
h : ¬w i = 0
⊢ ⋯.choose * ⋯.choose ≠ 0

Tactic:
← (IsAlgClosed.exists_eq_mul_self (w i)).choose_spec

Goal state after:
ι : Type u_1
inst✝³ : Fintype ι
K : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : DecidableEq K
w : ι → K
i : ι
h : ¬w i = 0
⊢ w i ≠ 0
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : SpecialLinearGroup ι F
L : Submodule F (ι → F)
A : SpecialLinearGroup ι F
⊢ (∀ (w : ι → F), ∃ b ∈ L, g • b = A • w - w) ↔ ∀ (w : ι → F), (g⁻¹ * A * g) • w - w ∈ L

Tactic:
refine ⟨fun hA w ↦ ?_, fun hA w ↦ ⟨g⁻¹ • (A • w - w), ?_, by simp⟩⟩

Goal state after:
case refine_1
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : SpecialLinearGroup ι F
L : Submodule F (ι → F)
A : SpecialLinearGroup ι F
hA : ∀ (w : ι → F), ∃ b ∈ L, g • b = A • w - w
w : ι → F
⊢ (g⁻¹ * A * g) • w - w ∈ L

case refine_2
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : SpecialLinearGroup ι F
L : Submodule F (ι → F)
A : SpecialLinearGroup ι F
hA : ∀ (w : ι → F), (g⁻¹ * A * g) • w - w ∈ L
w : ι → F
⊢ g⁻¹ • (A • w - w) ∈ L
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
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
u : SpecialLinearGroup R V
x : V
c : R := (LinearEquiv.smul_id_of_finrank_eq_one d1).symm ↑↑u
hc : c = (LinearEquiv.smul_id_of_finrank_eq_one d1).symm ↑↑u
⊢ ↑↑u x = LinearMap.id x

Tactic:
rw [LinearEquiv.eq_symm_apply] at hc

Goal state after:
case neg
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
u : SpecialLinearGroup R V
x : V
c : R := (LinearEquiv.smul_id_of_finrank_eq_one d1).symm ↑↑u
hc : (LinearEquiv.smul_id_of_finrank_eq_one d1) c = ↑↑u
⊢ ↑↑u x = LinearMap.id x
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

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✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ Q ((linearCombination R g) l) =
    (linearCombination R (polarSym2 ⇑Q ∘ Sym2.map g)) l.sym2Mul - (linearCombination R (⇑Q ∘ g)) (l * l)

Tactic:
[

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✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ Q ((linearCombination R g) l) =
    (linearCombination R (polarSym2 ⇑Q ∘ Sym2.map g)) l.sym2Mul - (linearCombination R (⇑Q ∘ g)) (l * l)
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case inl
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = Module.finrank R V
h' : 1 ≤ Module.finrank R V
⊢ ↑↑r ^ Module.finrank R V = 1

Tactic:
[

Goal state after:
case inl
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = Module.finrank R V
h' : 1 ≤ Module.finrank R V
⊢ ↑↑r ^ Module.finrank R V = 1
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case inr
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = 1
h' : Module.finrank R V < 1
⊢ ↑↑r ^ Module.finrank R V = 1

Tactic:
[

Goal state after:
case inr
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = 1
h' : Module.finrank R V < 1
⊢ ↑↑r ^ Module.finrank R V = 1