mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner

Goal state before:
pp: case pos.refine_4
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
⊢ AEStronglyMeasurable (fun x ↦ (μ⁻[f | m] x).toReal) μ

Tactic:
exact StronglyMeasurable.aestronglyMeasurable (by fun_prop)

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: case refine_1
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ AEStronglyMeasurable (fun x ↦ f ((∂Measure.map g μ/∂Measure.map g ν) (g x)).toReal) ν

Tactic:
exact StronglyMeasurable.aestronglyMeasurable (by fun_prop)

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: case refine_1
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
hm : m ≤ m𝓧
hμν : μ ≪ ν
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ AEStronglyMeasurable (fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal) (ν.trim hm)

Tactic:
exact StronglyMeasurable.aestronglyMeasurable (by fun_prop)

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

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val✝ : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : ∑ i, w₁ i = 1
hw₂ : ∑ i, w₂ i = 1
hweq : (Finset.affineCombination k Finset.univ p) w₁ = (Finset.affineCombination k Finset.univ p) w₂
j : ι
⊢ (Finset.affineCombination k Finset.univ fun i ↦ (b.coord j) (p i)) w₁ =
    (Finset.affineCombination k Finset.univ fun i ↦ (b.coord j) (p i)) w₂

Tactic:
← Function.comp_def (b.coord j) p,

