harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order.lean
theorem discreteTopology_iff_nhds [TopologicalSpace α] :
    DiscreteTopology α ↔ ∀ x : α, 𝓝 x = pure x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), 𝓝 x = pure x

Tactic:
simp [discreteTopology_iff_singleton_mem_nhds, le_pure_iff]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), {x} ∈ 𝓝 x) ↔ ∀ (x : α), 𝓝 x = pure x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), {x} ∈ 𝓝 x) ↔ ∀ (x : α), 𝓝 x = pure x

Tactic:
apply forall_congr' (fun x ↦ ?_)

Result:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
⊢ {x} ∈ 𝓝 x ↔ 𝓝 x = pure x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
⊢ {x} ∈ 𝓝 x ↔ 𝓝 x = pure x

Tactic:
simp [le_antisymm_iff, pure_le_nhds x]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem affinity_unitBall {r : ℝ} (hr : 0 < r) (x : E) : x +ᵥ r • ball (0 : E) 1 = ball x r

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
⊢ x +ᵥ r • ball 0 1 = ball x r

Tactic:
rw [smul_unitBall_of_pos hr, vadd_ball_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem all_eq_false' {p : α → Bool} {as : Array α} :
    as.all p = false ↔ ∃ x, x ∈ as ∧ ¬p x

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ (¬∀ (x : α), x ∈ as → p x = true) ↔ ∃ x, x ∈ as ∧ ¬p x = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ as.all p = false ↔ ∃ x, x ∈ as ∧ ¬p x = true

Tactic:
rw [Bool.eq_false_iff, Ne, all_eq_true']

Result:
α : Type u_1
p : α → Bool
as : Array α
⊢ (¬∀ (x : α), x ∈ as → p x = true) ↔ ∃ x, x ∈ as ∧ ¬p x = true
-- Mathlib/Order/Filter/Map.lean
theorem frequently_comap : (∃ᶠ a in comap f l, p a) ↔ ∃ᶠ b in l, ∃ a, f a = b ∧ p a

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
p : α → Prop
⊢ (∃ᶠ (a : α) in comap f l, p a) ↔ ∃ᶠ (b : β) in l, ∃ a, f a = b ∧ p a

Tactic:
simp only [Filter.Frequently, eventually_comap, not_exists, _root_.not_and]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean
lemma δ_naturality_apply {n : ℕ} (i : Fin (n + 2)) (x : S _⦋n + 1⦌) :
    f.app (op ⦋n⦌) (S.δ i x) = T.δ i (f.app (op ⦋n + 1⦌) x)

Proof state:
S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 2)
x : S _⦋n + 1⦌
⊢ (SimplicialObject.δ S i ≫ f.app (op ⦋n⦌)) x = (f.app (op ⦋n + 1⦌) ≫ SimplicialObject.δ T i) x

Tactic:
exact congr_fun (SimplicialObject.δ_naturality f i) x

Result:
no goals

Proof state:
S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 2)
x : S _⦋n + 1⦌
⊢ f.app (op ⦋n⦌) (SimplicialObject.δ S i x) = SimplicialObject.δ T i (f.app (op ⦋n + 1⦌) x)

Tactic:
show (S.δ i ≫ f.app (op ⦋n⦌)) x = (f.app (op ⦋n + 1⦌) ≫ T.δ i) x

Result:
S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 2)
x : S _⦋n + 1⦌
⊢ (SimplicialObject.δ S i ≫ f.app (op ⦋n⦌)) x = (f.app (op ⦋n + 1⦌) ≫ SimplicialObject.δ T i) x
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem content_dvd_coeff {p : R[X]} (n : ℕ) : p.content ∣ p.coeff n

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ p.content ∣ 0

Tactic:
apply dvd_zero

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
⊢ p.content ∣ p.coeff n

Tactic:
by_cases h : n ∈ p.support

Result:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∈ p.support
⊢ p.content ∣ p.coeff n

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∉ p.support
⊢ p.content ∣ p.coeff n

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∉ p.support
⊢ p.content ∣ p.coeff n

