harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/AdicCompletion/LocalRing.lean
theorem isLocalRing_of_isAdicComplete_maximal [IsAdicComplete m R] : IsLocalRing R where
  exists_pair_ne := ⟨0, 1, ne_of_mem_of_not_mem m.zero_mem
    (m.ne_top_iff_one.mp (Ideal.IsMaximal.ne_top hmax))⟩
  isUnit_or_isUnit_of_add_one {a b} hab

Proof state:
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
a b : R
hab : a + b = 1
h : a ∈ m ∧ b ∈ m
⊢ False

Tactic:
absurd m.add_mem h.1 h.2

Result:
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
a b : R
hab : a + b = 1
h : a ∈ m ∧ b ∈ m
⊢ a + b ∉ m

Proof state:
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
a b : R
hab : a + b = 1
⊢ a ∉ m ∨ b ∉ m

Tactic:
by_contra! h

Result:
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
a b : R
hab : a + b = 1
h : a ∈ m ∧ b ∈ m
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
a b : R
hab : a + b = 1
⊢ IsUnit a ∨ IsUnit b

Tactic:
simp only [isUnit_iff_nmem_of_isAdicComplete_maximal m]

Result:
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
a b : R
hab : a + b = 1
⊢ a ∉ m ∨ b ∉ m

Proof state:
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
a b : R
hab : a + b = 1
h : a ∈ m ∧ b ∈ m
⊢ a + b ∉ m

Tactic:
simpa [hab] using m.ne_top_iff_one.mp (Ideal.IsMaximal.ne_top hmax)

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem not_isSuccLimit_iff : ¬ IsSuccLimit a ↔ IsMin a ∨ ¬ IsSuccPrelimit a

Proof state:
α : Type u_1
a : α
inst✝ : Preorder α
⊢ ¬IsSuccLimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a

Tactic:
rw [IsSuccLimit, not_and_or, not_not]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem exists_seq_mono_tendsto (I : Box ι) :
    ∃ J : ℕ →o Box ι,
      (∀ n, Box.Icc (J n) ⊆ Box.Ioo I) ∧
        Tendsto (lower ∘ J) atTop (𝓝 I.lower) ∧ Tendsto (upper ∘ J) atTop (𝓝 I.upper)

Proof state:
ι : Type u_1
I : Box ι
a b : ι → ℕ → ℝ
ha_anti : ∀ (i : ι), StrictAnti (a i)
hb_mono : ∀ (i : ι), StrictMono (b i)
ha_mem : ∀ (i : ι) (k : ℕ), a i k ∈ Ioo (I.lower i) (I.upper i)
hb_mem : ∀ (i : ι) (l : ℕ), b i l ∈ Ioo (I.lower i) (I.upper i)
hab : ∀ (i : ι) (k l : ℕ), a i k < b i l
ha_tendsto : ∀ (i : ι), Tendsto (a i) atTop (𝓝 (I.lower i))
hb_tendsto : ∀ (i : ι), Tendsto (b i) atTop (𝓝 (I.upper i))
⊢ ∃ J,
    (∀ (n : ℕ), Box.Icc (J n) ⊆ Box.Ioo I) ∧
      Tendsto (lower ∘ ⇑J) atTop (𝓝 I.lower) ∧ Tendsto (upper ∘ ⇑J) atTop (𝓝 I.upper)

Tactic:
exact
  ⟨⟨fun k ↦ ⟨flip a k, flip b k, fun i ↦ hab _ _ _⟩, fun k l hkl ↦
      le_iff_bounds.2 ⟨fun i ↦ (ha_anti i).antitone hkl, fun i ↦ (hb_mono i).monotone hkl⟩⟩,
    fun n x hx i _ ↦ ⟨(ha_mem _ _).1.trans_le (hx.1 _), (hx.2 _).trans_lt (hb_mem _ _).2⟩,
    tendsto_pi_nhds.2 ha_tendsto, tendsto_pi_nhds.2 hb_tendsto⟩

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
⊢ ∃ J,
    (∀ (n : ℕ), Box.Icc (J n) ⊆ Box.Ioo I) ∧
      Tendsto (lower ∘ ⇑J) atTop (𝓝 I.lower) ∧ Tendsto (upper ∘ ⇑J) atTop (𝓝 I.upper)

Tactic:
choose a b ha_anti hb_mono ha_mem hb_mem hab ha_tendsto hb_tendsto using
  fun i ↦ exists_seq_strictAnti_strictMono_tendsto (I.lower_lt_upper i)

