harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean
/-- Whiskering commutes with the enriched composition. -/
@[reassoc]
lemma eComp_eHomWhiskerLeft (X Y : C) {Z Z' : C} (g : Z ⟶ Z') :
    eComp V X Y Z ≫ eHomWhiskerLeft V X g =
      _ ◁ eHomWhiskerLeft V Y g ≫ eComp V X Y Z'

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z Z' : C
g : Z ⟶ Z'
⊢ (ρ_ (EnrichedCategory.Hom X Y ⊗ EnrichedCategory.Hom Y Z)).inv ≫
      (EnrichedCategory.Hom X Y ⊗ EnrichedCategory.Hom Y Z) ◁ (eHomEquiv V) g ≫
        eComp V X Y Z ▷ EnrichedCategory.Hom Z Z' ≫ eComp V X Z Z' =
    EnrichedCategory.Hom X Y ◁
        ((ρ_ (EnrichedCategory.Hom Y Z)).inv ≫ EnrichedCategory.Hom Y Z ◁ (eHomEquiv V) g ≫ eComp V Y Z Z') ≫
      eComp V X Y Z'

Tactic:
simp [e_assoc']

Result:
no goals

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z Z' : C
g : Z ⟶ Z'
⊢ eComp V X Y Z ≫ (ρ_ (EnrichedCategory.Hom X Z)).inv ≫ EnrichedCategory.Hom X Z ◁ (eHomEquiv V) g ≫ eComp V X Z Z' =
    EnrichedCategory.Hom X Y ◁
        ((ρ_ (EnrichedCategory.Hom Y Z)).inv ≫ EnrichedCategory.Hom Y Z ◁ (eHomEquiv V) g ≫ eComp V Y Z Z') ≫
      eComp V X Y Z'

Tactic:
rw [rightUnitor_inv_naturality_assoc, ← whisker_exchange_assoc]

Result:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z Z' : C
g : Z ⟶ Z'
⊢ (ρ_ (EnrichedCategory.Hom X Y ⊗ EnrichedCategory.Hom Y Z)).inv ≫
      (EnrichedCategory.Hom X Y ⊗ EnrichedCategory.Hom Y Z) ◁ (eHomEquiv V) g ≫
        eComp V X Y Z ▷ EnrichedCategory.Hom Z Z' ≫ eComp V X Z Z' =
    EnrichedCategory.Hom X Y ◁
        ((ρ_ (EnrichedCategory.Hom Y Z)).inv ≫ EnrichedCategory.Hom Y Z ◁ (eHomEquiv V) g ≫ eComp V Y Z Z') ≫
      eComp V X Y Z'

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z Z' : C
g : Z ⟶ Z'
⊢ eComp V X Y Z ≫ eHomWhiskerLeft V X g = EnrichedCategory.Hom X Y ◁ eHomWhiskerLeft V Y g ≫ eComp V X Y Z'

Tactic:
dsimp [eHomWhiskerLeft]

Result:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z Z' : C
g : Z ⟶ Z'
⊢ eComp V X Y Z ≫ (ρ_ (EnrichedCategory.Hom X Z)).inv ≫ EnrichedCategory.Hom X Z ◁ (eHomEquiv V) g ≫ eComp V X Z Z' =
    EnrichedCategory.Hom X Y ◁
        ((ρ_ (EnrichedCategory.Hom Y Z)).inv ≫ EnrichedCategory.Hom Y Z ◁ (eHomEquiv V) g ≫ eComp V Y Z Z') ≫
      eComp V X Y Z'
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma CStarAlgebra.mul_star_le_algebraMap_norm_sq {a : A} :
    a * star a ≤ algebraMap ℝ A (‖a‖ ^ 2)

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
this : a * star a ≤ (algebraMap ℝ A) ‖a * star a‖
⊢ a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)

Tactic:
rwa [CStarRing.norm_self_mul_star, ← pow_two] at this

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)

Tactic:
have : a * star a ≤ algebraMap ℝ A ‖a * star a‖ := IsSelfAdjoint.le_algebraMap_norm_self

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
this : a * star a ≤ (algebraMap ℝ A) ‖a * star a‖
⊢ a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)
-- Mathlib/Topology/Algebra/Group/Basic.lean
lemma Filter.tendsto_sub_const_iff {G : Type*}
    [AddCommGroup G] [TopologicalSpace G] [ContinuousSub G]
    (b : G) {c : G} {f : α → G} {l : Filter α} :
    Tendsto (f · - b) l (𝓝 (c - b)) ↔ Tendsto f l (𝓝 c)

Proof state:
α : Type u
G : Type u_1
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun x => f x - b) l (𝓝 (c - b))
⊢ Tendsto f l (𝓝 c)

Tactic:
convert h.sub_const (-b) with k <;> rw [sub_sub, ← sub_eq_add_neg, sub_self, sub_zero]

Result:
no goals

Proof state:
α : Type u
G : Type u_1
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun x => f x - b) l (𝓝 (c - b)) ↔ Tendsto f l (𝓝 c)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Filter.Tendsto.sub_const h b⟩

Result:
α : Type u
G : Type u_1
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun x => f x - b) l (𝓝 (c - b))
⊢ Tendsto f l (𝓝 c)
-- Mathlib/Topology/Constructions.lean
lemma Pi.induced_precomp' {ι' : Type*} (φ : ι' → ι) :
    induced (fun (f : (∀ i, π i)) (j : ι') ↦ f (φ j)) Pi.topologicalSpace =
    ⨅ i', induced (eval (φ i')) (T (φ i'))

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
ι' : Type u_8
φ : ι' → ι
⊢ induced (fun f j => f (φ j)) topologicalSpace = ⨅ i', induced (eval (φ i')) (T (φ i'))

Tactic:
simp [Pi.topologicalSpace, induced_iInf, induced_compose, comp_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem ofNat_max (a b : Nat) : ((max a b : Nat) : Int) = max (a : Int) (b : Int)

Proof state:
a b : Nat
⊢ ↑(max a b) = max ↑a ↑b

Tactic:
simp only [Nat.max_def, Int.max_def, Int.ofNat_le]

Result:
a b : Nat
⊢ ↑(if a ≤ b then b else a) = if a ≤ b then ↑b else ↑a

Proof state:
a b : Nat
⊢ ↑(if a ≤ b then b else a) = if a ≤ b then ↑b else ↑a

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Dart.lean
theorem dart_edge_eq_mk'_iff' :
    ∀ {d : G.Dart} {u v : V},
      d.edge = s(u, v) ↔ d.fst = u ∧ d.snd = v ∨ d.fst = v ∧ d.snd = u

Proof state:
case mk.mk
V : Type u_1
G : SimpleGraph V
a b : V
h : G.Adj (a, b).1 (a, b).2
u v : V
⊢ { toProd := (a, b), adj := h }.edge = s(u, v) ↔
    { toProd := (a, b), adj := h }.toProd.1 = u ∧ { toProd := (a, b), adj := h }.toProd.2 = v ∨
      { toProd := (a, b), adj := h }.toProd.1 = v ∧ { toProd := (a, b), adj := h }.toProd.2 = u

Tactic:
rw [dart_edge_eq_mk'_iff]

Result:
case mk.mk
V : Type u_1
G : SimpleGraph V
a b : V
h : G.Adj (a, b).1 (a, b).2
u v : V
⊢ { toProd := (a, b), adj := h }.toProd = (u, v) ∨ { toProd := (a, b), adj := h }.toProd = (u, v).swap ↔
    { toProd := (a, b), adj := h }.toProd.1 = u ∧ { toProd := (a, b), adj := h }.toProd.2 = v ∨
      { toProd := (a, b), adj := h }.toProd.1 = v ∧ { toProd := (a, b), adj := h }.toProd.2 = u

Proof state:
case mk.mk
V : Type u_1
G : SimpleGraph V
a b : V
h : G.Adj (a, b).1 (a, b).2
u v : V
⊢ { toProd := (a, b), adj := h }.toProd = (u, v) ∨ { toProd := (a, b), adj := h }.toProd = (u, v).swap ↔
    { toProd := (a, b), adj := h }.toProd.1 = u ∧ { toProd := (a, b), adj := h }.toProd.2 = v ∨
      { toProd := (a, b), adj := h }.toProd.1 = v ∧ { toProd := (a, b), adj := h }.toProd.2 = u

Tactic:
simp

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
⊢ ∀ {d : G.Dart} {u v : V}, d.edge = s(u, v) ↔ d.toProd.1 = u ∧ d.toProd.2 = v ∨ d.toProd.1 = v ∧ d.toProd.2 = u

Tactic:
rintro ⟨⟨a, b⟩, h⟩ u v

Result:
case mk.mk
V : Type u_1
G : SimpleGraph V
a b : V
h : G.Adj (a, b).1 (a, b).2
u v : V
⊢ { toProd := (a, b), adj := h }.edge = s(u, v) ↔
    { toProd := (a, b), adj := h }.toProd.1 = u ∧ { toProd := (a, b), adj := h }.toProd.2 = v ∨
      { toProd := (a, b), adj := h }.toProd.1 = v ∧ { toProd := (a, b), adj := h }.toProd.2 = u
-- Mathlib/Algebra/Group/Action/Defs.lean
lemma smul_zpow (g : G) (a : H) (n : ℤ) : (g • a) ^ n = g ^ n • a ^ n

Proof state:
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
n : ℤ
⊢ (g • a) ^ n = g ^ n • a ^ n

Tactic:
cases n <;> simp [smul_pow, smul_inv]

Result:
no goals
-- Mathlib/Algebra/Module/Torsion.lean
theorem torsionOf_zero : torsionOf R M (0 : M) = ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ torsionOf R M 0 = ⊤

Tactic:
simp [torsionOf]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsOpen.closure_mul (ht : IsOpen t) (s : Set G) : closure s * t = s * t

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : IsOpen t
s : Set G
⊢ closure s * t = s * t

Tactic:
rw [← inv_inv (closure s * t), mul_inv_rev, inv_closure, ht.inv.mul_closure, mul_inv_rev, inv_inv,
  inv_inv]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Basic.lean
theorem GradedRing.proj_recompose (a : ⨁ i, 𝒜 i) (i : ι) :
    GradedRing.proj 𝒜 i ((decompose 𝒜).symm a) = (decompose 𝒜).symm (DirectSum.of _ i (a i))

Proof state:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : Semiring A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
⊢ (proj 𝒜 i) ((decompose 𝒜).symm a) = (decompose 𝒜).symm ((of (fun i => ↥(𝒜 i)) i) (a i))

Tactic:
rw [GradedRing.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
@[to_additive]
lemma Function.Surjective.smulCommClass [SMul M α] [SMul N α] [SMul M β] [SMul N β]
    [SMulCommClass M N α] {f : α → β} (hf : Surjective f) (h₁ : ∀ (c : M) x, f (c • x) = c • f x)
    (h₂ : ∀ (c : N) x, f (c • x) = c • f x) : SMulCommClass M N β where
  smul_comm c₁ c₂ := hf.forall.2 fun x ↦ by simp only [← h₁, ← h₂, smul_comm c₁ c₂ x]

Proof state:
M : Type u_1
N : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul M β
inst✝¹ : SMul N β
inst✝ : SMulCommClass M N α
f : α → β
hf : Surjective f
h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x
h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x
c₁ : M
c₂ : N
x : α
⊢ c₁ • c₂ • f x = c₂ • c₁ • f x

Tactic:
simp only [← h₁, ← h₂, smul_comm c₁ c₂ x]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean
theorem image_finset_prod_pi (l : Finset ι) (S : ι → Set α) :
    (fun f : ι → α => ∏ i ∈ l, f i) '' (l : Set ι).pi S = ∏ i ∈ l, S i

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
l : Finset ι
S : ι → Set α
⊢ (fun f => ∏ i ∈ l, f i) '' (↑l).pi S = ∏ i ∈ l, S i

Tactic:
ext

Result:
case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
l : Finset ι
S : ι → Set α
x✝ : α
⊢ x✝ ∈ (fun f => ∏ i ∈ l, f i) '' (↑l).pi S ↔ x✝ ∈ ∏ i ∈ l, S i

Proof state:
case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
l : Finset ι
S : ι → Set α
x✝ : α
⊢ x✝ ∈ (fun f => ∏ i ∈ l, f i) '' (↑l).pi S ↔ x✝ ∈ ∏ i ∈ l, S i

Tactic:
simp_rw [mem_finset_prod, mem_image, mem_pi, exists_prop, Finset.mem_coe]

Result:
no goals
-- Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean
theorem Function.Injective.noZeroSMulDivisors {R M N : Type*} [Zero R] [Zero M] [Zero N]
    [SMul R M] [SMul R N] [NoZeroSMulDivisors R N] (f : M → N) (hf : Function.Injective f)
    (h0 : f 0 = 0) (hs : ∀ (c : R) (x : M), f (c • x) = c • f x) : NoZeroSMulDivisors R M :=
  ⟨fun {_ _} h =>
    Or.imp_right (@hf _ _) <| h0.symm ▸ eq_zero_or_eq_zero_of_smul_eq_zero (by rw [← hs, h, h0])⟩

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : Zero N
inst✝² : SMul R M
inst✝¹ : SMul R N
inst✝ : NoZeroSMulDivisors R N
f : M → N
hf : Injective f
h0 : f 0 = 0
hs : ∀ (c : R) (x : M), f (c • x) = c • f x
x✝¹ : R
x✝ : M
h : x✝¹ • x✝ = 0
⊢ x✝¹ • f x✝ = 0

Tactic:
rw [← hs, h, h0]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma setIntegral_condKernel_univ_left (a : α) {t : Set Ω} (ht : MeasurableSet t)
    (hf : IntegrableOn f (Set.univ ×ˢ t) (κ a)) :
    ∫ b, ∫ ω in t, f (b, ω) ∂(Kernel.condKernel κ (a, b)) ∂(Kernel.fst κ a)
      = ∫ x in Set.univ ×ˢ t, f x ∂(κ a)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (Set.univ ×ˢ t) (κ a)
⊢ ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫ (b : β) in Set.univ, ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a

Tactic:
simp_rw [Measure.restrict_univ]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (Set.univ ×ˢ t) (κ a)
⊢ ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂κ a

Tactic:
rw [← setIntegral_condKernel a MeasurableSet.univ ht hf]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (Set.univ ×ˢ t) (κ a)
⊢ ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫ (b : β) in Set.univ, ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem iUnion_Icc_add_zsmul : ⋃ n : ℤ, Icc (a + n • p) (a + (n + 1) • p) = univ

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a : α
⊢ ⋃ n, Icc (a + n • p) (a + (n + 1) • p) = univ

Tactic:
simpa only [iUnion_Ioc_add_zsmul hp a, univ_subset_iff] using
  iUnion_mono fun n : ℤ => (Ioc_subset_Icc_self : Ioc (a + n • p) (a + (n + 1) • p) ⊆ Icc _ _)

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eval_interpolate_not_at_node (hx : ∀ i ∈ s, x ≠ v i) :
    eval x (interpolate s v r) =
      eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hx : ∀ i ∈ s, x ≠ v i
i : ι
hi : i ∈ s
⊢ r i * eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)

Tactic:
rw [← mul_assoc, mul_comm, eval_basis_not_at_node hi (hx _ hi)]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hx : ∀ i ∈ s, x ≠ v i
⊢ eval x ((interpolate s v) r) = eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i

Tactic:
simp_rw [interpolate_apply, mul_sum, eval_finset_sum, eval_mul, eval_C]

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hx : ∀ i ∈ s, x ≠ v i
⊢ ∑ x_1 ∈ s, r x_1 * eval x (Lagrange.basis s v x_1) =
    ∑ i ∈ s, eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hx : ∀ i ∈ s, x ≠ v i
⊢ ∑ x_1 ∈ s, r x_1 * eval x (Lagrange.basis s v x_1) =
    ∑ i ∈ s, eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)

Tactic:
refine sum_congr rfl fun i hi => ?_

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hx : ∀ i ∈ s, x ≠ v i
i : ι
hi : i ∈ s
⊢ r i * eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)
-- Mathlib/.lake/packages/batteries/Batteries/Control/Lawful/MonadLift.lean
theorem monadLift_map [LawfulMonad m] [LawfulMonad n] (f : α → β) (ma : m α) :
    monadLift (f <$> ma) = f <$> (monadLift ma : n α)

Proof state:
m : Type u_1 → Type u_2
n : Type u_1 → Type u_3
inst✝⁵ : Monad m
inst✝⁴ : Monad n
inst✝³ : MonadLiftT m n
inst✝² : LawfulMonadLiftT m n
α β : Type u_1
inst✝¹ : LawfulMonad m
inst✝ : LawfulMonad n
f : α → β
ma : m α
⊢ monadLift (f <$> ma) = f <$> monadLift ma

Tactic:
rw [← bind_pure_comp, ← bind_pure_comp, monadLift_bind]

Result:
m : Type u_1 → Type u_2
n : Type u_1 → Type u_3
inst✝⁵ : Monad m
inst✝⁴ : Monad n
inst✝³ : MonadLiftT m n
inst✝² : LawfulMonadLiftT m n
α β : Type u_1
inst✝¹ : LawfulMonad m
inst✝ : LawfulMonad n
f : α → β
ma : m α
⊢ (do
      let x ← monadLift ma
      monadLift (pure (f x))) =
    do
    let a ← monadLift ma
    pure (f a)

Proof state:
m : Type u_1 → Type u_2
n : Type u_1 → Type u_3
inst✝⁵ : Monad m
inst✝⁴ : Monad n
inst✝³ : MonadLiftT m n
inst✝² : LawfulMonadLiftT m n
α β : Type u_1
inst✝¹ : LawfulMonad m
inst✝ : LawfulMonad n
f : α → β
ma : m α
⊢ (do
      let x ← monadLift ma
      monadLift (pure (f x))) =
    do
    let a ← monadLift ma
    pure (f a)

Tactic:
simp only [bind_pure_comp, monadLift_pure]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_interval_sub_interval_comm (hab : IntervalIntegrable f μ a b)
    (hcd : IntervalIntegrable f μ c d) (hac : IntervalIntegrable f μ a c) :
    ((∫ x in a..b, f x ∂μ) - ∫ x in c..d, f x ∂μ) =
      (∫ x in a..c, f x ∂μ) - ∫ x in b..d, f x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hcd : IntervalIntegrable f μ c d
hac : IntervalIntegrable f μ a c
⊢ ∫ (x : ℝ) in a..b, f x ∂μ - ∫ (x : ℝ) in c..d, f x ∂μ = ∫ (x : ℝ) in a..c, f x ∂μ - ∫ (x : ℝ) in b..d, f x ∂μ

Tactic:
simp only [sub_eq_add_neg, ← integral_symm,
  integral_interval_add_interval_comm hab hcd.symm (hac.trans hcd)]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
theorem self_trans_symm (e : α ≃ β) : e.trans e.symm = Equiv.refl α := ext <| by simp

Proof state:
α : Sort u
β : Sort v
e : α ≃ β
⊢ ∀ (x : α), (e.trans e.symm) x = (Equiv.refl α) x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem nndist_conj_self (z : ℂ) : nndist (conj z) z = 2 * Real.nnabs z.im :=
  NNReal.eq <| by rw [← dist_nndist, NNReal.coe_mul, NNReal.coe_two, Real.coe_nnabs, dist_conj_self]

Proof state:
z : ℂ
⊢ ↑(nndist ((starRingEnd ℂ) z) z) = ↑(2 * Real.nnabs z.im)

Tactic:
rw [← dist_nndist, NNReal.coe_mul, NNReal.coe_two, Real.coe_nnabs, dist_conj_self]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Basic.lean
lemma comp_apply {M N O : ModuleCat.{v} R} (f : M ⟶ N) (g : N ⟶ O) (x : M) :
    (f ≫ g) x = g (f x)

Proof state:
R : Type u
inst✝ : Ring R
M N O : ModuleCat R
f : M ⟶ N
g : N ⟶ O
x : ↑M
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/Field.lean
theorem affineHomeomorph_image_Ico {𝕜 : Type*} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜]
    [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
    affineHomeomorph a b h.ne' '' Set.Ico c d = Set.Ico (a * c + b) (a * d + b)

Proof state:
𝕜 : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b c d : 𝕜
h : 0 < a
⊢ ⇑(affineHomeomorph a b ⋯) '' Set.Ico c d = Set.Ico (a * c + b) (a * d + b)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem hsymm_zero : hsymm σ R 0 = 1

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ hsymm σ R 0 = 1

Tactic:
simp [hsymm, eq_nil_of_card_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem not_forall (p : α → Prop) : (¬∀ x, p x) = ∃ x, ¬p x

Proof state:
α : Sort u_1
p : α → Prop
⊢ (¬∀ (x : α), p x) = ∃ x, ¬p x

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem coe_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → NonUnitalSubsemiring R}
    (hS : Directed (· ≤ ·) S) : ((⨆ i, S i : NonUnitalSubsemiring R) : Set R) = ⋃ i, S i :=
  Set.ext fun x ↦ by simp [mem_iSup_of_directed hS]

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
simp [mem_iSup_of_directed hS]

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/QuadraticMap.lean
theorem lineDeriv (f : QuadraticMap 𝕜 E F) : lineDeriv 𝕜 f = polar f

Proof state:
case h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : QuadraticMap 𝕜 E F
a b : E
⊢ lineDeriv 𝕜 (⇑f) a b = polar (⇑f) a b

Tactic:
exact (f.hasLineDerivAt a b).lineDeriv

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : QuadraticMap 𝕜 E F
⊢ lineDeriv 𝕜 ⇑f = polar ⇑f

Tactic:
ext a b

Result:
case h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : QuadraticMap 𝕜 E F
a b : E
⊢ lineDeriv 𝕜 (⇑f) a b = polar (⇑f) a b
-- Mathlib/SetTheory/Cardinal/Finsupp.lean
theorem mk_finsupp_lift_of_fintype (α : Type u) (β : Type v) [Fintype α] [Zero β] :
    #(α →₀ β) = lift.{u} #β ^ Fintype.card α

Proof state:
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Zero β
⊢ #(α →₀ β) = lift.{u, v} #β ^ Fintype.card α

Tactic:
simpa using (@Finsupp.equivFunOnFinite α β _ _).cardinal_eq

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem neighborSet_sSup (s : Set G.Subgraph) (v : V) :
    (sSup s).neighborSet v = ⋃ G' ∈ s, neighborSet G' v

Proof state:
case h
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v x✝ : V
⊢ x✝ ∈ (sSup s).neighborSet v ↔ x✝ ∈ ⋃ G' ∈ s, G'.neighborSet v

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v : V
⊢ (sSup s).neighborSet v = ⋃ G' ∈ s, G'.neighborSet v

Tactic:
ext

Result:
case h
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v x✝ : V
⊢ x✝ ∈ (sSup s).neighborSet v ↔ x✝ ∈ ⋃ G' ∈ s, G'.neighborSet v
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma homMk₅_app_four :
    (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨4, by valid⟩ = app₄ := rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.369477, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯
app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯
app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯
app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯
app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯
app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯
w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯
w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯
w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯
w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄ = app₃ ≫ g.map' 3 4 ⋯ ⋯
w₄ : f.map' 4 5 ⋯ ⋯ ≫ app₅ = app₄ ≫ g.map' 4 5 ⋯ ⋯
⊢ 4 < 5 + 1

Tactic:
valid

Result:
no goals
-- Mathlib/Order/Category/Preord.lean
lemma inv_hom_apply {X Y : Preord} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x

Proof state:
X Y : Preord
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Result:
no goals