harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Sigma/Basic.lean
theorem Sigma.curry_update {γ : ∀ a, β a → Type*} [DecidableEq α] [∀ a, DecidableEq (β a)]
    (i : Σ a, β a) (f : (i : Σ a, β a) → γ i.1 i.2) (x : γ i.1 i.2) :
    Sigma.curry (Function.update f i x) =
      Function.update (Sigma.curry f) i.1 (Function.update (Sigma.curry f i.1) i.2 x)

Proof state:
case mk.h.h.inr
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
ja : α
jb : β ja
ha : ia ≠ ja
⊢ update f ⟨ia, ib⟩ x ⟨ja, jb⟩ =
    update (fun x y => f ⟨x, y⟩) ⟨ia, ib⟩.fst (update (fun y => f ⟨⟨ia, ib⟩.fst, y⟩) ⟨ia, ib⟩.snd x) ja jb

Tactic:
rw [Function.update_of_ne (ne_of_apply_ne Sigma.fst _), Function.update_of_ne]

Result:
case mk.h.h.inr.h
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
ja : α
jb : β ja
ha : ia ≠ ja
⊢ ja ≠ ⟨ia, ib⟩.fst

α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
ja : α
jb : β ja
ha : ia ≠ ja
⊢ ⟨ja, jb⟩.fst ≠ ⟨ia, ib⟩.fst

Proof state:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
jb : β ia
hb : ib ≠ jb
h : ⟨ia, jb⟩ = ⟨ia, ib⟩
⊢ jb = ib

Tactic:
injection h

Result:
no goals

Proof state:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
ja : α
jb : β ja
ha : ia ≠ ja
⊢ ⟨ja, jb⟩.fst ≠ ⟨ia, ib⟩.fst

Tactic:
exact ha.symm