Tactic:
rw [mem_support_iff, Classical.not_not] at h

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ p.content ∣ p.coeff n

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ p.content ∣ p.coeff n

Tactic:
rw [h]

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ p.content ∣ 0

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∈ p.support
⊢ p.content ∣ p.coeff n

Tactic:
apply Finset.gcd_dvd h

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem multichoose_neg_succ (n : ℕ) : multichoose (-n : ℤ) (n + 1) = 0

Proof state:
n : ℕ
⊢ multichoose (-↑n) (n + 1) = 0

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero _),
  factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_succ_neg, smul_zero]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem surjOn_empty_iff : SurjOn f ∅ t ↔ t = ∅

Proof state:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
⊢ SurjOn f ∅ t ↔ t = ∅

Tactic:
simp [SurjOn, subset_empty_iff]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive] lemma inv_subset_div_right (hs : 1 ∈ s) : t⁻¹ ⊆ s / t

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s * t⁻¹

Tactic:
exact subset_mul_right _ hs

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s / t

Tactic:
rw [div_eq_mul_inv]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s * t⁻¹
-- Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
@[simp] lemma log_one : log 1 = 0

Proof state:
⊢ log 1 = 0

Tactic:
simp [log]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem eraseIdx_modifyHead_zero {f : α → α} {l : List α} :
    (l.modifyHead f).eraseIdx 0 = l.eraseIdx 0

Proof state:
α : Type u_1
f : α → α
l : List α
⊢ (modifyHead f l).eraseIdx 0 = l.eraseIdx 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem mul_right' (c : ℕ) (h : a ≡ b [MOD n]) : a * c ≡ b * c [MOD n * c]

Proof state:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD c * n]

Tactic:
exact h.mul_left' c

Result:
no goals

Proof state:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ a * c ≡ b * c [MOD n * c]

Tactic:
rw [mul_comm a, mul_comm b, mul_comm n]

Result:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD c * n]
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem pentagon_inv_inv_hom_hom_inv :
    (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom =
      W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom) ≫ (α_ (W ⊗ X) Y Z).inv =
    (W ◁ (α_ X Y Z).inv ≫ W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv) ≫ (α_ (W ⊗ X) Y Z).inv

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom = W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv

Tactic:
rw [← cancel_epi (W ◁ (α_ X Y Z).inv), ← cancel_mono (α_ (W ⊗ X) Y Z).inv]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom) ≫ (α_ (W ⊗ X) Y Z).inv =
    (W ◁ (α_ X Y Z).inv ≫ W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv) ≫ (α_ (W ⊗ X) Y Z).inv
-- Mathlib/Algebra/Order/BigOperators/Group/List.lean
@[to_additive exists_le_of_sum_le]
lemma exists_le_of_prod_le' [LinearOrder M] [MulLeftStrictMono M]
    [MulLeftMono M] [MulRightStrictMono M]
    [MulRightMono M] {l : List ι} (hl : l ≠ []) (f g : ι → M)
    (h : (l.map f).prod ≤ (l.map g).prod) : ∃ x ∈ l, f x ≤ g x

Proof state:
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : LinearOrder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
l : List ι
hl : l ≠ []
f g : ι → M
h : ∀ (x : ι), x ∈ l → g x < f x
⊢ (map g l).prod < (map f l).prod

Tactic:
exact prod_lt_prod_of_ne_nil hl _ _ h

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : LinearOrder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
l : List ι
hl : l ≠ []
f g : ι → M
h : (map f l).prod ≤ (map g l).prod
⊢ ∃ x, x ∈ l ∧ f x ≤ g x

Tactic:
contrapose! h

Result:
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : LinearOrder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
l : List ι
hl : l ≠ []
f g : ι → M
h : ∀ (x : ι), x ∈ l → g x < f x
⊢ (map g l).prod < (map f l).prod
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_univ [Fintype ι] : 𝔼 i, f i = (∑ i, f i) /ℚ Fintype.card ι

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
f : ι → M
inst✝ : Fintype ι
⊢ 𝔼 i : ι, f i = (↑(Fintype.card ι))⁻¹ • ∑ i : ι, f i

