harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} (i : δ):
    (zipWith f l₁ l₂).foldl g i = (zip l₁ l₂).foldl (fun r p => g r (f p.1 p.2)) i

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l₁ : Array α
l₂ : Array β
g : δ → γ → δ
f : α → β → γ
i : δ
⊢ foldl g i (zipWith f l₁ l₂) = foldl (fun r p => g r (f p.fst p.snd)) i (l₁.zip l₂)

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l₂ : Array β
g : δ → γ → δ
f : α → β → γ
i : δ
toList✝ : List α
⊢ foldl g i (zipWith f { toList := toList✝ } l₂) =
    foldl (fun r p => g r (f p.fst p.snd)) i ({ toList := toList✝ }.zip l₂)

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
g : δ → γ → δ
f : α → β → γ
i : δ
toList✝¹ : List α
toList✝ : List β
⊢ foldl g i (zipWith f { toList := toList✝¹ } { toList := toList✝ }) =
    foldl (fun r p => g r (f p.fst p.snd)) i ({ toList := toList✝¹ }.zip { toList := toList✝ })

Tactic:
simp [List.zipWith_foldl_eq_zip_foldl]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l₂ : Array β
g : δ → γ → δ
f : α → β → γ
i : δ
toList✝ : List α
⊢ foldl g i (zipWith f { toList := toList✝ } l₂) =
    foldl (fun r p => g r (f p.fst p.snd)) i ({ toList := toList✝ }.zip l₂)

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
g : δ → γ → δ
f : α → β → γ
i : δ
toList✝¹ : List α
toList✝ : List β
⊢ foldl g i (zipWith f { toList := toList✝¹ } { toList := toList✝ }) =
    foldl (fun r p => g r (f p.fst p.snd)) i ({ toList := toList✝¹ }.zip { toList := toList✝ })
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_add {x : ℝ≥0∞} (y z : ℝ) (hx : x ≠ 0) (h'x : x ≠ ⊤) : x ^ (y + z) = x ^ y * x ^ z

Proof state:
case coe
y z : ℝ
x : ℝ≥0
hx : ↑x ≠ 0
h'x : ↑x ≠ ⊤
this : x ≠ 0
⊢ ↑x ^ (y + z) = ↑x ^ y * ↑x ^ z

Tactic:
simp [← coe_rpow_of_ne_zero this, NNReal.rpow_add this]

Result:
no goals

Proof state:
case top
y z : ℝ
hx : ⊤ ≠ 0
h'x : ⊤ ≠ ⊤
⊢ ⊤ ^ (y + z) = ⊤ ^ y * ⊤ ^ z

Tactic:
exact (h'x rfl).elim

Result:
no goals

Proof state:
case coe
y z : ℝ
x : ℝ≥0
hx : ↑x ≠ 0
h'x : ↑x ≠ ⊤
⊢ ↑x ^ (y + z) = ↑x ^ y * ↑x ^ z

Tactic:
have : x ≠ 0 := fun h => by simp [h] at hx

Result:
case coe
y z : ℝ
x : ℝ≥0
hx : ↑x ≠ 0
h'x : ↑x ≠ ⊤
this : x ≠ 0
⊢ ↑x ^ (y + z) = ↑x ^ y * ↑x ^ z

Proof state:
y z : ℝ
x : ℝ≥0
hx : ↑x ≠ 0
h'x : ↑x ≠ ⊤
h : x = 0
⊢ False

Tactic:
simp [h] at hx

Result:
no goals

Proof state:
x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ⊤
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
cases x with
| top => exact (h'x rfl).elim
| coe x =>
  have : x ≠ 0 := fun h => by simp [h] at hx
  simp [← coe_rpow_of_ne_zero this, NNReal.rpow_add this]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodySumFun_add_le (x y : mixedSpace K) :
    convexBodySumFun (x + y) ≤ convexBodySumFun x + convexBodySumFun y

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
⊢ ∑ w : InfinitePlace K, ↑w.mult * (normAtPlace w) (x + y) ≤
    ∑ x_1 : InfinitePlace K, ↑x_1.mult * ((normAtPlace x_1) x + (normAtPlace x_1) y)

Tactic:
exact Finset.sum_le_sum
  fun _ _ ↦ mul_le_mul_of_nonneg_left (normAtPlace_add_le _ x y) (Nat.cast_pos.mpr mult_pos).le

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
⊢ convexBodySumFun (x + y) ≤ convexBodySumFun x + convexBodySumFun y

Tactic:
simp_rw [convexBodySumFun, ← Finset.sum_add_distrib, ← mul_add]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
⊢ ∑ w : InfinitePlace K, ↑w.mult * (normAtPlace w) (x + y) ≤
    ∑ x_1 : InfinitePlace K, ↑x_1.mult * ((normAtPlace x_1) x + (normAtPlace x_1) y)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_ushiftRight {x : BitVec w} {n : Nat} :
    (x >>> n).toInt = if n = 0 then x.toInt else x.toNat >>> n

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : ¬n = 0
⊢ 0 < n

Tactic:
omega

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
n : Nat
hn : n = 0
⊢ (x >>> n).toInt = if n = 0 then x.toInt else ↑(x.toNat >>> n)

Tactic:
simp [hn]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
n : Nat
hn : ¬n = 0
⊢ (x >>> n).toInt = if n = 0 then x.toInt else ↑(x.toNat >>> n)

Tactic:
rw [toInt_ushiftRight_of_lt (by omega), toInt_eq_toNat_cond]

Result:
case neg
w : Nat
x : BitVec w
n : Nat
hn : ¬n = 0
⊢ ↑(x.toNat >>> n) = if n = 0 then if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w) else ↑(x.toNat >>> n)

Proof state:
w : Nat
x : BitVec w
n : Nat
⊢ (x >>> n).toInt = if n = 0 then x.toInt else ↑(x.toNat >>> n)

Tactic:
by_cases hn : n = 0

Result:
case pos
w : Nat
x : BitVec w
n : Nat
hn : n = 0
⊢ (x >>> n).toInt = if n = 0 then x.toInt else ↑(x.toNat >>> n)

case neg
w : Nat
x : BitVec w
n : Nat
hn : ¬n = 0
⊢ (x >>> n).toInt = if n = 0 then x.toInt else ↑(x.toNat >>> n)

Proof state:
case neg
w : Nat
x : BitVec w
n : Nat
hn : ¬n = 0
⊢ ↑(x.toNat >>> n) = if n = 0 then if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w) else ↑(x.toNat >>> n)

Tactic:
simp [hn]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem range_incl : N.incl.range = N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ LinearMap.range (↑N).subtype = ↑N

Tactic:
rw [Submodule.range_subtype]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ N.incl.range = N

Tactic:
simp only [← toSubmodule_inj, LieModuleHom.toSubmodule_range, incl_coe]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ LinearMap.range (↑N).subtype = ↑N
-- Mathlib/Algebra/Order/Interval/Basic.lean
theorem length_add_le : ∀ s t : Interval α, (s + t).length ≤ s.length + t.length
  | ⊥, _ => by simp
  | _, ⊥ => by simp
  | (s : NonemptyInterval α), (t : NonemptyInterval α) => (s.length_add t).le

Proof state:
α : Type u_2
inst✝ : OrderedAddCommGroup α
x✝ : Interval α
⊢ (⊥ + x✝).length ≤ ⊥.length + x✝.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝ : OrderedAddCommGroup α
x✝ : Interval α
⊢ (x✝ + ⊥).length ≤ x✝.length + ⊥.length

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourierCoeff_eq_intervalIntegral (f : AddCircle T → E) (n : ℤ) (a : ℝ) :
    fourierCoeff f n = (1 / T) • ∫ x in a..a + T, @fourier T (-n) x • f x

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a : ℝ
this : ∀ (x : ℝ), (fourier (-n)) ↑x • f ↑x = (fun z => (fourier (-n)) z • f z) ↑x
⊢ fourierCoeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, (fun z => (fourier (-n)) z • f z) ↑x

Tactic:
rw [fourierCoeff, AddCircle.intervalIntegral_preimage T a (fun z => _ • _),
  volume_eq_smul_haarAddCircle, integral_smul_measure, ENNReal.toReal_ofReal hT.out.le,
  ← smul_assoc, smul_eq_mul, one_div_mul_cancel hT.out.ne', one_smul]

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a : ℝ
⊢ ∀ (x : ℝ), (fourier (-n)) ↑x • f ↑x = (fun z => (fourier (-n)) z • f z) ↑x

Tactic:
intro x

Result:
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a x : ℝ
⊢ (fourier (-n)) ↑x • f ↑x = (fun z => (fourier (-n)) z • f z) ↑x

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a : ℝ
this : ∀ (x : ℝ), (fourier (-n)) ↑x • f ↑x = (fun z => (fourier (-n)) z • f z) ↑x
⊢ fourierCoeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f ↑x

Tactic:
simp_rw (config := {singlePass := true}) [this]

Result:
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a : ℝ
this : ∀ (x : ℝ), (fourier (-n)) ↑x • f ↑x = (fun z => (fourier (-n)) z • f z) ↑x
⊢ fourierCoeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, (fun z => (fourier (-n)) z • f z) ↑x

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a : ℝ
⊢ fourierCoeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f ↑x

Tactic:
have : ∀ x : ℝ, @fourier T (-n) x • f x = (fun z : AddCircle T => @fourier T (-n) z • f z) x := by
  intro x; rfl

Result:
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a : ℝ
this : ∀ (x : ℝ), (fourier (-n)) ↑x • f ↑x = (fun z => (fourier (-n)) z • f z) ↑x
⊢ fourierCoeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f ↑x

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a x : ℝ
⊢ (fourier (-n)) ↑x • f ↑x = (fun z => (fourier (-n)) z • f z) ↑x

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replicate_append_replicate : replicate n a ++ replicate m a = replicate (n + m) a

Proof state:
case right
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
b : α✝
⊢ ¬n = 0 ∧ b = a ∨ ¬m = 0 ∧ b = a → b = a

Tactic:
rintro (⟨-, rfl⟩ | ⟨_, rfl⟩) <;> rfl

Result:
no goals

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
⊢ (replicate n a ++ replicate m a).length = n + m ∧ ∀ (b : α✝), b ∈ replicate n a ++ replicate m a → b = a

Tactic:
constructor

Result:
case left
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
⊢ (replicate n a ++ replicate m a).length = n + m

case right
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
⊢ ∀ (b : α✝), b ∈ replicate n a ++ replicate m a → b = a

Proof state:
case right
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
b : α✝
⊢ b ∈ replicate n a ++ replicate m a → b = a

Tactic:
simp only [mem_append, mem_replicate, ne_eq]

Result:
case right
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
b : α✝
⊢ ¬n = 0 ∧ b = a ∨ ¬m = 0 ∧ b = a → b = a

Proof state:
case right
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
⊢ ∀ (b : α✝), b ∈ replicate n a ++ replicate m a → b = a

Tactic:
intro b

Result:
case right
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
b : α✝
⊢ b ∈ replicate n a ++ replicate m a → b = a

Proof state:
case left
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
⊢ (replicate n a ++ replicate m a).length = n + m

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
⊢ replicate n a ++ replicate m a = replicate (n + m) a

Tactic:
rw [eq_replicate_iff]

Result:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
⊢ (replicate n a ++ replicate m a).length = n + m ∧ ∀ (b : α✝), b ∈ replicate n a ++ replicate m a → b = a
-- Mathlib/SetTheory/Ordinal/Enum.lean
theorem enumOrd_le_of_subset {t : Set Ordinal} (hs : ¬ BddAbove s) (hst : s ⊆ t) :
    enumOrd t ≤ enumOrd s

Proof state:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ {b | ∀ c < a, enumOrd s c < b} ⊆ {b | ∀ c < a, enumOrd t c < b}

Tactic:
intro b hb c hc

Result:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a b : Ordinal.{u}
hb : b ∈ {b | ∀ c < a, enumOrd s c < b}
c : Ordinal.{u}
hc : c < a
⊢ enumOrd t c < b

Proof state:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ enumOrd t a ≤ enumOrd s a

Tactic:
rw [enumOrd, enumOrd]

Result:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ sInf (t ∩ {b | ∀ c < a, enumOrd t c < b}) ≤ sInf (s ∩ {b | ∀ c < a, enumOrd s c < b})

Proof state:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ sInf (t ∩ {b | ∀ c < a, enumOrd t c < b}) ≤ sInf (s ∩ {b | ∀ c < a, enumOrd s c < b})

Tactic:
apply csInf_le_csInf' (enumOrd_nonempty hs a) (inter_subset_inter hst _)

Result:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ {b | ∀ c < a, enumOrd s c < b} ⊆ {b | ∀ c < a, enumOrd t c < b}

Proof state:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
⊢ enumOrd t ≤ enumOrd s

Tactic:
intro a

Result:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ enumOrd t a ≤ enumOrd s a

Proof state:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a b : Ordinal.{u}
hb : b ∈ {b | ∀ c < a, enumOrd s c < b}
c : Ordinal.{u}
hc : c < a
⊢ enumOrd t c < b

Tactic:
exact (enumOrd_le_of_subset hs hst c).trans_lt <| hb c hc

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
    (h : m.1.WF) {l : List ((a : α) × β a)} {k : α}
    (h' : (l.map Sigma.fst).contains k = false) :
    (m.insertMany l).1.getKey! k = m.getKey! k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
l : List ((a : α) × β a)
k : α
h' : (List.map Sigma.fst l).contains k = false
⊢ (m.insertMany l).val.getKey! k = m.getKey! k

Tactic:
simp_to_model [insertMany] using List.getKey!_insertList_of_contains_eq_false

Result:
no goals
-- Mathlib/Topology/Algebra/ConstMulAction.lean
theorem isOpenMap_quotient_mk'_mul [ContinuousConstSMul Γ T] :
    letI := MulAction.orbitRel Γ T
    IsOpenMap (Quotient.mk' : T → Quotient (MulAction.orbitRel Γ T)) := fun U hU => by
  rw [isOpen_coinduced, MulAction.quotient_preimage_image_eq_union_mul U]
  exact isOpen_iUnion fun γ => isOpenMap_smul γ U hU

Proof state:
Γ : Type u_4
inst✝³ : Group Γ
T : Type u_5
inst✝² : TopologicalSpace T
inst✝¹ : MulAction Γ T
inst✝ : ContinuousConstSMul Γ T
U : Set T
hU : IsOpen U
⊢ IsOpen (⋃ g, (fun x => g • x) '' U)

Tactic:
exact isOpen_iUnion fun γ => isOpenMap_smul γ U hU

Result:
no goals

Proof state:
Γ : Type u_4
inst✝³ : Group Γ
T : Type u_5
inst✝² : TopologicalSpace T
inst✝¹ : MulAction Γ T
inst✝ : ContinuousConstSMul Γ T
U : Set T
hU : IsOpen U
⊢ IsOpen (Quotient.mk' '' U)

Tactic:
rw [isOpen_coinduced, MulAction.quotient_preimage_image_eq_union_mul U]

Result:
Γ : Type u_4
inst✝³ : Group Γ
T : Type u_5
inst✝² : TopologicalSpace T
inst✝¹ : MulAction Γ T
inst✝ : ContinuousConstSMul Γ T
U : Set T
hU : IsOpen U
⊢ IsOpen (⋃ g, (fun x => g • x) '' U)
-- Mathlib/LinearAlgebra/Dimension/Finrank.lean
theorem finrank_eq (f : M ≃ₗ[R] M₂) : finrank R M = finrank R M₂

Proof state:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M ≃ₗ[R] M₂
⊢ finrank R M = finrank R M₂

Tactic:
unfold finrank

Result:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M ≃ₗ[R] M₂
⊢ toNat (Module.rank R M) = toNat (Module.rank R M₂)

Proof state:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M ≃ₗ[R] M₂
⊢ toNat (Module.rank R M) = toNat (Module.rank R M₂)

Tactic:
rw [← Cardinal.toNat_lift, f.lift_rank_eq, Cardinal.toNat_lift]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sheafification.lean
theorem isoSheafify_inv {P : Cᵒᵖ ⥤ D} (hP : Presheaf.IsSheaf J P) :
    (isoSheafify J hP).inv = sheafifyLift J (𝟙 _) hP

Proof state:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ toSheafify J P ≫ (isoSheafify J hP).inv = 𝟙 P

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ (isoSheafify J hP).inv = sheafifyLift J (𝟙 P) hP

Tactic:
apply sheafifyLift_unique

Result:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ toSheafify J P ≫ (isoSheafify J hP).inv = 𝟙 P
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isPrefix_map_iff {β} {f : α → β} {l₁ : List α} {l₂ : List β} :
    l₂ <+: l₁.map f ↔ ∃ l, l <+: l₁ ∧ l₂ = l.map f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l₁ : List α
l₂ : List β
⊢ l₂ <+: map f l₁ ↔ ∃ l, l <+: l₁ ∧ l₂ = map f l

Tactic:
rw [← filterMap_eq_map, isPrefix_filterMap_iff]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_mul_two : Principal (· * ·) 2

Proof state:
a b : Ordinal.{u_1}
ha : a < 2
hb : b < 2
⊢ (fun x1 x2 => x1 * x2) a b < 2

Tactic:
rw [← succ_one, lt_succ_iff] at *

Result:
a b : Ordinal.{u_1}
ha : a ≤ 1
hb : b ≤ 1
⊢ (fun x1 x2 => x1 * x2) a b ≤ 1

Proof state:
a b : Ordinal.{u_1}
ha : a ≤ 1
hb : b ≤ 1
⊢ (fun x1 x2 => x1 * x2) a b ≤ 1

Tactic:
convert mul_le_mul' ha hb

Result:
case h.e'_4
a b : Ordinal.{u_1}
ha : a ≤ 1
hb : b ≤ 1
⊢ 1 = 1 * 1

Proof state:
⊢ Principal (fun x1 x2 => x1 * x2) 2

Tactic:
intro a b ha hb

Result:
a b : Ordinal.{u_1}
ha : a < 2
hb : b < 2
⊢ (fun x1 x2 => x1 * x2) a b < 2

Proof state:
case h.e'_4
a b : Ordinal.{u_1}
ha : a ≤ 1
hb : b ≤ 1
⊢ 1 = 1 * 1

Tactic:
exact (mul_one 1).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem bne_assoc : ∀ (x y z : Bool), ((x != y) != z) = (x != (y != z))

Proof state:
⊢ ∀ (x y z : Bool), ((x != y) != z) = (x != (y != z))

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem coeff_mul_of_lt_order {φ ψ : R⟦X⟧} {n : ℕ} (h : ↑n < ψ.order) :
    coeff R n (φ * ψ) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
⊢ (coeff R n) (φ * ψ) = 0

Tactic:
suffices coeff R n (φ * ψ) = ∑ p ∈ antidiagonal n, 0 by rw [this, Finset.sum_const_zero]

Result:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
⊢ (coeff R n) (φ * ψ) = ∑ p ∈ antidiagonal n, 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
this : (coeff R n) (φ * ψ) = ∑ p ∈ antidiagonal n, 0
⊢ (coeff R n) (φ * ψ) = 0

Tactic:
rw [this, Finset.sum_const_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
⊢ ∀ x ∈ antidiagonal n, (coeff R x.1) φ * (coeff R x.2) ψ = 0

Tactic:
intro x hx

Result:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
x : ℕ × ℕ
hx : x ∈ antidiagonal n
⊢ (coeff R x.1) φ * (coeff R x.2) ψ = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
x : ℕ × ℕ
hx : x.1 + x.2 = n
⊢ x.2 ≤ n

Tactic:
omega

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
⊢ ∑ p ∈ antidiagonal n, (coeff R p.1) φ * (coeff R p.2) ψ = ∑ p ∈ antidiagonal n, 0

Tactic:
apply Finset.sum_congr rfl

Result:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
⊢ ∀ x ∈ antidiagonal n, (coeff R x.1) φ * (coeff R x.2) ψ = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
x : ℕ × ℕ
hx : x ∈ antidiagonal n
⊢ (coeff R x.1) φ * (coeff R x.2) ψ = 0

Tactic:
refine mul_eq_zero_of_right (coeff R x.fst φ) (coeff_of_lt_order x.snd (lt_of_le_of_lt ?_ h))

Result:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
x : ℕ × ℕ
hx : x ∈ antidiagonal n
⊢ ↑x.2 ≤ ↑n

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
x : ℕ × ℕ
hx : x.1 + x.2 = n
⊢ ↑x.2 ≤ ↑n

Tactic:
norm_cast

Result:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
x : ℕ × ℕ
hx : x.1 + x.2 = n
⊢ x.2 ≤ n

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
x : ℕ × ℕ
hx : x ∈ antidiagonal n
⊢ ↑x.2 ≤ ↑n

Tactic:
rw [mem_antidiagonal] at hx

Result:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
x : ℕ × ℕ
hx : x.1 + x.2 = n
⊢ ↑x.2 ≤ ↑n

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
⊢ (coeff R n) (φ * ψ) = ∑ p ∈ antidiagonal n, 0

Tactic:
rw [coeff_mul]

Result:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
⊢ ∑ p ∈ antidiagonal n, (coeff R p.1) φ * (coeff R p.2) ψ = ∑ p ∈ antidiagonal n, 0
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
lemma IsDiameter.pointReflection_center_right (h : s.IsDiameter p₁ p₂) :
    Equiv.pointReflection s.center p₂ = p₁

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ (Equiv.pointReflection s.center) p₂ = p₁

Tactic:
rw [← h.midpoint_eq_center, Equiv.pointReflection_midpoint_right]

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem Filter.comap_coLindelof_le {f : X → Y} (hf : Continuous f) :
    (Filter.coLindelof Y).comap f ≤ Filter.coLindelof X

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
t : Set X
ht : IsLindelof t
⊢ f ⁻¹' (f '' t)ᶜ ⊆ tᶜ

Tactic:
simpa using t.subset_preimage_image f

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
⊢ comap f (coLindelof Y) ≤ coLindelof X

Tactic:
rw [(hasBasis_coLindelof.comap f).le_basis_iff hasBasis_coLindelof]

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
⊢ ∀ (i' : Set X), IsLindelof i' → ∃ i, IsLindelof i ∧ f ⁻¹' iᶜ ⊆ i'ᶜ

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
⊢ ∀ (i' : Set X), IsLindelof i' → ∃ i, IsLindelof i ∧ f ⁻¹' iᶜ ⊆ i'ᶜ

Tactic:
intro t ht

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
t : Set X
ht : IsLindelof t
⊢ ∃ i, IsLindelof i ∧ f ⁻¹' iᶜ ⊆ tᶜ

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
t : Set X
ht : IsLindelof t
⊢ ∃ i, IsLindelof i ∧ f ⁻¹' iᶜ ⊆ tᶜ

Tactic:
refine ⟨f '' t, ht.image hf, ?_⟩

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
t : Set X
ht : IsLindelof t
⊢ f ⁻¹' (f '' t)ᶜ ⊆ tᶜ
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem ne_zero {a : ℤ} {b : ℕ} (h : a.gcd b = 1) : J(a | b) ≠ 0

Proof state:
case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
hb : b = 0
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h✝ : NeZero b
⊢ J(a | b) ≠ 0

Tactic:
contrapose! h

Result:
case inr
a : ℤ
b : ℕ
h✝ : NeZero b
h : J(a | b) = 0
⊢ a.gcd ↑b ≠ 1

Proof state:
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
⊢ J(a | b) ≠ 0

Tactic:
rcases eq_zero_or_neZero b with hb | _

Result:
case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
hb : b = 0
⊢ J(a | b) ≠ 0

case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h✝ : NeZero b
⊢ J(a | b) ≠ 0

Proof state:
case inr
a : ℤ
b : ℕ
h✝ : NeZero b
h : J(a | b) = 0
⊢ a.gcd ↑b ≠ 1

Tactic:
exact eq_zero_iff_not_coprime.1 h

Result:
no goals

Proof state:
case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
hb : b = 0
⊢ J(a | b) ≠ 0

Tactic:
rw [hb, zero_right]

Result:
case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
hb : b = 0
⊢ 1 ≠ 0