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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)

Tactic:
integrable_add_iff_integrable_right'

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (fun x ↦ log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)

𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal) (μ ⊗ₘ κ)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] =ᵐ[μ.restrict s] 0

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm]; rfl

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ s.indicator μ[s.indicator f | m] + ∅.indicator μ[sᶜ.indicator f | m] =ᵐ[μ] s.indicator μ[s.indicator f | m]

Tactic:
Set.indicator_empty',

Goal state after:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ s.indicator μ[s.indicator f | m] + 0 =ᵐ[μ] s.indicator μ[s.indicator f | m]
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
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝¹ : IsFiniteMeasure μ
inst✝ : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
L : ℕ → StrongDual ℝ E
c : ℕ → ℝ
hLc : ⋂ n, {x | RCLike.re ((L n) x) ≤ c n} = s
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s

Tactic:
simp_all only [← hLc, RCLike.re_to_real, mem_iInter, ae_all_iff]

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝¹ : IsFiniteMeasure μ
inst✝ : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
L : ℕ → StrongDual ℝ E
c : ℕ → ℝ
hs : IsClosed (⋂ n, {x | (L n) x ≤ c n})
hc : Convex ℝ (⋂ n, {x | (L n) x ≤ c n})
hf : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, f a ∈ {x | (L i) x ≤ c i}
⊢ ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ {x | (L i) x ≤ c i}
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᵐ[μ] μ[gs n | m]
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] =ᵐ[μ] μ[g | m]

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm]; rfl

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case inl
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
X : Ω → ℝ≥0∞
⊢ 0⁻[X | ⊥] =ᵐ[0] fun x ↦ (0 Set.univ)⁻¹ • ∫⁻ (ω : Ω), X ω ∂0

pp: case inr
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hP : NeZero P
⊢ P⁻[X | ⊥] =ᵐ[P] fun x ↦ (P Set.univ)⁻¹ • ∫⁻ (ω : Ω), X ω ∂P

Tactic:
· rw [ae_zero]; exact Filter.eventually_bot

Goal state after:
case inr
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hP : NeZero P
⊢ P⁻[X | ⊥] =ᵐ[P] fun x ↦ (P Set.univ)⁻¹ • ∫⁻ (ω : Ω), X ω ∂P
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᵐ[μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] ≤ᵐ[μ] μ[g | m]

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm]; rfl

Goal state after:
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
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]

Tactic:
apply (isCountablySpanning_spanningSets (μ.trim hm)).null_of_forall_restrict_null <;>
    rintro - ⟨n, rfl⟩
  · exact hm _ (measurableSet_spanningSets (μ.trim hm) n)
  have h1 := condExp_restrict_ae_eq_restrict hm (measurableSet_spanningSets (μ.trim hm) n) hf_int
  have h2 := condExp_restrict_ae_eq_restrict hm (measurableSet_spanningSets (μ.trim hm) n) hφ_int
  have : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n)) := isFiniteMeasure_restrict.2
    ((le_trim hm).trans_lt (measure_spanningSets_lt_top (μ.trim hm) n)).ne
  have h3 := hφ_cvx.map_condExp_le_of_isFiniteMeasure (μ := μ.restrict (spanningSets (μ.trim hm) n))
    hm hφ_cont (ae_restrict_of_ae hf) hs hf_int.restrict hφ_int.restrict
  filter_upwards [h1, h2, h3] with a ha hb hc
  simpa [← ha, ← hb]

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
⊢ x⁻¹ * w j ≤ 1

Tactic:
inv_mul_le_one₀ hxpos,

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 ≤ x
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
Q : Type u_6
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R Q
inst✝⁶ : Module S P
inst✝⁵ : IsScalarTower R S P
inst✝⁴ : Module S Q
inst✝³ : IsScalarTower R S Q
α : M →ₗ[R] P
β : N →ₗ[R] Q
ibcM : IsBaseChange S α
ibcN : IsBaseChange S β
ι : Type u_7
θ : Type u_8
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : Finite θ
b : Basis ι R M
c : Basis θ R N
f : M →ₗ[R] N
i : θ
j : ι
⊢ (toMatrix (basis b ibcM) (basis c ibcN)) ((ibcM.linearMapLeftRightHom β) f) i j =
    ((toMatrix b c) f).map (⇑(algebraMap R S)) i j

Tactic:
simp only [toMatrix_apply, Matrix.map_apply, basis_apply,
    linearMapLeftRightHom_comp_apply, basis_repr_comp_apply]

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 : V
hw : f w = 0
⊢ transvection f v ∘ₗ transvection f w = transvection f (v + w)

