mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
H : Set (ZMod n)ˣ
χ : DirichletCharacter R n
hχ : ∀ (x : (↥(Submonoid.map (Units.coeHom (ZMod n)) (Submonoid.closure H)))ˣ), χ ↑↑x = 1
x : (ZMod n)ˣ
hx : x ∈ Submonoid.closure H
⊢ x⁻¹ ∈ ↑(Submonoid.closure H)

Tactic:
by simpa [← Subgroup.closure_toSubmonoid_of_finite] using hx

Goal state after:
Module: Mathlib.Order.Grade

Goal state before:
pp: case inr
α : Type u_3
inst✝ : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : ↑a < c
hcb : c < ↑b
d : α
hd : d ∈ s
had : a < ⟨d, hd⟩
⊢ c ≤ d ∨ d ≤ c

Tactic:
obtain hbd | hdb := le_or_gt b ⟨d, hd⟩

Goal state after:
case inr.inl
α : Type u_3
inst✝ : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : ↑a < c
hcb : c < ↑b
d : α
hd : d ∈ s
had : a < ⟨d, hd⟩
hbd : b ≤ ⟨d, hd⟩
⊢ c ≤ d ∨ d ≤ c

case inr.inr
α : Type u_3
inst✝ : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : ↑a < c
hcb : c < ↑b
d : α
hd : d ∈ s
had : a < ⟨d, hd⟩
hdb : ⟨d, hd⟩ < b
⊢ c ≤ d ∨ d ≤ c
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
c : ℂ
Φ : ZMod N → E
⊢ auxDFT (c • Φ) = c • auxDFT Φ

Tactic:
ext

Goal state after:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
c : ℂ
Φ : ZMod N → E
x✝ : ZMod N
⊢ auxDFT (c • Φ) x✝ = (c • auxDFT Φ) x✝
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ₁ Φ₂ : ZMod N → E
⊢ auxDFT (Φ₁ + Φ₂) = auxDFT Φ₁ + auxDFT Φ₂

Tactic:
ext

Goal state after:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ₁ Φ₂ : ZMod N → E
x✝ : ZMod N
⊢ auxDFT (Φ₁ + Φ₂) x✝ = (auxDFT Φ₁ + auxDFT Φ₂) x✝
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
c : ℂ
Φ : ZMod N → E
⊢ auxDFT (c • Φ) = (RingHom.id ℂ) c • auxDFT Φ

Tactic:
ext

Goal state after:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
c : ℂ
Φ : ZMod N → E
x✝ : ZMod N
⊢ auxDFT (c • Φ) x✝ = ((RingHom.id ℂ) c • auxDFT Φ) x✝
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (∃ a ∉ t, insert a t = s) ↔ t ⊆ s ∧ #(s \ t) = 1

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (∃ a ∉ t, insert a t = s) → t ⊆ s ∧ #(s \ t) = 1

case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ t ⊆ s ∧ #(s \ t) = 1 → ∃ a ∉ t, insert a t = s
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
hst : s ⊆ t
⊢ (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) ↔ s ⊆ u ∧ u ⊆ t

Tactic:
constructor

Goal state after:
case pos.mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
hst : s ⊆ t
⊢ (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) → s ⊆ u ∧ u ⊆ t

