harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_biUnion₀ {t : Set β} {s : β → Set α} (ht : t.Countable)
    (hm : ∀ i ∈ t, NullMeasurableSet (s i) μ) (hd : t.Pairwise (AEDisjoint μ on s)) (f : α → ℝ≥0∞) :
    ∫⁻ a in ⋃ i ∈ t, s i, f a ∂μ = ∑' i : t, ∫⁻ a in s i, f a ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
t : Set β
s : β → Set α
ht : t.Countable
hm : ∀ i ∈ t, NullMeasurableSet (s i) μ
hd : t.Pairwise (AEDisjoint μ on s)
f : α → ℝ≥0∞
this : Encodable ↑t
⊢ ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ

Tactic:
rw [biUnion_eq_iUnion, lintegral_iUnion₀ (SetCoe.forall'.1 hm) (hd.subtype _ _)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
t : Set β
s : β → Set α
ht : t.Countable
hm : ∀ i ∈ t, NullMeasurableSet (s i) μ
hd : t.Pairwise (AEDisjoint μ on s)
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ

Tactic:
haveI := ht.toEncodable

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
t : Set β
s : β → Set α
ht : t.Countable
hm : ∀ i ∈ t, NullMeasurableSet (s i) μ
hd : t.Pairwise (AEDisjoint μ on s)
f : α → ℝ≥0∞
this : Encodable ↑t
⊢ ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal_transpose (M : o → Matrix m n α) :
    (blockDiagonal M)ᵀ = blockDiagonal fun k => (M k)ᵀ

Proof state:
case neg
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
h : ¬i✝.2 = j✝.2
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case pos
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
h : i✝.2 = j✝.2
⊢ M i✝.2 j✝.1 i✝.1 = M j✝.2 j✝.1 i✝.1

Tactic:
rw [h]

Result:
no goals

Proof state:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
⊢ (if i✝.2 = j✝.2 then M i✝.2 j✝.1 i✝.1 else 0) = if i✝.2 = j✝.2 then M j✝.2 j✝.1 i✝.1 else 0

Tactic:
split_ifs with h

Result:
case pos
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
h : i✝.2 = j✝.2
⊢ M i✝.2 j✝.1 i✝.1 = M j✝.2 j✝.1 i✝.1

case neg
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
h : ¬i✝.2 = j✝.2
⊢ 0 = 0

Proof state:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
⊢ (blockDiagonal M)ᵀ i✝ j✝ = blockDiagonal (fun k => (M k)ᵀ) i✝ j✝

Tactic:
simp only [transpose_apply, blockDiagonal_apply, eq_comm]

Result:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
⊢ (if i✝.2 = j✝.2 then M i✝.2 j✝.1 i✝.1 else 0) = if i✝.2 = j✝.2 then M j✝.2 j✝.1 i✝.1 else 0

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
⊢ (blockDiagonal M)ᵀ = blockDiagonal fun k => (M k)ᵀ

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
⊢ (blockDiagonal M)ᵀ i✝ j✝ = blockDiagonal (fun k => (M k)ᵀ) i✝ j✝
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma δ_zero_cocycle_comp {n : ℤ} (z₁ : Cocycle F G 0) (z₂ : Cochain G K n) (m : ℤ) :
    δ n m (z₁.1.comp z₂ (zero_add n)) =
      z₁.1.comp (δ n m z₂) (zero_add m)

Proof state:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cocycle F G 0
z₂ : Cochain G K n
m : ℤ
hnm : n + 1 = m
⊢ δ n m ((↑z₁).comp z₂ ⋯) = (↑z₁).comp (δ n m z₂) ⋯

Tactic:
simp [δ_zero_cochain_comp _ _ _ hnm]

Result:
no goals

Proof state:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cocycle F G 0
z₂ : Cochain G K n
m : ℤ
hnm : ¬n + 1 = m
⊢ δ n m ((↑z₁).comp z₂ ⋯) = (↑z₁).comp (δ n m z₂) ⋯

Tactic:
simp [δ_shape _ _ hnm]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cocycle F G 0
z₂ : Cochain G K n
m : ℤ
⊢ δ n m ((↑z₁).comp z₂ ⋯) = (↑z₁).comp (δ n m z₂) ⋯

Tactic:
by_cases hnm : n + 1 = m

Result:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cocycle F G 0
z₂ : Cochain G K n
m : ℤ
hnm : n + 1 = m
⊢ δ n m ((↑z₁).comp z₂ ⋯) = (↑z₁).comp (δ n m z₂) ⋯

case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cocycle F G 0
z₂ : Cochain G K n
m : ℤ
hnm : ¬n + 1 = m
⊢ δ n m ((↑z₁).comp z₂ ⋯) = (↑z₁).comp (δ n m z₂) ⋯
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
theorem toSubgraph_reverse (p : G.Walk u v) : p.reverse.toSubgraph = p.toSubgraph

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.toSubgraph = p✝.toSubgraph
⊢ G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝ ⊔ p✝.toSubgraph = G.subgraphOfAdj h✝ ⊔ p✝.toSubgraph

Tactic:
congr

Result:
case cons.e_a
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.toSubgraph = p✝.toSubgraph
⊢ G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝ = G.subgraphOfAdj h✝

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.toSubgraph = p✝.toSubgraph
⊢ p✝.toSubgraph ⊔ (G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝) = G.subgraphOfAdj h✝ ⊔ p✝.toSubgraph

Tactic:
rw [sup_comm]

Result:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.toSubgraph = p✝.toSubgraph
⊢ G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝ ⊔ p✝.toSubgraph = G.subgraphOfAdj h✝ ⊔ p✝.toSubgraph

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.toSubgraph = p✝.toSubgraph
⊢ (cons h✝ p✝).reverse.toSubgraph = (cons h✝ p✝).toSubgraph

Tactic:
simp only [*, Walk.toSubgraph, reverse_cons, toSubgraph_append, subgraphOfAdj_symm]

Result:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.toSubgraph = p✝.toSubgraph
⊢ p✝.toSubgraph ⊔ (G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝) = G.subgraphOfAdj h✝ ⊔ p✝.toSubgraph

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.reverse.toSubgraph = nil.toSubgraph

Tactic:
simp

Result:
no goals

Proof state:
case cons.e_a
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.toSubgraph = p✝.toSubgraph
⊢ G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝ = G.subgraphOfAdj h✝

Tactic:
ext <;> simp [-Set.bot_eq_empty]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.toSubgraph = p.toSubgraph

Tactic:
induction p with
| nil => simp
| cons _ _ _ =>
  simp only [*, Walk.toSubgraph, reverse_cons, toSubgraph_append, subgraphOfAdj_symm]
  rw [sup_comm]
  congr
  ext <;> simp [-Set.bot_eq_empty]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
/-- If each component of the counit is a split monomorphism, then the right adjoint is full. -/
lemma full_R_of_isSplitMono_counit_app [∀ X, IsSplitMono (h.counit.app X)] : R.Full where
  map_surjective {X Y} f

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
this : R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)
⊢ R.map (retraction (h.counit.app X) ≫ (h.homEquiv (R.obj X) Y).symm f) = f

Tactic:
simp [this]

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
⊢ R.map (retraction (h.counit.app X) ≫ (h.homEquiv (R.obj X) Y).symm f) = f

Tactic:
suffices R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X) by simp [this]

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
⊢ R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
⊢ R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)

Tactic:
rw [← id_comp (R.map (retraction (h.counit.app X)))]

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
⊢ 𝟙 (R.obj ((𝟭 D).obj X)) ≫ R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
⊢ 𝟙 (R.obj ((𝟭 D).obj X)) ≫ R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, id_comp, ← h.right_triangle_components X,
  assoc, ← Functor.map_comp, IsSplitMono.id, Functor.map_id, comp_id]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
⊢ ∃ a, R.map a = f

Tactic:
use (retraction (h.counit.app X) ≫ (h.homEquiv (R.obj X) Y).symm f)

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
⊢ R.map (retraction (h.counit.app X) ≫ (h.homEquiv (R.obj X) Y).symm f) = f
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean
lemma ncard_sdiff_of_not_mem (hrep : Represents s C) (h : c ∉ C) :
    (c.supp \ s).ncard = c.supp.ncard

Proof state:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
⊢ (c.supp \ s).ncard = c.supp.ncard

Tactic:
rw [(disjoint_supp_of_not_mem hrep h).sdiff_eq_right]

Result:
no goals
-- Mathlib/Data/List/Indexes.lean
theorem foldlIdxM_eq_foldlM_enum [LawfulMonad m] {β} (f : ℕ → β → α → m β) (b : β) (as : List α) :
    foldlIdxM f b as = List.foldlM (fun b p ↦ f p.fst b p.snd) b (enum as)

Proof state:
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → β → α → m β
b : β
as : List α
⊢ foldlIdxM f b as = List.foldlM (fun b p => f p.fst b p.snd) b as.enum

Tactic:
rw [foldlIdxM, foldlM_eq_foldl, foldlIdx_eq_foldl_enum]

Result:
no goals
-- Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
theorem sumIDeriv_eq_self_add (p : R[X]) : sumIDeriv p = p + derivative (sumIDeriv p)

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (⇑derivative)^[0] p + (∑ k ∈ range p.natDegree, (⇑derivative)^[k + 1] p + 0) =
    p + (∑ x ∈ range p.natDegree, derivative ((⇑derivative)^[x] p) + derivative ((⇑derivative)^[p.natDegree] p))

Tactic:
simp_rw [← Function.iterate_succ_apply' derivative, Nat.succ_eq_add_one,
  Function.iterate_zero_apply, iterate_derivative_eq_zero (Nat.lt_succ_self _)]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ sumIDeriv p = p + derivative (sumIDeriv p)

Tactic:
rw [sumIDeriv_apply, derivative_sum, sum_range_succ', sum_range_succ,
  add_comm, ← add_zero (Finset.sum _ _)]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (⇑derivative)^[0] p + (∑ k ∈ range p.natDegree, (⇑derivative)^[k + 1] p + 0) =
    p + (∑ x ∈ range p.natDegree, derivative ((⇑derivative)^[x] p) + derivative ((⇑derivative)^[p.natDegree] p))
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
lemma ker_quotientMap_mk {I J : Ideal R} [I.IsTwoSided] [J.IsTwoSided] :
    RingHom.ker (quotientMap (J.map _) (Quotient.mk I) le_comap_map) = I.map (Quotient.mk J)

Proof state:
R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
⊢ ker (quotientMap (map (Quotient.mk I) J) (Quotient.mk I) ⋯) = map (Quotient.mk J) I

Tactic:
rw [Ideal.quotientMap, Ideal.ker_quotient_lift, ← RingHom.comap_ker, Ideal.mk_ker,
  Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,
  ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, Ideal.map_sup, Ideal.map_quotient_self, bot_sup_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
lemma Real.hasProd_of_hasSum_log {f : ι → ℝ} (hfn : ∀ n, 0 < f n) {a : ℝ}
    (hf : HasSum (fun n => log (f n)) a) : HasProd f (rexp a) :=
  hf.rexp.congr (by simp [exp_log, hfn])

Proof state:
ι : Type u_2
f : ι → ℝ
hfn : ∀ (n : ι), 0 < f n
a : ℝ
hf : HasSum (fun n => log (f n)) a
⊢ ∀ (x : Finset ι), ∏ b ∈ x, (rexp ∘ fun n => log (f n)) b = ∏ b ∈ x, f b

Tactic:
simp [exp_log, hfn]

Result:
no goals
-- Mathlib/Topology/DenseEmbedding.lean
theorem comap_nhds_neBot (di : IsDenseInducing i) (b : β) : NeBot (comap i (𝓝 b)) :=
  comap_neBot fun s hs => by
    rcases mem_closure_iff_nhds.1 (di.dense b) s hs with ⟨_, ⟨ha, a, rfl⟩⟩
    exact ⟨a, ha⟩

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di : IsDenseInducing i
b : β
s : Set β
hs : s ∈ 𝓝 b
a : α
ha : i a ∈ s
⊢ ∃ a, i a ∈ s

Tactic:
exact ⟨a, ha⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di : IsDenseInducing i
b : β
s : Set β
hs : s ∈ 𝓝 b
⊢ ∃ a, i a ∈ s

Tactic:
rcases mem_closure_iff_nhds.1 (di.dense b) s hs with ⟨_, ⟨ha, a, rfl⟩⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di : IsDenseInducing i
b : β
s : Set β
hs : s ∈ 𝓝 b
a : α
ha : i a ∈ s
⊢ ∃ a, i a ∈ s
-- Mathlib/Algebra/Star/Conjneg.lean
@[simp] lemma conjneg_add (f g : G → R) : conjneg (f + g) = conjneg f + conjneg g

Proof state:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f g : G → R
⊢ conjneg (f + g) = conjneg f + conjneg g

Tactic:
ext

Result:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f g : G → R
x✝ : G
⊢ conjneg (f + g) x✝ = (conjneg f + conjneg g) x✝

Proof state:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f g : G → R
x✝ : G
⊢ conjneg (f + g) x✝ = (conjneg f + conjneg g) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/NormNum/Inv.lean
theorem isNat_ratCast {R : Type*} [DivisionRing R] : {q : ℚ} → {n : ℕ} →
    IsNat q n → IsNat (q : R) n
  | _, _, ⟨rfl⟩ => ⟨by simp⟩

Proof state:
R : Type u_1
inst✝ : DivisionRing R
n✝ : ℕ
⊢ ↑↑n✝ = ↑n✝

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuousWithinAt_tsum {f : ι → α → ℝ≥0∞}
    (h : ∀ i, LowerSemicontinuousWithinAt (f i) s x) :
    LowerSemicontinuousWithinAt (fun x' => ∑' i, f i x') s x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
s : Set α
ι : Type u_3
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun x' => ∑' (i : ι), f i x') s x

Tactic:
simp_rw [ENNReal.tsum_eq_iSup_sum]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
s : Set α
ι : Type u_3
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ s, ∑ i ∈ s, f i x') s x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
s : Set α
ι : Type u_3
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ s, ∑ i ∈ s, f i x') s x

Tactic:
refine lowerSemicontinuousWithinAt_iSup fun b => ?_

Result:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
s : Set α
ι : Type u_3
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
b : Finset ι
⊢ LowerSemicontinuousWithinAt (fun x' => ∑ i ∈ b, f i x') s x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
s : Set α
ι : Type u_3
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
b : Finset ι
⊢ LowerSemicontinuousWithinAt (fun x' => ∑ i ∈ b, f i x') s x

Tactic:
exact lowerSemicontinuousWithinAt_sum fun i _hi => h i

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem modEq_and_modEq_iff_modEq_mul {a b m n : ℤ} (hmn : m.natAbs.Coprime n.natAbs) :
    a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n] :=
  ⟨fun h => by
    rw [modEq_iff_dvd, modEq_iff_dvd] at h
    rw [modEq_iff_dvd, ← natAbs_dvd, ← dvd_natAbs, natCast_dvd_natCast, natAbs_mul]
    refine hmn.mul_dvd_of_dvd_of_dvd ?_ ?_ <;>
      rw [← natCast_dvd_natCast, natAbs_dvd, dvd_natAbs] <;>
      tauto,
    fun h => ⟨h.of_mul_right _, h.of_mul_left _⟩⟩

Proof state:
a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
h : m ∣ b - a ∧ n ∣ b - a
⊢ a ≡ b [ZMOD m * n]

Tactic:
rw [modEq_iff_dvd, ← natAbs_dvd, ← dvd_natAbs, natCast_dvd_natCast, natAbs_mul]

Result:
a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
h : m ∣ b - a ∧ n ∣ b - a
⊢ m.natAbs * n.natAbs ∣ (b - a).natAbs

Proof state:
a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
h : m ∣ b - a ∧ n ∣ b - a
⊢ m.natAbs * n.natAbs ∣ (b - a).natAbs

Tactic:
refine hmn.mul_dvd_of_dvd_of_dvd ?_ ?_ <;>
  rw [← natCast_dvd_natCast, natAbs_dvd, dvd_natAbs] <;>
  tauto

Result:
no goals

Proof state:
a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
h : a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n]
⊢ a ≡ b [ZMOD m * n]

Tactic:
rw [modEq_iff_dvd, modEq_iff_dvd] at h

Result:
a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
h : m ∣ b - a ∧ n ∣ b - a
⊢ a ≡ b [ZMOD m * n]
-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
theorem tendstoLocallyUniformly_iff [TopologicalSpace β] {F : ι → β → α} {f : β → α}
    {p : Filter ι} :
    TendstoLocallyUniformly F f p ↔
      ∀ ε > 0, ∀ x : β, ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, dist (f y) (F n y) < ε

Proof state:
α : Type u
β : Type v
ι : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
⊢ TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε

Tactic:
simp only [← tendstoLocallyUniformlyOn_univ, tendstoLocallyUniformlyOn_iff, nhdsWithin_univ,
  mem_univ, forall_const, exists_prop]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_add_zsmul' (a b : α) (m : ℤ) :
    toIcoDiv hp (a + m • p) b = toIcoDiv hp a b - m

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp (a + m • p) b = toIcoDiv hp a b - m

Tactic:
refine toIcoDiv_eq_of_sub_zsmul_mem_Ico _ ?_

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b - (toIcoDiv hp a b - m) • p ∈ Set.Ico (a + m • p) (a + m • p + p)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b - (toIcoDiv hp a b - m) • p ∈ Set.Ico (a + m • p) (a + m • p + p)

Tactic:
rw [sub_smul, ← sub_add, add_right_comm]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b - toIcoDiv hp a b • p + m • p ∈ Set.Ico (a + m • p) (a + p + m • p)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b - toIcoDiv hp a b • p + m • p ∈ Set.Ico (a + m • p) (a + p + m • p)

Tactic:
simpa using sub_toIcoDiv_zsmul_mem_Ico hp a b

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem S_add_one (n : ℤ) : S R (n + 1) = X * S R n - S R (n - 1)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ S R (n + 1) = X * S R n - S R (n - 1)

Tactic:
linear_combination (norm := ring_nf) S_add_two R (n - 1)

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem mem_of_mem_sInter {x y z : Class} (hy : y ∈ ⋂₀ x) (hz : z ∈ x) : y ∈ z

Proof state:
case intro.intro
x z : Class.{u_1}
hz : z ∈ x
w : ZFSet.{u_1}
hw : (⋂₀ x) w
⊢ ↑w ∈ z

Tactic:
exact coe_mem.2 (hw z hz)

Result:
no goals

Proof state:
x y z : Class.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
⊢ y ∈ z

Tactic:
obtain ⟨w, rfl, hw⟩ := hy

Result:
case intro.intro
x z : Class.{u_1}
hz : z ∈ x
w : ZFSet.{u_1}
hw : (⋂₀ x) w
⊢ ↑w ∈ z
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_ssubset_toFinset : hs.toFinset ⊂ ht.toFinset ↔ s ⊂ t

Proof state:
α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ hs.toFinset ⊂ ht.toFinset ↔ s ⊂ t

Tactic:
simp only [← Finset.coe_ssubset, Finite.coe_toFinset]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Finset.lean
lemma filter_piFinset_eq_map_consEquiv (P : (∀ i, α (succ i)) → Prop) [DecidablePred P] :
    {r ∈ piFinset S | P (tail r)} =
      (S 0 ×ˢ {r ∈ piFinset (tail S) | P r}).map (consEquiv α).toEmbedding

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst✝ : DecidablePred P
⊢ filter (fun r => P (tail r)) (piFinset S) =
    map (consEquiv α).toEmbedding (S 0 ×ˢ filter (fun r => P r) (piFinset (tail S)))

Tactic:
simp [← map_consEquiv_filter_piFinset, map_map]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem derivWithin_const_sub (c : F) :
    derivWithin (fun y => c - f y) s x = -derivWithin f s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
c : F
⊢ derivWithin (fun y => c - f y) s x = -derivWithin f s x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
c : F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => c - f y) s x = -derivWithin f s x

case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
c : F
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => c - f y) s x = -derivWithin f s x

Proof state:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
c : F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => c - f y) s x = -derivWithin f s x

Tactic:
simp [derivWithin, fderivWithin_const_sub hxs]

Result:
no goals

Proof state:
case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
c : F
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => c - f y) s x = -derivWithin f s x

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem coe_one : (↑(1 : FractionalIdeal S P) : Submodule R P) = 1

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
⊢ ↑1 = 1

Tactic:
rw [coe_one_eq_coeSubmodule_top, coeSubmodule_top]

Result:
no goals
-- Mathlib/Data/Finset/Interval.lean
/-- A function `f` from `Finset α` is monotone if and only if `f s ≤ f (insert a s)` for all `s` and
`a ∉ s`. -/
lemma monotone_iff_forall_le_insert : Monotone f ↔ ∀ s ⦃a⦄, a ∉ s → f s ≤ f (insert a s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
f : Finset α → β
inst✝ : DecidableEq α
⊢ Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s ≤ f (insert a s)

Tactic:
simp [monotone_iff_forall_le_cons]

Result:
no goals