Tactic:
ext; simp [comp_of_left_eq_apply hw]

Goal state after:
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 w : V
hv : f v = 0
hw : f w = 0
hvw : f (v + w) = 0
⊢ transvection hw ≪≫ₗ transvection hv = transvection hvw

Tactic:
ext; simp [comp_of_left_eq_apply hw]

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
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
feq : ∀ (i j : ι), f (b j) = (b.coord i) (f (b i)) • b j
i : ι := Classical.ofNonempty
r : R
⊢ Commute ((b.coord i) (f (b i))) r

Tactic:
obtain ⟨j, hij⟩ := exists_ne i

Goal state after:
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
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
feq : ∀ (i j : ι), f (b j) = (b.coord i) (f (b i)) • b j
i : ι := Classical.ofNonempty
r : R
j : ι
hij : j ≠ i
⊢ Commute ((b.coord i) (f (b i))) r
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ M →ₗ[R] CliffordAlgebra (Q' Q)

pp: case refine_1.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ?refine_1.refine_1 m ∈ (ι (Q' Q)).range ^ ↑⟨2, ⋯⟩

Tactic:
· exact (LinearMap.mulLeft R <| e0 Q).comp (v Q)

Goal state after:
case refine_1.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) m ∈ (ι (Q' Q)).range ^ ↑⟨2, ⋯⟩
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
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q
⊢ (changeForm ⋯) ((changeForm h) x) = x

Tactic:
exact (changeForm_changeForm _ _ x).trans <|
        by simp_rw [(add_neg_cancel B), changeForm_self_apply]

Goal state after:
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₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
b₂ : B
⊢ a₁ ᵍ⊗ₜ[R] ↑b₁ * 1 ᵍ⊗ₜ[R] b₂ = a₁ ᵍ⊗ₜ[R] (↑b₁ * b₂)

Tactic:
convert! tmul_coe_mul_zero_coe_tmul 𝒜 ℬ a₁ b₁ (@GradedMonoid.GOne.one _ (𝒜 ·) _ _) b₂

Goal state after:
case e'_3
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₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
b₂ : B
⊢ a₁ = a₁ * ↑GradedMonoid.GOne.one
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case mul
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (b : M), involute ↑y * (ι Q) b * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (b : M), involute ↑z * (ι Q) b * ↑z⁻¹ ∈ (ι Q).range
b : M
⊢ involute ↑(y * z) * (ι Q) b * ↑(y * z)⁻¹ ∈ (ι Q).range

Tactic:
simp_rw [mul_inv_rev, Units.val_mul, map_mul]
    suffices involute (Q := Q) ↑y * (involute (Q := Q) ↑z * ι Q b * ↑z⁻¹) * ↑y⁻¹ ∈ _ by
      simpa only [mul_assoc] using this
    obtain ⟨z', hz'⟩ := hz b
    obtain ⟨y', hy'⟩ := hy z'
    simp_rw [← hz', ← hy', LinearMap.mem_range_self]

Goal state after:
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)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
⊢ (gradedComm R 𝒜 ℬ) (((gradedMul R 𝒜 ℬ) x) y) = ((gradedMul R ℬ 𝒜) ((gradedComm R 𝒜 ℬ) x)) ((gradedComm R 𝒜 ℬ) y)

Tactic:
suffices (gradedMul R 𝒜 ℬ).compr₂ (gradedComm R 𝒜 ℬ).toLinearMap
      = (gradedMul R ℬ 𝒜 ∘ₗ (gradedComm R 𝒜 ℬ).toLinearMap).compl₂
        (gradedComm R 𝒜 ℬ).toLinearMap from
    LinearMap.congr_fun₂ this x y
  ext i₁ a₁ j₁ b₁ i₂ a₂ j₂ b₂
  dsimp
  rw [gradedComm_of_tmul_of, gradedComm_of_tmul_of, tmul_of_gradedMul_of_tmul]
  -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specialize `map_smul` to avoid timeouts.
  simp_rw [Units.smul_def, ← Int.cast_smul_eq_zsmul R, LinearEquiv.map_smul, map_smul,
    LinearMap.smul_apply]
  simp_rw [Int.cast_smul_eq_zsmul R, ← Units.smul_def, DirectSum.lof_eq_of, DirectSum.of_mul_of,
    ← DirectSum.lof_eq_of R, gradedComm_of_tmul_of, tmul_of_gradedMul_of_tmul, smul_smul,
    DirectSum.lof_eq_of, ← DirectSum.of_mul_of, ← DirectSum.lof_eq_of R]
  simp_rw [← uzpow_add, mul_add, add_mul, mul_comm i₁ j₂]
  congr 1
  abel_nf
  rw [two_nsmul, uzpow_add, uzpow_add, Int.units_mul_self, one_mul]

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ ∀ {n : ℕ} (x₀ : M) (x : Fin n → M),
    (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ x a)) (List.finRange n)).prod =
        GradedMonoid.mk n ((PiTensorProduct.tprod R) x) →
      (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ Fin.cons x₀ x a))
            (List.finRange (n + 1))).prod =
        GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))