case pos.mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
hst : s ⊆ t
⊢ s ⊆ u ∧ u ⊆ t → ∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ Icc s t = {u ∈ t.powerset | s ⊆ u}

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t a✝ : Finset α
⊢ a✝ ∈ Icc s t ↔ a✝ ∈ {u ∈ t.powerset | s ⊆ u}
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ Ico s t = {u ∈ t.ssubsets | s ⊆ u}

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t a✝ : Finset α
⊢ a✝ ∈ Ico s t ↔ a✝ ∈ {u ∈ t.ssubsets | s ⊆ u}
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ Ioc s t = {u ∈ t.powerset | s ⊂ u}

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t a✝ : Finset α
⊢ a✝ ∈ Ioc s t ↔ a✝ ∈ {u ∈ t.powerset | s ⊂ u}
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ Ioo s t = {u ∈ t.ssubsets | s ⊂ u}

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t a✝ : Finset α
⊢ a✝ ∈ Ioo s t ↔ a✝ ∈ {u ∈ t.ssubsets | s ⊂ u}
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ Iic s = s.powerset

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s a✝ : Finset α
⊢ a✝ ∈ Iic s ↔ a✝ ∈ s.powerset
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ Iio s = s.ssubsets

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s a✝ : Finset α
⊢ a✝ ∈ Iio s ↔ a✝ ∈ s.ssubsets
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ LocallyFiniteOrder.finsetIcc s t = image (fun x ↦ s ∪ x) (t \ s).powerset

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
a✝ : Finset α
⊢ a✝ ∈ LocallyFiniteOrder.finsetIcc s t ↔ a✝ ∈ image (fun x ↦ s ∪ x) (t \ s).powerset
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ⊆ u ∧ u ⊂ t ↔ ∃ a ⊂ t \ s, s ∪ a = u

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ⊆ u ∧ u ⊂ t → ∃ a ⊂ t \ s, s ∪ a = u

case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ (∃ a ⊂ t \ s, s ∪ a = u) → s ⊆ u ∧ u ⊂ t
Module: Mathlib.Analysis.InnerProductSpace.Affine

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ ⟪a -ᵥ b, a -ᵥ c⟫ = dist a c ^ 2 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0

Tactic:
real_inner_comm,

Goal state after:
V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ ⟪a -ᵥ c, a -ᵥ b⟫ = dist a c ^ 2 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Affine

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ ⟪a -ᵥ c, b -ᵥ c⟫ = dist b c ^ 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0

Tactic:
real_inner_comm,

Goal state after:
V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ ⟪b -ᵥ c, a -ᵥ c⟫ = dist b c ^ 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ comul =
    map ↑↑(equiv n 𝕜) ↑↑(equiv n 𝕜) ∘ₗ
      adjoint (↑↑(equiv n 𝕜).symm ∘ₗ mul' 𝕜 (n → 𝕜) ∘ₗ map ↑↑(equiv n 𝕜) ↑↑(equiv n 𝕜)) ∘ₗ ↑↑(equiv n 𝕜).symm

Tactic:
ext

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i✝ : n
⊢ (comul ∘ₗ LinearMap.single 𝕜 (fun i ↦ 𝕜) i✝) 1 =
    ((map ↑↑(equiv n 𝕜) ↑↑(equiv n 𝕜) ∘ₗ
          adjoint (↑↑(equiv n 𝕜).symm ∘ₗ mul' 𝕜 (n → 𝕜) ∘ₗ map ↑↑(equiv n 𝕜) ↑↑(equiv n 𝕜)) ∘ₗ ↑↑(equiv n 𝕜).symm) ∘ₗ
        LinearMap.single 𝕜 (fun i ↦ 𝕜) i✝)
      1
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ comul =
    map ↑↑(equiv n 𝕜) ↑↑(equiv n 𝕜) ∘ₗ
      adjoint (↑↑(equiv n 𝕜).symm ∘ₗ mul' 𝕜 (n → 𝕜) ∘ₗ map ↑↑(equiv n 𝕜) ↑↑(equiv n 𝕜)) ∘ₗ ↑↑(equiv n 𝕜).symm

Tactic:
ext
  simp only [comp_apply, ← toLinearMap_congr, LinearEquiv.coe_coe, ← LinearEquiv.symm_apply_eq]
  simp [TensorProduct.ext_iff_inner_left, adjoint_inner_right, inner_eq_star_dotProduct]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ counit = adjoint (↑↑(equiv n 𝕜).symm ∘ₗ Algebra.linearMap 𝕜 (n → 𝕜)) ∘ₗ ↑↑(equiv n 𝕜).symm

Tactic:
ext

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i✝ : n
⊢ (counit ∘ₗ LinearMap.single 𝕜 (fun i ↦ 𝕜) i✝) 1 =
    ((adjoint (↑↑(equiv n 𝕜).symm ∘ₗ Algebra.linearMap 𝕜 (n → 𝕜)) ∘ₗ ↑↑(equiv n 𝕜).symm) ∘ₗ
        LinearMap.single 𝕜 (fun i ↦ 𝕜) i✝)
      1
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: case e_6
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : FiniteDimensional 𝕜 E
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
⊢ ((↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) ∘ₗ LinearMap.rTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)) ∘ₗ
      ↑(assocIsometry 𝕜 E E E).symm.toLinearEquiv =
    (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) ∘ₗ LinearMap.lTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)

Tactic:
ext

Goal state after:
case e_6
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : FiniteDimensional 𝕜 E
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
x✝² x✝¹ x✝ : E
⊢ ((AlgebraTensorModule.curry
          ((AlgebraTensorModule.curry
              (((↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) ∘ₗ LinearMap.rTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)) ∘ₗ
                ↑(assocIsometry 𝕜 E E E).symm.toLinearEquiv))
            x✝²))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          ((AlgebraTensorModule.curry
              ((↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) ∘ₗ LinearMap.lTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)))
            x✝²))
        x✝¹)
      x✝
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: case e_6
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : FiniteDimensional 𝕜 E
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
⊢ (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) ∘ₗ LinearMap.rTensor E (toSpanSingleton 𝕜 E (e.symm 1)) =
    ↑(lidIsometry 𝕜 E).toLinearEquiv

