harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem nnnorm_eq_ciSup (f : PiLp ∞ β) : ‖f‖₊ = ⨆ i, ‖f i‖₊

Proof state:
case a
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ⊤ β
⊢ ↑‖f‖₊ = ↑(⨆ i, ‖f i‖₊)

Tactic:
simp [NNReal.coe_iSup, norm_eq_ciSup]

Result:
no goals

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ⊤ β
⊢ ‖f‖₊ = ⨆ i, ‖f i‖₊

Tactic:
ext

Result:
case a
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ⊤ β
⊢ ↑‖f‖₊ = ↑(⨆ i, ‖f i‖₊)
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem lie_le_inf : ⁅I, J⁆ ≤ I ⊓ J

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, J⁆ ≤ I ⊓ J

Tactic:
rw [le_inf_iff]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, J⁆ ≤ I ∧ ⁅I, J⁆ ≤ J

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, J⁆ ≤ I ∧ ⁅I, J⁆ ≤ J

Tactic:
exact ⟨lie_le_left I J, lie_le_right J I⟩

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem IsSeparatedFor.isSheafFor (t : IsSeparatedFor P R) :
    (∀ x : FamilyOfElements P R, x.Compatible → ∃ t, x.IsAmalgamation t) → IsSheafFor P R

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
t : IsSeparatedFor P R
⊢ (∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) →
    IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
exact And.intro t

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
t : IsSeparatedFor P R
⊢ (∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) → IsSheafFor P R

Tactic:
rw [← isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
t : IsSeparatedFor P R
⊢ (∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) →
    IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousWithinAt.comp_inter_of_eq {g : β → γ} {t : Set β} {y : β}
    (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x) (hy : f x = y) :
    ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g t (f x)
⊢ ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
exact hg.comp_inter hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
subst hy

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g t (f x)
⊢ ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem chain_conj (c P : α → Prop) (hchain : chain c) : chain (fun x => c x ∧ P x)

Proof state:
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
⊢ chain fun x => c x ∧ P x

Tactic:
intro x y ⟨hcx, _⟩ ⟨hcy, _⟩

Result:
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
x y : α
hcx : c x
right✝¹ : P x
hcy : c y
right✝ : P y
⊢ x ⊑ y ∨ y ⊑ x

Proof state:
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
x y : α
hcx : c x
right✝¹ : P x
hcy : c y
right✝ : P y
⊢ x ⊑ y ∨ y ⊑ x

Tactic:
exact hchain x y hcx hcy

Result:
no goals
-- Mathlib/Topology/Bornology/Basic.lean
theorem isBounded_compl_iff : IsBounded sᶜ ↔ IsCobounded s

Proof state:
α : Type u_2
x✝ : Bornology α
s : Set α
⊢ IsBounded sᶜ ↔ IsCobounded s

Tactic:
rw [isBounded_def, isCobounded_def, compl_compl]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
lemma indicator_eq_one_iff_mem : indicator s 1 i = (1 : M₀) ↔ i ∈ s

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s : Set ι
i : ι
inst✝ : Nontrivial M₀
⊢ s.indicator 1 i = 1 ↔ i ∈ s

Tactic:
simp [indicator_apply, imp_false]

Result:
no goals

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s : Set ι
i : ι
inst✝ : Nontrivial M₀
⊢ s.indicator 1 i = 1 ↔ i ∈ s

Tactic:
classical simp [indicator_apply, imp_false]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem rnDeriv_restrict_self (ν : Measure α) [SigmaFinite ν] {s : Set α} (hs : MeasurableSet s) :
    (ν.restrict s).rnDeriv ν =ᵐ[ν] s.indicator 1

Proof state:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝ : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ (ν.withDensity (s.indicator 1)).rnDeriv ν =ᶠ[ae ν] s.indicator 1

Tactic:
exact rnDeriv_withDensity _ (measurable_one.indicator hs)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝ : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ (ν.restrict s).rnDeriv ν =ᶠ[ae ν] s.indicator 1

Tactic:
rw [← withDensity_indicator_one hs]

Result:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝ : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ (ν.withDensity (s.indicator 1)).rnDeriv ν =ᶠ[ae ν] s.indicator 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mapM_id {l : Array α} {f : α → Id β} : l.mapM f = l.map f

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Id β
toList✝ : List α
⊢ mapM f { toList := toList✝ } = map f { toList := toList✝ }

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → Id β
⊢ mapM f l = map f l

Tactic:
induction l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Id β
toList✝ : List α
⊢ mapM f { toList := toList✝ } = map f { toList := toList✝ }
-- Mathlib/Probability/Process/Stopping.lean
theorem IsStoppingTime.measurableSet_ge (hτ : IsStoppingTime f τ) (i : ι) :
    MeasurableSet[f i] {ω | i ≤ τ ω}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ
⊢ MeasurableSet {ω | i ≤ τ ω}

Tactic:
rw [this]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ
⊢ MeasurableSet {ω | τ ω < i}ᶜ

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | i ≤ τ ω} ↔ ω ∈ {ω | τ ω < i}ᶜ

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_lt]

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ
⊢ MeasurableSet {ω | τ ω < i}ᶜ

