harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
lemma idemSnd_compl : (1 : AddMonoid.End (WithLp p (α × β))) - idemSnd = idemFst

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
⊢ 1 - idemSnd = idemFst

Tactic:
rw [← idemFst_add_idemSnd, add_sub_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_zero : ⌈(0 : α)⌉ = 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
⊢ ⌈0⌉ = 0

Tactic:
rw [← cast_zero, ceil_intCast]

Result:
no goals
-- Mathlib/Data/Sym/Basic.lean
theorem fill_filterNe [DecidableEq α] (a : α) (m : Sym α n) :
    (m.filterNe a).2.fill a (m.filterNe a).1 = m :=
  Sym.ext
    (by
      rw [coe_fill, filterNe, ← val_eq_coe, Subtype.coe_mk, Fin.val_mk]
      ext b; dsimp
      rw [count_add, count_filter, Sym.coe_replicate, count_replicate]
      obtain rfl | h := eq_or_ne a b
      · rw [if_pos rfl, if_neg (not_not.2 rfl), zero_add]
      · rw [if_pos h, if_neg h, add_zero])

Proof state:
case a
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter (fun x => a ≠ x) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m

Tactic:
dsimp

Result:
case a
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter (fun x => ¬a = x) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ↑(fill a (filterNe a m).fst (filterNe a m).snd) = ↑m

Tactic:
rw [coe_fill, filterNe, ← val_eq_coe, Subtype.coe_mk, Fin.val_mk]

Result:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ filter (fun x => a ≠ x) ↑m + ↑(replicate (count a ↑m) a) = ↑m

Proof state:
case a.inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ ((if ¬a = b then count b ↑m else 0) + if a = b then count a ↑m else 0) = count b ↑m

Tactic:
rw [if_pos h, if_neg h, add_zero]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ filter (fun x => a ≠ x) ↑m + ↑(replicate (count a ↑m) a) = ↑m

Tactic:
ext b

Result:
case a
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter (fun x => a ≠ x) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m

Proof state:
case a
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter (fun x => ¬a = x) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m

Tactic:
rw [count_add, count_filter, Sym.coe_replicate, count_replicate]

Result:
case a
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ ((if ¬a = b then count b ↑m else 0) + if a = b then count a ↑m else 0) = count b ↑m

Proof state:
case a
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ ((if ¬a = b then count b ↑m else 0) + if a = b then count a ↑m else 0) = count b ↑m

Tactic:
obtain rfl | h := eq_or_ne a b

Result:
case a.inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ((if ¬a = a then count a ↑m else 0) + if a = a then count a ↑m else 0) = count a ↑m

case a.inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ ((if ¬a = b then count b ↑m else 0) + if a = b then count a ↑m else 0) = count b ↑m

Proof state:
case a.inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ((if ¬a = a then count a ↑m else 0) + if a = a then count a ↑m else 0) = count a ↑m

Tactic:
rw [if_pos rfl, if_neg (not_not.2 rfl), zero_add]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
/-- Any intersection of translates of two sets `s` and `t` can be covered by a single translate of
`(s⁻¹ * s) ∩ (t⁻¹ * t)`.

This is useful to show that the intersection of approximate subgroups is an approximate subgroup. -/
@[to_additive
"Any intersection of translates of two sets `s` and `t` can be covered by a single translate of
`(-s + s) ∩ (-t + t)`.

This is useful to show that the intersection of approximate subgroups is an approximate subgroup."]
lemma exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul (s t : Set α) (a b : α) :
    ∃ z : α, a • s ∩ b • t ⊆ z • ((s⁻¹ * s) ∩ (t⁻¹ * t))

Proof state:
case inr.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
refine ⟨z, ?_⟩

Result:
case inr.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Proof state:
case inr.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
calc
  a • s ∩ b • t ⊆ (z • s⁻¹) * s ∩ ((z • t⁻¹) * t) := by
    gcongr <;> apply smul_set_subset_mul <;> simpa
  _ = z • ((s⁻¹ * s) ∩ (t⁻¹ * t)) := by simp_rw [Set.smul_set_inter, smul_mul_assoc]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ z • s⁻¹ * s ∩ (z • t⁻¹ * t) = z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
simp_rw [Set.smul_set_inter, smul_mul_assoc]

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
hAB : a • s ∩ b • t = ∅
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
exact ⟨1, by simp [hAB]⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a • s ∩ b • t ⊆ z • s⁻¹ * s ∩ (z • t⁻¹ * t)

Tactic:
gcongr <;> apply smul_set_subset_mul <;> simpa

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
obtain hAB | ⟨z, hzA, hzB⟩ := (a • s ∩ b • t).eq_empty_or_nonempty

Result:
case inl
α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
hAB : a • s ∩ b • t = ∅
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

case inr.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Proof state:
α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
hAB : a • s ∩ b • t = ∅
⊢ a • s ∩ b • t ⊆ 1 • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
simp [hAB]

Result:
no goals
-- Mathlib/Data/ULift.lean
theorem up_inj {x y : α} : up x = up y ↔ x = y

Proof state:
α : Sort u
x y : α
⊢ { down := x } = { down := y } ↔ x = y

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem whiskerLeft_iff {f g : a ⟶ b} (η θ : f ⟶ g) : 𝟙 a ◁ η = 𝟙 a ◁ θ ↔ η = θ

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η θ : f ⟶ g
⊢ 𝟙 a ◁ η = 𝟙 a ◁ θ ↔ η = θ

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem one_add_natCast (m : ℕ) : 1 + (m : Ordinal) = succ m

Proof state:
m : ℕ
⊢ ↑(m + 1) = ↑(succ m)

Tactic:
rfl

Result:
no goals

Proof state:
m : ℕ
⊢ 1 + ↑m = ↑(succ m)

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, add_comm]

Result:
m : ℕ
⊢ ↑(m + 1) = ↑(succ m)
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
lemma count_take_firstReturn_add_one :
    (p.toList.take (p.firstReturn + 1)).count U = (p.toList.take (p.firstReturn + 1)).count D

Proof state:
p : DyckWord
h : p ≠ 0
this :
  decide
      (count U
          (List.take
            ((range
                  (↑p).length)[findIdx
                  (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p)))
                  (range (↑p).length)] +
              1)
            ↑p) =
        count D
          (List.take
            ((range
                  (↑p).length)[findIdx
                  (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p)))
                  (range (↑p).length)] +
              1)
            ↑p)) =
    true
⊢ count U (List.take (p.firstReturn + 1) ↑p) = count D (List.take (p.firstReturn + 1) ↑p)

Tactic:
simpa using this

Result:
no goals

Proof state:
p : DyckWord
h : p ≠ 0
⊢ count U (List.take (p.firstReturn + 1) ↑p) = count D (List.take (p.firstReturn + 1) ↑p)

Tactic:
have := findIdx_getElem (w := (length_range p.toList.length).symm ▸ firstReturn_lt_length h)

Result:
p : DyckWord
h : p ≠ 0
this :
  decide
      (count U
          (List.take
            ((range
                  (↑p).length)[findIdx
                  (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p)))
                  (range (↑p).length)] +
              1)
            ↑p) =
        count D
          (List.take
            ((range
                  (↑p).length)[findIdx
                  (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p)))
                  (range (↑p).length)] +
              1)
            ↑p)) =
    true
⊢ count U (List.take (p.firstReturn + 1) ↑p) = count D (List.take (p.firstReturn + 1) ↑p)
-- Mathlib/Algebra/Group/Nat/Range.lean
theorem disjoint_range_addRightEmbedding (a : ℕ) (s : Finset ℕ) :
    Disjoint (range a) (map (addRightEmbedding a) s)

Proof state:
a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addRightEmbedding a) s)

Tactic:
rw [← addLeftEmbedding_eq_addRightEmbedding]

Result:
a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addLeftEmbedding a) s)

Proof state:
a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addLeftEmbedding a) s)

Tactic:
apply disjoint_range_addLeftEmbedding

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem gcd_fib_add_mul_self (m n : ℕ) : ∀ k, gcd (fib m) (fib (n + k * m)) = gcd (fib m) (fib n)
  | 0 => by simp
  | k + 1 => by
    rw [← gcd_fib_add_mul_self m n k, add_mul, ← add_assoc, one_mul, gcd_fib_add_self _ _]

Proof state:
m n : ℕ
⊢ (fib m).gcd (fib (n + 0 * m)) = (fib m).gcd (fib n)

Tactic:
simp

Result:
no goals

Proof state:
m n k : ℕ
⊢ (fib m).gcd (fib (n + (k + 1) * m)) = (fib m).gcd (fib n)