Tactic:
ext

Goal state after:
case e_6
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : FiniteDimensional 𝕜 E
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
x✝ : E
⊢ ((AlgebraTensorModule.curry
          ((↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) ∘ₗ LinearMap.rTensor E (toSpanSingleton 𝕜 E (e.symm 1))))
        1)
      x✝ =
    ((AlgebraTensorModule.curry ↑(lidIsometry 𝕜 E).toLinearEquiv) 1) x✝
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: case e_6
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : FiniteDimensional 𝕜 E
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
⊢ (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) ∘ₗ LinearMap.lTensor E (toSpanSingleton 𝕜 E (e.symm 1)) =
    ↑((commIsometry 𝕜 E 𝕜).trans (lidIsometry 𝕜 E)).toLinearEquiv

Tactic:
ext

Goal state after:
case e_6
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : FiniteDimensional 𝕜 E
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
x✝ : E
⊢ ((AlgebraTensorModule.curry
          ((↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) ∘ₗ LinearMap.lTensor E (toSpanSingleton 𝕜 E (e.symm 1))))
        x✝)
      1 =
    ((AlgebraTensorModule.curry ↑((commIsometry 𝕜 E 𝕜).trans (lidIsometry 𝕜 E)).toLinearEquiv) x✝) 1
Module: Mathlib.Analysis.InnerProductSpace.ExteriorPower

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ innerProductForm.flip.compAlternatingMap (ιMulti ℝ n) = innerProductForm.compAlternatingMap (ιMulti ℝ n)

Tactic:
ext

Goal state after:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝¹ x✝ : Fin n → E
⊢ (((innerProductForm.flip.compAlternatingMap (ιMulti ℝ n)) x✝¹).compAlternatingMap (ιMulti ℝ n)) x✝ =
    (((innerProductForm.compAlternatingMap (ιMulti ℝ n)) x✝¹).compAlternatingMap (ιMulti ℝ n)) x✝
Module: Mathlib.Analysis.InnerProductSpace.ExteriorPower

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝¹ x✝ : Fin n → E
⊢ (of fun i j ↦ ⟪x✝ j, x✝¹ i⟫)ᵀ = of fun i j ↦ ⟪x✝¹ j, x✝ i⟫

Tactic:
ext

