harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem Ioc_filter_dvd_card_eq_div (n p : ℕ) : #{x ∈ Ioc 0 n | p ∣ x} = n / p

Proof state:
case inl
p : ℕ
IH : #(Finset.filter (fun x => p ∣ x) (Ioc 0 0)) = 0 / p
⊢ Ioc 0 (succ 0) = insert (succ 0) (Ioc 0 0)

Tactic:
simp

Result:
no goals

Proof state:
case zero
p : ℕ
⊢ #(Finset.filter (fun x => p ∣ x) (Ioc 0 0)) = 0 / p

Tactic:
simp

Result:
no goals

Proof state:
case succ
p n : ℕ
IH : #(Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
h1 : Ioc 0 n.succ = insert n.succ (Ioc 0 n)
⊢ #(Finset.filter (fun x => p ∣ x) (Ioc 0 (n + 1))) = (n + 1) / p

Tactic:
simp [Nat.succ_div, add_ite, add_zero, h1, filter_insert, apply_ite card, card_insert_eq_ite, IH,
  Finset.mem_filter, mem_Ioc, not_le.2 (lt_add_one n)]

Result:
no goals

Proof state:
n p : ℕ
⊢ #(Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p

Tactic:
induction' n with n IH

Result:
case zero
p : ℕ
⊢ #(Finset.filter (fun x => p ∣ x) (Ioc 0 0)) = 0 / p

case succ
p n : ℕ
IH : #(Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
⊢ #(Finset.filter (fun x => p ∣ x) (Ioc 0 (n + 1))) = (n + 1) / p

Proof state:
case inr
p n : ℕ
IH : #(Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
hn : n > 0
⊢ Ioc 0 n.succ = insert n.succ (Ioc 0 n)

Tactic:
simp_rw [← Ico_succ_succ, Ico_insert_right (succ_le_succ hn.le), Ico_succ_right]

Result:
no goals

Proof state:
p n : ℕ
IH : #(Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
⊢ Ioc 0 n.succ = insert n.succ (Ioc 0 n)

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Result:
case inl
p : ℕ
IH : #(Finset.filter (fun x => p ∣ x) (Ioc 0 0)) = 0 / p
⊢ Ioc 0 (succ 0) = insert (succ 0) (Ioc 0 0)

case inr
p n : ℕ
IH : #(Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
hn : n > 0
⊢ Ioc 0 n.succ = insert n.succ (Ioc 0 n)
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem basisSets_add (U) (hU : U ∈ p.basisSets) :
    ∃ V ∈ p.basisSets, V + V ⊆ U

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ p.basisSets, V + V ⊆ U

Tactic:
use (s.sup p).ball 0 (r / 2)