Result:
ι : Type u_1
I : Box ι
a b : ι → ℕ → ℝ
ha_anti : ∀ (i : ι), StrictAnti (a i)
hb_mono : ∀ (i : ι), StrictMono (b i)
ha_mem : ∀ (i : ι) (k : ℕ), a i k ∈ Ioo (I.lower i) (I.upper i)
hb_mem : ∀ (i : ι) (l : ℕ), b i l ∈ Ioo (I.lower i) (I.upper i)
hab : ∀ (i : ι) (k l : ℕ), a i k < b i l
ha_tendsto : ∀ (i : ι), Tendsto (a i) atTop (𝓝 (I.lower i))
hb_tendsto : ∀ (i : ι), Tendsto (b i) atTop (𝓝 (I.upper i))
⊢ ∃ J,
    (∀ (n : ℕ), Box.Icc (J n) ⊆ Box.Ioo I) ∧
      Tendsto (lower ∘ ⇑J) atTop (𝓝 I.lower) ∧ Tendsto (upper ∘ ⇑J) atTop (𝓝 I.upper)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_attachWith (l : Array α) {p : {x // q x} → Prop} (f : ∀ a, p a → β) (H₁ H₂) :
    pmap f (l.attachWith q H₁) H₂ =
      l.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩)

Proof state:
α : Type ?u.40858
q : α → Prop
β : Type ?u.40888
l : Array α
p : { x // q x } → Prop
f : (a : { x // q x }) → p a → β
H₁ : ∀ (x : α), x ∈ l → q x
H₂ : ∀ (a : { x // q x }), a ∈ l.attachWith q H₁ → p a
a : α
h : a ∈ l
⊢ ⟨a, ⋯⟩ ∈ l.attachWith q H₁

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
q : α → Prop
β : Type u_2
l : Array α
p : { x // q x } → Prop
f : (a : { x // q x }) → p a → β
H₁ : ∀ (x : α), x ∈ l → q x
H₂ : ∀ (a : { x // q x }), a ∈ l.attachWith q H₁ → p a
⊢ pmap f (l.attachWith q H₁) H₂ = pmap (fun a h => f ⟨a, ⋯⟩ ⋯) l ⋯

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean
theorem not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_within_diff_singleton
    {f : ℝ → E} {g : ℝ → F} {a b c : ℝ} (hne : a ≠ b) (hc : c ∈ [[a, b]])
    (h_deriv : ∀ᶠ x in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x)
    (h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop)
    (hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g) : ¬IntervalIntegrable g volume a b

Proof state:
E : Type u_1
F : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
⊢ ∃ l, TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l

Tactic:
rcases (min_lt_max.2 hne).lt_or_lt c with hlt | hlt

Result:
case inl
E : Type u_1
F : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : a ⊓ b < c
⊢ ∃ l, TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l

case inr
E : Type u_1
F : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < a ⊔ b
⊢ ∃ l, TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem roots_of_cyclotomic (n : ℕ) (R : Type*) [CommRing R] [IsDomain R] :
    (cyclotomic' n R).roots = (primitiveRoots n R).val

Proof state:
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (cyclotomic' n R).roots = (primitiveRoots n R).val

Tactic:
rw [cyclotomic']

Result:
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (∏ μ ∈ primitiveRoots n R, (X - C μ)).roots = (primitiveRoots n R).val

Proof state:
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (∏ μ ∈ primitiveRoots n R, (X - C μ)).roots = (primitiveRoots n R).val

Tactic:
exact roots_prod_X_sub_C (primitiveRoots n R)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem beq_eq_decide_eq {_ : BEq α} [LawfulBEq α] [DecidableEq α] (a b : α) : (a == b) = (decide (a = b))

Proof state:
case neg
α : Type u_1
x✝ : BEq α
inst✝¹ : LawfulBEq α
inst✝ : DecidableEq α
a b : α
h✝ : ¬a = b
⊢ (a == b) = decide (a = b)

Tactic:
next h => simp [beq_eq_false_iff_ne.mpr h, decide_eq_false h]

Result:
no goals

Proof state:
α : Type u_1
x✝ : BEq α
inst✝¹ : LawfulBEq α
inst✝ : DecidableEq α
a b : α
h : a = b
⊢ (a == b) = decide (a = b)

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
x✝ : BEq α
inst✝¹ : LawfulBEq α
inst✝ : DecidableEq α
a b : α
h : ¬a = b
⊢ (a == b) = decide (a = b)

Tactic:
simp [beq_eq_false_iff_ne.mpr h, decide_eq_false h]

Result:
no goals

Proof state:
case pos
α : Type u_1
x✝ : BEq α
inst✝¹ : LawfulBEq α
inst✝ : DecidableEq α
a b : α
h✝ : a = b
⊢ (a == b) = decide (a = b)

case neg
α : Type u_1
x✝ : BEq α
inst✝¹ : LawfulBEq α
inst✝ : DecidableEq α
a b : α
h✝ : ¬a = b
⊢ (a == b) = decide (a = b)

Tactic:
next h => simp [h]

Result:
case neg
α : Type u_1
x✝ : BEq α
inst✝¹ : LawfulBEq α
inst✝ : DecidableEq α
a b : α
h✝ : ¬a = b
⊢ (a == b) = decide (a = b)

Proof state:
α : Type u_1
x✝ : BEq α
inst✝¹ : LawfulBEq α
inst✝ : DecidableEq α
a b : α
⊢ (a == b) = decide (a = b)

Tactic:
by_cases a = b

Result:
case pos
α : Type u_1
x✝ : BEq α
inst✝¹ : LawfulBEq α
inst✝ : DecidableEq α
a b : α
h✝ : a = b
⊢ (a == b) = decide (a = b)

case neg
α : Type u_1
x✝ : BEq α
inst✝¹ : LawfulBEq α
inst✝ : DecidableEq α
a b : α
h✝ : ¬a = b
⊢ (a == b) = decide (a = b)
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem map_restrict_ae_le_map_indicator_ae [Zero β] (hs : MeasurableSet s) :
    Filter.map f (ae <| μ.restrict s) ≤ Filter.map (s.indicator f) (ae μ)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
⊢ Filter.map f (ae (μ.restrict s)) ≤ Filter.map (s.indicator f) (ae μ)

Tactic:
intro t

Result:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))

Proof state:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0 → μ ((f ⁻¹' t)ᶜ ∩ s) = 0

Tactic:
exact fun h => measure_mono_null (Set.inter_subset_left.trans Set.subset_union_left) h

Result:
no goals

Proof state:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
⊢ t ∈ Filter.map f (ae (μ.restrict s)) → t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
exact id

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
by_cases ht : (0 : β) ∈ t

Result:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))

case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))

Proof state:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
rw [mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem ht hs]

Result:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
⊢ t ∈ Filter.map f (ae (μ.restrict s)) → t ∈ Filter.map f (ae (μ.restrict s))

Proof state:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
rw [mem_map_indicator_ae_iff_of_zero_nmem ht, mem_map_restrict_ae_iff hs]

Result:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0 → μ ((f ⁻¹' t)ᶜ ∩ s) = 0
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem rnDeriv_smul (s : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ] (r : ℝ) :
    (r • s).rnDeriv μ =ᵐ[μ] r • s.rnDeriv μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ
⊢ (r • s).rnDeriv μ =ᶠ[ae μ] r • s.rnDeriv μ

Tactic:
refine
  Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _)
    ((integrable_rnDeriv _ _).smul r) ?_

Result:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ
⊢ μ.withDensityᵥ ((r • s).rnDeriv μ) = μ.withDensityᵥ (r • s.rnDeriv μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ
⊢ μ.withDensityᵥ ((r • s).rnDeriv μ) = μ.withDensityᵥ (r • s.rnDeriv μ)

Tactic:
rw [withDensityᵥ_smul (rnDeriv s μ) r, ← add_right_inj ((r • s).singularPart μ),
  singularPart_add_withDensity_rnDeriv_eq, singularPart_smul, ← smul_add,
  singularPart_add_withDensity_rnDeriv_eq]

Result:
no goals
-- Mathlib/Logic/Equiv/Set.lean
theorem preimage_piEquivPiSubtypeProd_symm_pi {α : Type*} {β : α → Type*} (p : α → Prop)
    [DecidablePred p] (s : ∀ i, Set (β i)) :
    (piEquivPiSubtypeProd p β).symm ⁻¹' pi univ s =
      (pi univ fun i : { i // p i } => s i) ×ˢ pi univ fun i : { i // ¬p i } => s i

Proof state:
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
⊢ ⇑(piEquivPiSubtypeProd p β).symm ⁻¹' univ.pi s = (univ.pi fun i => s ↑i) ×ˢ univ.pi fun i => s ↑i

Tactic:
ext ⟨f, g⟩

Result:
case h.mk
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ (f, g) ∈ ⇑(piEquivPiSubtypeProd p β).symm ⁻¹' univ.pi s ↔ (f, g) ∈ (univ.pi fun i => s ↑i) ×ˢ univ.pi fun i => s ↑i

Proof state:
case h.mk
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ (f, g) ∈ ⇑(piEquivPiSubtypeProd p β).symm ⁻¹' univ.pi s ↔ (f, g) ∈ (univ.pi fun i => s ↑i) ×ˢ univ.pi fun i => s ↑i

Tactic:
simp only [mem_preimage, mem_univ_pi, prod_mk_mem_set_prod_eq, Subtype.forall, ← forall_and]

Result:
case h.mk
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ (∀ (i : α), (piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i) ↔
    ∀ (x : α), (∀ (b : p x), f ⟨x, b⟩ ∈ s x) ∧ ∀ (b : ¬p x), g ⟨x, b⟩ ∈ s x

Proof state:
case h.mk
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ (∀ (i : α), (piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i) ↔
    ∀ (x : α), (∀ (b : p x), f ⟨x, b⟩ ∈ s x) ∧ ∀ (b : ¬p x), g ⟨x, b⟩ ∈ s x

Tactic:
refine forall_congr' fun i => ?_

Result:
case h.mk
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
⊢ (piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔ (∀ (b : p i), f ⟨i, b⟩ ∈ s i) ∧ ∀ (b : ¬p i), g ⟨i, b⟩ ∈ s i

Proof state:
case h.mk
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
⊢ (piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔ (∀ (b : p i), f ⟨i, b⟩ ∈ s i) ∧ ∀ (b : ¬p i), g ⟨i, b⟩ ∈ s i

Tactic:
by_cases hi : p i <;> simp [hi]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ioo_sub_one_left_eq_Ioc_of_not_isMin (ha : ¬ IsMin a) (b : α) : Ioo (a - 1) b = Ico a b

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioo (a - 1) b = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Ioo_pred_left_eq_Ioc_of_not_isMin ha b

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
protected lemma zpow [StarOrderedRing R] [DecidableEq n]
    {M : Matrix n n R} (hM : M.PosSemidef) (z : ℤ) :
    (M ^ z).PosSemidef

Proof state:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
z : ℤ
⊢ (M ^ z).PosSemidef

Tactic:
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg

Result:
case intro.inl
n✝ : Type u_2
R : Type u_3
inst✝⁵ : Fintype n✝
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n✝
M : Matrix n✝ n✝ R
hM : M.PosSemidef
n : ℕ
⊢ (M ^ ↑n).PosSemidef

case intro.inr
n✝ : Type u_2
R : Type u_3
inst✝⁵ : Fintype n✝
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n✝
M : Matrix n✝ n✝ R
hM : M.PosSemidef
n : ℕ
⊢ (M ^ (-↑n)).PosSemidef

Proof state:
case intro.inl
n✝ : Type u_2
R : Type u_3
inst✝⁵ : Fintype n✝
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n✝
M : Matrix n✝ n✝ R
hM : M.PosSemidef
n : ℕ
⊢ (M ^ ↑n).PosSemidef

Tactic:
simpa using hM.pow n

Result:
no goals

Proof state:
case intro.inr
n✝ : Type u_2
R : Type u_3
inst✝⁵ : Fintype n✝
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n✝
M : Matrix n✝ n✝ R
hM : M.PosSemidef
n : ℕ
⊢ (M ^ (-↑n)).PosSemidef

Tactic:
simpa using (hM.pow n).inv

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
theorem rel_iSup_tprod [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (R : M → M → Prop)
    (m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∏' i, m (s i))) (s : β → α) :
    R (m (⨆ b : β, s b)) (∏' b : β, m (s b))

Proof state:
case intro
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Countable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : β → α
val✝ : Encodable β
⊢ R (m (⨆ i, ⨆ b ∈ decode₂ β i, s b)) (∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b))

Tactic:
exact m_iSup _

Result:
no goals

Proof state:
case intro
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Countable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : β → α
val✝ : Encodable β
⊢ R (m (⨆ b, s b)) (∏' (b : β), m (s b))

Tactic:
rw [← iSup_decode₂, ← tprod_iSup_decode₂ _ m0 s]

Result:
case intro
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Countable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : β → α
val✝ : Encodable β
⊢ R (m (⨆ i, ⨆ b ∈ decode₂ β i, s b)) (∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b))

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Countable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : β → α
⊢ R (m (⨆ b, s b)) (∏' (b : β), m (s b))

Tactic:
cases nonempty_encodable β

Result:
case intro
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Countable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : β → α
val✝ : Encodable β
⊢ R (m (⨆ b, s b)) (∏' (b : β), m (s b))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem sign_neg (z : Int) : Int.sign (-z) = -Int.sign z

Proof state:
z : Int
⊢ (-z).sign = -z.sign

Tactic:
match z with | 0 | succ _ | -[_+1] => rfl

Result:
no goals

Proof state:
z : Int
a✝ : Nat
⊢ (- -[a✝+1]).sign = - -[a✝+1].sign

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma jacobiTheta₂_fderiv_undef (z : ℂ) {τ : ℂ} (hτ : im τ ≤ 0) : jacobiTheta₂_fderiv z τ = 0

Proof state:
case h
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬0 < τ.im

Tactic:
exact not_lt.mpr hτ

Result:
no goals

Proof state:
case h
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬Summable fun b => jacobiTheta₂_term_fderiv b z τ

Tactic:
rw [summable_jacobiTheta₂_term_fderiv_iff]

Result:
case h
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬0 < τ.im

Proof state:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂_fderiv z τ = 0

Tactic:
apply tsum_eq_zero_of_not_summable

Result:
case h
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬Summable fun b => jacobiTheta₂_term_fderiv b z τ
-- Mathlib/Topology/Algebra/WithZeroTopology.lean
theorem isOpen_iff {s : Set Γ₀} : IsOpen s ↔ (0 : Γ₀) ∉ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s

Proof state:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ ((0 ∈ s → s ∈ 𝓝 0) ∧ ∀ (b : Γ₀), b ≠ 0 → b ∈ s → s ∈ 𝓝 b) ↔ 0 ∉ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s

Tactic:
simp +contextual [nhds_of_ne_zero, imp_iff_not_or,
  hasBasis_nhds_zero.mem_iff]

Result:
no goals

Proof state:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ IsOpen s ↔ 0 ∉ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s

Tactic:
rw [isOpen_iff_mem_nhds, ← and_forall_ne (0 : Γ₀)]

Result:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ ((0 ∈ s → s ∈ 𝓝 0) ∧ ∀ (b : Γ₀), b ≠ 0 → b ∈ s → s ∈ 𝓝 b) ↔ 0 ∉ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem singleton_inter_of_not_mem {a : α} {s : Finset α} (H : a ∉ s) : {a} ∩ s = ∅ :=
  eq_empty_of_forall_not_mem <| by
    simp only [mem_inter, mem_singleton]; rintro x ⟨rfl, h⟩; exact H h

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∉ s
⊢ ∀ (x : α), ¬(x = a ∧ x ∈ s)

Tactic:
rintro x ⟨rfl, h⟩

Result:
case intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
h : x ∈ s
H : x ∉ s
⊢ False

Proof state:
case intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
h : x ∈ s
H : x ∉ s
⊢ False

Tactic:
exact H h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∉ s
⊢ ∀ (x : α), x ∉ {a} ∩ s

Tactic:
simp only [mem_inter, mem_singleton]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∉ s
⊢ ∀ (x : α), ¬(x = a ∧ x ∈ s)
-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem glueDist_swap (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) :
    ∀ x y, glueDist Ψ Φ ε x.swap y.swap = glueDist Φ Ψ ε x y
  | .inl _, .inl _ => rfl
  | .inr _, .inr _ => rfl
  | .inl _, .inr _ => by simp only [glueDist, Sum.swap_inl, Sum.swap_inr, dist_comm, add_comm]
  | .inr _, .inl _ => by simp only [glueDist, Sum.swap_inl, Sum.swap_inr, dist_comm, add_comm]

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
val✝¹ : X
val✝ : Y
⊢ glueDist Ψ Φ ε (Sum.inl val✝¹).swap (Sum.inr val✝).swap = glueDist Φ Ψ ε (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
simp only [glueDist, Sum.swap_inl, Sum.swap_inr, dist_comm, add_comm]

Result:
no goals

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
val✝¹ : Y
val✝ : X
⊢ glueDist Ψ Φ ε (Sum.inr val✝¹).swap (Sum.inl val✝).swap = glueDist Φ Ψ ε (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
simp only [glueDist, Sum.swap_inl, Sum.swap_inr, dist_comm, add_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Prod.lean
lemma hasAntidiagonal_congr (A : Type*) [AddMonoid A]
    [H1 : HasAntidiagonal A] [H2 : HasAntidiagonal A] :
    H1.antidiagonal = H2.antidiagonal

Proof state:
case h.e'_3
A : Type u_2
inst✝ : AddMonoid A
H1 H2 : HasAntidiagonal A
⊢ H1 = H2

Tactic:
subsingleton

Result:
no goals

Proof state:
A : Type u_2
inst✝ : AddMonoid A
H1 H2 : HasAntidiagonal A
⊢ antidiagonal = antidiagonal

Tactic:
congr!

Result:
case h.e'_3
A : Type u_2
inst✝ : AddMonoid A
H1 H2 : HasAntidiagonal A
⊢ H1 = H2