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

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
this✝ : CompleteSpace ↥Y
this : SecondCountableTopology ↥Y
φY : ↥Y → ℝ := φ ∘ ⇑Y.subtypeL
fY : α → ↥Y := fun a ↦ if h : f a ∈ Y then ⟨f a, h⟩ else 0
fX : α → E := ⇑Y.subtypeL ∘ fY
⊢ φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]

Tactic:
have lem0 : ∀ᵐ a ∂μ, f a ∈ Y := by
    filter_upwards [htt] with a ha using
      (Submodule.closure_subset_topologicalClosure_span t) (subset_closure ha)

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
this✝ : CompleteSpace ↥Y
this : SecondCountableTopology ↥Y
φY : ↥Y → ℝ := φ ∘ ⇑Y.subtypeL
fY : α → ↥Y := fun a ↦ if h : f a ∈ Y then ⟨f a, h⟩ else 0
fX : α → E := ⇑Y.subtypeL ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
⊢ φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
⊢ (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) =ᵐ[ν]
    ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]

pp: case hf
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
⊢ StronglyMeasurable fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal

pp: case hg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
⊢ StronglyMeasurable ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]

Tactic:
· exact toReal_rnDeriv_map hμν hg

Goal state after:
case hf
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
⊢ StronglyMeasurable fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal

case hg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
⊢ StronglyMeasurable ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case inr
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
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
i : ι
w : ι → k
hw : ∑ i, w i = 1
h✝ : Nontrivial k
⊢ (affineCombination k univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) (1 - w i)

Tactic:
obtain ⟨j, hj⟩ := exists_ne i
  rw [shift_eq ⟨p j, mem_affineSpan k <| Set.mem_image_of_mem _ hj⟩]
  suffices ∃ q ∈ affineSpan k (p '' {i}ᶜ), w i • (p i -ᵥ p j) +ᵥ q = affineCombination k univ p w by
    simpa
  refine ⟨-(w i • (p i -ᵥ p j)) +ᵥ affineCombination k univ p w, ?_, by simp⟩
  rw [← affineCombination_piSingle k _ p (mem_univ i),
    ← affineCombination_piSingle k _ p (mem_univ j), affineCombination_vsub, ← map_smul, ← map_neg,
    weightedVSub_vadd_affineCombination]
  refine affineCombination_mem_affineSpan_image ?_ (fun i' _ hi ↦ by aesop) _
  simp [sum_add_distrib, ← mul_sum, hw]

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

Goal state before:
pp: case refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
hi : x = 1 - w i
hj : ∀ (j : Fin n), w j ∈ Set.Icc 0 1
j : Fin n
hji : j ≠ i
⊢ w j ≤ x

Tactic:
hi,

Goal state after:
case refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
hi : x = 1 - w i
hj : ∀ (j : Fin n), w j ∈ Set.Icc 0 1
j : Fin n
hji : j ≠ i
⊢ w j ≤ 1 - w 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
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A ((Algebra.linearMap R A).compLeft ι)
f : Dual R V
w : W
⊢ (ibc.toDualBaseChangeAux (1 ⊗ₜ[R] f)) w =
    (((basis b ibc).constr A)
        (ibc_pow.equiv ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (b.constr R).symm) (1 ⊗ₜ[R] f))))
      w

Tactic:
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 g : Dual R V
v x : V
hf : f v = 0
⊢ (transvection f v) ((transvection g v) x) = (transvection (f + g) v) x