Result:
case h
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (s.sup p).ball 0 (r / 2) ∈ p.basisSets ∧ (s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U

Proof state:
case h
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (s.sup p).ball 0 (r / 2) ∈ p.basisSets ∧ (s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U

Tactic:
refine ⟨p.basisSets_mem s (div_pos hr zero_lt_two), ?_⟩

Result:
case h
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU : U ∈ p.basisSets
⊢ ∃ V ∈ p.basisSets, V + V ⊆ U

Tactic:
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ p.basisSets, V + V ⊆ U

Proof state:
case h
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (s.sup p).ball (0 + 0) (r / 2 + r / 2) ⊆ U

Tactic:
rw [hU, add_zero, add_halves]

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U

Tactic:
refine Set.Subset.trans (ball_add_ball_subset (s.sup p) (r / 2) (r / 2) 0 0) ?_

Result:
case h
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (s.sup p).ball (0 + 0) (r / 2 + r / 2) ⊆ U
-- Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean
theorem unitization_range : (unitization s).range = Algebra.adjoin R (s : Set A)

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
s : S
⊢ Algebra.adjoin R ↑(NonUnitalAlgHom.range (NonUnitalSubalgebraClass.subtype s)) = Algebra.adjoin R ↑s

Tactic:
simp only [NonUnitalAlgHom.coe_range, NonUnitalSubalgebraClass.coe_subtype,
  Subtype.range_coe_subtype, SetLike.mem_coe]

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
s : S
⊢ Algebra.adjoin R {x | x ∈ s} = Algebra.adjoin R ↑s

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
s : S
⊢ (unitization s).range = Algebra.adjoin R ↑s

Tactic:
rw [unitization, Unitization.lift_range]

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
s : S
⊢ Algebra.adjoin R ↑(NonUnitalAlgHom.range (NonUnitalSubalgebraClass.subtype s)) = Algebra.adjoin R ↑s

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
s : S
⊢ Algebra.adjoin R {x | x ∈ s} = Algebra.adjoin R ↑s

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
lemma trans_dualMap_symm_flip : e.trans e.flip.symm.dualMap = Dual.eval R N

Proof state:
case h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
x✝¹ : N
x✝ : Dual R N
⊢ (↑(e ≪≫ₗ e.flip.symm.dualMap) x✝¹) x✝ = ((Dual.eval R N) x✝¹) x✝

Tactic:
simp [symm_flip]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ ↑(e ≪≫ₗ e.flip.symm.dualMap) = Dual.eval R N

Tactic:
ext

Result:
case h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
x✝¹ : N
x✝ : Dual R N
⊢ (↑(e ≪≫ₗ e.flip.symm.dualMap) x✝¹) x✝ = ((Dual.eval R N) x✝¹) x✝
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem hasFTaylorSeriesUpToOn_top_iff (hN : ∞ ≤ N) :
    HasFTaylorSeriesUpToOn N f p s ↔ ∀ n : ℕ, HasFTaylorSeriesUpToOn n f p s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
⊢ HasFTaylorSeriesUpToOn N f p s ↔ ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑n) f p s

Tactic:
simpa using hasFTaylorSeriesUpToOn_top_iff_add hN 0

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWith_eq_empty_iff {f : α → β → γ} {l l'} : zipWith f l l' = #[] ↔ l = #[] ∨ l' = #[]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : Array α
l' : Array β
⊢ zipWith f l l' = #[] ↔ l = #[] ∨ l' = #[]

Tactic:
cases l <;> cases l' <;> simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem lift_index_left {f : PadicSeq p} (hf : ¬f ≈ 0) (v1 v3 : ℕ) :
    padicNorm p (f (stationaryPoint hf)) =
    padicNorm p (f (max v1 (max (stationaryPoint hf) v3)))

Proof state:
case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ stationaryPoint hf ≤ ?a.b✝

Tactic:
apply le_max_left _ v3

Result:
no goals

Proof state:
case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ stationaryPoint hf ⊔ v3 ≤ v1 ⊔ (stationaryPoint hf ⊔ v3)

Tactic:
apply le_max_right

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (v1 ⊔ (stationaryPoint hf ⊔ v3)))

Tactic:
apply stationaryPoint_spec hf

Result:
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ stationaryPoint hf ≤ v1 ⊔ (stationaryPoint hf ⊔ v3)

case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Proof state:
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ stationaryPoint hf ≤ v1 ⊔ (stationaryPoint hf ⊔ v3)

Tactic:
apply le_trans

Result:
case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ stationaryPoint hf ≤ ?a.b✝

case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ ?a.b✝ ≤ v1 ⊔ (stationaryPoint hf ⊔ v3)

case a.b
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ ℕ

Proof state:
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
exact le_rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IsConnected.lean
theorem isConnected_iff_isColimit_pUnitCocone :
    IsConnected C ↔ Nonempty (IsColimit (pUnitCocone.{w} C))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
x✝ : Nonempty (IsColimit (pUnitCocone C))
h : IsColimit (pUnitCocone C)
⊢ IsConnected C

Tactic:
let colimitCocone : ColimitCocone (constPUnitFunctor C) := ⟨pUnitCocone.{w} C, h⟩

Result:
C : Type u
inst✝ : Category.{v, u} C
x✝ : Nonempty (IsColimit (pUnitCocone C))
h : IsColimit (pUnitCocone C)
colimitCocone : ColimitCocone (constPUnitFunctor C) := { cocone := pUnitCocone C, isColimit := h }
⊢ IsConnected C

Proof state:
C : Type u
inst✝ : Category.{v, u} C
x✝ : Nonempty (IsColimit (pUnitCocone C))
h : IsColimit (pUnitCocone C)
colimitCocone : ColimitCocone (constPUnitFunctor C) := { cocone := pUnitCocone C, isColimit := h }
⊢ IsConnected C

Tactic:
have : HasColimit (constPUnitFunctor.{w} C) := ⟨⟨colimitCocone⟩⟩

Result:
C : Type u
inst✝ : Category.{v, u} C
x✝ : Nonempty (IsColimit (pUnitCocone C))
h : IsColimit (pUnitCocone C)
colimitCocone : ColimitCocone (constPUnitFunctor C) := { cocone := pUnitCocone C, isColimit := h }
this : HasColimit (constPUnitFunctor C)
⊢ IsConnected C

Proof state:
C : Type u
inst✝ : Category.{v, u} C
x✝ : Nonempty (IsColimit (pUnitCocone C))
h : IsColimit (pUnitCocone C)
colimitCocone : ColimitCocone (constPUnitFunctor C) := { cocone := pUnitCocone C, isColimit := h }
this : HasColimit (constPUnitFunctor C)
⊢ IsConnected C

Tactic:
simp only [isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{w} C]

Result:
C : Type u
inst✝ : Category.{v, u} C
x✝ : Nonempty (IsColimit (pUnitCocone C))
h : IsColimit (pUnitCocone C)
colimitCocone : ColimitCocone (constPUnitFunctor C) := { cocone := pUnitCocone C, isColimit := h }
this : HasColimit (constPUnitFunctor C)
⊢ Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})