Tactic:
intro n x₀ x ih

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
⊢ (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ Fin.cons x₀ x a))
        (List.finRange (n + 1))).prod =
    GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case pos
ι : 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)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
⊢ (∑ x, if i = f x then ⋯.choose • a x else 0) = g i

pp: case neg
ι : 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)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∀ (j : Fin n), f j ≠ i
⊢ (∑ x, if i = f x then ⋯.choose • a x else 0) = g i

Tactic:
· calc ∑ x : Fin n, _ =
            if i = f hj.choose then (h (f hj.choose)).choose * a hj.choose else 0 := by
              convert! Finset.sum_eq_single (M := R) hj.choose ?_ ?_
              · simp
              · rintro j - h
                have hinj := f.injective.ne h
                rw [hj.choose_spec] at hinj
                simp [hinj.symm]
              · simp
          _ = g i := by
              simp only [hj.choose_spec, ↓reduceIte]
              rw [mul_comm]
              conv_rhs =>
                rw [← hj.choose_spec, (h (f hj.choose)).choose_spec]
              simp only [EmbeddingLike.apply_eq_iff_eq, exists_eq, ↓reduceDIte, Classical.choose_eq]
              congr!
              · exact hj.choose_spec.symm
              · simp [hj]

Goal state after:
case neg
ι : 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)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∀ (j : Fin n), f j ≠ i
⊢ (∑ x, if i = f x then ⋯.choose • a x else 0) = g i
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Basic

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type v
A : Matrix m n R
inst✝² : Zero R
inst✝¹ : LT n
inst✝ : WellFoundedLT n
i : m
h : A i ≠ 0
c : n
hc : c ∈ {j | A i j ≠ 0}
hmin : ∀ x ∈ {j | A i j ≠ 0}, ¬x < c
⊢ ∀ j < c, A i j = 0

Tactic:
by_contra

Goal state after:
m : Type u_1
n : Type u_2
R : Type v
A : Matrix m n R
inst✝² : Zero R
inst✝¹ : LT n
inst✝ : WellFoundedLT n
i : m
h : A i ≠ 0
c : n
hc : c ∈ {j | A i j ≠ 0}
hmin : ∀ x ∈ {j | A i j ≠ 0}, ¬x < c
this : ¬∀ j < c, A i j = 0
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case pos
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
hfg : Function.Injective f ∧ Function.Injective g
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

pp: case neg
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
hfg : ¬(Function.Injective f ∧ Function.Injective g)
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
· exact hA k f g hfg.1 hfg.2

Goal state after:
case neg
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
hfg : ¬(Function.Injective f ∧ Function.Injective g)
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case top
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✝ : LT m
l' : m → WithTop n
hl : A.IsPivotedBy l
hl' : A.IsPivotedBy l'
i : m
hc' : l' i = ⊤
⊢ l i = ⊤

Tactic:
hl.eq_top_iff,

Goal state after:
case top
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✝ : LT m
l' : m → WithTop n
hl : A.IsPivotedBy l
hl' : A.IsPivotedBy l'
i : m
hc' : l' i = ⊤
⊢ A i = 0
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 : ∀ (k : n), ∑ j ∈ Finset.univ.erase k, ‖A k j‖ < ‖A k k‖
⊢ A.det ≠ 0

Tactic:
contrapose! h
  suffices ∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖) by
    exact this.imp (fun a h ↦ by rwa [mem_closedBall_iff_norm', sub_zero] at h)
  refine eigenvalue_mem_ball ?_
  rw [Module.End.hasEigenvalue_iff, Module.End.eigenspace_zero, ne_comm]
  exact ne_of_lt (LinearMap.bot_lt_ker_of_det_eq_zero (by rwa [LinearMap.det_toLin']))

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

Goal state before:
pp: case mp.refine_4
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : (fromBlocks A B C D).IsDiag
i j : n
hij : i ≠ j
⊢ (fun i j ↦ D i j = 0) i j

Tactic:
exact h (Sum.inr_injective.ne hij)

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Pi

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

Tactic:
by
  ext p'
  obtain rfl | hp := eq_or_ne p p'
  · simp
  · simp [hp]

Goal state after: