mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case mp.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
p : ↥s
c : P
r : k
h : Nonempty ↥s
q x : P
hx : x ∈ s
heq : (1 - r) • (c -ᵥ ↑⋯.some) +ᵥ x = q
⊢ (1 - r) • (c -ᵥ ↑p) +ᵥ (1 - r) • (↑p -ᵥ ↑h.some) +ᵥ x = (1 - r) • (c -ᵥ ↑⋯.some) +ᵥ x

Tactic:
rw [vadd_vadd, ← smul_add, vsub_add_vsub_cancel]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case mpr.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
p : ↥s
c : P
r : k
h : Nonempty ↥s
q x : P
hx : x ∈ s
heq : (1 - r) • (c -ᵥ ↑p) +ᵥ x = q
⊢ (1 - r) • (c -ᵥ ↑⋯.some) +ᵥ (1 - r) • (↑h.some -ᵥ ↑p) +ᵥ x = (1 - r) • (c -ᵥ ↑p) +ᵥ x

Tactic:
rw [vadd_vadd, ← smul_add, vsub_add_vsub_cancel]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝¹² : CommSemiring R
S : Type u_2
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
M : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
⊢ IsBaseChange S (compRight R ε)

Tactic:
apply of_equiv (linearMapRightBaseChangeEquiv M ibc)
  intro f
  simp [linearMapRightBaseChangeEquiv, linearMapRightBaseChangeHom]

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

Goal state before:
pp: case neg
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
⊢ e ∈ transvections K V

Tactic:
have hf' : e.fixedSubmodule = LinearMap.ker f := by
      suffices finrank K (V ⧸ LinearMap.ker f) = 1 by
        apply Submodule.eq_of_le_of_finrank_le
        · intro x
          rw [mem_ker, ← Submodule.mem_bot K, ← hf]
          exact mem_map_of_mem
        rw [← Nat.add_le_add_iff_right, finrank_quotient_add_finrank] at he
        have := (LinearMap.ker f).finrank_quotient_add_finrank
        linarith
      rw [← Nat.add_left_inj, Submodule.finrank_quotient_add_finrank]
      rw [← f.finrank_ker_add_one_of_ne_zero, add_comm]
      aesop

Goal state after:
case neg
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
⊢ e ∈ transvections K V
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
hy :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝ +
      (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝ +
      ((foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝)

Tactic:
hy

Goal state after:
case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
hy :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝ +
      ((foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝) =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝ +
      ((foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) ((ι Q) m✝ * x✝) =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) ((ι Q) m✝ * x✝) + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) ((ι Q) m✝ * x✝)

Tactic:
rw [foldr'_ι_mul, foldr'_ι_mul, foldr'_ι_mul, hx]

Goal state after:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
⊢ ((contractLeftAux Q (d₁ + d₂)) m✝)
      (x✝, (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝) =
    ((contractLeftAux Q d₁) m✝) (x✝, (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝) +
      ((contractLeftAux Q d₂) m✝) (x✝, (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝
hy : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) y✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) y✝
⊢ c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) y✝ =
    c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝ + c • (foldr' Q (contractLeftAux Q d) ⋯ 0) y✝

Tactic:
hy

Goal state after:
case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝
hy : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) y✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) y✝
⊢ c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝ + c • (foldr' Q (contractLeftAux Q d) ⋯ 0) y✝ =
    c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝ + c • (foldr' Q (contractLeftAux Q d) ⋯ 0) y✝
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : M
b : CliffordAlgebra Q
⊢ (contractRight (b * (ι Q) a)) d = d a • b - (contractRight b) d * (ι Q) a

Tactic:
rw [contractRight_eq, reverse.map_mul, reverse_ι, contractLeft_ι_mul, map_sub, map_smul,
    reverse_reverse, reverse.map_mul, reverse_ι, contractRight_eq]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: r : ℝ
⊢ (LinearMap.toSpanSingleton ℝ ℂ Complex.I) r * (LinearMap.toSpanSingleton ℝ ℂ Complex.I) r = (algebraMap ℝ ℂ) (Q r)

Tactic:
dsimp [LinearMap.toSpanSingleton, LinearMap.id]

Goal state after:
r : ℝ
⊢ ↑r * Complex.I * (↑r * Complex.I) = ↑(-(r * r))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (algebraMap R (CliffordAlgebra (Q c₁ c₂))) (QuadraticMap.polar ⇑(Q c₁ c₂) (0, 1) (1, 0)) = 0

Tactic:
QuadraticMap.polar

Goal state after:
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (algebraMap R (CliffordAlgebra (Q c₁ c₂))) ((Q c₁ c₂) ((0, 1) + (1, 0)) - (Q c₁ c₂) (0, 1) - (Q c₁ c₂) (1, 0)) = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h) ((contractLeft d) x✝) = (contractLeft d) ((changeForm h) x✝)
hy : (changeForm h) ((contractLeft d) y✝) = (contractLeft d) ((changeForm h) y✝)
⊢ (contractLeft d) ((changeForm h) x✝) + (changeForm h) ((contractLeft d) y✝) =
    (contractLeft d) ((changeForm h) x✝) + (contractLeft d) ((changeForm h) y✝)

Tactic:
hy

Goal state after:
case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h) ((contractLeft d) x✝) = (contractLeft d) ((changeForm h) x✝)
hy : (changeForm h) ((contractLeft d) y✝) = (contractLeft d) ((changeForm h) y✝)
⊢ (contractLeft d) ((changeForm h) x✝) + (contractLeft d) ((changeForm h) y✝) =
    (contractLeft d) ((changeForm h) x✝) + (contractLeft d) ((changeForm h) y✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm ⋯) x✝ = x✝
hy : (changeForm ⋯) y✝ = y✝
⊢ x✝ + (changeForm ⋯) y✝ = x✝ + y✝

Tactic:
hy

Goal state after:
case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm ⋯) x✝ = x✝
hy : (changeForm ⋯) y✝ = y✝
⊢ x✝ + y✝ = x✝ + y✝
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
hy : (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) y✝
⊢ (changeForm ⋯) x✝ + (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) x✝ + (changeForm ⋯) y✝

Tactic:
hy

Goal state after:
case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
hy : (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) y✝
⊢ (changeForm ⋯) x✝ + (changeForm ⋯) y✝ = (changeForm ⋯) x✝ + (changeForm ⋯) y✝
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
⊢ LinearMap.det (transvection f v) = 1 + f v

Tactic:
set M := Fin n → S

Goal state after:
case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
⊢ LinearMap.det (transvection f v) = 1 + f v
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
a : 𝒜 0
b : ⨁ (i : ι), ℬ i
⊢ ↑(gradedComm R 𝒜 ℬ) ∘ₗ (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i)) ((lof R ι 𝒜 0) a) =
    (mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i)).flip ((lof R ι 𝒜 0) a)