Proof state:
C : Type u
inst✝ : Category.{v, u} C
x✝ : Nonempty (IsColimit (pUnitCocone C))
h : IsColimit (pUnitCocone C)
colimitCocone : ColimitCocone (constPUnitFunctor C) := { cocone := pUnitCocone C, isColimit := h }
this : HasColimit (constPUnitFunctor C)
⊢ Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})

Tactic:
exact ⟨colimit.isoColimitCocone colimitCocone⟩

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
⊢ IsConnected C ↔ Nonempty (IsColimit (pUnitCocone C))

Tactic:
refine ⟨fun inst => ⟨isColimitPUnitCocone C⟩, fun ⟨h⟩ => ?_⟩

Result:
C : Type u
inst✝ : Category.{v, u} C
x✝ : Nonempty (IsColimit (pUnitCocone C))
h : IsColimit (pUnitCocone C)
⊢ IsConnected C
-- Mathlib/Topology/ContinuousMap/Compact.lean
theorem summable_of_locally_summable_norm {ι : Type*} {F : ι → C(X, E)}
    (hF : ∀ K : Compacts X, Summable fun i => ‖(F i).restrict K‖) : Summable F

Proof state:
case intro
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
⊢ ∃ f, Filter.Tendsto (fun i => restrict (↑K) (∑ b ∈ i, F b)) Filter.atTop (nhds f)

Tactic:
have A : ∀ s : Finset ι, restrict (↑K) (∑ i ∈ s, F i) = ∑ i ∈ s, restrict K (F i) := by
  intro s
  ext1 x
  simp
  erw [restrict_apply, restrict_apply, restrict_apply, restrict_apply]
  simp? says simp only [coe_sum, Finset.sum_apply]
  congr!

Result:
case intro
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
A : ∀ (s : Finset ι), restrict (↑K) (∑ i ∈ s, F i) = ∑ i ∈ s, restrict (↑K) (F i)
⊢ ∃ f, Filter.Tendsto (fun i => restrict (↑K) (∑ b ∈ i, F b)) Filter.atTop (nhds f)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/DecidableEq.lean
theorem beq_eq_decide [BEq α] (a b : Array α) :
    (a == b) = if h : a.size = b.size then
      decide (∀ (i : Nat) (h' : i < a.size), a[i] == b[i]'(h ▸ h')) else false

Proof state:
α : Type u_1
inst✝ : BEq α
a b : Array α
⊢ (a == b) = if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), (a[i] == b[i]) = true) else false

Tactic:
simp [BEq.beq, isEqv_eq_decide]

Result:
no goals
-- Mathlib/Data/List/Sym.lean
theorem mem_sym2_cons_iff {x : α} {xs : List α} {z : Sym2 α} :
    z ∈ (x :: xs).sym2 ↔ z = s(x, x) ∨ (∃ y, y ∈ xs ∧ z = s(x, y)) ∨ z ∈ xs.sym2

Proof state:
α : Type u_1
x : α
xs : List α
z : Sym2 α
⊢ z = s(x, x) ∨ (∃ a ∈ xs, s(x, a) = z) ∨ z ∈ xs.sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2

Tactic:
simp only [eq_comm]

Result:
no goals

Proof state:
α : Type u_1
x : α
xs : List α
z : Sym2 α
⊢ z ∈ (x :: xs).sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2

Tactic:
simp only [List.sym2, map_cons, cons_append, mem_cons, mem_append, mem_map]

Result:
α : Type u_1
x : α
xs : List α
z : Sym2 α
⊢ z = s(x, x) ∨ (∃ a ∈ xs, s(x, a) = z) ∨ z ∈ xs.sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2
-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
theorem ContDiffAt.isSymmSndFDerivAt_of_omega (hf : ContDiffAt 𝕜 ω f x) :
    IsSymmSndFDerivAt 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 ω f univ x
⊢ IsSymmSndFDerivWithinAt 𝕜 f univ x

Tactic:
exact hf.isSymmSndFDerivWithinAt_of_omega uniqueDiffOn_univ (mem_univ _)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
hf : ContDiffAt 𝕜 ω f x
⊢ IsSymmSndFDerivAt 𝕜 f x

Tactic:
simp only [← isSymmSndFDerivWithinAt_univ, ← contDiffWithinAt_univ] at hf ⊢

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 ω f univ x
⊢ IsSymmSndFDerivWithinAt 𝕜 f univ x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem allM_toList [Monad m] [LawfulMonad m] (p : α → m Bool) (v : Vector α n) :
    v.toList.allM p = v.allM p

Proof state:
case mk
m : Type → Type u_1
α : Type u_2
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.allM p { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    allM p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
m : Type → Type u_1
α : Type u_2
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
v : Vector α n
⊢ List.allM p v.toList = allM p v

Tactic:
cases v

Result:
case mk
m : Type → Type u_1
α : Type u_2
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.allM p { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    allM p { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Algebra/RingQuot.lean
theorem neg_quot {R : Type uR} [Ring R] (r : R → R → Prop) {a} :
    (-⟨Quot.mk _ a⟩ : RingQuot r) = ⟨Quot.mk _ (-a)⟩

Proof state:
R : Type uR
inst✝ : Ring R
r : R → R → Prop
a : R
⊢ -{ toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (-a) }

Tactic:
show neg r _ = _

Result:
R : Type uR
inst✝ : Ring R
r : R → R → Prop
a : R
⊢ RingQuot.neg r { toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (-a) }

Proof state:
R : Type uR
inst✝ : Ring R
r : R → R → Prop
a : R
⊢ RingQuot.neg r { toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (-a) }

Tactic:
rw [neg_def]

Result:
R : Type uR
inst✝ : Ring R
r : R → R → Prop
a : R
⊢ (match { toQuot := Quot.mk (Rel r) a } with
    | { toQuot := a } => { toQuot := Quot.map (fun a => -a) ⋯ a }) =
    { toQuot := Quot.mk (Rel r) (-a) }

Proof state:
R : Type uR
inst✝ : Ring R
r : R → R → Prop
a : R
⊢ (match { toQuot := Quot.mk (Rel r) a } with
    | { toQuot := a } => { toQuot := Quot.map (fun a => -a) ⋯ a }) =
    { toQuot := Quot.mk (Rel r) (-a) }

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
lemma epi_of_epi_f {K L : HomologicalComplex V c} (φ : K ⟶ L)
    (hφ : ∀ i, Epi (φ.f i)) : Epi φ where
  left_cancellation g h eq

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z✝ : HomologicalComplex V c
g h : L ⟶ Z✝
eq : φ ≫ g = φ ≫ h
⊢ g = h

Tactic:
ext i

Result:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z✝ : HomologicalComplex V c
g h : L ⟶ Z✝
eq : φ ≫ g = φ ≫ h
i : ι
⊢ g.f i = h.f i

Proof state:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z✝ : HomologicalComplex V c
g h : L ⟶ Z✝
eq : φ ≫ g = φ ≫ h
i : ι
⊢ φ.f i ≫ g.f i = φ.f i ≫ h.f i

Tactic:
exact congr_hom eq i

Result:
no goals

Proof state:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z✝ : HomologicalComplex V c
g h : L ⟶ Z✝
eq : φ ≫ g = φ ≫ h
i : ι
⊢ g.f i = h.f i

Tactic:
rw [← cancel_epi (φ.f i)]

Result:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z✝ : HomologicalComplex V c
g h : L ⟶ Z✝
eq : φ ≫ g = φ ≫ h
i : ι
⊢ φ.f i ≫ g.f i = φ.f i ≫ h.f i
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_insertMany_empty_list_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (insertMany empty l).1.getD k' fallback =
      cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ (empty.insertMany l).val.getD k' fallback = cast ⋯ v

Tactic:
rw [getD_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals

Proof state:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
lemma CompleteSpace.fst_of_prod [UniformSpace β] [CompleteSpace (α × β)] [h : Nonempty β] :
    CompleteSpace α where
  complete hf :=
    let ⟨y⟩ := h
    let ⟨(a, b), hab⟩ := CompleteSpace.complete <| hf.prod <| cauchy_pure (a := y)
    ⟨a, by simpa only [map_fst_prod, nhds_prod_eq] using map_mono (m := Prod.fst) hab⟩

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace (α × β)
h : Nonempty β
f✝ : Filter α
hf : Cauchy f✝
y : β
a : α
b : β
hab : f✝ ×ˢ pure y ≤ 𝓝 (a, b)
⊢ f✝ ≤ 𝓝 a

Tactic:
simpa only [map_fst_prod, nhds_prod_eq] using map_mono (m := Prod.fst) hab

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem ne_zero_iff_exists_coeff_ne_zero_and_weight :
    f ≠ 0 ↔ (∃ n : ℕ, ∃ d : σ →₀ ℕ, coeff R d f ≠ 0 ∧ weight w d = n)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ ¬f ≠ 0 ↔ ¬∃ n d, (coeff R d) f ≠ 0 ∧ (weight w) d = n

Tactic:
simp only [ne_eq, not_not, not_exists, not_and, forall_apply_eq_imp_iff₂, imp_false]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ f = 0 ↔ ∀ (a : σ →₀ ℕ), (coeff R a) f = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ ∃ n d, (coeff R d) f ≠ 0 ∧ (weight w) d = n

Tactic:
refine not_iff_not.mp ?_

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ ¬f ≠ 0 ↔ ¬∃ n d, (coeff R d) f ≠ 0 ∧ (weight w) d = n

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ f = 0 ↔ ∀ (a : σ →₀ ℕ), (coeff R a) f = 0

Tactic:
exact MvPowerSeries.ext_iff

Result:
no goals