Goal state after:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝¹ x✝ : Fin n → E
i✝ j✝ : Fin n
⊢ (of fun i j ↦ ⟪x✝ j, x✝¹ i⟫)ᵀ i✝ j✝ = of (fun i j ↦ ⟪x✝¹ j, x✝ i⟫) i✝ j✝
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: case e'_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
A : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
⊢ Matrix.toEuclideanLin ((toMatrix b.toBasis b.toBasis) A) = ↑b.repr.toLinearEquiv ∘ₗ A ∘ₗ ↑b.repr.symm.toLinearEquiv

Tactic:
ext

Goal state after:
case e'_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
A : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
x✝ : EuclideanSpace 𝕜 ι
i✝ : ι
⊢ ((Matrix.toEuclideanLin ((toMatrix b.toBasis b.toBasis) A)) x✝).ofLp i✝ =
    ((↑b.repr.toLinearEquiv ∘ₗ A ∘ₗ ↑b.repr.symm.toLinearEquiv) x✝).ofLp i✝
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ (((rankOne 𝕜) x) x).IsPositive

Tactic:
simp_rw [ContinuousLinearMap.isPositive_iff, isSymmetric_rankOne_self, rankOne_apply,
    inner_smul_left, RCLike.conj_mul, ← RCLike.ofReal_pow, RCLike.ofReal_nonneg]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ True ∧ ∀ (x_1 : E), 0 ≤ ‖⟪x, x_1⟫‖ ^ 2
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
⊢ f.inverse.IsClosable ↔ f.closure.toFun.ker = ⊥

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
⊢ f.inverse.IsClosable → f.closure.toFun.ker = ⊥

case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
⊢ f.closure.toFun.ker = ⊥ → f.inverse.IsClosable
Module: Mathlib.Dynamics.BirkhoffSum.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝ : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
⊢ birkhoffSum f (-g) n x = -birkhoffSum f g n x

Tactic:
by
  simp [birkhoffSum]