Tactic:
ext i b

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
a : 𝒜 0
b✝ : ⨁ (i : ι), ℬ i
i : ι
b : ℬ i
⊢ ((↑(gradedComm R 𝒜 ℬ) ∘ₗ (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i)) ((lof R ι 𝒜 0) a)) ∘ₗ lof R ι ℬ i) b =
    ((mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i)).flip ((lof R ι 𝒜 0) a) ∘ₗ lof R ι ℬ i) b
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x✝ : (CliffordAlgebra Q)ˣ
hx✝ : x✝ ∈ lipschitzGroup Q
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
⊢ Submodule.map (DistribSMul.toLinearMap R (CliffordAlgebra Q) (ConjAct.toConjAct x)) (ι Q).range ≤ (ι Q).range

Tactic:
Submodule.map_le_iff_le_comap

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x✝ : (CliffordAlgebra Q)ˣ
hx✝ : x✝ ∈ lipschitzGroup Q
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
⊢ (ι Q).range ≤ Submodule.comap (DistribSMul.toLinearMap R (CliffordAlgebra Q) (ConjAct.toConjAct x)) (ι Q).range
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
m : ℕ
I : Type u_3
inst✝³ : LinearOrder I
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : Basis I R M
s : ↑(powersetCard I m)
⊢ b.ExteriorAlgebra ↑s = ιMulti_family R m (⇑b) s

Tactic:
by
  simp [basis_apply_ofCard]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case neg
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : PartialOrder m
hA : A.IsPivotedBy l
i₁ i₂ : m
hlt : i₁ < i₂
h₁ : ¬l i₁ = ⊤
⊢ l i₁ ≤ l i₂

