harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem ext : Function.Injective (val : αˣ → α)
  | ⟨v, i₁, vi₁, iv₁⟩, ⟨v', i₂, vi₂, iv₂⟩, e => by
    simp only at e; subst v'; congr
    simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁

Proof state:
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
vi₂ : v * i₂ = 1
iv₂ : i₂ * v = 1
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v, inv := i₂, val_inv := vi₂, inv_val := iv₂ }

Tactic:
congr

Result:
case e_inv
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
vi₂ : v * i₂ = 1
iv₂ : i₂ * v = 1
⊢ i₁ = i₂

Proof state:
case e_inv
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
vi₂ : v * i₂ = 1
iv₂ : i₂ * v = 1
⊢ i₁ = i₂

Tactic:
simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁

Result:
no goals

Proof state:
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
v' i₂ : α
vi₂ : v' * i₂ = 1
iv₂ : i₂ * v' = 1
e : ↑{ val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = ↑{ val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }

Tactic:
simp only at e

Result:
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
v' i₂ : α
vi₂ : v' * i₂ = 1
iv₂ : i₂ * v' = 1
e : v = v'
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }

Proof state:
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
v' i₂ : α
vi₂ : v' * i₂ = 1
iv₂ : i₂ * v' = 1
e : v = v'
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }

Tactic:
subst v'

Result:
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
vi₂ : v * i₂ = 1
iv₂ : i₂ * v = 1
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v, inv := i₂, val_inv := vi₂, inv_val := iv₂ }
-- Mathlib/CategoryTheory/Limits/Constructions/Pullbacks.lean
theorem hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair {C : Type u} [𝒞 : Category.{v} C]
    {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasLimit (pair X Y)]
    [HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))] : HasLimit (cospan f g) :=
  let π₁ : X ⨯ Y ⟶ X := prod.fst
  let π₂ : X ⨯ Y ⟶ Y := prod.snd
  let e := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
  HasLimit.mk
    { cone :=
        PullbackCone.mk (e ≫ π₁) (e ≫ π₂) <| by
          rw [Category.assoc, equalizer.condition]
          simp [e]
      isLimit :=
        PullbackCone.IsLimit.mk _ (fun s => equalizer.lift
          (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) <| by
            rw [← Category.assoc, limit.lift_π, ← Category.assoc, limit.lift_π]
            exact PullbackCone.condition _)
          (by simp [π₁, e]) (by simp [π₂, e]) fun s m h₁ h₂ => by
          ext
          · dsimp; simpa using h₁
          · simpa using h₂ }