Goal state after:
Module: Mathlib.Dynamics.BirkhoffSum.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝ : AddCommGroup G
f : α → α
g g' : α → G
n : ℕ
x : α
⊢ birkhoffSum f (g - g') n x = birkhoffSum f g n x - birkhoffSum f g' n x

Tactic:
by
  simp [birkhoffSum]

Goal state after:
Module: Mathlib.Dynamics.BirkhoffSum.Average

Goal state before:
pp: R : Type u_1
α : Type u_2
M : Type u_3
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : DivisionSemiring S
inst✝ : Module S M
⊢ birkhoffAverage R = birkhoffAverage S

Tactic:
ext

Goal state after:
R : Type u_1
α : Type u_2
M : Type u_3
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : DivisionSemiring S
inst✝ : Module S M
x✝³ : α → α
x✝² : α → M
x✝¹ : ℕ
x✝ : α
⊢ birkhoffAverage R x✝³ x✝² x✝¹ x✝ = birkhoffAverage S x✝³ x✝² x✝¹ x✝
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
⊢ 1 < ↑n

Tactic:
by norm_cast

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
g : Submodule 𝕜 (E × F)
x : F × E
⊢ (∃ y,
      (∀ (u : WithLp 2 (F × E)) (x : E) (x_1 : F),
          (x, x_1) ∈ g → toLp 2 (x_1, -x) = u → ⟪u.fst, y.fst⟫ + ⟪u.snd, y.snd⟫ = 0) ∧
        y.ofLp = x) ↔
    ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
g : Submodule 𝕜 (E × F)
x : F × E
⊢ (∃ y,
      (∀ (u : WithLp 2 (F × E)) (x : E) (x_1 : F),
          (x, x_1) ∈ g → toLp 2 (x_1, -x) = u → ⟪u.fst, y.fst⟫ + ⟪u.snd, y.snd⟫ = 0) ∧
        y.ofLp = x) →
    ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0

case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
g : Submodule 𝕜 (E × F)
x : F × E
⊢ (∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0) →
    ∃ y,
      (∀ (u : WithLp 2 (F × E)) (x : E) (x_1 : F),
          (x, x_1) ∈ g → toLp 2 (x_1, -x) = u → ⟪u.fst, y.fst⟫ + ⟪u.snd, y.snd⟫ = 0) ∧
        y.ofLp = x
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
x : F × E
⊢ (∃ (x_1 : x.1 ∈ T†.domain), ↑T† ⟨x.1, ⋯⟩ = x.2) ↔ ∀ (a : E) (a_1 : a ∈ T.domain), ⟪↑T ⟨a, ⋯⟩, x.1⟫ - ⟪a, x.2⟫ = 0

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
x : F × E
⊢ (∃ (x_1 : x.1 ∈ T†.domain), ↑T† ⟨x.1, ⋯⟩ = x.2) → ∀ (a : E) (a_1 : a ∈ T.domain), ⟪↑T ⟨a, ⋯⟩, x.1⟫ - ⟪a, x.2⟫ = 0

case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
x : F × E
⊢ (∀ (a : E) (a_1 : a ∈ T.domain), ⟪↑T ⟨a, ⋯⟩, x.1⟫ - ⟪a, x.2⟫ = 0) → ∃ (x_1 : x.1 ∈ T†.domain), ↑T† ⟨x.1, ⋯⟩ = x.2
Module: Mathlib.Analysis.InnerProductSpace.SingularValues

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
⊢ End.HasEigenvalue (adjoint T ∘ₗ T) 0 ↔ ∃ i < finrank 𝕜 E, T.singularValues i ≤ 0

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
⊢ End.HasEigenvalue (adjoint T ∘ₗ T) 0 → ∃ i < finrank 𝕜 E, T.singularValues i ≤ 0

case mpr
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
⊢ (∃ i < finrank 𝕜 E, T.singularValues i ≤ 0) → End.HasEigenvalue (adjoint T ∘ₗ T) 0
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
ι : Type u_6
ι' : Type u_7
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
x : E ⊗[𝕜] F
e : OrthonormalBasis ι 𝕜 E
f : OrthonormalBasis ι' 𝕜 F
| x

Tactic:
← (e.toBasis.tensorProduct f.toBasis).sum_repr x

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
ι : Type u_6
ι' : Type u_7
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
x : E ⊗[𝕜] F
e : OrthonormalBasis ι 𝕜 E
f : OrthonormalBasis ι' 𝕜 F
| ∑ i, ((e.toBasis.tensorProduct f.toBasis).repr x) i • (e.toBasis.tensorProduct f.toBasis) i
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
E' : Submodule 𝕜 E
F' : Submodule 𝕜 F
iE' : Module.Finite 𝕜 ↥E'
iF' : Module.Finite 𝕜 ↥F'
y : ↥E' ⊗[𝕜] ↥F'
hx : inner 𝕜 y y = 0
hz : {(mapIncl E' F') y} ⊆ ↑(mapIncl E' F').range
e : OrthonormalBasis (Fin (finrank 𝕜 ↥E')) 𝕜 ↥E'
f : OrthonormalBasis (Fin (finrank 𝕜 ↥F')) 𝕜 ↥F'
i : Fin (finrank 𝕜 ↥E')
j : Fin (finrank 𝕜 ↥F')
⊢ ((e.toBasis.tensorProduct f.toBasis).repr y) (i, j) = 0

Tactic:
inner_self y e f,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
E' : Submodule 𝕜 E
F' : Submodule 𝕜 F
iE' : Module.Finite 𝕜 ↥E'
iF' : Module.Finite 𝕜 ↥F'
y : ↥E' ⊗[𝕜] ↥F'
hz : {(mapIncl E' F') y} ⊆ ↑(mapIncl E' F').range
e : OrthonormalBasis (Fin (finrank 𝕜 ↥E')) 𝕜 ↥E'
f : OrthonormalBasis (Fin (finrank 𝕜 ↥F')) 𝕜 ↥F'
hx : ↑(∑ i, ‖((e.toBasis.tensorProduct f.toBasis).repr y) i‖ ^ 2) = 0
i : Fin (finrank 𝕜 ↥E')
j : Fin (finrank 𝕜 ↥F')
⊢ ((e.toBasis.tensorProduct f.toBasis).repr y) (i, j) = 0