mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: case h
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hf : StronglyMeasurable klFun
⊢ ∫ (x : 𝓧), klFun (ν[fun x ↦ ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] x) ∂ν ≤
    ∫ (x : 𝓧), ν[fun x ↦ klFun ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] x ∂ν

Tactic:
have hf_cont : ContinuousWithinAt klFun (Ici 0) 0 := by fun_prop

Goal state after:
case h
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hf : StronglyMeasurable klFun
hf_cont : ContinuousWithinAt klFun (Ici 0) 0
⊢ ∫ (x : 𝓧), klFun (ν[fun x ↦ ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] x) ∂ν ≤
    ∫ (x : 𝓧), ν[fun x ↦ klFun ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] x ∂ν
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: 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
h : Nonempty ↥s
c : P
⊢ s.shift c 0 = mk' c s.direction

Tactic:
by
  refine ext_of_direction_eq (by simp) ⟨c, ?_⟩
  suffices ∃ x ∈ s, (c -ᵥ h.some) +ᵥ x = c by simpa [shift, h]
  exact ⟨h.some, by simp⟩

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
⊢ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) x) =
    ⇑(homothety (s.points i) x) '' (s.faceOpposite i).closedInterior

Tactic:
rcases hx.1.eq_or_lt with hx0 | hxpos

Goal state after:
case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hx0 : 0 = x
⊢ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) x) =
    ⇑(homothety (s.points i) x) '' (s.faceOpposite i).closedInterior

case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
⊢ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) x) =
    ⇑(homothety (s.points i) x) '' (s.faceOpposite i).closedInterior
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
⊢ f x * (↑(-h.unit⁻¹) + 1 + ↑(-h.unit⁻¹) * f v) = 0

Tactic:
add_comm _ 1,

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
⊢ f x * (1 + ↑(-h.unit⁻¹) + ↑(-h.unit⁻¹) * f v) = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ (BilinForm.tensorDistrib R A) (((2 • ⅟2) • LinearMap.mul A A) ⊗ₜ[R] polarBilin Q) =
    BilinForm.tmul (LinearMap.mul A A) (polarBilin Q)

Tactic:
two_smul,

Goal state after:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ (BilinForm.tensorDistrib R A) (((⅟2 + ⅟2) • LinearMap.mul A A) ⊗ₜ[R] polarBilin Q) =
    BilinForm.tmul (LinearMap.mul A A) (polarBilin Q)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Star

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
⊢ (fun x ↦ reverse (involute x)) ((fun x ↦ reverse (involute x)) x) = x

Tactic:
simp only [reverse_involute_commute.eq, reverse_reverse, involute_involute]

Goal state after:
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 d' d₁ d₂ : Module.Dual R M
x : CliffordAlgebra Q
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0 + foldr' Q (contractLeftAux Q d₂) ⋯ 0) x

Tactic:
by
      rw [LinearMap.add_apply]
      induction x using CliffordAlgebra.left_induction with
      | algebraMap => simp_rw [foldr'_algebraMap, smul_zero, zero_add]
      | add _ _ hx hy => rw [map_add, map_add, map_add, add_add_add_comm, hx, hy]
      | ι_mul _ _ hx =>
        rw [foldr'_ι_mul, foldr'_ι_mul, foldr'_ι_mul, hx]
        dsimp only [contractLeftAux_apply_apply]
        rw [sub_add_sub_comm, mul_add, LinearMap.add_apply, add_smul]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ CliffordAlgebra Q →ₐ[R] ↥(even (Q' Q))

Tactic:
by
  refine CliffordAlgebra.lift Q ⟨?_, fun m => ?_⟩
  · refine LinearMap.codRestrict _ ?_ fun m => Submodule.mem_iSup_of_mem ⟨2, rfl⟩ ?_
    · exact (LinearMap.mulLeft R <| e0 Q).comp (v Q)
    rw [Subtype.coe_mk, pow_two]
    exact Submodule.mul_mem_mul (LinearMap.mem_range_self _ _) (LinearMap.mem_range_self _ _)
  · ext1
    simp only [Subalgebra.coe_mul, ← even_toSubmodule]
    rw [LinearMap.codRestrict_apply]
    simp [← mul_assoc, v_sq_scalar]

Goal state after:
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) ℤ
⊢ LinearMap.det (transvection f v) = 1 + f v

Tactic:
let γ : S →+* R :=
    (MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) (fun i ↦ b.coord i v)) :
      MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R)

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))
⊢ LinearMap.det (transvection f v) = 1 + f v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case mem.add
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
m₁' : CliffordAlgebra Q₁
i₁n : ℕ
x✝ y✝ : CliffordAlgebra Q₁
i✝ : ℕ
hx✝ : x✝ ∈ (ι Q₁).range ^ i✝
hy✝ : y✝ ∈ (ι Q₁).range ^ i✝
ihx : (map f₁) x✝ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) x✝)
ihy : (map f₁) y✝ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) y✝)
⊢ (map f₁) (x✝ + y✝) * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) (x✝ + y✝))