Tactic:
exact (hτ.measurableSet_lt i).compl

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet {ω | i ≤ τ ω}

Tactic:
have : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ := by
  ext1 ω; simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_lt]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ
⊢ MeasurableSet {ω | i ≤ τ ω}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | i ≤ τ ω} ↔ ω ∈ {ω | τ ω < i}ᶜ
-- Mathlib/CategoryTheory/Grothendieck.lean
theorem id_fiber (X : Grothendieck F) :
    Hom.fiber (𝟙 X) = eqToHom (by simp) :=
  rfl

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (𝟙 X).base).obj X.fiber = X.fiber

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToSimpleFunc_zero {m : MeasurableSpace α} (f : α →ₛ F) :
    setToSimpleFunc (0 : Set α → F →L[ℝ] F') f = 0

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
f : α →ₛ F
⊢ setToSimpleFunc 0 f = 0

Tactic:
simp [setToSimpleFunc]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma differentiable_hurwitzZetaEven_sub_hurwitzZetaEven (a b : UnitAddCircle) :
    Differentiable ℂ (fun s ↦ hurwitzZetaEven a s - hurwitzZetaEven b s)

Proof state:
a b : UnitAddCircle
z : ℂ
⊢ DifferentiableAt ℂ (fun s => hurwitzZetaEven a s - hurwitzZetaEven b s) z

Tactic:
rcases ne_or_eq z 1 with hz | rfl

Result:
case inl
a b : UnitAddCircle
z : ℂ
hz : z ≠ 1
⊢ DifferentiableAt ℂ (fun s => hurwitzZetaEven a s - hurwitzZetaEven b s) z

case inr
a b : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s => hurwitzZetaEven a s - hurwitzZetaEven b s) 1

Proof state:
case h.e'_11.h
a b : UnitAddCircle
x✝ : ℂ
⊢ hurwitzZetaEven a x✝ - hurwitzZetaEven b x✝ =
    hurwitzZetaEven a x✝ - 1 / (x✝ - 1) / x✝.Gammaℝ - (hurwitzZetaEven b x✝ - 1 / (x✝ - 1) / x✝.Gammaℝ)

Tactic:
abel

Result:
no goals

Proof state:
a b : UnitAddCircle
⊢ Differentiable ℂ fun s => hurwitzZetaEven a s - hurwitzZetaEven b s

Tactic:
intro z

Result:
a b : UnitAddCircle
z : ℂ
⊢ DifferentiableAt ℂ (fun s => hurwitzZetaEven a s - hurwitzZetaEven b s) z

Proof state:
case inr
a b : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s => hurwitzZetaEven a s - hurwitzZetaEven b s) 1

Tactic:
convert (differentiableAt_hurwitzZetaEven_sub_one_div a).sub
  (differentiableAt_hurwitzZetaEven_sub_one_div b) using 2 with s

Result:
case h.e'_11.h
a b : UnitAddCircle
x✝ : ℂ
⊢ hurwitzZetaEven a x✝ - hurwitzZetaEven b x✝ =
    hurwitzZetaEven a x✝ - 1 / (x✝ - 1) / x✝.Gammaℝ - (hurwitzZetaEven b x✝ - 1 / (x✝ - 1) / x✝.Gammaℝ)

Proof state:
case inl
a b : UnitAddCircle
z : ℂ
hz : z ≠ 1
⊢ DifferentiableAt ℂ (fun s => hurwitzZetaEven a s - hurwitzZetaEven b s) z

Tactic:
exact (differentiableAt_hurwitzZetaEven a hz).sub (differentiableAt_hurwitzZetaEven b hz)

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
/-- `zetaMul χ` takes nonnegative real values when `χ` is a quadratic character. -/
lemma zetaMul_nonneg {χ : DirichletCharacter ℂ N} (hχ : χ ^ 2 = 1) (n : ℕ) :
    0 ≤ zetaMul χ n

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
n : ℕ
⊢ 0 ≤ χ.zetaMul n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case inl
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
⊢ 0 ≤ χ.zetaMul 0

case inr
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
n : ℕ
hn : n ≠ 0
⊢ 0 ≤ χ.zetaMul n

Proof state:
case inl
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
⊢ 0 ≤ χ.zetaMul 0

Tactic:
simp only [ArithmeticFunction.map_zero, le_refl]