Tactic:
· exact (hA.lt_of_lt_of_ne_top hlt h₁).le

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case pos.refine_1
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (g x) ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    (-1) ^ (↑i + ↑x) * ↑s * (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ -1 ∈ MonoidHom.mrange ↑SignType.castHom

Tactic:
exact ⟨-1, by simp⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Goal state before:
pp: 𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
M : GL (Fin n) 𝔽
⊢ Fintype.card (Fin n) = Set.finrank 𝔽 (Set.range (↑M).col)

Tactic:
rw [Set.finrank, ← rank_eq_finrank_span_cols, rank_unit]

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

Goal state before:
pp: case neg.refine_2
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ |-↑A 0 1 % ↑A 1 1| < |↑A 1 1|

Tactic:
abs_eq_self.mpr <| Int.emod_nonneg _ hd

Goal state after:
case neg.refine_2
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ -↑A 0 1 % ↑A 1 1 < |↑A 1 1|
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case succ.mp
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
this : Quiver n := ⋯
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
⊢ 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j → Nonempty { p // p.length = m + 1 }

Tactic:
intro h_pos
      obtain ⟨l, hl_mem, hl_pos⟩ :
          ∃ l ∈ (Finset.univ : Finset n), 0 < (A ^ m) i l * A l j := by
        simpa [Finset.sum_pos_iff_of_nonneg
                 (fun x _ => mul_nonneg (pow_apply_nonneg hA m i x) (hA x j))]
          using h_pos
      have hAm_nonneg : 0 ≤ (A ^ m) i l := pow_apply_nonneg hA m i l
      have hA_nonneg' : 0 ≤ A l j := hA l j
      have h_Am : 0 < (A ^ m) i l := by by_contra! h; simp [le_antisymm h hAm_nonneg] at hl_pos
      have h_A : 0 < A l j := by by_contra! h; simp [le_antisymm h hA_nonneg'] at hl_pos
      obtain ⟨⟨p, rfl⟩⟩ := (ih i l).mp h_Am
      exact ⟨p.cons (PLift.up h_A), by simp⟩

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
e₁ e₂ : m ≃ n
h : A.IsHadamard
⊢ (A.submatrix ⇑e₁ ⇑e₂).IsHadamard

Tactic:
simpa [reindex_apply] using h.reindex e₁.symm e₂.symm

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✝² : CommRing R
inst✝¹ : StarRing R
A : Matrix n n R
inst✝ : IsReduced R
hA : A.IsHadamard
hcard : ↑(Fintype.card n) ≠ 0
h : A.det = 0
⊢ ↑(Fintype.card n) ^ ?m.29 h = 0

Tactic:
← hA.det_mul_star_det,

Goal state after:
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : StarRing R
A : Matrix n n R
inst✝ : IsReduced R
hA : A.IsHadamard
hcard : ↑(Fintype.card n) ≠ 0
h : A.det = 0
⊢ A.det * star A.det = 0
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: case add
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x✝ y✝ : ⨂[R] (i : ι), A i
h1 : (mul x✝) ((tprod R) 1) = x✝
h2 : (mul y✝) ((tprod R) 1) = y✝
⊢ (mul (x✝ + y✝)) ((tprod R) 1) = x✝ + y✝

Tactic:
simp [h1, h2]

Goal state after:
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
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
have : Fintype V := Fintype.ofFinite V
  have : Fintype (ℙ k V) := Fintype.ofFinite (ℙ k V)
  have : Fintype k := Fintype.ofFinite k
  have hV : Fintype.card { v : V // v ≠ 0 } = Fintype.card V - 1 := by simp
  simp_rw [← Fintype.card_eq_nat_card, ← Fintype.card_units (α := k), ← hV]
  rw [Fintype.card_congr (nonZeroEquivProjectivizationProdUnits k V), Fintype.card_prod]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : SpecialLinearGroup R V
hg : g ∈ Subgroup.center (SpecialLinearGroup R V)
x : V
⊢ ↑↑g x = ⋯.choose • x

Tactic:
let H := (mem_center_iff.mp hg).choose_spec.2

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : SpecialLinearGroup R V
hg : g ∈ Subgroup.center (SpecialLinearGroup R V)
x : V
H : ↑↑g = ⋯.choose • LinearMap.id := (Exists.choose_spec (mem_center_iff.mp hg)).right
⊢ ↑↑g x = ⋯.choose • x
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : Matrix.ProjectiveSpecialLinearGroup ι K
hg :
  g ∈
    (QuotientGroup.lift (Subgroup.center (Matrix.SpecialLinearGroup ι K))
        (toPermHom (Matrix.SpecialLinearGroup ι K) (ℙ K (ι → K))) ⋯).ker
⊢ g = 1

Tactic:
QuotientGroup.ker_lift,

Goal state after:
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : Matrix.ProjectiveSpecialLinearGroup ι K
hg :
  g ∈
    Subgroup.map (QuotientGroup.mk' (Subgroup.center (Matrix.SpecialLinearGroup ι K)))
      (toPermHom (Matrix.SpecialLinearGroup ι K) (ℙ K (ι → K))).ker
⊢ g = 1
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✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ((Q.toBilin bm) (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)) (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a) =
    Q (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)

Tactic:
LinearMap.map_sum₂,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ∑ i ∈ (bm.repr x).support, ((Q.toBilin bm) ((bm.repr x) i • bm i)) (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a) =
    Q (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
x y : M
hx : x ∈ {x | Q x = 0 ∧ Q.polarBilin x = 0}
hy : y ∈ {x | Q x = 0 ∧ Q.polarBilin x = 0}
⊢ x + y ∈ {x | Q x = 0 ∧ Q.polarBilin x = 0}

Tactic:
by
    refine ⟨?_, by simp [hx.2, hy.2]⟩
    have := congr_arg (· y) hx.2
    simp only [QuadraticMap.polarBilin_apply_apply, QuadraticMap.polar,
      LinearMap.zero_apply, sub_sub, sub_eq_zero] at this
    rw [this, hx.1, hy.1, zero_add]

Goal state after: