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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ klDiv μ ν = if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞

Tactic:
by
  rw [klDiv_eq_integral_klFun]
  by_cases hμν : μ ≪ ν
  swap; · simp [hμν]
  have h_int_iff := lintegral_ofReal_ne_top_iff_integrable
    (f := fun x ↦ klFun (μ.rnDeriv ν x).toReal) (μ := ν) ?_ ?_
  rotate_left
  · exact Measurable.aestronglyMeasurable (by fun_prop)
  · exact ae_of_all _ fun _ ↦ klFun_nonneg ENNReal.toReal_nonneg
  by_cases h_int : Integrable (llr μ ν) μ
  · simp only [hμν, h_int, and_self, ↓reduceIte]
    rw [ofReal_integral_eq_lintegral_ofReal]
    · rwa [integrable_klFun_rnDeriv_iff hμν]
    · exact ae_of_all _ fun _ ↦ klFun_nonneg ENNReal.toReal_nonneg
  · rw [← not_iff_not, ne_eq, Decidable.not_not] at h_int_iff
    symm
    simp [hμν, h_int, h_int_iff, integrable_klFun_rnDeriv_iff hμν]

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

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯) x ∂μ = ⟪indicatorConstLp 2 ⋯ ⋯ c, f⟫

Tactic:
L2.inner_indicatorConstLp_eq_setIntegral_inner 𝕜 f (hm s hs) c hμs.ne,

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯) x ∂μ = ∫ (x : α) in s, ⟪c, ↑↑f x⟫ ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hf : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ μ[f | m] =ᵐ[μ] f

Tactic:
refine ((condExp_congr_ae hf.ae_eq_mk).trans ?_).trans hf.ae_eq_mk.symm
  rw [condExp_of_stronglyMeasurable hm hf.stronglyMeasurable_mk
    ((integrable_congr hf.ae_eq_mk).mp hfi)]

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

Goal state before:
pp: case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
inst✝ : SigmaFinite (μ.trim hm)
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
t : Set α
ht : MeasurableSet t
hμt : (μ.trim hm) t < ∞
h_ae :
  ∀ᵐ (x : α) ∂μ,
    x ∈ t →
      AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x =
        ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) x
⊢ 0 ≤ ∫ (x : α) in t, AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x ∂μ

Tactic:
rw [setIntegral_congr_ae (hm t ht) h_ae,
      setIntegral_condExpL2_indicator ht hs ((le_trim hm).trans_lt hμt).ne hμs]

Goal state after:
case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
inst✝ : SigmaFinite (μ.trim hm)
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
t : Set α
ht : MeasurableSet t
hμt : (μ.trim hm) t < ∞
h_ae :
  ∀ᵐ (x : α) ∂μ,
    x ∈ t →
      AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x =
        ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) x
⊢ 0 ≤ μ.real (s ∩ t)
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 μ
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}
n : ℕ
h1 : ⇑(L n) ∘ μ[f | m] =ᵐ[μ] μ[⇑(L n) ∘ f | m]
h2 : μ[fun a ↦ (L n) (f a) | m] ≤ᵐ[μ] μ[fun x ↦ c n | m]
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ {x | (L n) x ≤ c n}

Tactic:
filter_upwards [h1, h2] with a ha hb

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}
n : ℕ
h1 : ⇑(L n) ∘ μ[f | m] =ᵐ[μ] μ[⇑(L n) ∘ f | m]
h2 : μ[fun a ↦ (L n) (f a) | m] ≤ᵐ[μ] μ[fun x ↦ c n | m]
a : α
ha : (⇑(L n) ∘ μ[f | m]) a = μ[⇑(L n) ∘ f | m] a
hb : μ[fun a ↦ (L n) (f a) | m] a ≤ μ[fun x ↦ c n | m] a
⊢ (L n) (μ[f | m] a) ≤ c n
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
⊢ P⁻[0 | mΩ] = 0

Tactic:
by_cases hm : mΩ ≤ mΩ₀
  swap; · simp [condLExp_of_not_le hm]
  by_cases hσ : SigmaFinite (P.trim hm)
  swap; · simp [condLExp_of_not_sigmaFinite hm hσ]
  exact condLExp_const hm P 0

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

Goal state before:
pp: case ht
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
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᵐ[μ.restrict (spanningSets (μ.trim hm) n)] μ[f | m]
this : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n))
h2 : ∀ᵐ (a : α) ∂μ.restrict (spanningSets (μ.trim hm) n), (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a ∈ s
⊢ (μ.restrict (spanningSets (μ.trim hm) n)) {x | (fun a ↦ μ[f | m] a ∈ s) x}ᶜ = 0

Tactic:
filter_upwards [h1, h2] with a ha hb

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
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᵐ[μ.restrict (spanningSets (μ.trim hm) n)] μ[f | m]
this : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n))
h2 : ∀ᵐ (a : α) ∂μ.restrict (spanningSets (μ.trim hm) n), (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a ∈ s
a : α
ha : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a = μ[f | m] a
hb : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a ∈ s
⊢ μ[f | m] a ∈ s
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: 𝓧 : 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) ν
⊢ Integrable (fun x ↦ f (ν[fun x ↦ ((∂μ/∂ν) x).toReal | m] x)) ν