Proof state:
case h.h₁
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = s.fst
h₂ : m ≫ e ≫ π₂ = s.snd
⊢ (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.fst =
    ((fun s => equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯) s ≫
        equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
      prod.fst

Tactic:
dsimp

Result:
case h.h₁
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = s.fst
h₂ : m ≫ e ≫ π₂ = s.snd
⊢ (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.fst =
    (equalizer.lift (prod.lift s.fst s.snd) ⋯ ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.fst

Proof state:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ ∀ (s : PullbackCone f g),
    (fun s => equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯) s ≫ e ≫ π₁ =
      s.fst

Tactic:
simp [π₁, e]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem eventually_prod_principal_iff {p : α × β → Prop} {s : Set β} :
    (∀ᶠ x : α × β in f ×ˢ 𝓟 s, p x) ↔ ∀ᶠ x : α in f, ∀ y : β, y ∈ s → p (x, y)

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
p : α × β → Prop
s : Set β
⊢ {a | ∀ b ∈ s, (a, b) ∈ {x | p x}} ∈ f ↔ {x | ∀ y ∈ s, p (x, y)} ∈ f

Tactic:
simp only [mem_setOf_eq]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
p : α × β → Prop
s : Set β
⊢ (∀ᶠ (x : α × β) in f ×ˢ 𝓟 s, p x) ↔ ∀ᶠ (x : α) in f, ∀ y ∈ s, p (x, y)

Tactic:
rw [eventually_iff, eventually_iff, mem_prod_principal]

Result:
α : Type u_1
β : Type u_2
f : Filter α
p : α × β → Prop
s : Set β
⊢ {a | ∀ b ∈ s, (a, b) ∈ {x | p x}} ∈ f ↔ {x | ∀ y ∈ s, p (x, y)} ∈ f
-- Mathlib/Data/Set/Image.lean
theorem preimage_iterate_eq {f : α → α} {n : ℕ} : Set.preimage f^[n] = (Set.preimage f)^[n]

Proof state:
case succ
α : Type u_1
f : α → α
n : ℕ
ih : preimage f^[n] = (preimage f)^[n]
⊢ preimage f^[n + 1] = (preimage f)^[n + 1]

Tactic:
rw [iterate_succ, iterate_succ', preimage_comp_eq, ih]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
n : ℕ
⊢ preimage f^[n] = (preimage f)^[n]

Tactic:
induction n with
| zero => simp
| succ n ih => rw [iterate_succ, iterate_succ', preimage_comp_eq, ih]

Result:
no goals

Proof state:
case zero
α : Type u_1
f : α → α
⊢ preimage f^[0] = (preimage f)^[0]

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp]
lemma map_const (μ : Measure α) {f : α → β} (hf : Measurable f) :
    map (const γ μ) f = const γ (μ.map f)

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure α
f : α → β
hf : Measurable f
x : γ
s : Set β
hs : MeasurableSet s
⊢ (((const γ μ).map f) x) s = ((const γ (Measure.map f μ)) x) s

Tactic:
rw [map_apply' _ hf _ hs, const_apply, const_apply, Measure.map_apply hf hs]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure α
f : α → β
hf : Measurable f
⊢ (const γ μ).map f = const γ (Measure.map f μ)

Tactic:
ext x s hs

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure α
f : α → β
hf : Measurable f
x : γ
s : Set β
hs : MeasurableSet s
⊢ (((const γ μ).map f) x) s = ((const γ (Measure.map f μ)) x) s
-- Mathlib/NumberTheory/LSeries/SumCoeff.lean
theorem LSeries_eq_mul_integral_of_nonneg (f : ℕ → ℝ) {r : ℝ} (hr : 0 ≤ r) {s : ℂ} (hs : r < s.re)
    (hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ (n : ℝ) ^ r) (hf : ∀ n, 0 ≤ f n) :
    LSeries (fun n ↦ f n) s =
      s * ∫ t in Set.Ioi (1 : ℝ), (∑ k ∈ Icc 1 ⌊t⌋₊, (f k : ℂ)) * t ^ (-(s + 1)) :=
  LSeries_eq_mul_integral' _ hr hs <| hO.congr_left fun _ ↦ by simp [abs_of_nonneg (hf _)]

Proof state:
f : ℕ → ℝ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hO : (fun n => ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n => ↑n ^ r
hf : ∀ (n : ℕ), 0 ≤ f n
x✝ : ℕ
⊢ ∑ k ∈ Icc 1 x✝, f k = ∑ k ∈ Icc 1 x✝, ‖↑(f k)‖

Tactic:
simp [abs_of_nonneg (hf _)]

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
lemma dens_map_le [Fintype β] (f : α ↪ β) : dens (s.map f) ≤ dens s

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
⊢ (map f s).dens ≤ s.dens

Tactic:
cases isEmpty_or_nonempty α

Result:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : IsEmpty α
⊢ (map f s).dens ≤ s.dens

case inr
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ (map f s).dens ≤ s.dens

Proof state:
case inr
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ ↑(#s) / ↑(Fintype.card β) ≤ ↑(#s) / ↑(Fintype.card α)

Tactic:
gcongr

Result:
case inr.ha
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ 0 ≤ ↑(#s)

case inr.hc
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ 0 < ↑(Fintype.card α)

case inr.h.h
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ Fintype.card α ≤ Fintype.card β

Proof state:
case inr
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ (map f s).dens ≤ s.dens

Tactic:
simp_rw [dens, card_map]

Result:
case inr
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ ↑(#s) / ↑(Fintype.card β) ≤ ↑(#s) / ↑(Fintype.card α)

Proof state:
case inr.h.h
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
exact Fintype.card_le_of_injective _ f.2

Result:
no goals

Proof state:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : IsEmpty α
⊢ (map f s).dens ≤ s.dens

Tactic:
simp [Subsingleton.elim s ∅]

Result:
no goals

Proof state:
case inr.ha
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ 0 ≤ ↑(#s)

Tactic:
positivity

Result:
no goals

Proof state:
case inr.hc
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ 0 < ↑(Fintype.card α)

Tactic:
exact mod_cast Fintype.card_pos

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[reassoc (attr := simp)]
lemma cyclesIso_inv_comp_iCycles : h.cyclesIso.inv ≫ S.iCycles = h.i

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : S.HasLeftHomology
⊢ h.cyclesIso.inv ≫ S.iCycles = h.i

Tactic:
simp only [← h.cyclesIso_hom_comp_i, Iso.inv_hom_id_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {h}
    (hl : DistinctKeys l) : getValueCast a (eraseKey k l) h =
      getValueCast a l (containsKey_of_containsKey_eraseKey hl h)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
h✝ : containsKey a (eraseKey k l) = true
h : (k == a) = false ∧ containsKey a l = true
hl : DistinctKeys l
⊢ (if false = true then none else getValueCast? a l) = some (getValueCast a l ⋯)

Tactic:
simp [← getValueCast?_eq_some_getValueCast]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
h✝ : containsKey a (eraseKey k l) = true
h : (k == a) = false ∧ containsKey a l = true
hl : DistinctKeys l
⊢ getValueCast a (eraseKey k l) h✝ = getValueCast a l ⋯

Tactic:
rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, getValueCast?_eraseKey hl, h.1]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
h✝ : containsKey a (eraseKey k l) = true
h : (k == a) = false ∧ containsKey a l = true
hl : DistinctKeys l
⊢ (if false = true then none else getValueCast? a l) = some (getValueCast a l ⋯)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
h : containsKey a (eraseKey k l) = true
hl : DistinctKeys l
⊢ getValueCast a (eraseKey k l) h = getValueCast a l ⋯

Tactic:
rw [containsKey_eraseKey hl, Bool.and_eq_true, Bool.not_eq_true'] at h

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
h✝ : containsKey a (eraseKey k l) = true
h : (k == a) = false ∧ containsKey a l = true
hl : DistinctKeys l
⊢ getValueCast a (eraseKey k l) h✝ = getValueCast a l ⋯
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem continuousOn_tan : ContinuousOn tan {x | cos x ≠ 0}

Proof state:
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
⊢ (fun x => sin x / cos x) = tan

Tactic:
ext1 x

Result:
case h
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
x : ℝ
⊢ sin x / cos x = tan x

Proof state:
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
⊢ ContinuousOn tan {x | cos x ≠ 0}

Tactic:
have h_eq : (fun x => sin x / cos x) = tan := by ext1 x; rw [tan_eq_sin_div_cos]

Result:
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
h_eq : (fun x => sin x / cos x) = tan
⊢ ContinuousOn tan {x | cos x ≠ 0}

Proof state:
⊢ ContinuousOn tan {x | cos x ≠ 0}

Tactic:
suffices ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0} by
  have h_eq : (fun x => sin x / cos x) = tan := by ext1 x; rw [tan_eq_sin_div_cos]
  rwa [h_eq] at this

Result:
⊢ ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}

Proof state:
case h
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
x : ℝ
⊢ sin x / cos x = tan x

Tactic:
rw [tan_eq_sin_div_cos]

Result:
no goals

Proof state:
⊢ ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}

Tactic:
exact continuousOn_sin.div continuousOn_cos fun x => id

Result:
no goals

Proof state:
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
h_eq : (fun x => sin x / cos x) = tan
⊢ ContinuousOn tan {x | cos x ≠ 0}

Tactic:
rwa [h_eq] at this

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/DotProduct.lean
lemma self_mul_conjTranspose_mulVec_eq_zero (A : Matrix m n R) (v : m → R) :
    (A * Aᴴ) *ᵥ v = 0 ↔ Aᴴ *ᵥ v = 0

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
v : m → R
⊢ (A * Aᴴ) *ᵥ v = 0 ↔ Aᴴ *ᵥ v = 0

Tactic:
simpa only [conjTranspose_conjTranspose] using conjTranspose_mul_self_mulVec_eq_zero Aᴴ _

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
lemma comap_map {f : α → β} (hf : f.Injective) : (M.map f hf.injOn).comap f = M

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : Injective f
⊢ (M.map f ⋯).comap f = M

Tactic:
simp [ext_iff_indep, preimage_image_eq _ hf, and_iff_left hf.injOn,
  image_eq_image hf]

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
lemma fderiv_fourierIntegral
    [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] {μ : Measure V}
    (hf : Integrable f μ) (hf' : Integrable (fun v : V ↦ ‖v‖ * ‖f v‖) μ) :
    fderiv ℝ (fourierIntegral 𝐞 μ L.toLinearMap₂ f) =
      fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f)

Proof state:
case h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ
w : W
⊢ fderiv ℝ (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w = fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w

Tactic:
exact (hasFDerivAt_fourierIntegral L hf hf' w).fderiv

Result:
no goals

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ
⊢ fderiv ℝ (fourierIntegral 𝐞 μ L.toLinearMap₂ f) = fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f)

Tactic:
ext w : 1

Result:
case h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ
w : W
⊢ fderiv ℝ (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w = fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
@[simp] lemma divInt_nonneg_iff_of_pos_right {a b : ℤ} (hb : 0 < b) : 0 ≤ a /. b ↔ 0 ≤ a

Proof state:
case mk'
a b : ℤ
hb : 0 < b
n : ℤ
d : ℕ
hd : d ≠ 0
hnd : n.natAbs.Coprime d
hab : a /. b = { num := n, den := d, den_nz := hd, reduced := hnd }
⊢ 0 ≤ { num := n, den := d, den_nz := hd, reduced := hnd } ↔ 0 ≤ a

Tactic:
rw [mk'_eq_divInt, divInt_eq_iff hb.ne' (mod_cast hd)] at hab

Result:
case mk'
a b : ℤ
hb : 0 < b
n : ℤ
d : ℕ
hd : d ≠ 0
hnd : n.natAbs.Coprime d
hab : a * ↑d = n * b
⊢ 0 ≤ { num := n, den := d, den_nz := hd, reduced := hnd } ↔ 0 ≤ a

Proof state:
a b : ℤ
hb : 0 < b
⊢ 0 ≤ a /. b ↔ 0 ≤ a

Tactic:
rcases hab : a /. b with ⟨n, d, hd, hnd⟩

Result:
case mk'
a b : ℤ
hb : 0 < b
n : ℤ
d : ℕ
hd : d ≠ 0
hnd : n.natAbs.Coprime d
hab : a /. b = { num := n, den := d, den_nz := hd, reduced := hnd }
⊢ 0 ≤ { num := n, den := d, den_nz := hd, reduced := hnd } ↔ 0 ≤ a

Proof state:
case mk'
a b : ℤ
hb : 0 < b
n : ℤ
d : ℕ
hd : d ≠ 0
hnd : n.natAbs.Coprime d
hab : a * ↑d = n * b
⊢ 0 ≤ { num := n, den := d, den_nz := hd, reduced := hnd } ↔ 0 ≤ a

Tactic:
rw [← num_nonneg, ← Int.mul_nonneg_iff_of_pos_right hb, ← hab,
  Int.mul_nonneg_iff_of_pos_right (mod_cast Nat.pos_of_ne_zero hd)]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem _root_.Function.LeftInverse.filter_comap {f : α → β} {g : β → α} (hfg : LeftInverse g f) :
    RightInverse (comap g) (comap f) := fun F ↦ by
  rw [comap_comap, hfg.comp_eq_id, comap_id]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
⊢ comap f (comap g F) = F

Tactic:
rw [comap_comap, hfg.comp_eq_id, comap_id]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
theorem lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable (x : V → ℝ) :
    Matrix.toLinearMap₂' ℝ (G.lapMatrix ℝ) x x = 0 ↔
      ∀ i j : V, G.Reachable i j → x i = x j

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
⊢ (((toLinearMap₂' ℝ) (lapMatrix ℝ G)) x) x = 0 ↔ ∀ (i j : V), G.Reachable i j → x i = x j

Tactic:
rw [lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj]

Result:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
⊢ (∀ (i j : V), G.Adj i j → x i = x j) ↔ ∀ (i j : V), G.Reachable i j → x i = x j

Proof state:
case cons
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j u✝ v✝ w✝ : V
hA : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h' : x v✝ = x w✝
⊢ x u✝ = x w✝

Tactic:
exact (h _ _ hA).trans h'

Result:
no goals

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
⊢ (∀ (i j : V), G.Adj i j → x i = x j) → ∀ (i j : V), G.Reachable i j → x i = x j

Tactic:
intro h i j ⟨w⟩

Result:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j : V
w : G.Walk i j
⊢ x i = x j

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
⊢ (∀ (i j : V), G.Adj i j → x i = x j) ↔ ∀ (i j : V), G.Reachable i j → x i = x j

Tactic:
refine ⟨?_, fun h i j hA ↦ h i j hA.reachable⟩

Result:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
⊢ (∀ (i j : V), G.Adj i j → x i = x j) → ∀ (i j : V), G.Reachable i j → x i = x j

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j : V
w : G.Walk i j
⊢ x i = x j

Tactic:
induction w with
| nil => rfl
| cons hA _ h' => exact (h _ _ hA).trans h'

Result:
no goals

Proof state:
case nil
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j u✝ : V
⊢ x u✝ = x u✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Int.lean
theorem toNat_add_toNat_neg_eq_nnnorm (n : ℤ) : ↑n.toNat + ↑(-n).toNat = ‖n‖₊

Proof state:
n : ℤ
⊢ ↑n.toNat + ↑(-n).toNat = ‖n‖₊

Tactic:
rw [← Nat.cast_add, toNat_add_toNat_neg_eq_natAbs, NNReal.natCast_natAbs]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₂_of_isCharTwoJNeZeroNF : W.b₂ = 1 + 4 * W.a₂

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 1 ^ 2 + 4 * W.a₂ = 1 + 4 * W.a₂

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.b₂ = 1 + 4 * W.a₂

Tactic:
rw [b₂, a₁_of_isCharTwoJNeZeroNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 1 ^ 2 + 4 * W.a₂ = 1 + 4 * W.a₂