Tactic:
rw [expect, card_univ]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Ioc_succ_singleton : Ioc b (b + 1) = {b + 1}

Proof state:
b : ℕ
⊢ Ioc b (b + 1) = {b + 1}

Tactic:
rw [← Nat.Icc_succ_left, Icc_self]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basis.lean
lemma TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply
    (m : M) (n : N) (i : ι) :
    (TensorProduct.equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ n) i =
    ℬ.repr m i • n

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
m : M
n : N
i : ι
⊢ ((equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ[R] n)) i = (ℬ.repr m) i • n

Tactic:
simp only [equivFinsuppOfBasisLeft_apply_tmul, Finsupp.mapRange_apply]

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem not_minimal_iff (hx : P x) : ¬ Minimal P x ↔ ∃ y, P y ∧ y ≤ x ∧ ¬ (x ≤ y)

Proof state:
α : Type u_1
P : α → Prop
x : α
inst✝ : LE α
hx : P x
⊢ ¬Minimal P x ↔ ∃ y, P y ∧ y ≤ x ∧ ¬x ≤ y

Tactic:
simp [Minimal, hx]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
@[simp]
lemma comp_add : κ ∘ₘ (μ + ν) = κ ∘ₘ μ + κ ∘ₘ ν

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
⊢ ⇑κ ∘ₘ (μ + ν) = ⇑κ ∘ₘ μ + ⇑κ ∘ₘ ν

Tactic:
simp_rw [comp_eq_comp_const_apply, Kernel.const_add, Kernel.comp_add_right, Kernel.add_apply]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma neg_one_pow_eq_one_iff_even {R : Type*} [Monoid R] [HasDistribNeg R] {n : ℕ}
    (h : (-1 : R) ≠ 1) : (-1 : R) ^ n = 1 ↔ Even n

Proof state:
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : -1 ≠ 1
⊢ (-1) ^ n = 1 ↔ Even n

Tactic:
simp [neg_one_pow_eq_ite, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem reverse_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
    (H : ∀ (a : α), a ∈ xs → P a) :
    (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h))

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : Array α
H : ∀ (a : α), a ∈ xs → P a
⊢ (pmap f xs H).reverse = pmap f xs.reverse ⋯

Tactic:
rw [pmap_reverse]

Result:
no goals

Proof state:
α : Type ?u.128818
β : Type ?u.128852
P : α → Prop
f : (a : α) → P a → β
xs : Array α
H : ∀ (a : α), a ∈ xs → P a
a : α
h : a ∈ xs.reverse
⊢ a ∈ xs

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_sub_int (a : α) (z : ℤ) : ⌊a - z⌋ = ⌊a⌋ - z :=
  Eq.trans (by rw [Int.cast_neg, sub_eq_add_neg]) (floor_add_int _ _)

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
z : ℤ
⊢ ⌊a - ↑z⌋ = ⌊a + ↑(-z)⌋

