harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Image.lean
theorem erase_image_subset_image_erase [DecidableEq α] (f : α → β) (s : Finset α) (a : α) :
    (s.image f).erase (f a) ⊆ (s.erase a).image f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
s : Finset α
a x : α
hx : x ∈ s
hb : f x ≠ f a
⊢ ∃ a_1, (a_1 ≠ a ∧ a_1 ∈ s) ∧ f a_1 = f x

Tactic:
exact ⟨_, ⟨ne_of_apply_ne f hb, hx⟩, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
s : Finset α
a : α
⊢ (image f s).erase (f a) ⊆ image f (s.erase a)

Tactic:
simp only [subset_iff, and_imp, exists_prop, mem_image, exists_imp, mem_erase]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
s : Finset α
a : α
⊢ ∀ ⦃x : β⦄, x ≠ f a → ∀ x_1 ∈ s, f x_1 = x → ∃ a_4, (a_4 ≠ a ∧ a_4 ∈ s) ∧ f a_4 = x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
s : Finset α
a : α
⊢ ∀ ⦃x : β⦄, x ≠ f a → ∀ x_1 ∈ s, f x_1 = x → ∃ a_4, (a_4 ≠ a ∧ a_4 ∈ s) ∧ f a_4 = x

Tactic:
rintro b hb x hx rfl

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
s : Finset α
a x : α
hx : x ∈ s
hb : f x ≠ f a
⊢ ∃ a_1, (a_1 ≠ a ∧ a_1 ∈ s) ∧ f a_1 = f x
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
@[simp]
lemma completedCosZeta_neg (a : UnitAddCircle) (s : ℂ) :
    completedCosZeta (-a) s = completedCosZeta a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ completedCosZeta (-a) s = completedCosZeta a s

Tactic:
simp [completedCosZeta]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem factorization_lt {n : ℕ} (p : ℕ) (hn : n ≠ 0) : n.factorization p < n

Proof state:
n p : ℕ
hn : n ≠ 0
⊢ n.factorization p < n

Tactic:
by_cases pp : p.Prime

Result:
case pos
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ n.factorization p < n

case neg
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ n.factorization p < n

Proof state:
case neg
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ n.factorization p < n

Tactic:
simpa only [factorization_eq_zero_of_non_prime n pp] using hn.bot_lt

Result:
no goals

Proof state:
case pos
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ n.factorization p < n

Tactic:
exact (Nat.pow_lt_pow_iff_right pp.one_lt).1 <| (ordProj_le p hn).trans_lt <|
  Nat.lt_pow_self pp.one_lt

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Powerset.lean
/-- A product over `powerset s` is equal to the double product over sets of subsets of `s` with
`#s = k`, for `k = 1, ..., #s`. -/
@[to_additive "A sum over `powerset s` is equal to the double sum over sets of subsets of `s` with
`#s = k`, for `k = 1, ..., #s`"]
lemma prod_powerset (s : Finset α) (f : Finset α → β) :
    ∏ t ∈ powerset s, f t = ∏ j ∈ range (#s + 1), ∏ t ∈ powersetCard j s, f t

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
s : Finset α
f : Finset α → β
⊢ ∏ t ∈ s.powerset, f t = ∏ j ∈ range (#s + 1), ∏ t ∈ powersetCard j s, f t

Tactic:
rw [powerset_card_disjiUnion, prod_disjiUnion]

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/IntPolynomial.lean
theorem int_monic_iff : (P.int R hP).Monic ↔ P.Monic

Proof state:
K : Type u_1
inst✝ : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
⊢ (int R P hP).Monic ↔ P.Monic

Tactic:
rw [Monic, Monic, ← int_leadingCoeff_eq, OneMemClass.coe_eq_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insertMany_list_le [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List ((a : α) × β a)} :
    (m.insertMany l).1.1.size ≤ m.1.size + l.length

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List ((a : α) × β a)
⊢ (m.insertMany l).val.val.size ≤ m.val.size + l.length

Tactic:
simp_to_model [insertMany] using List.length_insertList_le

Result:
no goals
-- Mathlib/Data/Finset/Fold.lean
theorem fold_congr {g : α → β} (H : ∀ x ∈ s, f x = g x) : s.fold op b f = s.fold op b g

Proof state:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
g : α → β
H : ∀ x ∈ s, f x = g x
⊢ fold op b f s = fold op b g s

Tactic:
rw [fold, fold, map_congr rfl H]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_eq_singleton_iff {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} {b : β} :
    l.mapFinIdx f = #[b] ↔ ∃ (a : α) (w : l = #[a]), f 0 a (by simp [w]) = b

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : (i : Nat) → α → i < l.size → β
b : β
⊢ l.mapFinIdx f = #[b] ↔ ∃ a w, f 0 a ⋯ = b

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
⊢ { toList := l }.mapFinIdx f = #[b] ↔ ∃ a w, f 0 a ⋯ = b

Proof state:
α : Type ?u.76595
β : Type ?u.76619
l : Array α
f : (i : Nat) → α → i < l.size → β
b : β
a : α
w : l = #[a]
⊢ 0 < l.size

Tactic:
simp [w]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
⊢ { toList := l }.mapFinIdx f = #[b] ↔ ∃ a w, f 0 a ⋯ = b

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem isCompl_principal (s : Set α) : IsCompl (𝓟 s) (𝓟 sᶜ) :=
  IsCompl.of_eq (by rw [inf_principal, inter_compl_self, principal_empty]) <| by
    rw [sup_principal, union_compl_self, principal_univ]

Proof state:
α : Type u
s : Set α
⊢ 𝓟 s ⊔ 𝓟 sᶜ = ⊤

Tactic:
rw [sup_principal, union_compl_self, principal_univ]

Result:
no goals

Proof state:
α : Type u
s : Set α
⊢ 𝓟 s ⊓ 𝓟 sᶜ = ⊥

Tactic:
rw [inf_principal, inter_compl_self, principal_empty]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
theorem natCast_lt_cast {m : ℕ} {n : ℚ} : (m : K) < n ↔ (m : ℚ) < n

Proof state:
K : Type u_5
inst✝ : LinearOrderedField K
m : ℕ
n : ℚ
⊢ ↑m < ↑n ↔ ↑m < n

Tactic:
rw [← cast_lt (K := K), cast_natCast]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_lt_of_lt_one_left [SMulPosStrictMono α β] (hb : 0 < b) (h : a < 1) : a • b < b

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Monoid α
inst✝⁴ : Zero β
inst✝³ : MulAction α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosStrictMono α β
hb : 0 < b
h : a < 1
⊢ a • b < b

Tactic:
simpa only [one_smul] using smul_lt_smul_of_pos_right h hb

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem isRight_congr (h : LiftRel r s x y) : x.isRight ↔ y.isRight

Proof state:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s x y
⊢ x.isRight = true ↔ y.isRight = true

Tactic:
cases h <;> rfl

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Basic.lean
theorem lift_single (F : G →* A) (a b) : lift k G A F (single a b) = b • F a

Proof state:
k : Type u₁
G : Type u₂
inst✝³ : CommSemiring k
inst✝² : Monoid G
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra k A
F : G →* A
a : G
b : k
⊢ ((lift k G A) F) (single a b) = b • F a

Tactic:
rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]

Result:
no goals
-- Mathlib/GroupTheory/Coset/Defs.lean
theorem preimage_image_mk (N : Subgroup α) (s : Set α) :
    mk ⁻¹' ((mk : α → α ⧸ N) '' s) = ⋃ x : N, (· * (x : α)) ⁻¹' s

Proof state:
case h
α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
x : α
⊢ x ∈ mk ⁻¹' (mk '' s) ↔ x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' s

Tactic:
simp only [QuotientGroup.eq, SetLike.exists, exists_prop, Set.mem_preimage, Set.mem_iUnion,
  Set.mem_image, ← eq_inv_mul_iff_mul_eq]

Result:
case h
α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
x : α
⊢ (∃ x_1 ∈ s, x_1⁻¹ * x ∈ N) ↔ ∃ x_1 ∈ N, x * x_1 ∈ s

Proof state:
α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
x : α
x✝ : ∃ x_1 ∈ s, x_1⁻¹ * x ∈ N
y : α
hs : y ∈ s
hN : y⁻¹ * x ∈ N
⊢ x * (y⁻¹ * x)⁻¹ ∈ s

Tactic:
simpa using hs

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
x : α
⊢ (∃ x_1 ∈ s, x_1⁻¹ * x ∈ N) ↔ ∃ x_1 ∈ N, x * x_1 ∈ s

Tactic:
exact
  ⟨fun ⟨y, hs, hN⟩ => ⟨_, N.inv_mem hN, by simpa using hs⟩, fun ⟨z, hz, hxz⟩ =>
    ⟨x * z, hxz, by simpa using hz⟩⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
x : α
x✝ : ∃ x_1 ∈ N, x * x_1 ∈ s
z : α
hz : z ∈ N
hxz : x * z ∈ s
⊢ (x * z)⁻¹ * x ∈ N

Tactic:
simpa using hz

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
⊢ mk ⁻¹' (mk '' s) = ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' s

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
x : α
⊢ x ∈ mk ⁻¹' (mk '' s) ↔ x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' s
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem Module.finrank_prod [Module.Finite R M] [Module.Finite R M'] :
    finrank R (M × M') = finrank R M + finrank R M'

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : StrongRankCondition R
inst✝³ : Free R M
inst✝² : Free R M'
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
⊢ finrank R (M × M') = finrank R M + finrank R M'

Tactic:
simp [finrank, rank_lt_aleph0 R M, rank_lt_aleph0 R M']

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem MeasurableSet.subtype_image {s : Set α} {t : Set s} (hs : MeasurableSet s) :
    MeasurableSet t → MeasurableSet (((↑) : s → α) '' t)

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set α
t : Set ↑s
hs : MeasurableSet s
⊢ MeasurableSet t → MeasurableSet (Subtype.val '' t)

Tactic:
rintro ⟨u, hu, rfl⟩

Result:
case intro.intro
α : Type u_1
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (Subtype.val '' (Subtype.val ⁻¹' u))

Proof state:
case intro.intro
α : Type u_1
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (s ∩ u)

Tactic:
exact hs.inter hu

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (Subtype.val '' (Subtype.val ⁻¹' u))

Tactic:
rw [Subtype.image_preimage_coe]

Result:
case intro.intro
α : Type u_1
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (s ∩ u)
-- Mathlib/RingTheory/Coalgebra/Basic.lean
theorem counit_comp_inr : counit ∘ₗ inr R A B = counit

Proof state:
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : B
⊢ (counit ∘ₗ inr R A B) x✝ = counit x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ counit ∘ₗ inr R A B = counit

Tactic:
ext

Result:
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : B
⊢ (counit ∘ₗ inr R A B) x✝ = counit x✝
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
/-- Any change of coordinates with empty source belongs to `continuousGroupoid`. -/
lemma ContinuousGroupoid.mem_of_source_eq_empty (f : PartialHomeomorph H H)
    (hf : f.source = ∅) : f ∈ continuousGroupoid H

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
⊢ f ∈ contDiffGroupoid 0 I

Tactic:
exact ContDiffGroupoid.mem_of_source_eq_empty f hf

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
⊢ f ∈ continuousGroupoid H

Tactic:
rw [← contDiffGroupoid_zero_eq (I := I)]

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
⊢ f ∈ contDiffGroupoid 0 I
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eval_basisDivisor_right : eval y (basisDivisor x y) = 0

Proof state:
F : Type u_1
inst✝ : Field F
x y : F
⊢ eval y (basisDivisor x y) = 0

Tactic:
simp only [basisDivisor, eval_mul, eval_C, eval_sub, eval_X, sub_self, mul_zero]

Result:
no goals
-- Mathlib/Order/Compare.lean
theorem cmpLE_eq_cmp {α} [Preorder α] [IsTotal α (· ≤ ·)] [DecidableRel (α := α) (· ≤ ·)]
    [DecidableRel (α := α) (· < ·)] (x y : α) : cmpLE x y = cmp x y

Proof state:
case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 < x2
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False

Tactic:
cases not_or_intro xy yx (total_of _ _ _)

Result:
no goals

Proof state:
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 < x2
x y : α
⊢ cmpLE x y = cmp x y

Tactic:
by_cases xy : x ≤ y <;> by_cases yx : y ≤ x <;> simp [cmpLE, lt_iff_le_not_le, *, cmp, cmpUsing]

Result:
case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 < x2
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False
-- Mathlib/Data/NNRat/Defs.lean
lemma coprime_num_den (q : ℚ≥0) : q.num.Coprime q.den

Proof state:
q : ℚ≥0
⊢ q.num.Coprime q.den

Tactic:
simpa [num, den] using Rat.reduced _

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem isRight_left (h : LiftRel r s x (inr d)) : x.isRight

Proof state:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
d : δ
h : LiftRel r s x (inr d)
⊢ x.isRight = true

Tactic:
cases h

Result:
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
d : δ
b✝ : β
a✝ : s b✝ d
⊢ (inr b✝).isRight = true

Proof state:
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
d : δ
b✝ : β
a✝ : s b✝ d
⊢ (inr b✝).isRight = true

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/FunctorToTypes.lean
@[simp]
lemma binaryProductIso_inv_comp_snd :
    (binaryProductIso F G).inv ≫ Limits.prod.snd = prod.snd

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ (binaryProductIso F G).inv ≫ Limits.prod.snd = prod.snd

Tactic:
simp [binaryProductIso, binaryProductLimitCone]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem splitUpper_def [DecidableEq ι] {i x} (h : x ∈ Ioo (I.lower i) (I.upper i))
    (h' : ∀ j, update I.lower i x j < I.upper j :=
      (forall_update_iff I.lower fun j y => y < I.upper j).2
        ⟨h.2, fun _ _ => I.lower_lt_upper _⟩) :
    I.splitUpper i x = (⟨update I.lower i x, I.upper, h'⟩ : Box ι)

Proof state:
ι : Type u_1
I : Box ι
inst✝ : DecidableEq ι
i : ι
x : ℝ
h : x ∈ Ioo (I.lower i) (I.upper i)
h' : optParam (∀ (j : ι), update I.lower i x j < I.upper j) ⋯
⊢ I.splitUpper i x = ↑{ lower := update I.lower i x, upper := I.upper, lower_lt_upper := h' }

Tactic:
simp (config := { unfoldPartialApp := true }) only [splitUpper, mk'_eq_coe, max_eq_left h.1.le,
  update, and_self]

Result:
no goals
-- Mathlib/Probability/BorelCantelli.lean
theorem iIndepFun.condExp_natural_ae_eq_of_lt [SecondCountableTopology β] [CompleteSpace β]
    [NormedSpace ℝ β] (hf : ∀ i, StronglyMeasurable (f i)) (hfi : iIndepFun (fun _ => mβ) f μ)
    (hij : i < j) : μ[f j|Filtration.natural f hf i] =ᵐ[μ] fun _ => μ[f j]

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst✝⁵ : LinearOrder ι
mβ : MeasurableSpace β
inst✝⁴ : NormedAddCommGroup β
inst✝³ : BorelSpace β
f : ι → Ω → β
i j : ι
inst✝² : SecondCountableTopology β
inst✝¹ : CompleteSpace β
inst✝ : NormedSpace ℝ β
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (fun x => mβ) f μ
hij : i < j
this : IsProbabilityMeasure μ
⊢ μ[f j|↑(Filtration.natural f hf) i] =ᶠ[ae μ] fun x => ∫ (x : Ω), f j x ∂μ

Tactic:
exact condExp_indep_eq (hf j).measurable.comap_le (Filtration.le _ _)
  (comap_measurable <| f j).stronglyMeasurable (hfi.indep_comap_natural_of_lt hf hij)

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst✝⁵ : LinearOrder ι
mβ : MeasurableSpace β
inst✝⁴ : NormedAddCommGroup β
inst✝³ : BorelSpace β
f : ι → Ω → β
i j : ι
inst✝² : SecondCountableTopology β
inst✝¹ : CompleteSpace β
inst✝ : NormedSpace ℝ β
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (fun x => mβ) f μ
hij : i < j
⊢ μ[f j|↑(Filtration.natural f hf) i] =ᶠ[ae μ] fun x => ∫ (x : Ω), f j x ∂μ

Tactic:
have : IsProbabilityMeasure μ := hfi.isProbabilityMeasure

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst✝⁵ : LinearOrder ι
mβ : MeasurableSpace β
inst✝⁴ : NormedAddCommGroup β
inst✝³ : BorelSpace β
f : ι → Ω → β
i j : ι
inst✝² : SecondCountableTopology β
inst✝¹ : CompleteSpace β
inst✝ : NormedSpace ℝ β
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (fun x => mβ) f μ
hij : i < j
this : IsProbabilityMeasure μ
⊢ μ[f j|↑(Filtration.natural f hf) i] =ᶠ[ae μ] fun x => ∫ (x : Ω), f j x ∂μ
-- Mathlib/Data/Finset/Lattice/Basic.lean
theorem inter_left_comm (s₁ s₂ s₃ : Finset α) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
  ext fun _ => by simp only [mem_inter, and_left_comm]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finset α
x✝ : α
⊢ x✝ ∈ s₁ ∩ (s₂ ∩ s₃) ↔ x✝ ∈ s₂ ∩ (s₁ ∩ s₃)

Tactic:
simp only [mem_inter, and_left_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_modify_self (h : m.1.WF) [Inhabited α] {k : α} {f : β → β}
    (hc : (Const.modify m k f).contains k) : (Const.modify m k f).getKey k hc = k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
inst✝ : Inhabited α
k : α
f : β → β
hc : (modify m k f).contains k = true
⊢ (modify m k f).getKey k hc = k

Tactic:
simp_to_model [Const.modify] using List.Const.getKey_modifyKey_self

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem divp_mul_cancel (a : α) (u : αˣ) : a /ₚ u * u = a :=
  (mul_assoc _ _ _).trans <| by rw [Units.inv_mul, mul_one]

Proof state:
α : Type u
inst✝ : Monoid α
a : α
u : αˣ
⊢ a * (↑u⁻¹ * ↑u) = a

Tactic:
rw [Units.inv_mul, mul_one]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem iteratedFDerivWithin_zero_fun {i : ℕ} :
    iteratedFDerivWithin 𝕜 i (fun _ : E ↦ (0 : F)) s = 0

Proof state:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
⊢ iteratedFDerivWithin 𝕜 0 (fun x => 0) s = 0

Tactic:
ext

Result:
case zero.h.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
x✝¹ : E
x✝ : Fin 0 → E
⊢ (iteratedFDerivWithin 𝕜 0 (fun x => 0) s x✝¹) x✝ = (0 x✝¹) x✝

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
i : ℕ
⊢ iteratedFDerivWithin 𝕜 i (fun x => 0) s = 0

Tactic:
cases i with
| zero => ext; simp
| succ i => apply iteratedFDerivWithin_succ_const

Result:
no goals

Proof state:
case zero.h.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
x✝¹ : E
x✝ : Fin 0 → E
⊢ (iteratedFDerivWithin 𝕜 0 (fun x => 0) s x✝¹) x✝ = (0 x✝¹) x✝

Tactic:
simp

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
i : ℕ
⊢ iteratedFDerivWithin 𝕜 (i + 1) (fun x => 0) s = 0

Tactic:
apply iteratedFDerivWithin_succ_const

Result:
no goals
-- Mathlib/Data/Finsupp/Order.lean
@[simp] lemma single_nonpos : single i a ≤ 0 ↔ a ≤ 0

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
i : ι
a : α
⊢ single i a ≤ 0 ↔ a ≤ 0

Tactic:
classical exact Pi.single_nonpos

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
i : ι
a : α
⊢ single i a ≤ 0 ↔ a ≤ 0

Tactic:
exact Pi.single_nonpos

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
theorem sigma_condition : I.fstSigmaMap ≫ Sigma.desc K.π = I.sndSigmaMap ≫ Sigma.desc K.π

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
⊢ I.fstSigmaMap ≫ Sigma.desc K.π = I.sndSigmaMap ≫ Sigma.desc K.π

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b✝ : J.L
⊢ Sigma.ι I.left b✝ ≫ I.fstSigmaMap ≫ Sigma.desc K.π = Sigma.ι I.left b✝ ≫ I.sndSigmaMap ≫ Sigma.desc K.π

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b✝ : J.L
⊢ Sigma.ι I.left b✝ ≫ I.fstSigmaMap ≫ Sigma.desc K.π = Sigma.ι I.left b✝ ≫ I.sndSigmaMap ≫ Sigma.desc K.π

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma add_biSup' {p : ι → Prop} (h : ∃ i, p i) (f : ι → ℝ≥0∞) :
    a + ⨆ i, ⨆ _ : p i, f i = ⨆ i, ⨆ _ : p i, a + f i

Proof state:
ι : Sort u_1
a : ℝ≥0∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℝ≥0∞
this : Nonempty { i // p i }
⊢ a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i

Tactic:
simp only [iSup_subtype', add_iSup]

Result:
no goals

Proof state:
ι : Sort u_1
a : ℝ≥0∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℝ≥0∞
⊢ a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i

Tactic:
haveI : Nonempty {i // p i} := nonempty_subtype.2 h

Result:
ι : Sort u_1
a : ℝ≥0∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℝ≥0∞
this : Nonempty { i // p i }
⊢ a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i