Tactic:
by
  simp [transvection, map_add, hf, add_smul, 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✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
⊢ ((Finsupp.single i 1).sum fun i a ↦ a • b i) + r • b j = b i + r • b j + (Finsupp.single i 1) j • b j

Tactic:
simp [single_eq_of_ne' hij, add_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case hg
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
⊢ ∀ (i : ι), 0 • b i = 0

Tactic:
simp [single_eq_of_ne' hij, add_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case hgg
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
⊢ ∀ (j : ι) (a₁ a₂ : R), (a₁ + a₂) • b j = a₁ • b j + a₂ • b j

Tactic:
simp [single_eq_of_ne' hij, add_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case h
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]
hV : Subsingleton V
x : V
⊢ f x = (1 • 1) x

Tactic:
apply hV.allEq

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

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
this : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
⊢ ∀ (m : A ⊗[R] V),
    (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) m *
        (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) m =
      (algebraMap A (A ⊗[R] CliffordAlgebra Q)) ((QuadraticForm.baseChange A Q) m)

Tactic:
let : Invertible (2 : A ⊗[R] CliffordAlgebra Q) :=
      (Invertible.map (algebraMap R _) 2).copy 2 (map_ofNat _ _).symm

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
this✝ : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
this : Invertible 2 := (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2).copy 2 ⋯
⊢ ∀ (m : A ⊗[R] V),
    (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) m *
        (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) m =
      (algebraMap A (A ⊗[R] CliffordAlgebra Q)) ((QuadraticForm.baseChange A Q) m)
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: 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).fixedSubmodule ⊔ K ∙ w = ⊤

Tactic:
Submodule.sup_span_singleton_eq_top_iff hw

Goal state after:
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
⊢ finrank K (V ⧸ (↑e).fixedSubmodule) = 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

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
A : Type u_3
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² x✝¹ x✝ : M
⊢ ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) (x✝¹ + x✝), ⋯⟩ =
    ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝¹, ⋯⟩ +
      ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝, ⋯⟩

Tactic:
simp only [map_add, mul_add]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type u_3
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² x✝¹ x✝ : M
⊢ ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝¹ + (CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝, ⋯⟩ =
    ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝¹, ⋯⟩ +
      ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) 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 ℤˣ)
j₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (-1) ^ (j₁ * i₂) • (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)

Tactic:
by
  dsimp only [mul_def, mulHom_apply, of_symm_of]
  dsimp [auxEquiv, tmul]
  rw [decompose_coe, decompose_coe]
  simp_rw [← lof_eq_of R]
  rw [tmul_of_gradedMul_of_tmul]
  simp_rw [lof_eq_of R]
  -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specialize `map_smul` to `LinearEquiv.map_smul`
  rw [@Units.smul_def _ _ (_) (_), ← Int.cast_smul_eq_zsmul R, LinearEquiv.map_smul, map_smul,
    Int.cast_smul_eq_zsmul R, ← @Units.smul_def _ _ (_) (_)]
  rw [congr_symm_tmul]
  dsimp
  simp_rw [decompose_symm_mul, decompose_symm_of, Equiv.symm_apply_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basis

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

Tactic:
subst s_card
  simp [basis_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
m n : ℕ
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)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
⊢ b.ExteriorAlgebra ↑s * b.ExteriorAlgebra ↑t = Equiv.Perm.sign (permOfDisjoint h) • b.ExteriorAlgebra ↑(disjUnion h)

Tactic:
simpa only [basis_apply_powersetCard] using ιMulti_family_mul_of_disjoint R b s t h

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
⊢ toTensorAlgebra ((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv) a) b) =
    toTensorAlgebra a * toTensorAlgebra b