Goal state after:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val✝ : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : ∑ i, w₁ i = 1
hw₂ : ∑ i, w₂ i = 1
hweq : (Finset.affineCombination k Finset.univ p) w₁ = (Finset.affineCombination k Finset.univ p) w₂
j : ι
⊢ (Finset.affineCombination k Finset.univ (⇑(b.coord j) ∘ p)) w₁ =
    (Finset.affineCombination k Finset.univ (⇑(b.coord j) ∘ p)) w₂
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
v : ιa ⊕ ιb → Mᵢ
h : σ₂ = σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)
this : Perm.sign (σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) = Perm.sign σ₁ * (Perm.sign sl * Perm.sign sr)
⊢ (Perm.sign σ₁ • (a fun i₁ ↦ v (σ₁ (Sum.inl i₁))) ⊗ₜ[R'] b fun i₂ ↦ v (σ₁ (Sum.inr i₂))) =
    Perm.sign σ₂ • (a fun i₁ ↦ v (σ₂ (Sum.inl i₁))) ⊗ₜ[R'] b fun i₂ ↦ v (σ₂ (Sum.inr i₂))

Tactic:
h,

Goal state after:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
v : ιa ⊕ ιb → Mᵢ
h : σ₂ = σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)
this : Perm.sign (σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) = Perm.sign σ₁ * (Perm.sign sl * Perm.sign sr)
⊢ (Perm.sign σ₁ • (a fun i₁ ↦ v (σ₁ (Sum.inl i₁))) ⊗ₜ[R'] b fun i₂ ↦ v (σ₁ (Sum.inr i₂))) =
    Perm.sign (σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) •
      (a fun i₁ ↦ v ((σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) (Sum.inl i₁))) ⊗ₜ[R']
        b fun i₂ ↦ v ((σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) (Sum.inr i₂))
Module: Mathlib.LinearAlgebra.Dual.BaseChange

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
V : Type u_2
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
W : Type u_3
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module R W
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A W
inst✝² : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst✝¹ : Free R V
inst✝ : Module.Finite R V
⊢ A ⊗[R] Dual R V ≃ₗ[A] Dual A W

Tactic:
apply LinearEquiv.ofBijective ibc.toDualBaseChangeAux
  let b := Free.chooseBasis R V
  set ι := Free.ChooseBasisIndex R V
  have ibc_pow : IsBaseChange A ((Algebra.linearMap R A).compLeft ι) := (linearMap R A).finitePow ι
  suffices ibc.toDualBaseChangeAux =
      (((b.constr R).symm.baseChange ..).trans ibc_pow.equiv).trans ((ibc.basis b).constr A) from
    this ▸ LinearEquiv.bijective _
  ext f w
  simp only [AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars,
    LinearEquiv.coe_coe, LinearEquiv.trans_apply]
  induction w using ibc.inductionOn with
  | zero => simp
  | tmul v =>
    simp only [toDualBaseChangeAux_tmul, one_mul]
    conv_lhs => rw [← Basis.sum_equivFun b v, map_sum]
    simp [LinearEquiv.baseChange, basis_repr_comp_apply]
  | smul a w h => simp [h]
  | add x y hx hy => simp [map_add, hx, hy]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f : Dual R V
v w x : V
hw : f w = 0
⊢ (transvection f v) ((transvection f w) x) = (transvection f (v + w)) x

Tactic:
simp [transvection, map_add, hw, add_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : StrongRankCondition R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
⊢ ∃ a, f = a • 1

Tactic:
by
  rcases subsingleton_or_nontrivial V with hV | hV
  · use 1
    ext x
    apply hV.allEq
  let ι := Free.ChooseBasisIndex R V
  let b : Basis ι R V := Free.chooseBasis R V
  rcases subsingleton_or_nontrivial ι with hι | hι
  · have : Nonempty ι := Free.instNonemptyChooseBasisIndexOfNontrivial R V
    have : Fintype ι := Fintype.ofFinite ι
    simp_all [finrank_eq_card_basis b, ← Nat.card_eq_fintype_card]
  exact exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis b h

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

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
x y : A ⊗[R] M₂
hx : Q₁ x = Q₂ x
hy : Q₁ y = Q₂ y
x✝¹ x✝ : M₂
⊢ Q₁ (1 ⊗ₜ[R] (x✝¹ + x✝)) - Q₁ (1 ⊗ₜ[R] x✝¹) - Q₁ (1 ⊗ₜ[R] x✝) =
    Q₂ (1 ⊗ₜ[R] (x✝¹ + x✝)) - Q₂ (1 ⊗ₜ[R] x✝¹) - Q₂ (1 ⊗ₜ[R] x✝)

Tactic:
h,

Goal state after:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
x y : A ⊗[R] M₂
hx : Q₁ x = Q₂ x
hy : Q₁ y = Q₂ y
x✝¹ x✝ : M₂
⊢ Q₂ (1 ⊗ₜ[R] (x✝¹ + x✝)) - Q₁ (1 ⊗ₜ[R] x✝¹) - Q₁ (1 ⊗ₜ[R] x✝) =
    Q₂ (1 ⊗ₜ[R] (x✝¹ + x✝)) - Q₂ (1 ⊗ₜ[R] x✝¹) - Q₂ (1 ⊗ₜ[R] x✝)
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
x y : A ⊗[R] M₂
hx : Q₁ x = Q₂ x
hy : Q₁ y = Q₂ y
x✝¹ x✝ : M₂
⊢ Q₂ (1 ⊗ₜ[R] (x✝¹ + x✝)) - Q₁ (1 ⊗ₜ[R] x✝¹) - Q₁ (1 ⊗ₜ[R] x✝) =
    Q₂ (1 ⊗ₜ[R] (x✝¹ + x✝)) - Q₂ (1 ⊗ₜ[R] x✝¹) - Q₂ (1 ⊗ₜ[R] x✝)

Tactic:
h,

Goal state after:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
x y : A ⊗[R] M₂
hx : Q₁ x = Q₂ x
hy : Q₁ y = Q₂ y
x✝¹ x✝ : M₂
⊢ Q₂ (1 ⊗ₜ[R] (x✝¹ + x✝)) - Q₂ (1 ⊗ₜ[R] x✝¹) - Q₁ (1 ⊗ₜ[R] x✝) =
    Q₂ (1 ⊗ₜ[R] (x✝¹ + x✝)) - Q₂ (1 ⊗ₜ[R] x✝¹) - Q₂ (1 ⊗ₜ[R] x✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case algebraMap
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
r✝ : R
⊢ (contractLeft d) ((contractLeft d') ((algebraMap R (CliffordAlgebra Q)) r✝)) =
    -(contractLeft d') ((contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r✝))

Tactic:
simp_rw [contractLeft_algebraMap, map_zero, neg_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (ι (Q c₁ c₂)) (0, 1) * (ι (Q c₁ c₂)) (1, 0) = 0 • (ι (Q c₁ c₂)) (0, 1) - (ι (Q c₁ c₂)) (1, 0) * (ι (Q c₁ c₂)) (0, 1)

Tactic:
by
    rw [zero_smul, zero_sub, eq_neg_iff_add_eq_zero, ι_mul_ι_add_swap, QuadraticMap.polar]
    simp

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 Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
x : CliffordAlgebra Q'
⊢ (Q' m - (BilinMap.toQuadraticMap B) m) • x = Q m • x

Tactic:
h,

Goal state after:
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
m : M
x : CliffordAlgebra Q'
⊢ (Q' m - (Q' - Q) m) • x = Q m • x
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)
⊢ ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) ≃ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i

Tactic:
by
  refine TensorProduct.directSum R R 𝒜 ℬ ≪≫ₗ ?_ ≪≫ₗ (TensorProduct.directSum R R ℬ 𝒜).symm
  exact LinearEquiv.ofLinearMap (gradedCommAux _ _ _) (gradedCommAux _ _ _)
    (gradedCommAux_comp_gradedCommAux _ _ _) (gradedCommAux_comp_gradedCommAux _ _ _)

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 Q' : QuadraticForm R M
h : Q' = -Q
m : M
⊢ -(algebraMap R ↥(even Q')) (Q' m) = (algebraMap R ↥(even Q')) (Q m)

Tactic:
h,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
m : M
⊢ -(algebraMap R ↥(even Q')) ((-Q) m) = (algebraMap R ↥(even Q')) (Q m)
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 Q' : QuadraticForm R M
h : Q' = -Q
m₁ m₂ m₃ : M
⊢ Q' m₂ • ((even.ι Q').bilin m₁) m₃ = Q m₂ • -((even.ι Q').bilin m₁) m₃

Tactic:
h,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
m₁ m₂ m₃ : M
⊢ (-Q) m₂ • ((even.ι Q').bilin m₁) m₃ = Q m₂ • -((even.ι Q').bilin m₁) m₃
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd
he :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range =
    e.toAddMonoidHom.graph
r : R
x : M ⧸ L.goursatFst
⊢ (r • x, r • e x) ∈
    (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range

Tactic:
← Prod.smul_mk

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd
he :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range =
    e.toAddMonoidHom.graph
r : R
x : M ⧸ L.goursatFst
⊢ r • (x, e x) ∈
    (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
⊢ ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
intro k

Goal state after:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
⊢ ∀ (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsEmpty m
A : Matrix m n R
⊢ A.IsTotallyUnimodular

Tactic:
intro k

Goal state after:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsEmpty m
A : Matrix m n R
k : ℕ
⊢ ∀ (f : Fin k → m) (g : Fin k → n),
    Function.Injective f → Function.Injective g → (A.submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: 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 : Nonempty n → ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
⊢ (A.fromRows B).IsTotallyUnimodular

Tactic:
intro k

Goal state after:
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 : Nonempty n → ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
⊢ ∀ (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
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : a = i
hv : M i.succ b + ∑ c, M (i.succ.succAbove c) b = 0 b
⊢ -∑ x, M (i.succ.succAbove x) b = M (i.castSucc.succAbove a) b

Tactic:
h,

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : a = i
hv : M i.succ b + ∑ c, M (i.succ.succAbove c) b = 0 b
⊢ -∑ x, M (i.succ.succAbove x) b = M (i.castSucc.succAbove i) b
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
⊢ ∑ j,
      (-1) ^ (↑i₀ + ↑j) * M.updateRow i₀ (∑ k, 1 • M k) i₀ j *
        ((M.updateRow i₀ (∑ k, 1 • M k)).submatrix i₀.succAbove j.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
simp only [updateRow_apply, if_true, one_smul, submatrix_updateRow_succAbove, Finset.sum_apply]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
⊢ ∑ x, ((-1) ^ (↑i₀ + ↑x) * ∑ c, M c x) * (M.submatrix i₀.succAbove x.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
let em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) :=
    MulEquiv.funMultiplicative _ _
  let H' : Subgroup (Multiplicative (ι → ℤ)) := H.comap em
  let eH' : H' ≃* H := (MulEquiv.subgroupCongr <| Subgroup.comap_equiv_eq_map_symm em H).trans
    (MulEquiv.subgroupMap em.symm _).symm
  have h : H'.index = H.index := Subgroup.index_comap_of_surjective _ em.surjective
  rw [← h, ← Subgroup.index_toAddSubgroup, addSubgroup_index_ne_zero_iff]
  exact ⟨fun ⟨e⟩ ↦ ⟨(eH'.symm.trans (AddEquiv.toMultiplicative e)).trans em⟩,
    fun ⟨e⟩ ↦ ⟨(MulEquiv.toAdditive ((eH'.trans e).trans em.symm)).trans
      (AddEquiv.additiveMultiplicative _)⟩⟩

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

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : A.det = 0
⊢ LinearMap.det (Matrix.toLin' A) = 0

Tactic:
rwa [LinearMap.det_toLin']

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
⊢ A.det * star A.det = 0

Tactic:
h,

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
⊢ 0 * star 0 = 0
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
inst✝ : IsCancelAdd R
⊢ LinearIndependent R A.row ↔ A.Nonsingular

Tactic:
linearIndependent_row_iff

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
inst✝ : IsCancelAdd R
⊢ A.Nonsingular ↔ A.Nonsingular
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
A : Matrix n n R
inst✝¹ : IsCancelAdd R
inst✝ : Finite n
this : (α : Type u_3) → [Finite α] → Fintype α
⊢ A.Nonsingular ↔ LinearIndependent R A.row

Tactic:
linearIndependent_row_iff

Goal state after:
R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
A : Matrix n n R
inst✝¹ : IsCancelAdd R
inst✝ : Finite n
this : (α : Type u_3) → [Finite α] → Fintype α
⊢ A.Nonsingular ↔ A.Nonsingular
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 : ↑(Set.singleton i₀)ᶜ) → M ↑i
x : M i₀
⊢ (equivPiTensorComplSingletonTensor R M i₀).symm (((tprod R) fun j ↦ m j) ⊗ₜ[R] x) =
    ⨂ₜ[R] (i : ι), Function.subtypeNeLift i₀ m x i

Tactic:
apply (equivPiTensorComplSingletonTensor R M i₀).injective

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 : ↑(Set.singleton i₀)ᶜ) → M ↑i
x : M i₀
⊢ (equivPiTensorComplSingletonTensor R M i₀)
      ((equivPiTensorComplSingletonTensor R M i₀).symm (((tprod R) fun j ↦ m j) ⊗ₜ[R] x)) =
    (equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), Function.subtypeNeLift i₀ m x i)
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: k✝ : Type u_1
V✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : AddCommGroup V✝
inst✝⁴ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
hc : Nat.card V = Nat.card k ^ n
⊢ ↑(Nat.card (ℙ k V)) * ↑(Nat.card k - 1) = (∑ x ∈ Finset.range n, ↑(Nat.card k) ^ x) * ↑(Nat.card k - 1)

Tactic:
conv_rhs => rw [Int.natCast_sub this.le, Int.natCast_one, geom_sum_mul]

Goal state after:
k✝ : Type u_1
V✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : AddCommGroup V✝
inst✝⁴ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
hc : Nat.card V = Nat.card k ^ n
⊢ ↑(Nat.card (ℙ k V)) * ↑(Nat.card k - 1) = ↑(Nat.card k) ^ n - 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
D D' : ℙ K V
⊢ ∀ {c d : ℙ K V}, D ≠ D' → c ≠ d → ∃ g, g • D = c ∧ g • D' = d

Tactic:
E

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 : ℙ K V
⊢ ∀ {d : ℙ K V}, D ≠ D' → E ≠ d → ∃ g, g • D = E ∧ g • D' = d
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: 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' : ℙ K V
⊢ ∀ {c d : ℙ K V}, D ≠ D' → c ≠ d → ∃ g, g • D = c ∧ g • D' = d

Tactic:
E

Goal state after:
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 : ℙ K V
⊢ ∀ {d : ℙ K V}, D ≠ D' → E ≠ d → ∃ g, g • D = E ∧ g • D' = d