Tactic:
| add _ _ _ _ _ ihx ihy =>

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

Goal state before:
pp: case mem.mem_mul.e_a.e_a.mem.add
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
m₂' : CliffordAlgebra Q₂
i₂n : ℕ
x✝ y✝ : CliffordAlgebra Q₂
i✝ : ℕ
hx✝ : x✝ ∈ (ι Q₂).range ^ i✝
hy✝ : y✝ ∈ (ι Q₂).range ^ i✝
ihx : (ι Qₙ) (f₁ v₁) * (map f₂) x✝ = (-1) ^ ↑i✝ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁))
ihy : (ι Qₙ) (f₁ v₁) * (map f₂) y✝ = (-1) ^ ↑i✝ • ((map f₂) y✝ * (ι Qₙ) (f₁ v₁))
⊢ (ι Qₙ) (f₁ v₁) * (map f₂) (x✝ + y✝) = (-1) ^ ↑i✝ • ((map f₂) (x✝ + y✝) * (ι Qₙ) (f₁ v₁))

Tactic:
| add _ _ _ _ _ ihx ihy =>

Goal state after:
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)ˣ
⊢ ↑x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ↔ x ∈ lipschitzGroup Q

Tactic:
simp only [Submonoid.mem_map, Subgroup.mem_toSubmonoid, Units.coeHom_apply]

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)ˣ
⊢ (∃ x_1 ∈ lipschitzGroup Q, ↑x_1 = ↑x) ↔ x ∈ lipschitzGroup Q
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
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ star x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid

Tactic:
simp only [Submonoid.mem_map, Subgroup.mem_toSubmonoid, Units.coeHom_apply]

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
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ ∃ x_1 ∈ lipschitzGroup Q, ↑x_1 = star x
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : Ring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Module ι (Additive ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
⊢ F (↑a ᵍ⊗ₜ[R] 1 * 1 ᵍ⊗ₜ[R] ↑b) = (-1) ^ (j * i) • F ((-1) ^ (j * i) • ↑a ᵍ⊗ₜ[R] ↑b)

Tactic:
AlgHom.map_smul_of_tower,

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 : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
⊢ F (↑a ᵍ⊗ₜ[R] 1 * 1 ᵍ⊗ₜ[R] ↑b) = (-1) ^ (j * i) • (-1) ^ (j * i) • F (↑a ᵍ⊗ₜ[R] ↑b)
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✝ + y✝) = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨x✝ + y✝, ⋯⟩

