harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem entourageProd_subset [UniformSpace α] [UniformSpace β]
    {s : Set ((α × β) × α × β)} (h : s ∈ 𝓤 (α × β)) :
    ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s

Proof state:
case intro
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set ((α × β) × α × β)
h : s ∈ 𝓤 (α × β)
w : Set (α × α) × Set (β × β)
hw : (w.1 ∈ 𝓤 α ∧ w.2 ∈ 𝓤 β) ∧ entourageProd (id w.1) (id w.2) ⊆ s
⊢ ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s

Tactic:
use w.1, hw.1.1, w.2, hw.1.2, hw.2

Result:
no goals

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set ((α × β) × α × β)
h : s ∈ 𝓤 (α × β)
⊢ ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s

Tactic:
rcases (((𝓤 α).basis_sets.uniformity_prod (𝓤 β).basis_sets).mem_iff' s).1 h with ⟨w, hw⟩

Result:
case intro
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set ((α × β) × α × β)
h : s ∈ 𝓤 (α × β)
w : Set (α × α) × Set (β × β)
hw : (w.1 ∈ 𝓤 α ∧ w.2 ∈ 𝓤 β) ∧ entourageProd (id w.1) (id w.2) ⊆ s
⊢ ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem left_unitality_hom  (X : C) :
    δ F (𝟙_ C) X ≫ η F ▷ F.obj X ≫ (λ_ (F.obj X)).hom = F.map (λ_ X).hom

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F (𝟙_ C) X ≫ η F ▷ F.obj X ≫ (λ_ (F.obj X)).hom = F.map (λ_ X).hom

Tactic:
rw [← Category.assoc, ← Iso.eq_comp_inv, left_unitality, ← Category.assoc,
  ← F.map_comp, Iso.hom_inv_id, F.map_id, id_comp]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearPMap.lean
theorem inverse_closure (hf : LinearMap.ker f.toFun = ⊥) (hf' : f.IsClosable)
    (hcf : LinearMap.ker f.closure.toFun = ⊥) :
    f.inverse.closure = f.closure.inverse

Proof state:
case h
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
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : f.IsClosable
hcf : LinearMap.ker f.closure.toFun = ⊥
⊢ f.inverse.closure.graph = f.closure.inverse.graph

Tactic:
rw [closure_inverse_graph hf hf' hcf,
  ((inverse_isClosable_iff hf hf').mpr hcf).graph_closure_eq_closure_graph]

Result:
no goals

Proof state:
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
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : f.IsClosable
hcf : LinearMap.ker f.closure.toFun = ⊥
⊢ f.inverse.closure = f.closure.inverse

Tactic:
apply eq_of_eq_graph

Result:
case h
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
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : f.IsClosable
hcf : LinearMap.ker f.closure.toFun = ⊥
⊢ f.inverse.closure.graph = f.closure.inverse.graph
-- Mathlib/Algebra/Prime/Lemmas.lean
theorem Irreducible.of_map {F : Type*} [Monoid M] [Monoid N] [FunLike F M N] [MonoidHomClass F M N]
    {f : F} [IsLocalHom f] {x} (hfx : Irreducible (f x)) : Irreducible x :=
  ⟨fun hu ↦ hfx.not_unit <| hu.map f,
   by rintro p q rfl
      exact (hfx.isUnit_or_isUnit <| map_mul f p q).imp (.of_map f _) (.of_map f _)⟩

Proof state:
M : Type u_1
N : Type u_2
F : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : FunLike F M N
inst✝¹ : MonoidHomClass F M N
f : F
inst✝ : IsLocalHom f
p q : M
hfx : Irreducible (f (p * q))
⊢ IsUnit p ∨ IsUnit q

Tactic:
exact (hfx.isUnit_or_isUnit <| map_mul f p q).imp (.of_map f _) (.of_map f _)

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
F : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : FunLike F M N
inst✝¹ : MonoidHomClass F M N
f : F
inst✝ : IsLocalHom f
x : M
hfx : Irreducible (f x)
⊢ ∀ (a b : M), x = a * b → IsUnit a ∨ IsUnit b

Tactic:
rintro p q rfl

Result:
M : Type u_1
N : Type u_2
F : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : FunLike F M N
inst✝¹ : MonoidHomClass F M N
f : F
inst✝ : IsLocalHom f
p q : M
hfx : Irreducible (f (p * q))
⊢ IsUnit p ∨ IsUnit q
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_sub_eq_right_of_degree_lt (h : degree p < degree q) : degree (p - q) = degree q

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < q.degree
⊢ (p - q).degree = q.degree

Tactic:
rw [← degree_neg q] at h

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ (p - q).degree = q.degree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ (p - q).degree = q.degree

Tactic:
rw [sub_eq_add_neg, degree_add_eq_right_of_degree_lt h, degree_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_eq_fst_find?_zipIdx {xs : Array α} {p : α → Bool} :
    xs.findIdx? p = (xs.zipIdx.find? fun ⟨x, _⟩ => p x).map (·.2)

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx? p { toList := xs } =
    Option.map (fun x => x.snd)
      (find?
        (fun x =>
          match x with
          | (x, snd) => p x)
        { toList := xs }.zipIdx)

Tactic:
simp [List.findIdx?_eq_fst_find?_zipIdx]

Result:
no goals

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
⊢ findIdx? p xs =
    Option.map (fun x => x.snd)
      (find?
        (fun x =>
          match x with
          | (x, snd) => p x)
        xs.zipIdx)

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx? p { toList := xs } =
    Option.map (fun x => x.snd)
      (find?
        (fun x =>
          match x with
          | (x, snd) => p x)
        { toList := xs }.zipIdx)
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem bot_or_exists_ne_one (H : Subgroup G) : H = ⊥ ∨ ∃ x ∈ H, x ≠ (1 : G)

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H = ⊥ ∨ ∃ x ∈ H, x ≠ 1

Tactic:
convert H.bot_or_nontrivial

Result:
case h.e'_2.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ Nontrivial ↥H

Proof state:
case h.e'_2.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ Nontrivial ↥H

Tactic:
rw [nontrivial_iff_exists_ne_one]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem dist_eq_of_L2 (x y : PiLp 2 β) :
    dist x y = √(∑ i, dist (x i) (y i) ^ 2)

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ dist x y = √(∑ i : ι, dist (x i) (y i) ^ 2)

Tactic:
simp_rw [dist_eq_norm, norm_eq_of_L2, sub_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem map_sub_range' (a s n : Nat) (h : a ≤ s) :
    map (· - a) (range' s n step) = range' (s - a) n step

Proof state:
step a s n : Nat
h : a ≤ s
⊢ map (fun x => x - a) (range' s n step) = range' (s - a) n step

Tactic:
conv => lhs; rw [← Nat.add_sub_cancel' h]

Result:
step a s n : Nat
h : a ≤ s
⊢ map (fun x => x - a) (range' (a + (s - a)) n step) = range' (s - a) n step

Proof state:
case h
step a s n : Nat
h : a ≤ s
x : Nat
⊢ ((fun x => x - a) ∘ fun x => a + x) x = id x

Tactic:
apply Nat.add_sub_cancel_left

Result:
no goals

Proof state:
step a s n : Nat
h : a ≤ s
⊢ map (fun x => x - a) (range' (a + (s - a)) n step) = range' (s - a) n step

Tactic:
rw [← map_add_range', map_map, (?_ : _∘_ = _), map_id]

Result:
step a s n : Nat
h : a ≤ s
⊢ ((fun x => x - a) ∘ fun x => a + x) = id

Proof state:
step a s n : Nat
h : a ≤ s
⊢ ((fun x => x - a) ∘ fun x => a + x) = id

Tactic:
funext x

Result:
case h
step a s n : Nat
h : a ≤ s
x : Nat
⊢ ((fun x => x - a) ∘ fun x => a + x) x = id x
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_eval_cast (n k : ℕ) :
    (((ascPochhammer ℕ n).eval k : ℕ) : S) = ((ascPochhammer S n).eval k : S)

Proof state:
S : Type u
inst✝ : Semiring S
n k : ℕ
⊢ ↑(eval k (ascPochhammer ℕ n)) = eval (↑k) (ascPochhammer S n)

Tactic:
rw [← ascPochhammer_map (algebraMap ℕ S), eval_map, ← eq_natCast (algebraMap ℕ S),
    eval₂_at_natCast,Nat.cast_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y → x % y < y

Proof state:
n : Nat
x y : BitVec n
⊢ 0 < y → x % y < y

Tactic:
simp only [ofNat_eq_ofNat, lt_def, toNat_ofNat, Nat.zero_mod, umod, toNat_ofNatLt]

Result:
n : Nat
x y : BitVec n
⊢ 0 < y.toNat → (x % y).toNat < y.toNat

Proof state:
n : Nat
x y : BitVec n
⊢ 0 < y.toNat → (x % y).toNat < y.toNat

Tactic:
apply Nat.mod_lt

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_natCast (n : ℕ) : fract (n : α) = 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
n : ℕ
⊢ fract ↑n = 0

Tactic:
simp [fract]

Result:
no goals
-- Mathlib/Computability/EpsilonNFA.lean
theorem toεNFA_εClosure (M : NFA α σ) (S : Set σ) : M.toεNFA.εClosure S = S

Proof state:
case h.step
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a s✝ : σ
a✝ : M.toεNFA.εClosure S s✝
h : a ∈ M.toεNFA.step s✝ none
⊢ a ∈ S

Tactic:
cases h

Result:
no goals

Proof state:
case h
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ M.toεNFA.εClosure S → a ∈ S

Tactic:
rintro (⟨_, h⟩ | ⟨_, _, h, _⟩)

Result:
case h.base
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : σ
h : a ∈ S
⊢ a ∈ S

case h.step
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a s✝ : σ
a✝ : M.toεNFA.εClosure S s✝
h : a ∈ M.toεNFA.step s✝ none
⊢ a ∈ S

Proof state:
case h.base
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : σ
h : a ∈ S
⊢ a ∈ S

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
⊢ M.toεNFA.εClosure S = S

Tactic:
ext a

Result:
case h
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ M.toεNFA.εClosure S ↔ a ∈ S

Proof state:
case h
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ M.toεNFA.εClosure S ↔ a ∈ S

Tactic:
refine ⟨?_, εNFA.εClosure.base _⟩

Result:
case h
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ M.toεNFA.εClosure S → a ∈ S
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem idxOf_eq_size [BEq α] [LawfulBEq α] {l : Array α} (h : a ∉ l) : l.idxOf a = l.size

Proof state:
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : Array α
h : ¬a ∈ l
⊢ idxOf a l = l.size

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
h : ¬a ∈ { toList := l }
⊢ idxOf a { toList := l } = { toList := l }.size

Proof state:
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
h : ¬a ∈ { toList := l }
⊢ ¬?m.97767 ∈ ?m.97770

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
h : ¬a ∈ { toList := l }
⊢ idxOf a { toList := l } = { toList := l }.size

Tactic:
simp [List.idxOf_eq_length (by simpa using h)]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
lemma induceHom_injective (hi : Set.InjOn φ s) :
    Function.Injective (induceHom φ φst)

Proof state:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
s : Set V
t : Set W
φ : G →g G'
φst : Set.MapsTo (⇑φ) s t
hi : Set.InjOn (⇑φ) s
⊢ Injective ⇑(induceHom φ φst)

Tactic:
erw [Set.MapsTo.restrict_inj] <;> assumption

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
lemma card_le_card_of_surjective {α : Type u} {β : Type v} [Finite α] (f : α → β)
    (hf : Surjective f) : Nat.card β ≤ Nat.card α

Proof state:
α : Type u
β : Type v
inst✝ : Finite α
f : α → β
hf : Surjective f
⊢ Nat.card β ≤ Nat.card α

Tactic:
have : lift.{u} #β ≤ lift.{v} #α := mk_le_of_surjective (ULift.map_surjective.2 hf)

Result:
α : Type u
β : Type v
inst✝ : Finite α
f : α → β
hf : Surjective f
this : lift.{u, v} #β ≤ lift.{v, u} #α
⊢ Nat.card β ≤ Nat.card α

Proof state:
α : Type u
β : Type v
inst✝ : Finite α
f : α → β
hf : Surjective f
this : lift.{u, v} #β ≤ lift.{v, u} #α
⊢ lift.{v, u} #α < ℵ₀

Tactic:
simp [lt_aleph0_of_finite]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : Finite α
f : α → β
hf : Surjective f
this : lift.{u, v} #β ≤ lift.{v, u} #α
⊢ Nat.card β ≤ Nat.card α

Tactic:
simpa using toNat_le_toNat this (by simp [lt_aleph0_of_finite])

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem append_nil (s : Seq α) : append s nil = s

Proof state:
α : Type u
s : Seq α
⊢ s.append nil = s

Tactic:
apply coinduction2 s

Result:
case H
α : Type u
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = s.append nil ∧ s2 = s) (s.append nil).destruct s.destruct

Proof state:
case H.cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ x✝ = x✝ ∧ ∃ s, s✝.append nil = s.append nil ∧ s✝ = s

Tactic:
exact ⟨rfl, _, rfl, rfl⟩

Result:
no goals

Proof state:
case H.nil
α : Type u
s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = s.append nil ∧ s2 = s) (nil.append nil).destruct nil.destruct

Tactic:
trivial

Result:
no goals

Proof state:
case H.cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = s.append nil ∧ s2 = s) (some (x✝, s✝.append nil)) (some (x✝, s✝))

Tactic:
dsimp

Result:
case H.cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ x✝ = x✝ ∧ ∃ s, s✝.append nil = s.append nil ∧ s✝ = s

Proof state:
case H
α : Type u
s✝ s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = s.append nil ∧ s2 = s) (s.append nil).destruct s.destruct

Tactic:
cases s

Result:
case H.nil
α : Type u
s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = s.append nil ∧ s2 = s) (nil.append nil).destruct nil.destruct

case H.cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = s.append nil ∧ s2 = s) ((cons x✝ s✝).append nil).destruct (cons x✝ s✝).destruct

Proof state:
case H
α : Type u
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = s.append nil ∧ s2 = s) (s.append nil).destruct s.destruct

Tactic:
intro s

Result:
case H
α : Type u
s✝ s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = s.append nil ∧ s2 = s) (s.append nil).destruct s.destruct

Proof state:
case H.cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = s.append nil ∧ s2 = s) ((cons x✝ s✝).append nil).destruct (cons x✝ s✝).destruct

Tactic:
rw [cons_append, destruct_cons, destruct_cons]

Result:
case H.cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = s.append nil ∧ s2 = s) (some (x✝, s✝.append nil)) (some (x✝, s✝))
-- Mathlib/Data/Real/EReal.lean
theorem coe_toReal_le {x : EReal} (h : x ≠ ⊥) : ↑x.toReal ≤ x

Proof state:
x : EReal
h : x ≠ ⊥
⊢ ↑x.toReal ≤ x

Tactic:
by_cases h' : x = ⊤

Result:
case pos
x : EReal
h : x ≠ ⊥
h' : x = ⊤
⊢ ↑x.toReal ≤ x

case neg
x : EReal
h : x ≠ ⊥
h' : ¬x = ⊤
⊢ ↑x.toReal ≤ x

Proof state:
case pos
x : EReal
h : x ≠ ⊥
h' : x = ⊤
⊢ ↑x.toReal ≤ x

Tactic:
simp only [h', le_top]

Result:
no goals

Proof state:
case neg
x : EReal
h : x ≠ ⊥
h' : ¬x = ⊤
⊢ ↑x.toReal ≤ x

Tactic:
simp only [le_refl, coe_toReal h' h]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_congr (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} :
    f =o[𝓝 b] g ↔ (f ∘ e) =o[𝓝 (e.symm b)] (g ∘ e)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 (e.symm b)) (f ∘ ⇑e) (g ∘ ⇑e)

Tactic:
exact forall₂_congr fun c _hc => e.isBigOWith_congr

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ f =o[𝓝 b] g ↔ (f ∘ ⇑e) =o[𝓝 (e.symm b)] (g ∘ ⇑e)

Tactic:
simp only [IsLittleO_def]

Result:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 (e.symm b)) (f ∘ ⇑e) (g ∘ ⇑e)
-- Mathlib/Analysis/Fourier/FourierTransform.lean
theorem fourierIntegral_const_smul (e : AddChar 𝕜 𝕊) (μ : Measure V)
    (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (r : ℂ) :
    fourierIntegral e μ L (r • f) = r • fourierIntegral e μ L f

Proof state:
case h
𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
w : W
⊢ fourierIntegral e μ L (r • f) w = (r • fourierIntegral e μ L f) w

Tactic:
simp only [Pi.smul_apply, fourierIntegral, smul_comm _ r, integral_smul]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
⊢ fourierIntegral e μ L (r • f) = r • fourierIntegral e μ L f

Tactic:
ext1 w

Result:
case h
𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
w : W
⊢ fourierIntegral e μ L (r • f) w = (r • fourierIntegral e μ L f) w
-- Mathlib/CategoryTheory/Preadditive/Yoneda/Projective.lean
theorem projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj (P : C) :
    Projective P ↔ (preadditiveCoyonedaObj P).PreservesEpimorphisms

Proof state:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
h : (preadditiveCoyonedaObj P ⋙ forget (ModuleCat (End P)ᵐᵒᵖ)).PreservesEpimorphisms
⊢ (preadditiveCoyonedaObj P).PreservesEpimorphisms

Tactic:
exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveCoyonedaObj P)
    (forget _)

Result:
no goals

Proof state:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (preadditiveCoyonedaObj P).PreservesEpimorphisms → (coyoneda.obj (op P)).PreservesEpimorphisms

Tactic:
intro

Result:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
a✝ : (preadditiveCoyonedaObj P).PreservesEpimorphisms
⊢ (coyoneda.obj (op P)).PreservesEpimorphisms

Proof state:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
a✝ : (preadditiveCoyonedaObj P).PreservesEpimorphisms
⊢ (coyoneda.obj (op P)).PreservesEpimorphisms

Tactic:
exact (inferInstance : (preadditiveCoyonedaObj P ⋙ forget _).PreservesEpimorphisms)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Projective P ↔ (preadditiveCoyonedaObj P).PreservesEpimorphisms

Tactic:
rw [projective_iff_preservesEpimorphisms_coyoneda_obj]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (coyoneda.obj (op P)).PreservesEpimorphisms ↔ (preadditiveCoyonedaObj P).PreservesEpimorphisms

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (coyoneda.obj (op P)).PreservesEpimorphisms ↔ (preadditiveCoyonedaObj P).PreservesEpimorphisms

Tactic:
refine ⟨fun h : (preadditiveCoyonedaObj P ⋙ forget _).PreservesEpimorphisms => ?_, ?_⟩

Result:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
h : (preadditiveCoyonedaObj P ⋙ forget (ModuleCat (End P)ᵐᵒᵖ)).PreservesEpimorphisms
⊢ (preadditiveCoyonedaObj P).PreservesEpimorphisms

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (preadditiveCoyonedaObj P).PreservesEpimorphisms → (coyoneda.obj (op P)).PreservesEpimorphisms
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_add_coeff_mul (f g : R[X]) :
    (f * g).coeff (f.natDegree + g.natDegree) = f.coeff f.natDegree * g.coeff g.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
f g : R[X]
⊢ (f * g).coeff (f.natDegree + g.natDegree) = f.coeff f.natDegree * g.coeff g.natDegree

Tactic:
simp only [coeff_natDegree, coeff_mul_degree_add_degree]

Result:
no goals
-- Mathlib/RingTheory/Coalgebra/Basic.lean
theorem comul_comp_lsingle (i : ι) :
    comul ∘ₗ (lsingle i : A i →ₗ[R] _) = TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul

Proof state:
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i : ι
⊢ comul ∘ₗ lsingle i = TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul

Tactic:
ext

Result:
case h
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i : ι
x✝ : A i
⊢ (comul ∘ₗ lsingle i) x✝ = (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) x✝

Proof state:
case h
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i : ι
x✝ : A i
⊢ (comul ∘ₗ lsingle i) x✝ = (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mem_mapIdx {b : β} {l : Vector α n} :
    b ∈ l.mapIdx f ↔ ∃ (i : Nat) (h : i < n), f i l[i] = b

Proof state:
case mpr
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
b : β
l : Vector α n
⊢ (∃ i h, f i l[i] = b) → b ∈ mapIdx f l

Tactic:
rintro ⟨i, h, rfl⟩

Result:
case mpr.intro.intro
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
l : Vector α n
i : Nat
h : i < n
⊢ f i l[i] ∈ mapIdx f l

Proof state:
case mpr.intro.intro
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
l : Vector α n
i : Nat
h : i < n
⊢ ∃ i_1 h_1, (mapIdx f l)[i_1] = f i l[i]

Tactic:
exact ⟨i, by simpa using h, by simp⟩

Result:
no goals

Proof state:
case mp
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
b : β
l : Vector α n
h : b ∈ mapIdx f l
⊢ ∃ i h, f i l[i] = b

Tactic:
exact exists_of_mem_mapIdx h

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
l : Vector α n
i : Nat
h : i < n
⊢ (mapIdx f l)[i] = f i l[i]

Tactic:
simp

Result:
no goals

Proof state:
case mp
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
b : β
l : Vector α n
⊢ b ∈ mapIdx f l → ∃ i h, f i l[i] = b

Tactic:
intro h

Result:
case mp
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
b : β
l : Vector α n
h : b ∈ mapIdx f l
⊢ ∃ i h, f i l[i] = b

Proof state:
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
b : β
l : Vector α n
⊢ b ∈ mapIdx f l ↔ ∃ i h, f i l[i] = b

Tactic:
constructor

Result:
case mp
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
b : β
l : Vector α n
⊢ b ∈ mapIdx f l → ∃ i h, f i l[i] = b

case mpr
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
b : β
l : Vector α n
⊢ (∃ i h, f i l[i] = b) → b ∈ mapIdx f l

Proof state:
case mpr.intro.intro
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
l : Vector α n
i : Nat
h : i < n
⊢ f i l[i] ∈ mapIdx f l

Tactic:
rw [mem_iff_getElem]

Result:
case mpr.intro.intro
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
l : Vector α n
i : Nat
h : i < n
⊢ ∃ i_1 h_1, (mapIdx f l)[i_1] = f i l[i]

Proof state:
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
l : Vector α n
i : Nat
h : i < n
⊢ i < n

Tactic:
simpa using h

Result:
no goals