Tactic:
by
  have h := integrable_comp_rnDeriv_trim hm hμν hf hf_cvx hf_cont_at h_int
  refine integrable_of_integrable_trim hm ((integrable_congr ?_).mp h)
  filter_upwards [toReal_rnDeriv_trim hm hμν] with a ha
  rw [ha]

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

Goal state before:
pp: case inl
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
c : P
r : k
h : s = ⊥
⊢ (s.shift c r).direction = s.direction

Tactic:
simp [shift, h]

Goal state after:
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
s : AffineSubspace k P
c : P
r : k
h✝ : (↑s).Nonempty
h : Nonempty ↥s
⊢ (s.shift c r).direction = s.direction

Tactic:
simp [shift, h]

Goal state after:
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
s : AffineSubspace k P
c : P
h✝ : (↑s).Nonempty
h : Nonempty ↥s
⊢ s.shift c 1 = s

Tactic:
simp [shift, h]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ ((b.repr v).sum fun a₁ b_1 ↦ ((basis b ibc).repr (b_1 • ε (b a₁))) i) = (algebraMap R S) ((b.repr v) i)

Tactic:
rw [Finsupp.sum_eq_single i]

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ ((basis b ibc).repr ((b.repr v) i • ε (b i))) i = (algebraMap R S) ((b.repr v) i)

case h₀
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ ∀ (b_1 : ι), (b.repr v) b_1 ≠ 0 → b_1 ≠ i → ((basis b ibc).repr ((b.repr v) b_1 • ε (b b_1))) i = 0

case h₁
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ (b.repr v) i = 0 → ((basis b ibc).repr (0 • ε (b i))) i = 0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case inr.mp.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p x : P
hmem : x ∈ s
heq : (1 - r) • (c -ᵥ ↑h.some) +ᵥ x = p
⊢ r • ((t • (x -ᵥ ↑h.some) +ᵥ ↑h.some) -ᵥ c) +ᵥ c = (1 - r) • (c -ᵥ ↑h.some) +ᵥ x

Tactic:
vadd_vsub_assoc,

Goal state after:
case inr.mp.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p x : P
hmem : x ∈ s
heq : (1 - r) • (c -ᵥ ↑h.some) +ᵥ x = p
⊢ r • (t • (x -ᵥ ↑h.some) + (↑h.some -ᵥ c)) +ᵥ c = (1 - r) • (c -ᵥ ↑h.some) +ᵥ 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✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedAddMonoid k
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Module k V
n : ℕ
inst✝¹ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
inst✝ : ZeroLEOneClass k
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
x✝ :
  (affineCombination k univ s.points) w ∈ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0)
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hshift : (affineCombination k univ s.points) w ∈ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0)
⊢ w = Pi.single i 1

Tactic:
rw [SetLike.mem_coe, s.independent.affineCombination_mem_shift_iff i hw, sub_zero] at hshift

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedAddMonoid k
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Module k V
n : ℕ
inst✝¹ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
inst✝ : ZeroLEOneClass k
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
x✝ :
  (affineCombination k univ s.points) w ∈ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0)
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hshift : w i = 1
⊢ w = Pi.single i 1
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case e_f.h
ι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 : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
σ : Perm (ιa ⊕ ιb)
⊢ ∑ y with ⟦y⟧ = Quotient.mk'' σ, sign y • domDomCongr y (a.domCoprod b) =
    domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ)

Tactic:
set f := sumCongrHom ιa ιb

Goal state after:
case e_f.h
ι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 : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
σ : Perm (ιa ⊕ ιb)
f : Perm ιa × Perm ιb →* Perm (ιa ⊕ ιb) := sumCongrHom ιa ιb
⊢ ∑ y with ⟦y⟧ = Quotient.mk'' σ, sign y • domDomCongr y (a.domCoprod b) =
    domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ)
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case neg
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
i j : ι
h✝ : ∀ (v : V), ∃ x x_1, ∃ (_ : x • v + x_1 • f v = 0), ¬(x = 0 ∧ x_1 = 0)
s t : R
h : s • b i + t • f (b i) = 0
h' : ¬(s = 0 ∧ t = 0)
hj : ¬i = j
this : t = 0 ∨ (b.repr (f (b i))) j = 0
⊢ ¬t = 0

Tactic:
contrapose h'

Goal state after:
case neg
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
i j : ι
h✝ : ∀ (v : V), ∃ x x_1, ∃ (_ : x • v + x_1 • f v = 0), ¬(x = 0 ∧ x_1 = 0)
s t : R
h : s • b i + t • f (b i) = 0
hj : ¬i = j
this : t = 0 ∨ (b.repr (f (b i))) j = 0
h' : t = 0
⊢ s = 0 ∧ t = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : QuadraticModuleCat R
i : X ≅ Y
x : ↑X.toModuleCat
⊢ (QuadraticModuleCat.Hom.toIsometry i.inv) ((QuadraticModuleCat.Hom.toIsometry i.hom) x) = x

Tactic:
change (i.hom ≫ i.inv).toIsometry x = x
    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 : QuadraticForm R M
d : Module.Dual R M
a : CliffordAlgebra Q
r : R
⊢ (contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r * a) =
    (contractLeft d) a * (algebraMap R (CliffordAlgebra Q)) r

Tactic:
contractLeft_algebraMap_mul,

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : CliffordAlgebra Q
r : R
⊢ (algebraMap R (CliffordAlgebra Q)) r * (contractLeft d) a = (contractLeft d) a * (algebraMap R (CliffordAlgebra Q)) r
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case neg
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : f v = 0
hv : ¬v = 0
hf : ¬f = 0
⊢ LinearMap.det (transvection f v) = 1 + f v

Tactic:
obtain ⟨ι, b, i, j, hi, hj⟩ := exists_basis_of_pairing_eq_zero hfv hf hv

Goal state after:
case neg
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : f v = 0
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
⊢ LinearMap.det (transvection f v) = 1 + f v
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case neg.hy
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : f v = 0
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
x y : ↑ι
⊢ (Finsupp.single i ((Finsupp.single y 1) j)) x = Matrix.single i j 1 x y

Tactic:
· by_cases h : i = x ∧ j = y
      · rw [h.1, h.2]; simp
      · rcases not_and_or.mp h with h' | h' <;>
          simp [Finsupp.single_eq_of_ne' h',
            Finsupp.single_eq_of_ne h',
            Matrix.single_apply_of_ne (h := h)]

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

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : ¬f v = 0
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this✝ : Fintype ↑ι
this : (toMatrix b b) (transvection f v) = Matrix.diagonal (Function.update 1 i (1 + f v))
⊢ ((toMatrix b b) (transvection f v)).det = 1 + f v

Tactic:
by
      rw [this]
      simp only [Matrix.det_diagonal]
      rw [Finset.prod_eq_single i]
      · simp
      · intro j _ hj
        simp [Function.update_of_ne hj]
      · simp

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

Goal state before:
pp: case add
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
inst✝¹ : Ring A
inst✝ : Algebra R A
f g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x✝ x y : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
hy : y ∈ evenOdd Q 0
ihx : f ⟨x, hx⟩ = g ⟨x, hx⟩
ihy : f ⟨y, hy⟩ = g ⟨y, hy⟩
⊢ f ⟨x + y, ⋯⟩ = g ⟨x + y, ⋯⟩

Tactic:
have := congr_arg₂ (· + ·) ihx ihy
    exact (map_add f _ _).trans (this.trans <| (map_add g _ _).symm)

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

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 b : M
inst✝¹ : Invertible ((ι Q) a)
inst✝ : Invertible (Q a)
⊢ (ι Q) a * (ι Q) b * ⅟((ι Q) a) = (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)

Tactic:
rw [invOf_ι, map_smul, mul_smul_comm, ι_mul_ι_mul_ι, ← map_smul, smul_sub, smul_smul, smul_smul,
    invOf_mul_self, one_smul]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ExteriorAlgebra R M
⊢ x ∈ Submodule.span R (Set.range fun x ↦ (ιMulti R x.fst) x.snd)

Tactic:
induction x using DirectSum.Decomposition.inductionOn fun i => ⋀[R]^i M with

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: 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
⊢ Basis ι (ZMod n) (ModN G n)

Tactic:
let g : H →ₗ[ℤ] (ι →₀ ZMod n) := nG.liftQ (mod.comp f) hker

Goal state after:
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
⊢ Basis ι (ZMod n) (ModN G n)
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:

Tactic:
∑ x : Fin n, _ = c h.choose * if i = f h.choose then a h.choose else 0 := by
              refine Finset.sum_eq_single h.choose ?_ (by simp)
              rintro j - hj
              have hinj := f.injective.ne hj
              rw [h.choose_spec] at hinj
              simp [hinj.symm]
          _ = c h.choose * a h.choose := by simp [h.choose_spec]

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

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps π : {i : I} → A i →ₐ[R] B
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext i aᵢ
    simp [ι, ← ι_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
h : H'.index = H.index
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
rw [← h, ← Subgroup.index_toAddSubgroup, addSubgroup_index_ne_zero_iff]

Goal state after:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
h : H'.index = H.index
⊢ Nonempty (↥(Subgroup.toAddSubgroup H') ≃+ (ι → ℤ)) ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))
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
k : ℕ
hk : A.den = (A i j).den * k
⊢ ↑(↑(A i j).num * ↑k).num = ↑(A i j).num * ↑k

Tactic:
← Int.cast_natCast k,

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 i j).num * ↑↑k).num = ↑(A i j).num * ↑↑k