Result:
no goals

Proof state:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
n : ℕ
hn : n ≠ 0
⊢ 0 ≤ χ.zetaMul n

Tactic:
simpa only [χ.isMultiplicative_zetaMul.multiplicative_factorization _ hn] using
  Finset.prod_nonneg
    fun p hp ↦ zetaMul_prime_pow_nonneg hχ (Nat.prime_of_mem_primeFactors hp) _

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
lemma fromRows_inj : Function.Injective2 (@fromRows R m₁ m₂ n)

Proof state:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
x1 x2 : Matrix m₁ n R
y1 y2 : Matrix m₂ n R
⊢ x1.fromRows y1 = x2.fromRows y2 → x1 = x2 ∧ y1 = y2

Tactic:
simp [← Matrix.ext_iff]

Result:
no goals

Proof state:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
⊢ Function.Injective2 fromRows

Tactic:
intros x1 x2 y1 y2

Result:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
x1 x2 : Matrix m₁ n R
y1 y2 : Matrix m₂ n R
⊢ x1.fromRows y1 = x2.fromRows y2 → x1 = x2 ∧ y1 = y2
-- Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean
lemma σ₀_mk₀_eq (x : C) : (nerve C).σ (0 : Fin 1) (.mk₀ x) = .mk₁ (𝟙 x) :=
  ComposableArrows.ext₁ rfl rfl (by simp; rfl)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
x : C
⊢ ComposableArrows.hom (SimplicialObject.σ (nerve C) 0 (ComposableArrows.mk₀ x)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ (𝟙 x)).hom ≫ eqToHom ⋯

Tactic:
simp

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
x : C
⊢ ComposableArrows.hom (SimplicialObject.σ (nerve C) 0 (ComposableArrows.mk₀ x)) =
    𝟙 (ComposableArrows.left (SimplicialObject.σ (nerve C) 0 (ComposableArrows.mk₀ x)))

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
x : C
⊢ ComposableArrows.hom (SimplicialObject.σ (nerve C) 0 (ComposableArrows.mk₀ x)) =
    𝟙 (ComposableArrows.left (SimplicialObject.σ (nerve C) 0 (ComposableArrows.mk₀ x)))

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
lemma homMk'_mk_id (f : S ⟶ T.obj Y) : homMk' (mk f) (𝟙 Y) = eqToHom (by simp) :=
  homMk'_id _

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : S ⟶ T.obj Y
⊢ mk f = mk ((mk f).hom ≫ T.map (𝟙 Y))

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem jacobiSymNat.even_even (a b : ℕ) (hb₀ : Nat.beq (b / 2) 0 = false) (ha : a % 2 = 0)
    (hb₁ : b % 2 = 0) : jacobiSymNat a b = 0

Proof state:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : (↑a).gcd ↑b = 1
h : 2 ∣ a.gcd b
⊢ False

Tactic:
change 2 ∣ (a : ℤ).gcd b at h

Result:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : (↑a).gcd ↑b = 1
h : 2 ∣ (↑a).gcd ↑b
⊢ False

Proof state:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : (↑a).gcd ↑b = 1
⊢ False

Tactic:
have h : 2 ∣ a.gcd b := Nat.dvd_gcd (Nat.dvd_of_mod_eq_zero ha) (Nat.dvd_of_mod_eq_zero hb₁)

Result:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : (↑a).gcd ↑b = 1
h : 2 ∣ a.gcd b
⊢ False

Proof state:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : (↑a).gcd ↑b = 1
h : Even 1
⊢ False

Tactic:
exact Nat.not_even_one h

Result:
no goals

Proof state:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : (↑a).gcd ↑b = 1
h : 2 ∣ (↑a).gcd ↑b
⊢ False

Tactic:
rw [hf, ← even_iff_two_dvd] at h

Result:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : (↑a).gcd ↑b = 1
h : Even 1
⊢ False

Proof state:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
⊢ jacobiSymNat a b = 0

Tactic:
refine jacobiSym.eq_zero_iff.mpr
  ⟨ne_of_gt ((Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb₀)).trans_le (Nat.div_le_self b 2)),
    fun hf => ?_⟩

Result:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : (↑a).gcd ↑b = 1
⊢ False
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_const_sub_Ioc : (fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)

Tactic:
have := image_comp (fun x => a + x) fun x => -x

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)

Tactic:
simp [sub_eq_add_neg, this, add_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)

Tactic:
dsimp [Function.comp_def] at this

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)
-- Mathlib/Data/Set/Card.lean
theorem ncard_pos (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
⊢ 0 < s.ncard ↔ s.Nonempty

Tactic:
rw [pos_iff_ne_zero, Ne, ncard_eq_zero hs, nonempty_iff_ne_empty]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem inter_product [DecidableEq α] [DecidableEq β] : (s ∩ s') ×ˢ t = s ×ˢ t ∩ s' ×ˢ t

Proof state:
case h.mk
α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ (s ∩ s') ×ˢ t ↔ (x, y) ∈ s ×ˢ t ∩ s' ×ˢ t

Tactic:
simp only [← and_and_right, mem_inter, mem_product]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (s ∩ s') ×ˢ t = s ×ˢ t ∩ s' ×ˢ t

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ (s ∩ s') ×ˢ t ↔ (x, y) ∈ s ×ˢ t ∩ s' ×ˢ t
-- Mathlib/Probability/Kernel/Composition/CompMap.lean
theorem deterministic_comp_eq_map (hf : Measurable f) (κ : Kernel α β) :
    deterministic f hf ∘ₖ κ = map κ f

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((deterministic f hf ∘ₖ κ) a) s = ((κ.map f) a) s

Tactic:
simp_rw [map_apply' _ hf _ hs, comp_apply' _ _ _ hs, deterministic_apply' hf _ hs,
  lintegral_indicator_const_comp hf hs, one_mul]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
⊢ deterministic f hf ∘ₖ κ = κ.map f

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((deterministic f hf ∘ₖ κ) a) s = ((κ.map f) a) s
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem firstDiff_le_longestPrefix {s : Set (∀ n, E n)} (hs : IsClosed s) {x y : ∀ n, E n}
    (hx : x ∉ s) (hy : y ∈ s) : firstDiff x y ≤ longestPrefix x s

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ firstDiff x y + 1 ≤ shortestPrefixDiff x s

Tactic:
exact firstDiff_lt_shortestPrefixDiff hs hx hy

Result:
no goals

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ firstDiff x y ≤ longestPrefix x s

Tactic:
rw [longestPrefix, le_tsub_iff_right]

Result:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ firstDiff x y + 1 ≤ shortestPrefixDiff x s

E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ 1 ≤ shortestPrefixDiff x s

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ 1 ≤ shortestPrefixDiff x s

Tactic:
exact shortestPrefixDiff_pos hs ⟨y, hy⟩ hx

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommFoldr_coe (l : List α) (comm) (b : β) :
    noncommFoldr f (l : Multiset α) comm b = l.foldr f b

Proof state:
α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : {x | x ∈ ↑l}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ noncommFoldr f (↑l) comm b = List.foldr f b l

Tactic:
simp only [noncommFoldr, coe_foldr, coe_attach, List.attach, List.attachWith, Function.comp_def]

Result:
α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : {x | x ∈ ↑l}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr (fun x => f ↑x) b (List.pmap Subtype.mk l ⋯) = List.foldr f b l

Proof state:
α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : {x | x ∈ ↑l}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr f b (List.map Subtype.val (List.pmap Subtype.mk l ⋯)) = List.foldr f b l

Tactic:
simp [List.map_pmap]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : {x | x ∈ ↑l}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr (fun x => f ↑x) b (List.pmap Subtype.mk l ⋯) = List.foldr f b l

Tactic:
rw [← List.foldr_map]

Result:
α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : {x | x ∈ ↑l}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr f b (List.map Subtype.val (List.pmap Subtype.mk l ⋯)) = List.foldr f b l
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem push_rankD (arr : Array UFNode) : rankD (arr.push ⟨arr.size, 0⟩) i = rankD arr i

Proof state:
i : Nat
arr : Array UFNode
⊢ rankD (arr.push { parent := arr.size, rank := 0 }) i = rankD arr i

Tactic:
simp only [rankD, Array.size_push, Array.get_eq_getElem, Array.getElem_push, dite_eq_ite]

Result:
i : Nat
arr : Array UFNode
⊢ (if i < arr.size + 1 then (if h : i < arr.size then arr[i] else { parent := arr.size, rank := 0 }).rank else 0) =
    if h : i < arr.size then arr[i].rank else 0

Proof state:
i : Nat
arr : Array UFNode
⊢ (if i < arr.size + 1 then (if h : i < arr.size then arr[i] else { parent := arr.size, rank := 0 }).rank else 0) =
    if h : i < arr.size then arr[i].rank else 0

Tactic:
split <;> split <;> first | simp | cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)

Result:
no goals

Proof state:
case isFalse.isFalse
i : Nat
arr : Array UFNode
h✝¹ : ¬i < arr.size + 1
h✝ : ¬i < arr.size
⊢ 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case isFalse.isTrue
i : Nat
arr : Array UFNode
h✝¹ : ¬i < arr.size + 1
h✝ : i < arr.size
⊢ 0 = arr[i].rank

Tactic:
cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)

Result:
no goals