Tactic:
rw [Int.cast_neg, sub_eq_add_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem State.IsExtensionBy_rfl (state : State aig) {h}
    (hmarked : state.cache.marks[idx]'h = true) :
    State.IsExtensionBy state state idx (have := state.cache.hmarks; omega)

Proof state:
aig : AIG Nat
idx : Nat
omega : idx < aig.decls.size
state : State aig
h : idx < state.cache.marks.size
hmarked : state.cache.marks[idx] = true
⊢ state.IsExtensionBy state idx ⋯

Tactic:
apply Cache.IsExtensionBy_rfl <;> assumption

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
theorem pullbackSymmetry_inv_comp_fst [HasPullback f g] :
    (pullbackSymmetry f g).inv ≫ pullback.fst f g = pullback.snd g f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (pullbackSymmetry f g).inv ≫ pullback.fst f g = pullback.snd g f

Tactic:
simp [Iso.inv_comp_eq]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem comp_smul (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (c : 𝕜₂) :
    p.comp (c • f) = ‖c‖₊ • p.comp f :=
  ext fun _ => by
    rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm,
      smul_eq_mul, comp_apply]

Proof state:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : SeminormedCommRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜₂ E₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
c : 𝕜₂
x✝ : E
⊢ (p.comp (c • f)) x✝ = (‖c‖₊ • p.comp f) x✝

Tactic:
rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm,
  smul_eq_mul, comp_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.isoProd_inv {X Y : C} [HasBinaryBiproduct X Y] :
    (biprod.isoProd X Y).inv = biprod.lift prod.fst prod.snd

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoProd X Y).inv = lift prod.fst prod.snd

Tactic:
ext <;> simp [Iso.inv_comp_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Basic.lean
theorem homOfLe_ι {G G' : Subpresheaf F} (h : G ≤ G') :
    Subpresheaf.homOfLe h ≫ G'.ι = G.ι

Proof state:
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : G ≤ G'
x✝ : Cᵒᵖ
a✝ : G.toPresheaf.obj x✝
⊢ (homOfLe h ≫ G'.ι).app x✝ a✝ = G.ι.app x✝ a✝

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : G ≤ G'
⊢ homOfLe h ≫ G'.ι = G.ι

Tactic:
ext

Result:
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : G ≤ G'
x✝ : Cᵒᵖ
a✝ : G.toPresheaf.obj x✝
⊢ (homOfLe h ≫ G'.ι).app x✝ a✝ = G.ι.app x✝ a✝
-- Mathlib/Algebra/Homology/ComplexShapeSigns.lean
lemma σ_symm (i₁ : I₁) (i₂ : I₂) :
    σ c₂ c₁ c₁₂ i₂ i₁ = σ c₁ c₂ c₁₂ i₁ i₂

Proof state:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₂ c₁ c₁₂
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c₁₂
inst✝¹ : TotalComplexShapeSymmetry c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetrySymmetry c₁ c₂ c₁₂
i₁ : I₁
i₂ : I₂
⊢ c₂.σ c₁ c₁₂ i₂ i₁ = c₁.σ c₂ c₁₂ i₁ i₂

Tactic:
apply TotalComplexShapeSymmetrySymmetry.σ_symm

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive all_zero_of_le_zero_le_of_sum_eq_zero]
lemma all_one_of_le_one_le_of_prod_eq_one :
    (∀ x ∈ s, (1 : α) ≤ x) → s.prod = 1 → ∀ x ∈ s, x = (1 : α) :=
  Quotient.inductionOn s (by
    simp only [quot_mk_to_coe, prod_coe, mem_coe]
    exact fun l => List.all_one_of_le_one_le_of_prod_eq_one)

Proof state:
α : Type u_2
inst✝ : OrderedCommMonoid α
s : Multiset α
⊢ ∀ (a : List α), (∀ x ∈ ⟦a⟧, 1 ≤ x) → prod ⟦a⟧ = 1 → ∀ x ∈ ⟦a⟧, x = 1

Tactic:
simp only [quot_mk_to_coe, prod_coe, mem_coe]

Result:
α : Type u_2
inst✝ : OrderedCommMonoid α
s : Multiset α
⊢ ∀ (a : List α), (∀ x ∈ a, 1 ≤ x) → a.prod = 1 → ∀ x ∈ a, x = 1

Proof state:
α : Type u_2
inst✝ : OrderedCommMonoid α
s : Multiset α
⊢ ∀ (a : List α), (∀ x ∈ a, 1 ≤ x) → a.prod = 1 → ∀ x ∈ a, x = 1

Tactic:
exact fun l => List.all_one_of_le_one_le_of_prod_eq_one

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Strong.lean
theorem whiskerLeft_naturality_id (f : a' ⟶ G.obj a) :
    f ◁ (θ.naturality (𝟙 a)).hom ≫ f ◁ θ.app a ◁ H.mapId a =
      f ◁ G.mapId a ▷ θ.app a ≫ f ◁ (λ_ (θ.app a)).hom ≫ f ◁ (ρ_ (θ.app a)).inv

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
G H : OplaxFunctor B C
θ : StrongOplaxNatTrans G H
a : B
a' : C
f : a' ⟶ G.obj a
⊢ f ◁ (θ.naturality (𝟙 a)).hom ≫ f ◁ θ.app a ◁ H.mapId a =
    f ◁ G.mapId a ▷ θ.app a ≫ f ◁ (λ_ (θ.app a)).hom ≫ f ◁ (ρ_ (θ.app a)).inv

Tactic:
apply θ.toOplax.whiskerLeft_naturality_id

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_apply_getElem_zero (l : List α) (h : Nodup l) (hl : 1 < l.length) :
    formPerm l l[0] = l[1]

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
h : [].Nodup
hl : 1 < [].length
⊢ [].formPerm [][0] = [][1]

Tactic:
simp at hl

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x : α
h : [x].Nodup
hl : 1 < [x].length
⊢ [x].formPerm [x][0] = [x][1]

Tactic:
simp at hl

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
tl : List α
h : (x :: y :: tl).Nodup
hl : 1 < (x :: y :: tl).length
⊢ (x :: y :: tl).formPerm (x :: y :: tl)[0] = (x :: y :: tl)[1]

Tactic:
rw [getElem_cons_zero, formPerm_apply_head _ _ _ h, getElem_cons_succ, getElem_cons_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
hl : 1 < l.length
⊢ l.formPerm l[0] = l[1]

Tactic:
rcases l with (_ | ⟨x, _ | ⟨y, tl⟩⟩)

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
h : [].Nodup
hl : 1 < [].length
⊢ [].formPerm [][0] = [][1]

case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x : α
h : [x].Nodup
hl : 1 < [x].length
⊢ [x].formPerm [x][0] = [x][1]

case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
tl : List α
h : (x :: y :: tl).Nodup
hl : 1 < (x :: y :: tl).length
⊢ (x :: y :: tl).formPerm (x :: y :: tl)[0] = (x :: y :: tl)[1]
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoLocallyUniformlyOn.tendsto_at (hf : TendstoLocallyUniformlyOn F f p s) {a : α}
    (ha : a ∈ s) : Tendsto (fun i => F i a) p (𝓝 (f a))

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
hf : TendstoLocallyUniformlyOn F f p s
a : α
ha : a ∈ s
⊢ 𝓟 {a} ≤ 𝓝[s] a

Tactic:
simpa only [Filter.principal_singleton] using pure_le_nhdsWithin ha

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
hf : TendstoLocallyUniformlyOn F f p s
a : α
ha : a ∈ s
⊢ Tendsto (fun i => F i a) p (𝓝 (f a))

Tactic:
refine ((tendstoLocallyUniformlyOn_iff_filter.mp hf) a ha).tendsto_at ?_

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
hf : TendstoLocallyUniformlyOn F f p s
a : α
ha : a ∈ s
⊢ 𝓟 {a} ≤ 𝓝[s] a
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem pairwiseDisjoint_smul_iff {s : Set α} {t : Finset α} :
    s.PairwiseDisjoint (· • t) ↔ (s ×ˢ t : Set (α × α)).InjOn fun p => p.1 * p.2

Proof state:
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s : Set α
t : Finset α
⊢ (s.PairwiseDisjoint fun x => x • t) ↔ Set.InjOn (fun p => p.1 * p.2) (s ×ˢ ↑t)

Tactic:
simp_rw [← pairwiseDisjoint_coe, coe_smul_finset, Set.pairwiseDisjoint_smul_iff]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Cast.lean
theorem cast_eq_of_cons_eq_cons {u v v' w : U} {p : Path u v} {p' : Path u v'} {e : v ⟶ w}
    {e' : v' ⟶ w} (h : p.cons e = p'.cons e') : p.cast rfl (obj_eq_of_cons_eq_cons h) = p'

Proof state:
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ HEq p p'

Tactic:
exact heq_of_cons_eq_cons h

Result:
no goals

Proof state:
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ Path.cast ⋯ ⋯ p = p'

Tactic:
rw [Path.cast_eq_iff_heq]

Result:
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ HEq p p'
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem mem_nil {x} : ¬x ∈ (.nil : RBNode α)

Proof state:
α : Type u_1
x : α
⊢ ¬x ∈ nil

Tactic:
simp [Membership.mem, EMem]

Result:
no goals
-- Mathlib/Order/Filter/Tendsto.lean
theorem tendsto_iSup {f : α → β} {x : ι → Filter α} {y : Filter β} :
    Tendsto f (⨆ i, x i) y ↔ ∀ i, Tendsto f (x i) y

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : α → β
x : ι → Filter α
y : Filter β
⊢ Tendsto f (⨆ i, x i) y ↔ ∀ (i : ι), Tendsto f (x i) y

Tactic:
simp only [Tendsto, map_iSup, iSup_le_iff]

Result:
no goals
-- Mathlib/Data/ENat/Basic.lean
theorem lift_add (a b : ℕ∞) (h : a + b < ⊤) :
    lift (a + b) h = lift a (add_lt_top.1 h).1 + lift b (add_lt_top.1 h).2

Proof state:
a b : ℕ∞
h : a + b < ⊤
⊢ (a + b).lift h = a.lift ⋯ + b.lift ⋯

Tactic:
apply coe_inj.1

Result:
a b : ℕ∞
h : a + b < ⊤
⊢ ↑((a + b).lift h) = ↑(a.lift ⋯ + b.lift ⋯)

Proof state:
a b : ℕ∞
h : a + b < ⊤
⊢ ↑((a + b).lift h) = ↑(a.lift ⋯ + b.lift ⋯)

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/ExistsUnique.lean
theorem ExistsUnique.elim₂ {p : α → Sort*} [∀ x, Subsingleton (p x)]
    {q : ∀ (x) (_ : p x), Prop} {b : Prop} (h₂ : ∃! x, ∃! h : p x, q x h)
    (h₁ : ∀ (x) (h : p x), q x h → (∀ (y) (hy : p y), q y hy → y = x) → b) : b

Proof state:
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x, ∃ h, q x h
⊢ ∀ (x : α), (∃ h, q x h) → (∀ (y : α), (∃ h, q y h) → y = x) → b

Tactic:
exact fun x ⟨hxp, hxq⟩ H ↦ h₁ x hxp hxq fun y hyp hyq ↦ H y ⟨hyp, hyq⟩

Result:
no goals

Proof state:
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₂ : ∃! x, ∃! h, q x h
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
⊢ b

Tactic:
simp only [existsUnique_iff_exists] at h₂

Result:
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x, ∃ h, q x h
⊢ b

Proof state:
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x, ∃ h, q x h
⊢ b

Tactic:
apply h₂.elim

Result:
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x, ∃ h, q x h
⊢ ∀ (x : α), (∃ h, q x h) → (∀ (y : α), (∃ h, q y h) → y = x) → b
-- Mathlib/Probability/Kernel/Composition/Comp.lean
lemma comp_add_left (μ : Kernel α β) (κ η : Kernel β γ) :
    (κ + η) ∘ₖ μ = κ ∘ₖ μ + η ∘ₖ μ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel β γ
⊢ (κ + η) ∘ₖ μ = κ ∘ₖ μ + η ∘ₖ μ

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel β γ
a : α
s : Set γ
hs : MeasurableSet s
⊢ (((κ + η) ∘ₖ μ) a) s = ((κ ∘ₖ μ + η ∘ₖ μ) a) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel β γ
a : α
s : Set γ
hs : MeasurableSet s
⊢ (((κ + η) ∘ₖ μ) a) s = ((κ ∘ₖ μ + η ∘ₖ μ) a) s

Tactic:
simp_rw [comp_apply' _ _ _ hs, add_apply, Measure.add_apply, comp_apply' _ _ _ hs,
  lintegral_add_left (Kernel.measurable_coe κ hs)]

Result:
no goals