Tactic:
| add _ _ _ _ _ ihx ihy =>

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend ⋯
b : Module.Basis (↑I) K (ι' → K) := Module.Basis.extend ⋯
b' : Module.Basis (↑I) L (ι' → L) := (Module.Basis.baseChange L b).map (piScalarRight K L L ι')
v' : ι → ↑I := fun i ↦ ⟨v i, ⋯⟩
hv' : ⇑b' ∘ v' = fun i ↦ ⇑(algebraMap K L) ∘ v i
i j : ι
hij : v' i = v' j
⊢ i = j

Tactic:
by have : Injective v := hv.injective; aesop

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
h : LinearIndependent R v
this : IsDomain R
⊢ LinearIndependent S (⇑(Pi.algebraMap ι' R S) ∘ v)

Tactic:
set K := FractionRing R

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
h : LinearIndependent R v
this : IsDomain R
K : Type u_3 := FractionRing R
⊢ LinearIndependent S (⇑(Pi.algebraMap ι' R S) ∘ v)
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 ℚ
i : m
j : n
⊢ ↑(A.num i j) / ↑A.den = A i j

Tactic:
obtain ⟨k, hk⟩ := den_dvd_iff.mp (dvd_refl A.den) i j

Goal state after:
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
⊢ ↑(A.num i j) / ↑A.den = A i j
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: case inl
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i : n
⊢ A.diag i = A i i

Tactic:
diag

Goal state after:
case inl
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i : n
⊢ A i i = A i i
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
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
⊢ Aᵀ.IsIrreducible

Tactic:
refine ⟨hA_T_nonneg, ?_⟩

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
⊢ IsSStronglyConnected n
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
D D' E E' : ℙ K V
hD : D ≠ D'
hE : E ≠ E'
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
⊢ ∃ g, g • D = E ∧ g • D' = E'

Tactic:
rw [← linearIndependent_pair_iff_ne] at hD hE

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
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
⊢ ∃ g, g • D = E ∧ g • D' = E'
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
⊢ ⊤ ≤ span Set.univ

Tactic:
SetLike.le_def

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ∀ ⦃x : ℙ K V⦄, x ∈ ⊤ → x ∈ span Set.univ
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: case inl
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
y : V
hy₁ : y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₁ : 0 ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
⊢ 0 + y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}

pp: case inr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
x y : V
hx₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hy₁ : y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₂ : x ≠ 0
⊢ x + y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}

Tactic:
· rwa [zero_add]

Goal state after:
case inr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
x y : V
hx₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hy₁ : y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₂ : x ≠ 0
⊢ x + y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
hp2 : mk K u hu ∈ Submodule.projectivization p
hp3 : mk K v hv ∈ Submodule.projectivization p
h1 : Submodule.span K {u, v} ≤ p
this : Module.Finite K ↥p
⊢ p = Submodule.span K {u, v}

Tactic:
refine Submodule.eq_of_le_of_finrank_eq h1 ?_ |>.symm

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
hp2 : mk K u hu ∈ Submodule.projectivization p
hp3 : mk K v hv ∈ Submodule.projectivization p
h1 : Submodule.span K {u, v} ≤ p
this : Module.Finite K ↥p
⊢ Module.finrank K ↥(Submodule.span K {u, v}) = Module.finrank K ↥p
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
A B : SpecialLinearGroup R V
⊢ LinearEquiv.det (↑A * ↑B) = 1

Tactic:
by simp [A.prop, B.prop]

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
A B : SpecialLinearGroup R V
⊢ LinearEquiv.det (↑A / ↑B) = 1

Tactic:
by simp [A.prop, B.prop]

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 : ↥(Subgroup.center (SpecialLinearGroup R V))
x : V
⊢ centerEquivRootsOfUnity g • x = ↑↑g x

Tactic:
rw [← LinearEquiv.coe_toLinearMap, centerEquivRootsOfUnity_apply]

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 : ↥(Subgroup.center (SpecialLinearGroup R V))
x : V
⊢ centerEquivRootsOfUnity g • x = (centerEquivRootsOfUnity g • LinearMap.id) x
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
⊢ (weightedSumSquares ℝ w).IsometryEquiv (weightedSumSquares ℝ fun i ↦ ↑(sign (w i)))

Tactic:
have hwu : ∀ i, w i / |(u i : ℝ)| = sign (w i) := fun i ↦ by
    by_cases hi : w i = 0
    · simp [hi]
    · simp only [hi, ↓reduceDIte, Units.val_mk0, u]; field_simp; simp

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
hu : ∀ (i : ι), 1 / √|↑(u i)| ≠ 0
hwu : ∀ (i : ι), w i / |↑(u i)| = ↑(sign (w i))
⊢ (weightedSumSquares ℝ w).IsometryEquiv (weightedSumSquares ℝ fun i ↦ ↑(sign (w i)))
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
N : Submodule R M
hN : N ≤ Q.radical
m m' : M
hmm' : N.quotientRel m m'
⊢ Q m = Q m'

Tactic:
by
  rw [Submodule.quotientRel_def] at hmm'
  rw [(by simp : m = m' + (m - m')), QuadraticMap.map_add Q m' (m - m'),
    (hN hmm').1, add_zero, polar_comm, ← polarBilin_apply_apply]
  simp [(hN hmm').2]

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

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module ℝ M
inst✝ : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
w : Fin (finrank ℝ M) → SignType
hw : Equivalent Q (weightedSumSquares ℝ fun i ↦ ↑(w i))
i : Fin (finrank ℝ M)
⊢ (fun x ↦ ↑(w x)) i = -1 ∨ (fun x ↦ ↑(w x)) i = 0 ∨ (fun x ↦ ↑(w x)) i = 1

Tactic:
cases h : w i <;> simp [h]

Goal state after:
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
m : M
h : 2 • Q m - Q m = 0
⊢ Q m = 0

Tactic:
two_smul,

Goal state after:
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
m : M
h : Q m + Q m - Q m = 0
⊢ Q m = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X Y Z : QuadraticModuleCat R
⊢ (forget₂ (QuadraticModuleCat R) (ModuleCat R)).map (α_ X Y Z).hom =
    (((Iso.refl
              ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj (X ⊗ Y) ⊗
                (forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj Z)).symm ≪≫
          ((Iso.refl
                ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X ⊗
                  (forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj Y)).symm ⊗ᵢ
            Iso.refl ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj Z))) ≪≫
        α_ ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X) ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj Y)
            ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj Z) ≪≫
          (Iso.refl ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X) ⊗ᵢ
              Iso.refl
                ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj Y ⊗
                  (forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj Z)) ≪≫
            Iso.refl
              ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X ⊗
                (forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj (Y ⊗ Z))).hom

Tactic:
by
        dsimp only [forget₂_obj, forget₂_map_associator_hom]
        simp only [Iso.refl_symm, Iso.trans_hom,
          MonoidalCategory.tensorIso_hom, Iso.refl_hom, MonoidalCategory.id_tensorHom_id]
        dsimp only [toModuleCat_tensor, ModuleCat.of_coe]
        rw [Category.id_comp, Category.id_comp, Category.comp_id, MonoidalCategory.id_tensorHom_id,
          Category.id_comp]

Goal state after: