harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- Twisting by a Dirichlet character `χ` distributes over convolution. -/
lemma mul_convolution_distrib {R : Type*} [CommSemiring R] {n : ℕ} (χ : DirichletCharacter R n)
    (f g : ℕ → R) :
    (((χ ·) : ℕ → R) * f) ⍟ (((χ ·) : ℕ → R) * g) = ((χ ·) : ℕ → R) * (f ⍟ g)

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
χ : DirichletCharacter R n✝
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ χ ↑p.1 * f p.1 * (χ ↑p.2 * g p.2) = χ ↑p.1 * χ ↑p.2 * (f p.1 * g p.2)

Tactic:
exact mul_mul_mul_comm ..

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
χ : DirichletCharacter R n✝
f g : ℕ → R
n : ℕ
⊢ ((fun x => χ ↑x) * f ⍟ ((fun x => χ ↑x) * g)) n = ((fun x => χ ↑x) * (f ⍟ g)) n

Tactic:
simp only [Pi.mul_apply, LSeries.convolution_def, Finset.mul_sum]

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
χ : DirichletCharacter R n✝
f g : ℕ → R
n : ℕ
⊢ ∑ x ∈ n.divisorsAntidiagonal, χ ↑x.1 * f x.1 * (χ ↑x.2 * g x.2) = ∑ i ∈ n.divisorsAntidiagonal, χ ↑n * (f i.1 * g i.2)

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
χ : DirichletCharacter R n✝
f g : ℕ → R
n : ℕ
⊢ ∑ x ∈ n.divisorsAntidiagonal, χ ↑x.1 * f x.1 * (χ ↑x.2 * g x.2) = ∑ i ∈ n.divisorsAntidiagonal, χ ↑n * (f i.1 * g i.2)

Tactic:
refine Finset.sum_congr rfl fun p hp ↦ ?_

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
χ : DirichletCharacter R n✝
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ χ ↑p.1 * f p.1 * (χ ↑p.2 * g p.2) = χ ↑n * (f p.1 * g p.2)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
χ : DirichletCharacter R n
f g : ℕ → R
⊢ (fun x => χ ↑x) * f ⍟ ((fun x => χ ↑x) * g) = (fun x => χ ↑x) * (f ⍟ g)

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
χ : DirichletCharacter R n✝
f g : ℕ → R
n : ℕ
⊢ ((fun x => χ ↑x) * f ⍟ ((fun x => χ ↑x) * g)) n = ((fun x => χ ↑x) * (f ⍟ g)) n

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
χ : DirichletCharacter R n✝
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ χ ↑p.1 * f p.1 * (χ ↑p.2 * g p.2) = χ ↑n * (f p.1 * g p.2)

Tactic:
rw [(mem_divisorsAntidiagonal.mp hp).1.symm, cast_mul, map_mul]

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
χ : DirichletCharacter R n✝
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ χ ↑p.1 * f p.1 * (χ ↑p.2 * g p.2) = χ ↑p.1 * χ ↑p.2 * (f p.1 * g p.2)
-- Mathlib/Probability/Distributions/Exponential.lean
lemma exponentialPDF_of_nonneg {r x : ℝ} (hx : 0 ≤ x) :
    exponentialPDF r x = ENNReal.ofReal (r * rexp (-(r * x)))

Proof state:
r x : ℝ
hx : 0 ≤ x
⊢ exponentialPDF r x = ENNReal.ofReal (r * rexp (-(r * x)))

Tactic:
simp only [exponentialPDF_eq, if_pos hx]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem norm_embedding_of_isReal {w : InfinitePlace K} (hw : IsReal w) (x : K) :
    ‖embedding_of_isReal hw x‖ = w x

Proof state:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
hw : w.IsReal
x : K
⊢ ‖(embedding_of_isReal hw) x‖ = w x

Tactic:
rw [← norm_embedding_eq, ← embedding_of_isReal_apply hw, Complex.norm_real]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
/-- See `ENNReal.inv_mul_cancel_left` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`. -/
protected lemma inv_mul_cancel_left' (ha₀ : a = 0 → b = 0) (ha : a = ∞ → b = 0) :
    a⁻¹ * (a * b) = b

Proof state:
case inr.inl
b : ℝ≥0∞
ha₀✝ : ⊤ = 0 → b = 0
ha : ⊤ = ⊤ → b = 0
ha₀ : ⊤ ≠ 0
⊢ ⊤⁻¹ * (⊤ * b) = b

Tactic:
simp_all

Result:
no goals

Proof state:
case inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha : a = ⊤ → b = 0
ha₀ : a ≠ 0
⊢ a⁻¹ * (a * b) = b

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Result:
case inr.inl
b : ℝ≥0∞
ha₀✝ : ⊤ = 0 → b = 0
ha : ⊤ = ⊤ → b = 0
ha₀ : ⊤ ≠ 0
⊢ ⊤⁻¹ * (⊤ * b) = b

case inr.inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha✝ : a = ⊤ → b = 0
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a⁻¹ * (a * b) = b

Proof state:
case inr.inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha✝ : a = ⊤ → b = 0
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a⁻¹ * (a * b) = b

Tactic:
simp [← mul_assoc, ENNReal.inv_mul_cancel, *]

Result:
no goals

Proof state:
a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ⊤ → b = 0
⊢ a⁻¹ * (a * b) = b

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0

Result:
case inl
b : ℝ≥0∞
ha₀ : 0 = 0 → b = 0
ha : 0 = ⊤ → b = 0
⊢ 0⁻¹ * (0 * b) = b

case inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha : a = ⊤ → b = 0
ha₀ : a ≠ 0
⊢ a⁻¹ * (a * b) = b

Proof state:
case inl
b : ℝ≥0∞
ha₀ : 0 = 0 → b = 0
ha : 0 = ⊤ → b = 0
⊢ 0⁻¹ * (0 * b) = b

Tactic:
simp_all

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem fderivWithin_comp_derivWithin_of_eq {t : Set F} (hl : DifferentiableWithinAt 𝕜 l t y)
    (hf : DifferentiableWithinAt 𝕜 f s x) (hs : MapsTo f s t) (hy : y = f x) :
    derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : F → E) (derivWithin f s x)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
y : F
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hy : y = f x
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)

Tactic:
exact fderivWithin_comp_derivWithin x hl hf hs

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
y : F
t : Set F
hl : DifferentiableWithinAt 𝕜 l t y
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hy : y = f x
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)

Tactic:
rw [hy] at hl

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
y : F
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hy : y = f x
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ofMkLEMk_comp {B A₁ A₂ : C} {f : A₁ ⟶ B} {g : A₂ ⟶ B} [Mono f] [Mono g] (h : mk f ≤ mk g) :
    ofMkLEMk f g h ≫ g = f

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst✝¹ : Mono f
inst✝ : Mono g
h : mk f ≤ mk g
⊢ ofMkLEMk f g h ≫ g = f

Tactic:
simp [ofMkLEMk]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem sup_powerset_len [DecidableEq α] (x : Multiset α) :
    (Finset.sup (Finset.range (card x + 1)) fun k => x.powersetCard k) = x.powerset

Proof state:
α : Type u_2
inst✝ : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun k => powersetCard k x) = x.powerset

Tactic:
convert bind_powerset_len x using 1

Result:
case h.e'_2
α : Type u_2
inst✝ : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun k => powersetCard k x) = (range (x.card + 1)).bind fun k => powersetCard k x

Proof state:
case h.e'_2
α : Type u_2
inst✝ : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun k => powersetCard k x) = (range (x.card + 1)).bind fun k => powersetCard k x

Tactic:
rw [Multiset.bind, Multiset.join, ← Finset.range_val, ← Finset.sum_eq_multiset_sum]

Result:
case h.e'_2
α : Type u_2
inst✝ : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun k => powersetCard k x) = ∑ x_1 ∈ Finset.range (x.card + 1), powersetCard x_1 x

Proof state:
case h.e'_2
α : Type u_2
inst✝ : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun k => powersetCard k x) = ∑ x_1 ∈ Finset.range (x.card + 1), powersetCard x_1 x

Tactic:
exact
  Eq.symm (finset_sum_eq_sup_iff_disjoint.mpr fun _ _ _ _ h => pairwise_disjoint_powersetCard x h)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_pos {p : ℝ} {x : ℝ≥0} (hx_pos : 0 < x) : 0 < x ^ p

Proof state:
p✝ : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
hp_pos : 0 < p
⊢ 0 < x ^ p

Tactic:
rw [← zero_rpow hp_pos.ne']

Result:
p✝ : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
hp_pos : 0 < p
⊢ 0 ^ p < x ^ p

Proof state:
case inl
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_pos : 0 < p
⊢ 0 < x ^ p

Tactic:
exact rpow_pos_of_nonneg hp_pos

Result:
no goals

Proof state:
case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ p

Tactic:
rw [← neg_neg p, rpow_neg, inv_pos]

Result:
case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ (-p)

Proof state:
case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ (-p)

Tactic:
exact rpow_pos_of_nonneg (neg_pos.mpr hp_neg)

Result:
no goals

Proof state:
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
⊢ ∀ {p : ℝ}, 0 < p → 0 < x ^ p

Tactic:
intro p hp_pos

Result:
p✝ : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
hp_pos : 0 < p
⊢ 0 < x ^ p

Proof state:
p✝ : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
hp_pos : 0 < p
⊢ 0 ^ p < x ^ p

Tactic:
exact rpow_lt_rpow hx_pos hp_pos

Result:
no goals

Proof state:
case inr.inl
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
⊢ 0 < x ^ 0

Tactic:
simp only [zero_lt_one, rpow_zero]

Result:
no goals

Proof state:
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
⊢ 0 < x ^ p

Tactic:
rcases lt_trichotomy (0 : ℝ) p with (hp_pos | rfl | hp_neg)

Result:
case inl
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_pos : 0 < p
⊢ 0 < x ^ p

case inr.inl
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
⊢ 0 < x ^ 0

case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ p

Proof state:
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
⊢ 0 < x ^ p

Tactic:
have rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p := by
  intro p hp_pos
  rw [← zero_rpow hp_pos.ne']
  exact rpow_lt_rpow hx_pos hp_pos

Result:
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
⊢ 0 < x ^ p
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem sub_zero {X Y : C} (a : X ⟶ Y) : a - 0 = a

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ prod.lift a 0 ≫ σ = a

Tactic:
conv_lhs =>
  congr; congr; rw [← Category.comp_id a]
  case a.g => rw [show 0 = a ≫ (0 : Y ⟶ Y) by simp]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ prod.lift (a ≫ 𝟙 Y) (a ≫ 0) ≫ σ = a

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ prod.lift (a ≫ 𝟙 Y) (a ≫ 0) ≫ σ = a

Tactic:
rw [← prod.comp_lift, Category.assoc, lift_σ, Category.comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ 0 = a ≫ 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a - 0 = a

Tactic:
rw [sub_def]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ prod.lift a 0 ≫ σ = a
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem xn_modEq_x2n_add (n j) : xn a1 (2 * n + j) + xn a1 j ≡ 0 [MOD xn a1 n]

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 (2 * n + j) + xn a1 j ≡ 0 [MOD xn a1 n]

Tactic:
rw [two_mul, add_assoc, xn_add, add_assoc, ← zero_add 0]

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 n * xn a1 (n + j) + (Pell.d a1 * yn a1 n * yn a1 (n + j) + xn a1 j) ≡ 0 + 0 [MOD xn a1 n]

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ Pell.d a1 * yn a1 n * yn a1 (n + j) + xn a1 j ≡ 0 [MOD xn a1 n]

Tactic:
rw [yn_add, left_distrib, add_assoc, ← zero_add 0]

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ Pell.d a1 * yn a1 n * (xn a1 n * yn a1 j) + (Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j) ≡ 0 + 0 [MOD
    xn a1 n]

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ Pell.d a1 * yn a1 n * (xn a1 n * yn a1 j) + (Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j) ≡ 0 + 0 [MOD
    xn a1 n]

Tactic:
exact
  ((dvd_mul_right _ _).mul_left _).modEq_zero_nat.add (xn_modEq_x2n_add_lem _ _ _).modEq_zero_nat

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 n * xn a1 (n + j) + (Pell.d a1 * yn a1 n * yn a1 (n + j) + xn a1 j) ≡ 0 + 0 [MOD xn a1 n]

Tactic:
refine (dvd_mul_right (xn a1 n) (xn a1 (n + j))).modEq_zero_nat.add ?_

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ Pell.d a1 * yn a1 n * yn a1 (n + j) + xn a1 j ≡ 0 [MOD xn a1 n]
-- Mathlib/Data/Finset/NoncommProd.lean
theorem mul_noncommProd_erase [DecidableEq α] (s : Finset α) {a : α} (h : a ∈ s) (f : α → β) (comm)
    (comm' := fun _ hx _ hy hxy ↦ comm (s.mem_of_mem_erase hx) (s.mem_of_mem_erase hy) hxy) :
    f a * (s.erase a).noncommProd f comm' = s.noncommProd f comm

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
f : α → β
comm : (↑s).Pairwise (Commute on f)
comm' : optParam (∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → (Commute on f) x x_1) ⋯
⊢ f a * (s.erase a).noncommProd f comm' = s.noncommProd f comm

Tactic:
simpa only [← Multiset.map_erase_of_mem _ _ h] using
  Multiset.mul_noncommProd_erase (s.1.map f) (Multiset.mem_map_of_mem f h) _

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
f : α → β
comm : (↑s).Pairwise (Commute on f)
comm' : optParam (∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → (Commute on f) x x_1) ⋯
⊢ f a * (s.erase a).noncommProd f comm' = s.noncommProd f comm

Tactic:
classical
simpa only [← Multiset.map_erase_of_mem _ _ h] using
  Multiset.mul_noncommProd_erase (s.1.map f) (Multiset.mem_map_of_mem f h) _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem length_unattach {p : α → Prop} {l : List { x // p x }} :
    l.unattach.length = l.length

Proof state:
α : Type u_1
p : α → Prop
l : List { x // p x }
⊢ (map (fun x => x.val) l).length = l.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : List { x // p x }
⊢ l.unattach.length = l.length

Tactic:
unfold unattach

Result:
α : Type u_1
p : α → Prop
l : List { x // p x }
⊢ (map (fun x => x.val) l).length = l.length
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem IsTransitive.sUnion' (H : ∀ y ∈ x, IsTransitive y) :
    (⋃₀ x : ZFSet).IsTransitive := fun y hy z hz => by
  rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩
  exact mem_sUnion_of_mem ((H w hw).mem_trans hz hw') hw

Proof state:
x : ZFSet.{u}
H : ∀ y ∈ x, y.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ ⋃₀ x

Tactic:
rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩

Result:
case intro.intro
x : ZFSet.{u}
H : ∀ y ∈ x, y.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
w : ZFSet.{u}
hw : w ∈ x
hw' : y ∈ w
⊢ z ∈ ⋃₀ x

Proof state:
case intro.intro
x : ZFSet.{u}
H : ∀ y ∈ x, y.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
w : ZFSet.{u}
hw : w ∈ x
hw' : y ∈ w
⊢ z ∈ ⋃₀ x

Tactic:
exact mem_sUnion_of_mem ((H w hw).mem_trans hz hw') hw

Result:
no goals
-- Mathlib/Data/Matrix/PEquiv.lean
theorem toMatrix_symm [DecidableEq m] [DecidableEq n] [Zero α] [One α] (f : m ≃. n) :
    (f.symm.toMatrix : Matrix n m α) = f.toMatrixᵀ

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
⊢ f.symm.toMatrix = f.toMatrixᵀ

Tactic:
ext

Result:
case a
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
i✝ : n
j✝ : m
⊢ f.symm.toMatrix i✝ j✝ = f.toMatrixᵀ i✝ j✝

Proof state:
case a
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
i✝ : n
j✝ : m
⊢ (if i✝ ∈ f j✝ then 1 else 0) = of (fun x y => if x ∈ f y then 1 else 0) i✝ j✝

Tactic:
congr

Result:
no goals

Proof state:
case a
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
i✝ : n
j✝ : m
⊢ f.symm.toMatrix i✝ j✝ = f.toMatrixᵀ i✝ j✝

Tactic:
simp only [transpose, mem_iff_mem f, toMatrix_apply]

Result:
case a
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
i✝ : n
j✝ : m
⊢ (if i✝ ∈ f j✝ then 1 else 0) = of (fun x y => if x ∈ f y then 1 else 0) i✝ j✝
-- Mathlib/Topology/Order/Basic.lean
theorem SecondCountableTopology.of_separableSpace_orderTopology [OrderTopology α] [DenselyOrdered α]
    [SeparableSpace α] : SecondCountableTopology α

Proof state:
case intro.intro
α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : SeparableSpace α
s : Set α
hc : s.Countable
hd : Dense s
⊢ SecondCountableTopology α

Tactic:
refine ⟨⟨_, ?_, hd.topology_eq_generateFrom⟩⟩

Result:
case intro.intro
α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : SeparableSpace α
s : Set α
hc : s.Countable
hd : Dense s
⊢ (Ioi '' s ∪ Iio '' s).Countable

Proof state:
case intro.intro
α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : SeparableSpace α
s : Set α
hc : s.Countable
hd : Dense s
⊢ (Ioi '' s ∪ Iio '' s).Countable

Tactic:
exact (hc.image _).union (hc.image _)

Result:
no goals

Proof state:
α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : SeparableSpace α
⊢ SecondCountableTopology α

Tactic:
rcases exists_countable_dense α with ⟨s, hc, hd⟩

Result:
case intro.intro
α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : SeparableSpace α
s : Set α
hc : s.Countable
hd : Dense s
⊢ SecondCountableTopology α
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem mem_discrete_iff {c d : C} (f : c ⟶ d) :
    f ∈ discrete.arrows c d ↔ ∃ h : c = d, f = eqToHom h :=
  ⟨by rintro ⟨⟩; exact ⟨rfl, rfl⟩, by rintro ⟨rfl, rfl⟩; constructor⟩

Proof state:
C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
⊢ f ∈ discrete.arrows c d → ∃ (h : c = d), f = eqToHom h

Tactic:
rintro ⟨⟩

Result:
case id
C : Type u
inst✝ : Groupoid C
c d : C
⊢ ∃ (h : c = c), 𝟙 c = eqToHom h

Proof state:
case id
C : Type u
inst✝ : Groupoid C
c d : C
⊢ ∃ (h : c = c), 𝟙 c = eqToHom h

Tactic:
exact ⟨rfl, rfl⟩

Result:
no goals

Proof state:
case intro
C : Type u
inst✝ : Groupoid C
c : C
⊢ eqToHom ⋯ ∈ discrete.arrows c c

Tactic:
constructor

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
⊢ (∃ (h : c = d), f = eqToHom h) → f ∈ discrete.arrows c d

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case intro
C : Type u
inst✝ : Groupoid C
c : C
⊢ eqToHom ⋯ ∈ discrete.arrows c c
-- Mathlib/Data/List/Dedup.lean
theorem dedup_cons_of_mem' {a : α} {l : List α} (h : a ∈ dedup l) : dedup (a :: l) = dedup l :=
  pwFilter_cons_of_neg <| by simpa only [forall_mem_ne, not_not] using h

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l.dedup
⊢ ¬∀ b ∈ pwFilter (fun x1 x2 => x1 ≠ x2) l, a ≠ b

Tactic:
simpa only [forall_mem_ne, not_not] using h

Result:
no goals
-- Mathlib/FieldTheory/AlgebraicClosure.lean
theorem map_eq_of_algEquiv (i : E ≃ₐ[F] K) :
    (algebraicClosure F E).map i = algebraicClosure F K :=
  (map_le_of_algHom i.toAlgHom).antisymm
    (fun x h ↦ ⟨_, (map_mem_algebraicClosure_iff i.symm).2 h, by simp⟩)

Proof state:
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra F K
i : E ≃ₐ[F] K
x : K
h : x ∈ algebraicClosure F K
⊢ ↑↑i (↑i.symm x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem not_isUnit (hp : p.IsUnitTrinomial) : ¬IsUnit p

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ¬IsUnit (trinomial k m n ↑u ↑v ↑w)

Tactic:
exact fun h =>
  ne_zero_of_lt hmn
    ((trinomial_natDegree hkm hmn w.ne_zero).symm.trans
      (natDegree_eq_of_degree_eq_some (degree_eq_zero_of_isUnit h)))

Result:
no goals

Proof state:
p : ℤ[X]
hp : p.IsUnitTrinomial
⊢ ¬IsUnit p

Tactic:
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ¬IsUnit (trinomial k m n ↑u ↑v ↑w)
-- Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean
theorem liminf_ae_eq_of_forall_ae_eq (s : ℕ → Set α) {t : Set α}
    (h : ∀ n, s n =ᵐ[μ] t) : liminf (α := Set α) s atTop =ᵐ[μ] t

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), s n =ᶠ[ae μ] t
⊢ liminf s atTop =ᶠ[ae μ] t

Tactic:
simp only [eventuallyEq_set, ← eventually_countable_forall] at h

Result:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
t : Set α
h : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
⊢ liminf s atTop =ᶠ[ae μ] t

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
t : Set α
h : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
⊢ liminf s atTop =ᶠ[ae μ] t

Tactic:
refine eventuallyEq_set.2 <| h.mono fun x hx ↦ ?_

Result:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
t : Set α
h : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
x : α
hx : ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
⊢ x ∈ liminf s atTop ↔ x ∈ t

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
t : Set α
h : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
x : α
hx : ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
⊢ x ∈ liminf s atTop ↔ x ∈ t

Tactic:
simp only [mem_liminf_iff_eventually_mem, hx, eventually_const]

Result:
no goals