Result:
no goals
-- Mathlib/ModelTheory/Satisfiability.lean
theorem isSatisfiable_onTheory_iff {L' : Language.{w, w'}} {φ : L →ᴸ L'} (h : φ.Injective) :
    (φ.onTheory T).IsSatisfiable ↔ T.IsSatisfiable

Proof state:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
h' : T.IsSatisfiable
this : Inhabited ↑(Nonempty.some h')
⊢ (φ.onTheory T).IsSatisfiable

Tactic:
exact Model.isSatisfiable (h'.some.defaultExpansion h)

Result:
no goals

Proof state:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
⊢ (φ.onTheory T).IsSatisfiable ↔ T.IsSatisfiable

Tactic:
classical
  refine ⟨isSatisfiable_of_isSatisfiable_onTheory φ, fun h' => ?_⟩
  haveI : Inhabited h'.some := Classical.inhabited_of_nonempty'
  exact Model.isSatisfiable (h'.some.defaultExpansion h)

Result:
no goals

Proof state:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
h' : T.IsSatisfiable
⊢ (φ.onTheory T).IsSatisfiable

Tactic:
haveI : Inhabited h'.some := Classical.inhabited_of_nonempty'

Result:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
h' : T.IsSatisfiable
this : Inhabited ↑(Nonempty.some h')
⊢ (φ.onTheory T).IsSatisfiable

Proof state:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
⊢ (φ.onTheory T).IsSatisfiable ↔ T.IsSatisfiable

Tactic:
refine ⟨isSatisfiable_of_isSatisfiable_onTheory φ, fun h' => ?_⟩

Result:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
h' : T.IsSatisfiable
⊢ (φ.onTheory T).IsSatisfiable
-- Mathlib/RingTheory/LinearDisjoint.lean
lemma mulRightMap_ker_eq_bot_iff_linearIndependent {ι : Type*} (b : ι → B) :
    LinearMap.ker (Submodule.mulRightMap (toSubmodule A) (N := toSubmodule B) b) = ⊥ ↔
    LinearIndependent A (B.val ∘ b)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
⊢ LinearMap.ker ((toSubmodule A).mulRightMap b) = ⊥ ↔ LinearIndependent (↥A) (⇑B.val ∘ b)

Tactic:
simp_rw [LinearIndependent, LinearMap.ker_eq_bot]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
⊢ LinearMap.ker ((toSubmodule A).mulRightMap b) = ⊥ ↔ Function.Injective ⇑(Finsupp.linearCombination (↥A) (⇑B.val ∘ b))
-- Mathlib/Order/KrullDimension.lean
lemma krullDim_le_one_iff_forall_isMin {α : Type*} [PartialOrder α] [OrderTop α] :
    krullDim α ≤ 1 ↔ ∀ x : α, x ≠ ⊤ → IsMin x

Proof state:
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ krullDim α ≤ 1 ↔ ∀ (x : α), x ≠ ⊤ → IsMin x

Tactic:
simp [krullDim_le_one_iff, ← or_iff_not_imp_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem?_zero_ofNat_zero : (BitVec.ofNat (w+1) 0)[0]? = some false

Proof state:
w : Nat
⊢ (0#(w + 1))[0]? = some false

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Separation/Regular.lean
theorem Topology.IsClosedEmbedding.normalSpace [TopologicalSpace Y] [NormalSpace Y]
    {f : X → Y} (hf : IsClosedEmbedding f) : NormalSpace X where
  normal s t hs ht hst

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X → Y
hf : IsClosedEmbedding f
s t : Set X
hs : IsClosed s
ht : IsClosed t
hst : Disjoint s t
⊢ SeparatedNhds s t

Tactic:
have H : SeparatedNhds (f '' s) (f '' t) :=
  NormalSpace.normal (f '' s) (f '' t) (hf.isClosedMap s hs) (hf.isClosedMap t ht)
    (disjoint_image_of_injective hf.injective hst)

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X → Y
hf : IsClosedEmbedding f
s t : Set X
hs : IsClosed s
ht : IsClosed t
hst : Disjoint s t
H : SeparatedNhds (f '' s) (f '' t)
⊢ SeparatedNhds s t

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X → Y
hf : IsClosedEmbedding f
s t : Set X
hs : IsClosed s
ht : IsClosed t
hst : Disjoint s t
H : SeparatedNhds (f '' s) (f '' t)
⊢ SeparatedNhds s t

Tactic:
exact (H.preimage hf.continuous).mono (subset_preimage_image _ _) (subset_preimage_image _ _)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Ultra/Basic.lean
lemma mem_closedBall_iff {x y: X} {r : ℝ} :
    y ∈ closedBall x r ↔ x ∈ closedBall y r

Proof state:
case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
hr : 0 ≤ r
⊢ y ∈ closedBall x r ↔ x ∈ closedBall y r

Tactic:
constructor <;> intro h <;>
rw [← closedBall_eq_of_mem h] <;>
simp [hr]

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
⊢ y ∈ closedBall x r ↔ x ∈ closedBall y r

Tactic:
cases le_or_lt 0 r with
| inl hr =>
  constructor <;> intro h <;>
  rw [← closedBall_eq_of_mem h] <;>
  simp [hr]
| inr hr => simp [closedBall_eq_empty.mpr hr]

Result:
no goals

Proof state:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
hr : r < 0
⊢ y ∈ closedBall x r ↔ x ∈ closedBall y r

Tactic:
simp [closedBall_eq_empty.mpr hr]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem prod_le_prod_of_subset_of_one_le' (h : s ⊆ t) (hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) :
    ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s t : Finset ι
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ ∏ i ∈ t \ s ∪ s, f i = ∏ i ∈ t, f i

Tactic:
rw [sdiff_union_of_subset h]

Result:
no goals

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s t : Finset ι
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ ∀ i ∈ t \ s, 1 ≤ f i

Tactic:
simpa only [mem_sdiff, and_imp]

Result:
no goals

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s t : Finset ι
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

Tactic:
calc
∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
_ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
_ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]

Result:
no goals

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s t : Finset ι
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

Tactic:
classical calc
    ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
      le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
    _ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
    _ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
@[reassoc (attr := simp)]
lemma map_s_comp_map (φ : W.RightFraction X Y) (L : C ⥤ D) (hL : W.IsInvertedBy L) :
    L.map φ.s ≫ φ.map L hL = L.map φ.f

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
φ : W.RightFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ L.map φ.s ≫ φ.map L hL = L.map φ.f

Tactic:
letI := hL _ φ.hs

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
φ : W.RightFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
this : IsIso (L.map φ.s) := hL φ.s φ.hs
⊢ L.map φ.s ≫ φ.map L hL = L.map φ.f

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
φ : W.RightFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
this : IsIso (L.map φ.s) := hL φ.s φ.hs
⊢ L.map φ.s ≫ φ.map L hL = L.map φ.f

Tactic:
simp [map]

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_ne_zero (h : f.natDegree ≠ 0) : f.natSepDegree ≠ 0

Proof state:
case h
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ rootOfSplits (algebraMap F f.SplittingField) ⋯ ⋯ ∈ (f.aroots f.SplittingField).toFinset

Tactic:
rw [Multiset.mem_toFinset, mem_aroots]

Result:
case h
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ f ≠ 0 ∧ (aeval (rootOfSplits (algebraMap F f.SplittingField) ⋯ ⋯)) f = 0

Proof state:
case h
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ rootOfSplits (algebraMap F f.SplittingField) ⋯ ⋯ ∈ (f.aroots f.SplittingField).toFinset

Tactic:
classical
rw [Multiset.mem_toFinset, mem_aroots]
exact ⟨ne_of_apply_ne _ h, map_rootOfSplits _ (SplittingField.splits f) (ne_of_apply_ne _ h)⟩

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ f.natSepDegree ≠ 0

Tactic:
rw [natSepDegree, ne_eq, Finset.card_eq_zero, ← ne_eq, ← Finset.nonempty_iff_ne_empty]

Result:
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ (f.aroots f.SplittingField).toFinset.Nonempty

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ (f.aroots f.SplittingField).toFinset.Nonempty

Tactic:
use rootOfSplits _ (SplittingField.splits f) (ne_of_apply_ne _ h)

Result:
case h
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ rootOfSplits (algebraMap F f.SplittingField) ⋯ ⋯ ∈ (f.aroots f.SplittingField).toFinset

Proof state:
case h
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ f ≠ 0 ∧ (aeval (rootOfSplits (algebraMap F f.SplittingField) ⋯ ⋯)) f = 0

Tactic:
exact ⟨ne_of_apply_ne _ h, map_rootOfSplits _ (SplittingField.splits f) (ne_of_apply_ne _ h)⟩

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_eq_encard_iff_encard_diff_eq_encard_diff (h : (s ∩ t).Finite) :
    s.encard = t.encard ↔ (s \ t).encard = (t \ s).encard

Proof state:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ s.encard = t.encard ↔ (s \ t).encard = (t \ s).encard

Tactic:
rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
  WithTop.add_right_inj h.encard_lt_top.ne]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpL1_of_aestronglyMeasurable' (hfm : AEStronglyMeasurable[m] f μ)
    (hfi : Integrable f μ) : condExpL1 hm μ f =ᵐ[μ] f

Proof state:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ ↑↑((condExpL1CLM F' hm μ) (Integrable.toL1 f hfi)) =ᶠ[ae μ] ↑↑(Integrable.toL1 f hfi)

Tactic:
rw [condExpL1CLM_of_aestronglyMeasurable']

Result:
case hfm
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ AEStronglyMeasurable (↑↑(Integrable.toL1 f hfi)) μ

Proof state:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ ↑↑((condExpL1CLM F' hm μ) (Integrable.toL1 f hfi)) =ᶠ[ae μ] f

Tactic:
refine EventuallyEq.trans ?_ (Integrable.coeFn_toL1 hfi)

Result:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ ↑↑((condExpL1CLM F' hm μ) (Integrable.toL1 f hfi)) =ᶠ[ae μ] ↑↑(Integrable.toL1 f hfi)

Proof state:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ ↑↑(condExpL1 hm μ f) =ᶠ[ae μ] f

Tactic:
rw [condExpL1_eq hfi]

Result:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ ↑↑((condExpL1CLM F' hm μ) (Integrable.toL1 f hfi)) =ᶠ[ae μ] f

Proof state:
case hfm
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ AEStronglyMeasurable (↑↑(Integrable.toL1 f hfi)) μ

Tactic:
exact hfm.congr hfi.coeFn_toL1.symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem xor_mod_two_eq_one : ((a ^^^ b) % 2 = 1) ↔ ¬ ((a % 2 = 1) ↔ (b % 2 = 1))

Proof state:
a b : Nat
⊢ (a ^^^ b) % 2 = 1 ↔ ¬(a % 2 = 1 ↔ b % 2 = 1)

Tactic:
simp only [mod_two_eq_one_iff_testBit_zero]

Result:
a b : Nat
⊢ (a ^^^ b).testBit 0 = true ↔ ¬(a.testBit 0 = true ↔ b.testBit 0 = true)

Proof state:
a b : Nat
⊢ (a ^^^ b).testBit 0 = true ↔ ¬(a.testBit 0 = true ↔ b.testBit 0 = true)

Tactic:
rw [testBit_xor]

Result:
a b : Nat
⊢ (a.testBit 0 ^^ b.testBit 0) = true ↔ ¬(a.testBit 0 = true ↔ b.testBit 0 = true)

Proof state:
a b : Nat
⊢ (a.testBit 0 ^^ b.testBit 0) = true ↔ ¬(a.testBit 0 = true ↔ b.testBit 0 = true)

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem ωb_mul_ω (q : ℕ+) : (ωb : X q) * ω = 1

Proof state:
q : ℕ+
⊢ ωb * ω = 1

Tactic:
rw [mul_comm, ω_mul_ωb]

Result:
no goals
-- Mathlib/Topology/LocallyFinite.lean
theorem iInter_compl_mem_nhds (hf : LocallyFinite f) (hc : ∀ i, IsClosed (f i)) (x : X) :
    (⋂ (i) (_ : x ∉ f i), (f i)ᶜ) ∈ 𝓝 x

Proof state:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ IsOpen (⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ)

Tactic:
suffices IsClosed (⋃ i : { i // x ∉ f i }, f i) by
  rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this

Result:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ IsClosed (⋃ i, f ↑i)

Proof state:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ IsClosed (⋃ i, f ↑i)

Tactic:
exact (hf.comp_injective Subtype.val_injective).isClosed_iUnion fun i => hc _

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ ⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ ∈ 𝓝 x

Tactic:
refine IsOpen.mem_nhds ?_ (mem_iInter₂.2 fun i => id)

Result:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ IsOpen (⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ)

Proof state:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
this : IsClosed (⋃ i, f ↑i)
⊢ IsOpen (⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ)

Tactic:
rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
theorem limitObjIsoLimitCompEvaluation_inv_π_app [HasLimitsOfShape J C] (F : J ⥤ K ⥤ C) (j : J)
    (k : K) :
    (limitObjIsoLimitCompEvaluation F k).inv ≫ (limit.π F j).app k =
      limit.π (F ⋙ (evaluation K C).obj k) j

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (limit.π F j).app k = (preservesLimitIso ((evaluation K C).obj k) F).hom ≫ limit.π (F ⋙ (evaluation K C).obj k) j

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (preservesLimitIso ((evaluation K C).obj k) F).inv ≫ (limit.π F j).app k = limit.π (F ⋙ (evaluation K C).obj k) j

Tactic:
rw [Iso.inv_comp_eq]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (limit.π F j).app k = (preservesLimitIso ((evaluation K C).obj k) F).hom ≫ limit.π (F ⋙ (evaluation K C).obj k) j

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (limitObjIsoLimitCompEvaluation F k).inv ≫ (limit.π F j).app k = limit.π (F ⋙ (evaluation K C).obj k) j

Tactic:
dsimp [limitObjIsoLimitCompEvaluation]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (preservesLimitIso ((evaluation K C).obj k) F).inv ≫ (limit.π F j).app k = limit.π (F ⋙ (evaluation K C).obj k) j
-- Mathlib/GroupTheory/Nilpotent.lean
theorem nilpotent_iff_lowerCentralSeries : IsNilpotent G ↔ ∃ n, lowerCentralSeries G n = ⊥

Proof state:
case h
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ lowerCentralSeries G n ≤ H n

Tactic:
exact descending_central_series_ge_lower H ⟨h0, hs⟩ n

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ lowerCentralSeries G n = ⊥

Tactic:
rw [eq_bot_iff, ← hn]

Result:
case h
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ lowerCentralSeries G n ≤ H n

Proof state:
case mp.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ ∃ n, lowerCentralSeries G n = ⊥

Tactic:
use n

Result:
case h
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ lowerCentralSeries G n = ⊥

Proof state:
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) ↔ ∃ n, lowerCentralSeries G n = ⊥

Tactic:
constructor

Result:
case mp
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ n, lowerCentralSeries G n = ⊥

case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n, lowerCentralSeries G n = ⊥) → ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Proof state:
case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n, lowerCentralSeries G n = ⊥) → ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
rintro ⟨n, hn⟩

Result:
case mpr.intro
G : Type u_1
inst✝ : Group G
n : ℕ
hn : lowerCentralSeries G n = ⊥
⊢ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Proof state:
case mp
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ n, lowerCentralSeries G n = ⊥

Tactic:
rintro ⟨n, H, ⟨h0, hs⟩, hn⟩

Result:
case mp.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ ∃ n, lowerCentralSeries G n = ⊥

Proof state:
case mpr.intro
G : Type u_1
inst✝ : Group G
n : ℕ
hn : lowerCentralSeries G n = ⊥
⊢ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
exact ⟨n, lowerCentralSeries G, lowerCentralSeries_isDescendingCentralSeries, hn⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
⊢ IsNilpotent G ↔ ∃ n, lowerCentralSeries G n = ⊥

Tactic:
rw [nilpotent_iff_finite_descending_central_series]

Result:
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) ↔ ∃ n, lowerCentralSeries G n = ⊥
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem const_min (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => min a (f x)

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : α → ℝ
hf : LocallyLipschitz f
a : ℝ
⊢ LocallyLipschitz fun x => a ⊓ f x

Tactic:
simpa [min_comm] using (hf.min_const a)

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
@[simp] lemma add_eq_top : x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤

Proof state:
α : Type u
inst✝ : Add α
x y : WithTop α
⊢ x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem div {q r : ℚ} (hq : q ≠ 0) (hr : r ≠ 0) :
    padicValRat p (q / r) = padicValRat p q - padicValRat p r

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
⊢ padicValRat p (q / r) = padicValRat p q - padicValRat p r

Tactic:
rw [div_eq_mul_inv, padicValRat.mul hq (inv_ne_zero hr), padicValRat.inv r, sub_eq_add_neg]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem spanSingleton_pow (x : P) (n : ℕ) : spanSingleton S x ^ n = spanSingleton S (x ^ n)

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
n : ℕ
⊢ spanSingleton S x ^ n = spanSingleton S (x ^ n)

Tactic:
induction' n with n hn

Result:
case zero
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
⊢ spanSingleton S x ^ 0 = spanSingleton S (x ^ 0)

case succ
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
n : ℕ
hn : spanSingleton S x ^ n = spanSingleton S (x ^ n)
⊢ spanSingleton S x ^ (n + 1) = spanSingleton S (x ^ (n + 1))

Proof state:
case zero
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
⊢ spanSingleton S x ^ 0 = spanSingleton S (x ^ 0)

Tactic:
rw [pow_zero, pow_zero, spanSingleton_one]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
n : ℕ
hn : spanSingleton S x ^ n = spanSingleton S (x ^ n)
⊢ spanSingleton S x ^ (n + 1) = spanSingleton S (x ^ (n + 1))

Tactic:
rw [pow_succ, hn, spanSingleton_mul_spanSingleton, pow_succ]

Result:
no goals