harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem of_inter_eq_of_symmDiff_eq_zero_negative (hu : MeasurableSet u) (hv : MeasurableSet v)
    (hw : MeasurableSet w) (hsu : s ≤[u] 0) (hsv : s ≤[v] 0) (hs : s (u ∆ v) = 0) :
    s (w ∩ u) = s (w ∩ v)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hsv : s ≤[v] 0
hs : ↑s (u ∆ v) = 0
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)

Tactic:
rw [← s.neg_le_neg_iff _ hv, neg_zero] at hsv

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : ↑s (u ∆ v) = 0
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : ↑s (u ∆ v) = 0
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)

Tactic:
have := of_inter_eq_of_symmDiff_eq_zero_positive hu hv hw hsu hsv

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : ↑s (u ∆ v) = 0
this : ↑(-s) (u ∆ v) = 0 → ↑(-s) (w ∩ u) = ↑(-s) (w ∩ v)
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : ↑s (u ∆ v) = 0
this : ↑s (u ∆ v) = 0 → ↑s (w ∩ u) = ↑s (w ∩ v)
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)

Tactic:
exact this hs

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : s ≤[u] 0
hsv : s ≤[v] 0
hs : ↑s (u ∆ v) = 0
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)

Tactic:
rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hsv : s ≤[v] 0
hs : ↑s (u ∆ v) = 0
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : ↑s (u ∆ v) = 0
this : ↑(-s) (u ∆ v) = 0 → ↑(-s) (w ∩ u) = ↑(-s) (w ∩ v)
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)

Tactic:
simp only [Pi.neg_apply, neg_inj, neg_eq_zero, coe_neg] at this

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : ↑s (u ∆ v) = 0
this : ↑s (u ∆ v) = 0 → ↑s (w ∩ u) = ↑s (w ∩ v)
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)
-- Mathlib/Algebra/Order/Round.lean
theorem sub_half_lt_round (x : α) : x - 1 / 2 < round x

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ x + 1 / 2 - 1 < ↑⌊x + 1 / 2⌋

Tactic:
exact Int.sub_one_lt_floor (x + 1 / 2)

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ x - 1 / 2 = x + 1 / 2 - 1

Tactic:
linarith

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ x - 1 / 2 < ↑(round x)

Tactic:
rw [round_eq x, show x - 1 / 2 = x + 1 / 2 - 1 by linarith]

Result:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ x + 1 / 2 - 1 < ↑⌊x + 1 / 2⌋
-- Mathlib/Order/Partition/Finpartition.lean
theorem mem_atomise :
    t ∈ (atomise s F).parts ↔
      t.Nonempty ∧ ∃ Q ⊆ F, {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} = t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
⊢ t ∈ (atomise s F).parts ↔ t.Nonempty ∧ ∃ Q ⊆ F, filter (fun i => ∀ u ∈ F, u ∈ Q ↔ i ∈ u) s = t

Tactic:
simp only [atomise, ofErase, bot_eq_empty, mem_erase, mem_image, nonempty_iff_ne_empty,
  mem_singleton, and_comm, mem_powerset, exists_prop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Basic.lean
theorem tail_dropLast (l : List α) : tail (dropLast l) = dropLast (tail l)

Proof state:
case h.isFalse.isFalse
α : Type u_1
l : List α
i✝ : Nat
h✝¹ : ¬i✝ + 1 < l.length - 1
h✝ : ¬i✝ < l.length - 1 - 1
⊢ none = none

Tactic:
rfl

Result:
no goals

Proof state:
case h
α : Type u_1
l : List α
i✝ : Nat
⊢ l.dropLast.tail[i✝]? = l.tail.dropLast[i✝]?

Tactic:
simp only [getElem?_tail, getElem?_dropLast, length_tail]

Result:
case h
α : Type u_1
l : List α
i✝ : Nat
⊢ (if i✝ + 1 < l.length - 1 then l[i✝ + 1]? else none) = if i✝ < l.length - 1 - 1 then l[i✝ + 1]? else none

Proof state:
case h.isTrue.isTrue
α : Type u_1
l : List α
i✝ : Nat
h✝¹ : i✝ + 1 < l.length - 1
h✝ : i✝ < l.length - 1 - 1
⊢ l[i✝ + 1]? = l[i✝ + 1]?

Tactic:
rfl

Result:
no goals

Proof state:
case h.isFalse.isTrue
α : Type u_1
l : List α
i✝ : Nat
h✝¹ : ¬i✝ + 1 < l.length - 1
h✝ : i✝ < l.length - 1 - 1
⊢ none = l[i✝ + 1]?

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ l.dropLast.tail = l.tail.dropLast

Tactic:
ext1

Result:
case h
α : Type u_1
l : List α
i✝ : Nat
⊢ l.dropLast.tail[i✝]? = l.tail.dropLast[i✝]?

Proof state:
case h
α : Type u_1
l : List α
i✝ : Nat
⊢ (if i✝ + 1 < l.length - 1 then l[i✝ + 1]? else none) = if i✝ < l.length - 1 - 1 then l[i✝ + 1]? else none

Tactic:
split <;> split

Result:
case h.isTrue.isTrue
α : Type u_1
l : List α
i✝ : Nat
h✝¹ : i✝ + 1 < l.length - 1
h✝ : i✝ < l.length - 1 - 1
⊢ l[i✝ + 1]? = l[i✝ + 1]?

case h.isTrue.isFalse
α : Type u_1
l : List α
i✝ : Nat
h✝¹ : i✝ + 1 < l.length - 1
h✝ : ¬i✝ < l.length - 1 - 1
⊢ l[i✝ + 1]? = none

case h.isFalse.isTrue
α : Type u_1
l : List α
i✝ : Nat
h✝¹ : ¬i✝ + 1 < l.length - 1
h✝ : i✝ < l.length - 1 - 1
⊢ none = l[i✝ + 1]?

case h.isFalse.isFalse
α : Type u_1
l : List α
i✝ : Nat
h✝¹ : ¬i✝ + 1 < l.length - 1
h✝ : ¬i✝ < l.length - 1 - 1
⊢ none = none

Proof state:
case h.isTrue.isFalse
α : Type u_1
l : List α
i✝ : Nat
h✝¹ : i✝ + 1 < l.length - 1
h✝ : ¬i✝ < l.length - 1 - 1
⊢ l[i✝ + 1]? = none

Tactic:
omega

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem BddBelow_zero [Nonempty Γ] : BddBelow (Function.support (0 : Γ → R))

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : LinearOrder Γ
inst✝ : Nonempty Γ
⊢ BddBelow (Function.support 0)

Tactic:
simp only [support_zero', bddBelow_empty]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.toMatrix₂_apply (B : M₁ →ₗ[R] M₂ →ₗ[R] N₂) (i : n) (j : m) :
    LinearMap.toMatrix₂ b₁ b₂ B i j = B (b₁ i) (b₂ j)

Proof state:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] N₂
i : n
j : m
⊢ (toMatrix₂ b₁ b₂) B i j = (B (b₁ i)) (b₂ j)

Tactic:
simp only [toMatrix₂, LinearEquiv.trans_apply, toMatrix₂'_apply, LinearEquiv.arrowCongr_apply,
  Basis.equivFun_symm_apply, Pi.single_apply, ite_smul, one_smul, zero_smul, sum_ite_eq',
  mem_univ, ↓reduceIte, LinearEquiv.refl_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem iSupIndep.dfinsupp_sumAddHom_injective {p : ι → AddSubgroup N} (h : iSupIndep p) :
    Function.Injective (sumAddHom fun i => (p i).subtype)

Proof state:
ι : Type u_1
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : iSupIndep p
⊢ Function.Injective ⇑(sumAddHom fun i => (p i).subtype)

Tactic:
rw [← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)] at h

Result:
ι : Type u_1
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : iSupIndep (⇑AddSubgroup.toIntSubmodule ∘ p)
⊢ Function.Injective ⇑(sumAddHom fun i => (p i).subtype)

Proof state:
ι : Type u_1
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : iSupIndep (⇑AddSubgroup.toIntSubmodule ∘ p)
⊢ Function.Injective ⇑(sumAddHom fun i => (p i).subtype)

Tactic:
exact h.dfinsupp_lsum_injective

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₄_of_isShortNF_of_char_three : W.c₄ = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ W.c₄ = 0

Tactic:
rw [c₄_of_isShortNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ -48 * W.a₄ = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ -48 * W.a₄ = 0

Tactic:
linear_combination -16 * W.a₄ * CharP.cast_eq_zero R 3

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem fst_univ : ρ.fst univ = ρ univ

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ ρ.fst univ = ρ univ

Tactic:
rw [fst_apply MeasurableSet.univ, preimage_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.sub_eq_iff_eq_add (a b c : BitVec w) : (a + (~~~b + 1#w) == c) = (a == c + b)

Proof state:
w : Nat
a b c : BitVec w
⊢ (a + (~~~b + 1#w) == c) = (a == c + b)

Tactic:
rw [Bool.eq_iff_iff, beq_iff_eq, beq_iff_eq, ← BitVec.neg_eq_not_add, ← @BitVec.sub_toAdd]

Result:
w : Nat
a b c : BitVec w
⊢ a - b = c ↔ a = c + b

Proof state:
w : Nat
a b c : BitVec w
⊢ a - b = c ↔ a = c + b

Tactic:
exact _root_.BitVec.sub_eq_iff_eq_add

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem toSubmonoid_injective : Function.Injective (toSubmonoid : Subgroup G → Submonoid G) :=
  -- fun p q h => SetLike.ext'_iff.2 (show _ from SetLike.ext'_iff.1 h)
  fun p q h => by
    have := SetLike.ext'_iff.1 h
    rw [coe_toSubmonoid, coe_toSubmonoid] at this
    exact SetLike.ext'_iff.2 this

Proof state:
G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : ↑p.toSubmonoid = ↑q.toSubmonoid
⊢ p = q

Tactic:
rw [coe_toSubmonoid, coe_toSubmonoid] at this

Result:
G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : ↑p = ↑q
⊢ p = q

Proof state:
G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : ↑p = ↑q
⊢ p = q

Tactic:
exact SetLike.ext'_iff.2 this

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
⊢ p = q

Tactic:
have := SetLike.ext'_iff.1 h

Result:
G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : ↑p.toSubmonoid = ↑q.toSubmonoid
⊢ p = q
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc (attr := simp)]
lemma inl_v_descCochain_v (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + (-1) = p₂) (h₂₃ : p₂ + n = p₃) :
    (inl φ).v p₁ p₂ h₁₂ ≫ (descCochain φ α β h).v p₂ p₃ h₂₃ =
        α.v p₁ p₃ (by rw [← h₂₃, ← h₁₂, ← h, add_comm m, add_assoc, neg_add_cancel_left])

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
⊢ p₁ + -1 = p₂

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
⊢ p₁ + m = p₃

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
⊢ -1 + n = m

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.122158, u_1} C
inst✝³ : Category.{?u.122162, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
⊢ p₁ + m = p₃

Tactic:
rw [← h₂₃, ← h₁₂, ← h, add_comm m, add_assoc, neg_add_cancel_left]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
⊢ (inl φ).v p₁ p₂ h₁₂ ≫ (descCochain φ α β h).v p₂ p₃ h₂₃ = α.v p₁ p₃ ⋯

Tactic:
simpa only [Cochain.comp_v _ _ (show -1 + n = m by omega) p₁ p₂ p₃
  (by omega) (by omega)] using
    Cochain.congr_v (inl_descCochain φ α β h) p₁ p₃ (by omega)

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
⊢ p₂ + n = p₃

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem of_zsmul : a ≡ b [PMOD z • p] → a ≡ b [PMOD p] := fun ⟨m, hm⟩ =>
  ⟨m * z, by rwa [mul_smul]⟩

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b : α
z : ℤ
x✝ : a ≡ b [PMOD z • p]
m : ℤ
hm : b - a = m • z • p
⊢ b - a = (m * z) • p

Tactic:
rwa [mul_smul]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_neg (a b : α) : emultiplicity a (-b) = emultiplicity a b

Proof state:
α : Type u_1
inst✝ : Ring α
a b : α
⊢ ∀ (n : ℕ), a ^ n ∣ -b ↔ a ^ n ∣ b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Ring α
a b : α
⊢ emultiplicity a (-b) = emultiplicity a b

Tactic:
rw [emultiplicity_eq_emultiplicity_iff]

Result:
α : Type u_1
inst✝ : Ring α
a b : α
⊢ ∀ (n : ℕ), a ^ n ∣ -b ↔ a ^ n ∣ b
-- Mathlib/Order/Filter/Pi.lean
theorem pi_inf_principal_pi_eq_bot [∀ i, NeBot (f i)] {I : Set ι} :
    pi f ⊓ 𝓟 (Set.pi I s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ pi f ⊓ 𝓟 (I.pi s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥

Tactic:
rw [← univ_pi_piecewise_univ I, pi_inf_principal_univ_pi_eq_bot]

Result:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ (∃ i, f i ⊓ 𝓟 (I.piecewise s (fun x => univ) i) = ⊥) ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ (∃ i, f i ⊓ 𝓟 (I.piecewise s (fun x => univ) i) = ⊥) ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥

Tactic:
refine exists_congr fun i => ?_

Result:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
i : ι
⊢ f i ⊓ 𝓟 (I.piecewise s (fun x => univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ pi f ⊓ 𝓟 (I.pi s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥

Tactic:
classical
rw [← univ_pi_piecewise_univ I, pi_inf_principal_univ_pi_eq_bot]
refine exists_congr fun i => ?_
by_cases hi : i ∈ I <;> simp [hi, NeBot.ne']

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
i : ι
⊢ f i ⊓ 𝓟 (I.piecewise s (fun x => univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥

Tactic:
by_cases hi : i ∈ I <;> simp [hi, NeBot.ne']

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Images.lean
theorem image.lift_fac (F' : MonoFactorisation f) : image.lift F' ≫ F'.m = image.ι f

Proof state:
case hf.h
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑x = (Hom.hom (ι f)) x

Tactic:
rfl

Result:
no goals

Proof state:
case hf.h
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 => (Hom.hom f) x_1 = ↑x) ⋯) =
    (Hom.hom (ι f)) x

Tactic:
rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]

Result:
case hf.h
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑x = (Hom.hom (ι f)) x

Proof state:
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f

Tactic:
ext x

Result:
case hf.h
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ (Hom.hom (lift F' ≫ F'.m)) x = (Hom.hom (ι f)) x

Proof state:
case hf.h
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ (Hom.hom (lift F' ≫ F'.m)) x = (Hom.hom (ι f)) x

Tactic:
change (F'.e ≫ F'.m) _ = _

Result:
case hf.h
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 => (Hom.hom f) x_1 = ↑x) ⋯) =
    (Hom.hom (ι f)) x
-- Mathlib/Topology/UniformSpace/Completion.lean
theorem extension_map [CompleteSpace γ] [T0Space γ] {f : β → γ} {g : α → β}
    (hf : UniformContinuous f) (hg : UniformContinuous g) :
    Completion.extension f ∘ Completion.map g = Completion.extension (f ∘ g) :=
  Completion.ext (continuous_extension.comp continuous_map) continuous_extension <| by
    simp [hf, hg, hf.comp hg, map_coe, extension_coe]

Proof state:
α : Type u_1
inst✝⁴ : UniformSpace α
β : Type u_2
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
⊢ ∀ (a : α), (Completion.extension f ∘ Completion.map g) ↑a = Completion.extension (f ∘ g) ↑a

Tactic:
simp [hf, hg, hf.comp hg, map_coe, extension_coe]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem ghostFun_intCast (i : ℤ) : ghostFun (i : 𝕎 R) = i :=
  show ghostFun i.castDef = _ by
    cases i <;> simp [*, Int.castDef, ghostFun_natCast, ghostFun_neg, -Pi.natCast_def,
      -Pi.intCast_def]

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
i : ℤ
⊢ WittVector.ghostFun i.castDef = ↑i

Tactic:
cases i <;> simp [*, Int.castDef, ghostFun_natCast, ghostFun_neg, -Pi.natCast_def,
  -Pi.intCast_def]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
/-- The norm, relative to `ℤ`, of `ζ ^ 2 ^ k - 1` in a `2 ^ (k + 1)`-th cyclotomic extension of `ℚ`
is `(-2) ^ 2 ^ k`. -/
lemma norm_toInteger_pow_sub_one_of_two [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑((2 : ℕ+) ^ (k + 1))) :
    Algebra.norm ℤ (hζ.toInteger ^ 2 ^ k - 1) = (-2) ^ (2 : ℕ) ^ k

Proof state:
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))
this : NumberField K
⊢ (Algebra.norm ℤ) (hζ.toInteger ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Tactic:
rw [Algebra.norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) rfl.le]

Result:
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))
this : NumberField K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger ^ 2 ^ k - 1)) = (algebraMap ℤ ℚ) ((-2) ^ 2 ^ k)

Proof state:
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))
⊢ (Algebra.norm ℤ) (hζ.toInteger ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Tactic:
have : NumberField K := IsCyclotomicExtension.numberField {2 ^ (k + 1)} ℚ K

Result:
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))
this : NumberField K
⊢ (Algebra.norm ℤ) (hζ.toInteger ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Proof state:
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))
this : NumberField K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger ^ 2 ^ k - 1)) = (algebraMap ℤ ℚ) ((-2) ^ 2 ^ k)

Tactic:
simp [hζ.norm_pow_sub_one_two (cyclotomic.irreducible_rat (pow_pos (by decide) _))]

Result:
no goals

Proof state:
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))
this : NumberField K
⊢ 0 < 2

Tactic:
decide

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Basic.lean
/-- A morphism from an object `X` with non-empty fiber to a connected object `A` is an
epimorphism. -/
lemma epi_of_nonempty_of_isConnected {X A : C} [IsConnected A] [h : Nonempty (F.obj X)]
    (f : X ⟶ A) : Epi f := Epi.mk <| fun {Z} u v huv ↦ by
  apply evaluation_injective_of_isConnected F A Z (F.map f (Classical.arbitrary _))
  simpa using congr_fun (F.congr_map huv) _

Proof state:
case a
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X A : C
inst✝ : IsConnected A
h : Nonempty (F.obj X).carrier
f : X ⟶ A
Z : C
u v : A ⟶ Z
huv : f ≫ u = f ≫ v
⊢ (fun f_1 => F.map f_1 (F.map f (Classical.arbitrary (F.obj X).carrier))) u =
    (fun f_1 => F.map f_1 (F.map f (Classical.arbitrary (F.obj X).carrier))) v

Tactic:
simpa using congr_fun (F.congr_map huv) _

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X A : C
inst✝ : IsConnected A
h : Nonempty (F.obj X).carrier
f : X ⟶ A
Z : C
u v : A ⟶ Z
huv : f ≫ u = f ≫ v
⊢ u = v

Tactic:
apply evaluation_injective_of_isConnected F A Z (F.map f (Classical.arbitrary _))

Result:
case a
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X A : C
inst✝ : IsConnected A
h : Nonempty (F.obj X).carrier
f : X ⟶ A
Z : C
u v : A ⟶ Z
huv : f ≫ u = f ≫ v
⊢ (fun f_1 => F.map f_1 (F.map f (Classical.arbitrary (F.obj X).carrier))) u =
    (fun f_1 => F.map f_1 (F.map f (Classical.arbitrary (F.obj X).carrier))) v
-- Mathlib/RingTheory/Ideal/Height.lean
@[gcongr]
lemma Ideal.primeHeight_mono {I J : Ideal R} [I.IsPrime] [J.IsPrime] (h : I ≤ J) :
    I.primeHeight ≤ J.primeHeight

Proof state:
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
inst✝ : J.IsPrime
h : I ≤ J
⊢ Order.height { asIdeal := I, isPrime := inst✝¹ } ≤ Order.height { asIdeal := J, isPrime := inst✝ }

Tactic:
gcongr

Result:
case hab
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
inst✝ : J.IsPrime
h : I ≤ J
⊢ { asIdeal := I, isPrime := inst✝¹ } ≤ { asIdeal := J, isPrime := inst✝ }

Proof state:
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
inst✝ : J.IsPrime
h : I ≤ J
⊢ I.primeHeight ≤ J.primeHeight

Tactic:
unfold primeHeight

Result:
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
inst✝ : J.IsPrime
h : I ≤ J
⊢ Order.height { asIdeal := I, isPrime := inst✝¹ } ≤ Order.height { asIdeal := J, isPrime := inst✝ }

Proof state:
case hab
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
inst✝ : J.IsPrime
h : I ≤ J
⊢ { asIdeal := I, isPrime := inst✝¹ } ≤ { asIdeal := J, isPrime := inst✝ }

Tactic:
exact h

Result:
no goals