Tactic:
rw [← gcd_fib_add_mul_self m n k, add_mul, ← add_assoc, one_mul, gcd_fib_add_self _ _]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem measure_le_le_exp_mul_mgf [IsFiniteMeasure μ] (ε : ℝ) (ht : t ≤ 0)
    (h_int : Integrable (fun ω => exp (t * X ω)) μ) :
    (μ {ω | X ω ≤ ε}).toReal ≤ exp (-t * ε) * mgf X μ t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ (μ {ω | X ω ≤ ε}).toReal ≤ rexp (- -t * -ε) * mgf (-X) μ (-t)

Tactic:
refine Eq.trans_le ?_ (measure_ge_le_exp_mul_mgf (-ε) (neg_nonneg.mpr ht) ?_)

Result:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ (μ {ω | X ω ≤ ε}).toReal = (μ {ω | -ε ≤ (-X) ω}).toReal

case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ Integrable (fun ω => rexp (-t * (-X) ω)) μ

Proof state:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ Integrable (fun ω => rexp (t * X ω)) μ

Tactic:
exact h_int

Result:
no goals

Proof state:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ (μ {ω | X ω ≤ ε}).toReal = (μ {ω | -ε ≤ (-X) ω}).toReal

Tactic:
congr with ω

Result:
case refine_1.e_a.h.e_6.h.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ω : Ω
⊢ ω ∈ {ω | X ω ≤ ε} ↔ ω ∈ {ω | -ε ≤ (-X) ω}

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ (μ {ω | X ω ≤ ε}).toReal ≤ rexp (-t * ε) * mgf X μ t

Tactic:
rw [← neg_neg t, ← mgf_neg, neg_neg, ← neg_mul_neg (-t)]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ (μ {ω | X ω ≤ ε}).toReal ≤ rexp (- -t * -ε) * mgf (-X) μ (-t)

Proof state:
case refine_1.e_a.h.e_6.h.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ω : Ω
⊢ ω ∈ {ω | X ω ≤ ε} ↔ ω ∈ {ω | -ε ≤ (-X) ω}

Tactic:
simp only [Pi.neg_apply, neg_le_neg_iff]

Result:
no goals

Proof state:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ Integrable (fun ω => rexp (-t * (-X) ω)) μ

Tactic:
simp_rw [Pi.neg_apply, neg_mul_neg]

Result:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ Integrable (fun ω => rexp (t * X ω)) μ
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem zero_mul (a : Rat) : 0 * a = 0

Proof state:
a : Rat
⊢ 0 * a = 0

Tactic:
simp [mul_def]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
/-- The fundamental cocircuit of `X` and `e` has the junk value `{e}` if `e ∉ X` -/
lemma fundCocircuit_eq_of_not_mem (M : Matroid α) (heX : e ∉ X) : M.fundCocircuit e X = {e}

Proof state:
case neg
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∉ M.E
⊢ M.fundCocircuit e X = {e}

Tactic:
rw [fundCocircuit_eq_of_not_mem_ground _ he]

Result:
no goals

Proof state:
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
⊢ M.fundCocircuit e X = {e}

Tactic:
by_cases he : e ∈ M.E

Result:
case pos
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∈ M.E
⊢ M.fundCocircuit e X = {e}

case neg
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∉ M.E
⊢ M.fundCocircuit e X = {e}

Proof state:
case pos
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∈ M.E
⊢ e ∈ M✶.E \ X

Tactic:
exact ⟨he, heX⟩

Result:
no goals

Proof state:
case pos
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∈ M.E
⊢ M.fundCocircuit e X = {e}

Tactic:
rw [fundCocircuit, fundCircuit_eq_of_mem]

Result:
case pos
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∈ M.E
⊢ e ∈ M✶.E \ X
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_eraseKey_of_false [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
    (hka : (k == a) = false) : getValue? a (eraseKey k l) = getValue? a l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
hka : (k == a) = false
⊢ getValue? a (eraseKey k l) = getValue? a l

Tactic:
simp [getValue?_eq_getEntry?, getEntry?_eraseKey_of_false hka]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem unzip_zip {l₁ : Array α} {l₂ : Array β} (h : l₁.size = l₂.size) :
    unzip (zip l₁ l₂) = (l₁, l₂)

Proof state:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
h : { toList := toList✝ }.size = l₂.size
⊢ ({ toList := toList✝ }.zip l₂).unzip = ({ toList := toList✝ }, l₂)

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
h : { toList := toList✝¹ }.size = { toList := toList✝ }.size
⊢ ({ toList := toList✝¹ }.zip { toList := toList✝ }).unzip = ({ toList := toList✝¹ }, { toList := toList✝ })

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
h : { toList := toList✝¹ }.size = { toList := toList✝ }.size
⊢ ({ toList := toList✝¹ }.zip { toList := toList✝ }).unzip = ({ toList := toList✝¹ }, { toList := toList✝ })

Tactic:
simp_all only [size_toArray, List.zip_toArray, List.unzip_toArray, List.unzip_zip, Prod.map_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₁.size = l₂.size
⊢ (l₁.zip l₂).unzip = (l₁, l₂)

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
h : { toList := toList✝ }.size = l₂.size
⊢ ({ toList := toList✝ }.zip l₂).unzip = ({ toList := toList✝ }, l₂)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem Function.const_comp {f : α → β} {c : γ} :
    (Function.const β c ∘ f) = Function.const α c

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
c : γ
⊢ const β c ∘ f = const α c

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
/-- `succ` commutes with `succAbove`. -/
@[simp] lemma succ_succAbove_succ {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
    i.succ.succAbove j.succ = (i.succAbove j).succ

Proof state:
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ

Tactic:
rwa [succAbove_of_castSucc_lt _ _ h, succAbove_succ_of_le, succ_castSucc]

Result:
no goals

Proof state:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i < j.succ
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ

Tactic:
rw [succAbove_of_lt_succ _ _ h, succAbove_succ_of_lt _ _ h]

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ

Tactic:
obtain h | h := i.lt_or_le (succ j)

Result:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i < j.succ
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ

case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean
theorem set_walk_self_length_zero_eq (u : V) : {p : G.Walk u u | p.length = 0} = {Walk.nil}

Proof state:
V : Type u
G : SimpleGraph V
u : V
⊢ {p | p.length = 0} = {Walk.nil}

Tactic:
ext p

Result:
case h
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p ∈ {p | p.length = 0} ↔ p ∈ {Walk.nil}

Proof state:
case h
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p ∈ {p | p.length = 0} ↔ p ∈ {Walk.nil}

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Ext.lean
theorem toNonUnitalNonAssocSemiring_injective :
    Function.Injective (@toNonUnitalNonAssocSemiring R)

Proof state:
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocRing R
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Result:
case h_add.h.h
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocRing R
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
x y : R
⊢ x + y = x + y

case h_mul.h.h
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocRing R
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
x y : R
⊢ x * y = x * y

Proof state:
R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocSemiring R)

Tactic:
intro _ _ h

Result:
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocRing R
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
⊢ a₁✝ = a₂✝
-- Mathlib/RingTheory/NonUnitalSubring/Defs.lean
theorem coe_eq_zero_iff {x : s} : (x : R) = 0 ↔ x = 0

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : NonUnitalSubring R
x : ↥s
⊢ ↑x = 0 ↔ x = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
theorem hasProd_iff_tendsto_nat [T2Space M] {f : ℕ → M} (hf : Multipliable f) :
    HasProd f m ↔ Tendsto (fun n : ℕ ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : T2Space M
f : ℕ → M
hf : Multipliable f
⊢ HasProd f m ↔ Tendsto (fun n => ∏ i ∈ range n, f i) atTop (𝓝 m)

Tactic:
refine ⟨fun h ↦ h.tendsto_prod_nat, fun h ↦ ?_⟩

Result:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : T2Space M
f : ℕ → M
hf : Multipliable f
h : Tendsto (fun n => ∏ i ∈ range n, f i) atTop (𝓝 m)
⊢ HasProd f m

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : T2Space M
f : ℕ → M
hf : Multipliable f
h : Tendsto (fun n => ∏ i ∈ range n, f i) atTop (𝓝 m)
⊢ HasProd f m

Tactic:
rw [tendsto_nhds_unique h hf.hasProd.tendsto_prod_nat]

Result:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : T2Space M
f : ℕ → M
hf : Multipliable f
h : Tendsto (fun n => ∏ i ∈ range n, f i) atTop (𝓝 m)
⊢ HasProd f (∏' (b : ℕ), f b)

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : T2Space M
f : ℕ → M
hf : Multipliable f
h : Tendsto (fun n => ∏ i ∈ range n, f i) atTop (𝓝 m)
⊢ HasProd f (∏' (b : ℕ), f b)

Tactic:
exact hf.hasProd

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem le_iff_exists_sup : a ≤ b ↔ ∃ c, b = a ⊔ c

Proof state:
case mp
α : Type u
inst✝ : SemilatticeSup α
a b : α
h : a ≤ b
⊢ ∃ c, b = a ⊔ c

Tactic:
exact ⟨b, (sup_eq_right.mpr h).symm⟩

Result:
no goals

Proof state:
case mp
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ≤ b → ∃ c, b = a ⊔ c

Tactic:
intro h

Result:
case mp
α : Type u
inst✝ : SemilatticeSup α
a b : α
h : a ≤ b
⊢ ∃ c, b = a ⊔ c

Proof state:
case mpr.intro
α : Type u
inst✝ : SemilatticeSup α
a c : α
⊢ a ≤ a ⊔ c

Tactic:
exact le_sup_left

Result:
no goals

Proof state:
case mpr
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ (∃ c, b = a ⊔ c) → a ≤ b

Tactic:
rintro ⟨c, rfl : _ = _ ⊔ _⟩

Result:
case mpr.intro
α : Type u
inst✝ : SemilatticeSup α
a c : α
⊢ a ≤ a ⊔ c

Proof state:
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ≤ b ↔ ∃ c, b = a ⊔ c

Tactic:
constructor

Result:
case mp
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ≤ b → ∃ c, b = a ⊔ c

case mpr
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ (∃ c, b = a ⊔ c) → a ≤ b
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_natCast [DecidableEq n] [Semiring α] [StarRing α] (d : ℕ) :
    (d : Matrix n n α)ᴴ = d

Proof state:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Semiring α
inst✝ : StarRing α
d : ℕ
⊢ (↑d)ᴴ = ↑d

Tactic:
simp [conjTranspose, Matrix.map_natCast, diagonal_natCast]

Result:
no goals
-- Mathlib/Data/Nat/BinaryRec.lean
theorem bit_val (b n) : bit b n = 2 * n + b.toNat

Proof state:
b : Bool
n : Nat
⊢ bit b n = 2 * n + b.toNat

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
@[simp] lemma analyticWithinAt_univ :
    AnalyticWithinAt 𝕜 f univ x ↔ AnalyticAt 𝕜 f x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ AnalyticWithinAt 𝕜 f univ x ↔ AnalyticAt 𝕜 f x

Tactic:
simp [AnalyticWithinAt, AnalyticAt]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Pi.lean
theorem pi_eq_sum_univ {ι : Type*} [Fintype ι] [DecidableEq ι] {R : Type*} [Semiring R]
    (x : ι → R) : x = ∑ i, (x i) • fun j => if i = j then (1 : R) else 0

Proof state:
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
R : Type u_5
inst✝ : Semiring R
x : ι → R
⊢ x = ∑ i : ι, x i • fun j => if i = j then 1 else 0

Tactic:
ext

Result:
case h
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
R : Type u_5
inst✝ : Semiring R
x : ι → R
x✝ : ι
⊢ x x✝ = (∑ i : ι, x i • fun j => if i = j then 1 else 0) x✝

Proof state:
case h
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
R : Type u_5
inst✝ : Semiring R
x : ι → R
x✝ : ι
⊢ x x✝ = (∑ i : ι, x i • fun j => if i = j then 1 else 0) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem comap_iSup {β ι} (f : α → β) (m : ι → OuterMeasure β) :
    comap f (⨆ i, m i) = ⨆ i, comap f (m i) :=
  ext fun s => by simp only [comap_apply, iSup_apply]

Proof state:
α : Type u_1
β : Type u_3
ι : Sort u_4
f : α → β
m : ι → OuterMeasure β
s : Set α
⊢ ((comap f) (⨆ i, m i)) s = (⨆ i, (comap f) (m i)) s

Tactic:
simp only [comap_apply, iSup_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem length_take : ∀ (i : Nat) (l : List α), length (take i l) = min i (length l)
  | 0, l => by simp [Nat.zero_min]
  | succ n, [] => by simp [Nat.min_zero]
  | succ n, _ :: l => by simp [Nat.succ_min_succ, length_take]

Proof state:
α : Type u_1
l : List α
⊢ (take 0 l).length = min 0 l.length

Tactic:
simp [Nat.zero_min]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
head✝ : α
l : List α
⊢ (take n.succ (head✝ :: l)).length = min n.succ (head✝ :: l).length

Tactic:
simp [Nat.succ_min_succ, length_take]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
⊢ (take n.succ []).length = min n.succ [].length

Tactic:
simp [Nat.min_zero]

Result:
no goals