Tactic:
← LinearMap.compr₂_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
⊢ ((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra) a) b =
    toTensorAlgebra a * toTensorAlgebra b
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
i : Fin n
⊢ ↑(bN' i) = Pi.single (f i) (a i)

Tactic:
simp only [map_apply, bN']

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
i : Fin n
⊢ ↑((bM.equivFun.submoduleMap N) (bN i)) = Pi.single (f i) (a i)
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: case h
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
l : M × N
hl : l ∈ L.toAddSubgroup
hl' :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype)
      ⟨l, hl⟩ =
    (x, e x)
⊢ (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype)
      ⟨r • l, ⋯⟩ =
    r • (x, e x)

Tactic:
← hl'

Goal state after:
case h
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
l : M × N
hl : l ∈ L.toAddSubgroup
hl' :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype)
      ⟨l, hl⟩ =
    (x, e x)
⊢ (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype)
      ⟨r • l, ⋯⟩ =
    r •
      (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap
              (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
          L.toAddSubgroup.subtype)
        ⟨l, hl⟩
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: case refine_1
G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
x : G
c : ι → ℤ
hc : ∀ (b : ι), (f x) b = ↑n * c b
⊢ x ∈ nG

Tactic:
refine ⟨b.repr.symm ⟨(f x).support, c, by simp [hc, NeZero.ne]⟩, b.repr.injective ?_⟩

Goal state after:
case refine_1
G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
x : G
c : ι → ℤ
hc : ∀ (b : ι), (f x) b = ↑n * c b
⊢ b.repr (((LinearMap.lsmul ℤ G) ↑n) (b.repr.symm { support := (f x).support, toFun := c, mem_support_toFun := ⋯ })) =
    b.repr x
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: G : Type u_1
inst✝³ : AddCommGroup G
n : ℕ
inst✝² : NeZero n
inst✝¹ : Free ℤ G
inst✝ : Module.Finite ℤ G
⊢ Nat.card (ModN G n) = n ^ finrank ℤ G

Tactic:
simp [Nat.card_congr (basis <| Module.Free.chooseBasis ℤ G).repr.toEquiv,
    Nat.card_eq_fintype_card, Module.finrank_eq_card_chooseBasisIndex]

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

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

Tactic:
apply (frobenius_inj K[X] p).iterate k

Goal state after:
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (⇑(frobenius K[X] p))^[k] (M ^ p ^ k).charpoly = (⇑(frobenius K[X] p))^[k] M.charpoly
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
⊢ (M ^ p).trace = M.trace ^ p

Tactic:
have h := FiniteField.trace_pow_card M; rwa [ZMod.card] at h

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

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) = v (i - j - (Equiv.subRight j) x) * w ((Equiv.subRight j) x)

Tactic:
simp only [Equiv.subRight_apply, sub_sub_sub_cancel_right]

Goal state after:
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
this :
  (reindex R M (Equiv.subtypeNeSumPUnit i₀).symm) (⨂ₜ[R] (i : ι), m i) =
    (tprod R) fun j ↦ m ((Equiv.subtypeNeSumPUnit i₀) j)
⊢ ((tprod R) fun i₁ ↦
        m ((Equiv.optionSubtypeNe i₀) ((Equiv.optionEquivSumPUnit { i // ¬i = i₀ }).symm (Sum.inl i₁)))) ⊗ₜ[R]
      (subsingletonEquiv ())
        ((tprod R) fun i₂ ↦
          m ((Equiv.optionSubtypeNe i₀) ((Equiv.optionEquivSumPUnit { i // ¬i = i₀ }).symm (Sum.inr i₂)))) =
    ((tprod R) fun j ↦ m ↑j) ⊗ₜ[R] m i₀

Tactic:
congr; simp

Goal state after:
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
  simp only [LinearEquiv.apply_symm_apply, equivPiTensorComplSingletonTensor_tprod,
    Function.subtypeNeLift_self]
  congr
  ext ⟨i, hi⟩
  rw [Function.subtypeNeLift_of_neq _ _ _ _ hi]
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: case succ.e_f.hg
R : Type u_1
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
n : ℕ
hn :
  ∀ {ι : Type u_2} [Finite ι] {M : ι → Type u_3} {γ : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (M i)]
    [inst_1 : (i : ι) → Module R (M i)] {g : ⦃i : ι⦄ → γ i → M i},
    (∀ (i : ι), Submodule.span R (Set.range g) = ⊤) →
      ∀ {φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N},
        (∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))) → Nat.card ι = n → φ = φ'
ι : Type u_2
inst✝² : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
hι : Nat.card ι = n + 1
this : Nonempty ι
i₀ : ι
e : (⨂[R] (i : ι), M i) ≃ₗ[R] M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) :=
  equivPiTensorComplSingletonTensor R M i₀ ≪≫ₗ TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀)
ψ ψ' : M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) →ₗ[R] N
h :
  ∀ (j : (i : ι) → γ i),
    ψ
        ((TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀))
          ((equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), g (j i)))) =
      ψ'
        ((TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀))
          ((equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), g (j i))))
g₀ : γ i₀
i✝ : ↑{i₀}ᶜ
⊢ Submodule.span R (Set.range fun j ↦ g j) = ⊤

Tactic:
exact hg _

Goal state after: