harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Final.lean
theorem reflectsLimit_of_comp {B : Type u₄} [Category.{v₄} B] {H : E ⥤ B}
    [ReflectsLimit (F ⋙ G) H] : ReflectsLimit G H where
  reflects {c} hc

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
⊢ Nonempty (IsLimit c)

Tactic:
refine ⟨isLimitWhiskerEquiv F _ (isLimitOfReflects H ?_)⟩

Result:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
⊢ IsLimit (H.mapCone (Cone.whisker F c))

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
hc' : IsLimit (Cone.whisker F (H.mapCone c)) := (isLimitWhiskerEquiv F (H.mapCone c)).symm hc
⊢ ∀ (j : C),
    (Cone.whisker F (H.mapCone c)).π.app j =
      (Iso.refl (Cone.whisker F (H.mapCone c)).pt).hom ≫ (H.mapCone (Cone.whisker F c)).π.app j

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
hc' : IsLimit (Cone.whisker F (H.mapCone c)) := (isLimitWhiskerEquiv F (H.mapCone c)).symm hc
⊢ IsLimit (H.mapCone (Cone.whisker F c))

Tactic:
exact IsLimit.ofIsoLimit hc' (Cones.ext (Iso.refl _) (by simp))

Result:
no goals

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
⊢ IsLimit (H.mapCone (Cone.whisker F c))

Tactic:
let hc' := (isLimitWhiskerEquiv F _).symm hc

Result:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
hc' : IsLimit (Cone.whisker F (H.mapCone c)) := (isLimitWhiskerEquiv F (H.mapCone c)).symm hc
⊢ IsLimit (H.mapCone (Cone.whisker F c))
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem iterate_add_minimalPeriod_eq : f^[n + minimalPeriod f x] x = f^[n] x

Proof state:
case e_a
α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[minimalPeriod f x] x = x

Tactic:
exact isPeriodicPt_minimalPeriod f x

Result:
no goals

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

Tactic:
congr

Result:
case e_a
α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[minimalPeriod f x] x = x

Proof state:
α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[n + minimalPeriod f x] x = f^[n] x

Tactic:
rw [iterate_add_apply]

Result:
α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[n] (f^[minimalPeriod f x] x) = f^[n] x
-- Mathlib/Topology/Separation/Basic.lean
theorem Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete {ι : Type*} {p : ι → Prop}
    {t : ι → Set X} {s : Set X} [DiscreteTopology s] {x : X} (hb : (𝓝 x).HasBasis p t)
    (hx : x ∈ s) : ∃ i, p i ∧ t i ∩ s = {x}

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_3
p : ι → Prop
t : ι → Set X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hb : (𝓝 x).HasBasis p t
hx : x ∈ s
⊢ ∃ i, p i ∧ t i ∩ s = {x}

Tactic:
rcases (nhdsWithin_hasBasis hb s).mem_iff.1 (singleton_mem_nhdsWithin_of_mem_discrete hx) with
  ⟨i, hi, hix⟩

Result:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_3
p : ι → Prop
t : ι → Set X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hb : (𝓝 x).HasBasis p t
hx : x ∈ s
i : ι
hi : p i
hix : t i ∩ s ⊆ {x}
⊢ ∃ i, p i ∧ t i ∩ s = {x}

Proof state:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_3
p : ι → Prop
t : ι → Set X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hb : (𝓝 x).HasBasis p t
hx : x ∈ s
i : ι
hi : p i
hix : t i ∩ s ⊆ {x}
⊢ ∃ i, p i ∧ t i ∩ s = {x}

Tactic:
exact ⟨i, hi, hix.antisymm <| singleton_subset_iff.2 ⟨mem_of_mem_nhds <| hb.mem_of_mem hi, hx⟩⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
lemma eval_C_X_comp_eval₂_map_C_X :
    (evalRingHom (C X : R[X][Y])).comp (eval₂RingHom (mapRingHom <| algebraMap R R[X][Y]) (C Y)) =
      .id _

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ (evalRingHom (C X)).comp (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) (C Y)) = RingHom.id R[X][Y]

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Order/Ideal.lean
/-- A non-empty directed union of ideals of sets in a preorder is an ideal. -/
lemma isIdeal_sUnion_of_directedOn {C : Set (Set P)} (hidl : ∀ I ∈ C, IsIdeal I)
    (hD : DirectedOn (· ⊆ ·) C) (hNe : C.Nonempty) : IsIdeal C.sUnion

Proof state:
P : Type u_1
inst✝ : Preorder P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hD : DirectedOn (fun x1 x2 => x1 ⊆ x2) C
hNe : C.Nonempty
⊢ IsIdeal (⋃₀ C)

Tactic:
refine ⟨isLowerSet_sUnion (fun I hI ↦ (hidl I hI).1), Set.nonempty_sUnion.2 ?_,
  directedOn_sUnion hD (fun J hJ => (hidl J hJ).3)⟩

Result:
P : Type u_1
inst✝ : Preorder P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hD : DirectedOn (fun x1 x2 => x1 ⊆ x2) C
hNe : C.Nonempty
⊢ ∃ s ∈ C, s.Nonempty

Proof state:
P : Type u_1
inst✝ : Preorder P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hD : DirectedOn (fun x1 x2 => x1 ⊆ x2) C
hNe : C.Nonempty
I : Set P
hI : I ∈ C
⊢ ∃ s ∈ C, s.Nonempty

Tactic:
exact ⟨I, ⟨hI, (hidl I hI).2⟩⟩

Result:
no goals

Proof state:
P : Type u_1
inst✝ : Preorder P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hD : DirectedOn (fun x1 x2 => x1 ⊆ x2) C
hNe : C.Nonempty
⊢ ∃ s ∈ C, s.Nonempty

Tactic:
let ⟨I, hI⟩ := hNe

Result:
P : Type u_1
inst✝ : Preorder P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hD : DirectedOn (fun x1 x2 => x1 ⊆ x2) C
hNe : C.Nonempty
I : Set P
hI : I ∈ C
⊢ ∃ s ∈ C, s.Nonempty
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
@[simp]
lemma valuation_intCast (n : ℤ) : valuation (n : ℚ_[p]) = padicValInt p n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
⊢ (↑n).valuation = ↑(padicValInt p n)

Tactic:
rw [← Rat.cast_intCast, valuation_ratCast, padicValRat.of_int]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem prodPrimeFactors_add_of_squarefree [CommSemiring R] {f g : ArithmeticFunction R}
    (hf : IsMultiplicative f) (hg : IsMultiplicative g) {n : ℕ} (hn : Squarefree n) :
    ∏ᵖ p ∣ n, (f + g) p = (f * g) n

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ∈ n.primeFactors.powerset
⊢ (∏ i ∈ t, f i) * ∏ i ∈ n.primeFactors \ t, g i = f t.val.prod * g (n / t.val.prod)

Tactic:
rw [t.prod_val, Function.id_def,
  ← prod_primeFactors_sdiff_of_squarefree hn (Finset.mem_powerset.mp ht),
  hf.map_prod_of_subset_primeFactors n t (Finset.mem_powerset.mp ht),
  ← hg.map_prod_of_subset_primeFactors n (_ \ t) Finset.sdiff_subset]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ (ArithmeticFunction.prodPrimeFactors fun p => (f + g) p) n = (f * g) n

Tactic:
rw [prodPrimeFactors_apply hn.ne_zero]

Result:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (f + g) p = (f * g) n

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (f + g) p = (f * g) n

Tactic:
simp_rw [add_apply (f := f) (g := g)]

Result:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ x ∈ n.primeFactors, (f x + g x) = (f * g) n

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∑ t ∈ n.primeFactors.powerset, (∏ i ∈ t, f i) * ∏ i ∈ n.primeFactors \ t, g i =
    ∑ i ∈ (↑n.primeFactorsList).toFinset.powerset, f i.val.prod * g (n / i.val.prod)

Tactic:
apply Finset.sum_congr rfl

Result:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∀ x ∈ n.primeFactors.powerset, (∏ i ∈ x, f i) * ∏ i ∈ n.primeFactors \ x, g i = f x.val.prod * g (n / x.val.prod)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∀ x ∈ n.primeFactors.powerset, (∏ i ∈ x, f i) * ∏ i ∈ n.primeFactors \ x, g i = f x.val.prod * g (n / x.val.prod)

Tactic:
intro t ht

Result:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ∈ n.primeFactors.powerset
⊢ (∏ i ∈ t, f i) * ∏ i ∈ n.primeFactors \ t, g i = f t.val.prod * g (n / t.val.prod)
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem toFractionRing_smul [SMul R (FractionRing K[X])] (c : R) (p : RatFunc K) :
    toFractionRing (c • p) = c • toFractionRing p

Proof state:
K : Type u
inst✝¹ : CommRing K
R : Type u_1
inst✝ : SMul R (FractionRing K[X])
c : R
p : RatFunc K
⊢ (c • p).toFractionRing = c • p.toFractionRing

Tactic:
cases p

Result:
case ofFractionRing
K : Type u
inst✝¹ : CommRing K
R : Type u_1
inst✝ : SMul R (FractionRing K[X])
c : R
toFractionRing✝ : FractionRing K[X]
⊢ (c • { toFractionRing := toFractionRing✝ }).toFractionRing = c • { toFractionRing := toFractionRing✝ }.toFractionRing

Proof state:
case ofFractionRing
K : Type u
inst✝¹ : CommRing K
R : Type u_1
inst✝ : SMul R (FractionRing K[X])
c : R
toFractionRing✝ : FractionRing K[X]
⊢ (c • { toFractionRing := toFractionRing✝ }).toFractionRing = c • { toFractionRing := toFractionRing✝ }.toFractionRing

Tactic:
rw [← ofFractionRing_smul]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem isBasis_iff_maximal (hX : X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.IsBasis I X ↔ Maximal (fun I => M.Indep I ∧ I ⊆ X) I

Tactic:
rw [IsBasis, and_iff_left hX]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem bind_const (f : α →ₛ β) : f.bind (const α) = f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ f.bind (const α) = f

Tactic:
ext

Result:
case H
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
a✝ : α
⊢ (f.bind (const α)) a✝ = f a✝

Proof state:
case H
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
a✝ : α
⊢ (f.bind (const α)) a✝ = f a✝

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/SpreadingOut.lean
lemma Scheme.IsGermInjective.of_openCover
    {X : Scheme.{u}} (𝒰 : X.OpenCover) [∀ i, (𝒰.obj i).IsGermInjective] : X.IsGermInjective

Proof state:
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), (𝒰.obj i).IsGermInjective
x : ↑↑X.toPresheafedSpace
⊢ X.IsGermInjectiveAt ((ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) (Exists.choose ⋯))

Tactic:
infer_instance

Result:
no goals

Proof state:
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), (𝒰.obj i).IsGermInjective
⊢ X.IsGermInjective

Tactic:
intro x

Result:
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), (𝒰.obj i).IsGermInjective
x : ↑↑X.toPresheafedSpace
⊢ X.IsGermInjectiveAt x

Proof state:
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), (𝒰.obj i).IsGermInjective
x : ↑↑X.toPresheafedSpace
⊢ X.IsGermInjectiveAt x

Tactic:
rw [← (𝒰.covers x).choose_spec]

Result:
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), (𝒰.obj i).IsGermInjective
x : ↑↑X.toPresheafedSpace
⊢ X.IsGermInjectiveAt ((ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) (Exists.choose ⋯))
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[simp] lemma enorm_abs (r : ℝ) : ‖|r|‖ₑ = ‖r‖ₑ

Proof state:
r : ℝ
⊢ ‖|r|‖ₑ = ‖r‖ₑ

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem cons_injective_iff {α} {x₀ : α} {x : Fin n → α} :
    Function.Injective (cons x₀ x : Fin n.succ → α) ↔ x₀ ∉ Set.range x ∧ Function.Injective x

Proof state:
case refine_1.intro
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
i : Fin n
hi : x i = x₀
⊢ False

Tactic:
replace h := @h i.succ 0

Result:
case refine_1.intro
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
i : Fin n
hi : x i = x₀
h : cons x₀ x i.succ = cons x₀ x 0 → i.succ = 0
⊢ False

Proof state:
case refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
⊢ Injective x

Tactic:
simpa [Function.comp] using h.comp (Fin.succ_injective _)

Result:
no goals

Proof state:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
⊢ Injective (cons x₀ x) ↔ x₀ ∉ Set.range x ∧ Injective x

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ cons_injective_of_injective h.1 h.2⟩

Result:
case refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
⊢ x₀ ∉ Set.range x

case refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
⊢ Injective x

Proof state:
case refine_1.intro
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
i : Fin n
hi : x i = x₀
h : cons x₀ x i.succ = cons x₀ x 0 → i.succ = 0
⊢ False

Tactic:
simp [hi, succ_ne_zero] at h

Result:
no goals

Proof state:
case refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
⊢ x₀ ∉ Set.range x

Tactic:
rintro ⟨i, hi⟩

Result:
case refine_1.intro
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
i : Fin n
hi : x i = x₀
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem mod_eq_zero_of_dvd {m n : Nat} (H : m ∣ n) : n % m = 0

Proof state:
m n : Nat
H✝ : m ∣ n
z : Nat
H : n = m * z
⊢ n % m = 0

Tactic:
rw [H, mul_mod_right]

Result:
no goals

Proof state:
m n : Nat
H : m ∣ n
⊢ n % m = 0

Tactic:
let ⟨z, H⟩ := H

Result:
m n : Nat
H✝ : m ∣ n
z : Nat
H : n = m * z
⊢ n % m = 0
-- Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
theorem mapL_add [DecidableEq ι] (i : ι) (u v : E i →L[𝕜] E' i) :
    mapL (update f i (u + v)) = mapL (update f i u) + mapL (update f i v)

Proof state:
ι : Type uι
inst✝⁶ : Fintype ι
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
u v : E i →L[𝕜] E' i
⊢ mapL (update f i (u + v)) = mapL (update f i u) + mapL (update f i v)

Tactic:
ext x

Result:
case h
ι : Type uι
inst✝⁶ : Fintype ι
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
u v : E i →L[𝕜] E' i
x : ⨂[𝕜] (i : ι), E i
⊢ (mapL (update f i (u + v))) x = (mapL (update f i u) + mapL (update f i v)) x

Proof state:
case h
ι : Type uι
inst✝⁶ : Fintype ι
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
u v : E i →L[𝕜] E' i
x : ⨂[𝕜] (i : ι), E i
⊢ (mapL (update f i (u + v))) x = (mapL (update f i u) + mapL (update f i v)) x

Tactic:
simp only [mapL_apply, mapL_add_smul_aux, ContinuousLinearMap.coe_add,
  PiTensorProduct.map_update_add, LinearMap.add_apply, ContinuousLinearMap.add_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem of_mem_zip {a b} {l₁ : Array α} {l₂ : Array β} : (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂

Proof state:
case mk
α : Type u_1
β : Type u_2
a : α
b : β
l₂ : Array β
toList✝ : List α
⊢ (a, b) ∈ { toList := toList✝ }.zip l₂ → a ∈ { toList := toList✝ } ∧ b ∈ l₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
a : α
b : β
toList✝¹ : List α
toList✝ : List β
⊢ (a, b) ∈ { toList := toList✝¹ }.zip { toList := toList✝ } → a ∈ { toList := toList✝¹ } ∧ b ∈ { toList := toList✝ }

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
l₁ : Array α
l₂ : Array β
⊢ (a, b) ∈ l₁.zip l₂ → a ∈ l₁ ∧ b ∈ l₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
a : α
b : β
l₂ : Array β
toList✝ : List α
⊢ (a, b) ∈ { toList := toList✝ }.zip l₂ → a ∈ { toList := toList✝ } ∧ b ∈ l₂

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
a : α
b : β
toList✝¹ : List α
toList✝ : List β
⊢ (a, b) ∈ { toList := toList✝¹ }.zip { toList := toList✝ } → a ∈ { toList := toList✝¹ } ∧ b ∈ { toList := toList✝ }

Tactic:
simpa using List.of_mem_zip

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem order_zero_of_unit {f : PowerSeries R} : IsUnit f → f.order = 0

Proof state:
case intro.mk.self
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ f.order = 0 ∧ ?intro.mk.b

case intro.mk.b
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ Prop

Tactic:
rw [← add_eq_zero, ← hf, ← nonpos_iff_eq_zero, ← @order_one R _ _, ← hu]

Result:
case intro.mk.self
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ (↑{ val := u, inv := v, val_inv := hu, inv_val := hv }).order + ?m.102492 ≤ (u * v).order

R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ ℕ∞

R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ ℕ∞

Proof state:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R⟦X⟧
⊢ IsUnit f → f.order = 0

Tactic:
rintro ⟨⟨u, v, hu, hv⟩, hf⟩

Result:
case intro.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ f.order = 0

Proof state:
case intro.mk.self
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ (↑{ val := u, inv := v, val_inv := hu, inv_val := hv }).order + ?m.102492 ≤ (u * v).order

R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ ℕ∞

R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ ℕ∞

Tactic:
exact order_mul_ge _ _

Result:
no goals

Proof state:
case intro.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ f.order = 0

Tactic:
apply And.left

Result:
case intro.mk.self
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ f.order = 0 ∧ ?intro.mk.b

case intro.mk.b
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ Prop
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integrable_of_summable_norm_restrict {f : C(X, E)} {s : ι → Compacts X}
    (hf : Summable fun i : ι => ‖f.restrict (s i)‖ * ENNReal.toReal (μ <| s i))
    (hs : ⋃ i : ι, ↑(s i) = (univ : Set X)) : Integrable f μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝⁵ : Countable ι
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace X
inst✝² : BorelSpace X
inst✝¹ : MetrizableSpace X
inst✝ : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal
hs : ⋃ i, ↑(s i) = univ
⊢ Integrable (⇑f) μ

Tactic:
simpa only [hs, integrableOn_univ] using integrableOn_iUnion_of_summable_norm_restrict hf

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SeparationQuotient.lean
theorem norm_liftNormedAddGroupHom_apply_le (f : NormedAddGroupHom M N)
    (hf : ∀ x, ‖x‖ = 0 → f x = 0) (x : SeparationQuotient M) :
    ‖liftNormedAddGroupHom f hf x‖ ≤ ‖f‖ * ‖x‖

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (x : M), ‖x‖ = 0 → f x = 0
x : SeparationQuotient M
⊢ ‖(liftNormedAddGroupHom f hf) x‖ ≤ ‖f‖ * ‖x‖

Tactic:
obtain ⟨x, rfl⟩ := surjective_mk x

Result:
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (x : M), ‖x‖ = 0 → f x = 0
x : M
⊢ ‖(liftNormedAddGroupHom f hf) (mk x)‖ ≤ ‖f‖ * ‖mk x‖

Proof state:
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (x : M), ‖x‖ = 0 → f x = 0
x : M
⊢ ‖(liftNormedAddGroupHom f hf) (mk x)‖ ≤ ‖f‖ * ‖mk x‖

Tactic:
exact le_opNorm f x

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem map_sup (f : G →g G') (H₁ H₂ : G.Subgraph) : (H₁ ⊔ H₂).map f = H₁.map f ⊔ H₂.map f

Proof state:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
⊢ Subgraph.map f (H₁ ⊔ H₂) = Subgraph.map f H₁ ⊔ Subgraph.map f H₂

Tactic:
ext <;> simp [Set.image_union, map_adj, sup_adj, Relation.Map, or_and_right, exists_or]

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Cartesian.lean
theorem pre_map {A₁ A₂ A₃ : C} [Exponentiable A₁] [Exponentiable A₂] [Exponentiable A₃]
    (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) : pre (f ≫ g) = pre g ≫ pre f

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
A₁ A₂ A₃ : C
inst✝² : Exponentiable A₁
inst✝¹ : Exponentiable A₂
inst✝ : Exponentiable A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ (conjugateEquiv (exp.adjunction A₃) (exp.adjunction A₁)) ((tensoringLeft C).map (f ≫ g)) =
    (conjugateEquiv (exp.adjunction A₃) (exp.adjunction A₁)) ((tensoringLeft C).map f ≫ (tensoringLeft C).map g)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
A₁ A₂ A₃ : C
inst✝² : Exponentiable A₁
inst✝¹ : Exponentiable A₂
inst✝ : Exponentiable A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ pre (f ≫ g) = pre g ≫ pre f

Tactic:
rw [pre, pre, pre, conjugateEquiv_comp]

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
A₁ A₂ A₃ : C
inst✝² : Exponentiable A₁
inst✝¹ : Exponentiable A₂
inst✝ : Exponentiable A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ (conjugateEquiv (exp.adjunction A₃) (exp.adjunction A₁)) ((tensoringLeft C).map (f ≫ g)) =
    (conjugateEquiv (exp.adjunction A₃) (exp.adjunction A₁)) ((tensoringLeft C).map f ≫ (tensoringLeft C).map g)