harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/PNat/Factors.lean
theorem to_ofPNatMultiset (v : Multiset ℕ+) (h) : (ofPNatMultiset v h : Multiset ℕ+) = v

Proof state:
case h.h
v : Multiset ℕ+
h✝ : ∀ p ∈ v, p.Prime
p : ℕ+
h : p.Prime
⊢ Coe.coe ⟨↑p, h⟩ = id p

Tactic:
apply Subtype.eq

Result:
case h.h.a
v : Multiset ℕ+
h✝ : ∀ p ∈ v, p.Prime
p : ℕ+
h : p.Prime
⊢ ↑(Coe.coe ⟨↑p, h⟩) = ↑(id p)

Proof state:
v : Multiset ℕ+
h : ∀ p ∈ v, p.Prime
⊢ (fun p h => Coe.coe ⟨↑p, h⟩) = fun p x => id p

Tactic:
funext p h

Result:
case h.h
v : Multiset ℕ+
h✝ : ∀ p ∈ v, p.Prime
p : ℕ+
h : p.Prime
⊢ Coe.coe ⟨↑p, h⟩ = id p

Proof state:
v : Multiset ℕ+
h : ∀ p ∈ v, p.Prime
⊢ (ofPNatMultiset v h).toPNatMultiset = v

Tactic:
dsimp [ofPNatMultiset, toPNatMultiset]

Result:
v : Multiset ℕ+
h : ∀ p ∈ v, p.Prime
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => ⟨↑p, hp⟩) v h) = v

Proof state:
v : Multiset ℕ+
h : ∀ p ∈ v, p.Prime
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => ⟨↑p, hp⟩) v h) = v

Tactic:
have : (fun (p : ℕ+) (h : p.Prime) => (Coe.coe : Nat.Primes → ℕ+) ⟨p, h⟩) = fun p _ => id p := by
  funext p h
  apply Subtype.eq
  rfl

Result:
v : Multiset ℕ+
h : ∀ p ∈ v, p.Prime
this : (fun p h => Coe.coe ⟨↑p, h⟩) = fun p x => id p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => ⟨↑p, hp⟩) v h) = v

Proof state:
v : Multiset ℕ+
h : ∀ p ∈ v, p.Prime
this : (fun p h => Coe.coe ⟨↑p, h⟩) = fun p x => id p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => ⟨↑p, hp⟩) v h) = v

Tactic:
rw [Multiset.map_pmap, this, Multiset.pmap_eq_map, Multiset.map_id]

Result:
no goals

Proof state:
case h.h.a
v : Multiset ℕ+
h✝ : ∀ p ∈ v, p.Prime
p : ℕ+
h : p.Prime
⊢ ↑(Coe.coe ⟨↑p, h⟩) = ↑(id p)

Tactic:
rfl

Result:
no goals
-- Mathlib/ModelTheory/DirectLimit.lean
theorem lift_of {i} (x : G i) : lift L ι G f g Hg (of L ι G f i x) = g i x

Proof state:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
i : ι
x : G i
⊢ (lift L ι G f g Hg) ((of L ι G f i) x) = (g i) x

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem range_eval_eq_rootSet_minpoly :
    (range fun φ : K →+* A => φ x) = (minpoly ℚ x).rootSet A

Proof state:
case h.e'_2
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
⊢ (range fun φ => φ x) = range fun ψ => ψ x

Tactic:
ext a

Result:
case h.e'_2.h
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
a : A
⊢ (a ∈ range fun φ => φ x) ↔ a ∈ range fun ψ => ψ x

Proof state:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
⊢ (range fun φ => φ x) = (minpoly ℚ x).rootSet A

Tactic:
convert (NumberField.isAlgebraic K).range_eval_eq_rootSet_minpoly A x using 1

Result:
case h.e'_2
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
⊢ (range fun φ => φ x) = range fun ψ => ψ x

Proof state:
case h.e'_2.h
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
a : A
⊢ (a ∈ range fun φ => φ x) ↔ a ∈ range fun ψ => ψ x

Tactic:
exact ⟨fun ⟨φ, hφ⟩ => ⟨φ.toRatAlgHom, hφ⟩, fun ⟨φ, hφ⟩ => ⟨φ.toRingHom, hφ⟩⟩

Result:
no goals
-- Mathlib/ModelTheory/DirectLimit.lean
theorem Equiv_isup_symm_inclusion (i : ι) :
    (Equiv_iSup S).symm.toEmbedding.comp (Substructure.inclusion (le_iSup _ _))
    = of L ι _ (fun _ _ h ↦ Substructure.inclusion (S.monotone h)) i

Proof state:
L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
i : ι
⊢ (Equiv_iSup S).symm.toEmbedding.comp (Substructure.inclusion ⋯) =
    of L ι (fun x => ↥(S x)) (fun x x_1 h => Substructure.inclusion ⋯) i

Tactic:
ext x

Result:
case h
L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
i : ι
x : ↥(S i)
⊢ ((Equiv_iSup S).symm.toEmbedding.comp (Substructure.inclusion ⋯)) x =
    (of L ι (fun x => ↥(S x)) (fun x x_1 h => Substructure.inclusion ⋯) i) x

Proof state:
case h
L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
i : ι
x : ↥(S i)
⊢ ((Equiv_iSup S).symm.toEmbedding.comp (Substructure.inclusion ⋯)) x =
    (of L ι (fun x => ↥(S x)) (fun x x_1 h => Substructure.inclusion ⋯) i) x

Tactic:
exact Equiv_isup_symm_inclusion_apply _ x

Result:
no goals
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.add {t : Set E} (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 y t) :
    StarConvex 𝕜 (x + y) (s + t)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x + y) ((fun x => x.1 + x.2) '' s ×ˢ t)

Tactic:
exact (hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x + y) (s + t)

Tactic:
rw [← add_image_prod]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x + y) ((fun x => x.1 + x.2) '' s ×ˢ t)
-- Mathlib/Analysis/Convex/Visible.lean
/-- A set whose convex hull is closed lies in the cone based at a point `x` generated by its points
visible from `x` through its convex hull. -/
lemma IsClosed.convexHull_subset_affineSpan_isVisible (hs : IsClosed (convexHull ℝ s))
    (hx : x ∉ convexHull ℝ s) :
    convexHull ℝ s ⊆ affineSpan ℝ ({x} ∪ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y})

Proof state:
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
x : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed ((convexHull ℝ) s)
hx : x ∉ (convexHull ℝ) s
⊢ (convexHull ℝ) s ⊆ ↑(affineSpan ℝ ({x} ∪ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y}))

Tactic:
rintro y hy

Result:
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
x : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed ((convexHull ℝ) s)
hx : x ∉ (convexHull ℝ) s
y : V
hy : y ∈ (convexHull ℝ) s
⊢ y ∈ ↑(affineSpan ℝ ({x} ∪ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y}))

Proof state:
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
x : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed ((convexHull ℝ) s)
hx : x ∉ (convexHull ℝ) s
y : V
hy : y ∈ (convexHull ℝ) s
⊢ y ∈ ↑(affineSpan ℝ ({x} ∪ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y}))

Tactic:
obtain ⟨z, hz, hxzy, hxz⟩ := hs.exists_wbtw_isVisible hy x

Result:
case intro.intro.intro
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
x : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed ((convexHull ℝ) s)
hx : x ∉ (convexHull ℝ) s
y : V
hy : y ∈ (convexHull ℝ) s
z : V
hz : z ∈ (convexHull ℝ) s
hxzy : Wbtw ℝ x z y
hxz : IsVisible ℝ ((convexHull ℝ) s) x z
⊢ y ∈ ↑(affineSpan ℝ ({x} ∪ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y}))

Proof state:
case intro.intro.intro
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
x : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed ((convexHull ℝ) s)
hx : x ∉ (convexHull ℝ) s
y : V
hy : y ∈ (convexHull ℝ) s
z : V
hz : z ∈ (convexHull ℝ) s
hxzy : Wbtw ℝ x z y
hxz : IsVisible ℝ ((convexHull ℝ) s) x z
⊢ y ∈ ↑(affineSpan ℝ ({x} ∪ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y}))

Tactic:
exact AffineSubspace.right_mem_of_wbtw hxzy (subset_affineSpan _ _ <| subset_union_left rfl)
  (affineSpan_mono _ subset_union_right <| convexHull_subset_affineSpan _ <|
    hxz.mem_convexHull_isVisible hx hz) (ne_of_mem_of_not_mem hz hx).symm

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Free.lean
theorem basisAux_map_smul (a : A) (x : A ⊗[R] M) : basisAux A b (a • x) = a • basisAux A b x :=
  TensorProduct.induction_on x (by simp)
    (fun x y => by simp only [TensorProduct.smul_tmul', basisAux_tmul, smul_assoc])
    fun x y hx hy => by simp [hx, hy]

Proof state:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
x✝ : A ⊗[R] M
x : A
y : M
⊢ (basisAux A b) (a • x ⊗ₜ[R] y) = a • (basisAux A b) (x ⊗ₜ[R] y)

Tactic:
simp only [TensorProduct.smul_tmul', basisAux_tmul, smul_assoc]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
x✝ x y : A ⊗[R] M
hx : (basisAux A b) (a • x) = a • (basisAux A b) x
hy : (basisAux A b) (a • y) = a • (basisAux A b) y
⊢ (basisAux A b) (a • (x + y)) = a • (basisAux A b) (x + y)

Tactic:
simp [hx, hy]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
x : A ⊗[R] M
⊢ (basisAux A b) (a • 0) = a • (basisAux A b) 0

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem pi_of_empty {α : Type*} [Fintype α] [IsEmpty α] {β : α → Type*}
    {m : ∀ a, MeasurableSpace (β a)} (μ : ∀ a : α, Measure (β a)) (x : ∀ a, β a := isEmptyElim) :
    Measure.pi μ = dirac x

Proof state:
α : Type u_4
inst✝¹ : Fintype α
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : optParam ((a : α) → β a) fun a => isEmptyElim a
this : ∀ (a : α), SigmaFinite (μ a)
s : (i : α) → Set (β i)
x✝ : ∀ (i : α), MeasurableSet (s i)
⊢ (dirac x) (univ.pi s) = ∏ i : α, (μ i) (s i)

Tactic:
rw [Fintype.prod_empty, dirac_apply_of_mem]

Result:
α : Type u_4
inst✝¹ : Fintype α
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : optParam ((a : α) → β a) fun a => isEmptyElim a
this : ∀ (a : α), SigmaFinite (μ a)
s : (i : α) → Set (β i)
x✝ : ∀ (i : α), MeasurableSet (s i)
⊢ x ∈ univ.pi s

Proof state:
α : Type u_4
inst✝¹ : Fintype α
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : optParam ((a : α) → β a) fun a => isEmptyElim a
⊢ Measure.pi μ = dirac x

Tactic:
haveI : ∀ a, SigmaFinite (μ a) := isEmptyElim

Result:
α : Type u_4
inst✝¹ : Fintype α
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : optParam ((a : α) → β a) fun a => isEmptyElim a
this : ∀ (a : α), SigmaFinite (μ a)
⊢ Measure.pi μ = dirac x

Proof state:
α : Type u_4
inst✝¹ : Fintype α
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : optParam ((a : α) → β a) fun a => isEmptyElim a
this : ∀ (a : α), SigmaFinite (μ a)
⊢ Measure.pi μ = dirac x

Tactic:
refine pi_eq fun s _ => ?_

Result:
α : Type u_4
inst✝¹ : Fintype α
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : optParam ((a : α) → β a) fun a => isEmptyElim a
this : ∀ (a : α), SigmaFinite (μ a)
s : (i : α) → Set (β i)
x✝ : ∀ (i : α), MeasurableSet (s i)
⊢ (dirac x) (univ.pi s) = ∏ i : α, (μ i) (s i)

Proof state:
α : Type u_4
inst✝¹ : Fintype α
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : optParam ((a : α) → β a) fun a => isEmptyElim a
this : ∀ (a : α), SigmaFinite (μ a)
s : (i : α) → Set (β i)
x✝ : ∀ (i : α), MeasurableSet (s i)
⊢ x ∈ univ.pi s

Tactic:
exact isEmptyElim (α := α)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Stream.lean
theorem snd_take_eq_drop [Stream σ α] (s : σ) (n : Nat) :
    (take s n).snd = drop s n

Proof state:
case succ
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
n : Nat
ih : ∀ (s : σ), (take s n).snd = drop s n
s : σ
⊢ (match next? s with
      | none => ([], s)
      | some (a, s) => (a :: (take s n).fst, (take s n).snd)).snd =
    match next? s with
    | none => s
    | some (fst, s) => drop s n

Tactic:
split <;> simp [ih]

Result:
no goals

Proof state:
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
s : σ
n : Nat
⊢ (take s n).snd = drop s n

Tactic:
induction n generalizing s with
| zero => rfl
| succ n ih =>
  simp only [take, drop]
  split <;> simp [ih]

Result:
no goals

Proof state:
case zero
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
s : σ
⊢ (take s 0).snd = drop s 0

Tactic:
rfl

Result:
no goals

Proof state:
case succ
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
n : Nat
ih : ∀ (s : σ), (take s n).snd = drop s n
s : σ
⊢ (take s (n + 1)).snd = drop s (n + 1)

Tactic:
simp only [take, drop]

Result:
case succ
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
n : Nat
ih : ∀ (s : σ), (take s n).snd = drop s n
s : σ
⊢ (match next? s with
      | none => ([], s)
      | some (a, s) => (a :: (take s n).fst, (take s n).snd)).snd =
    match next? s with
    | none => s
    | some (fst, s) => drop s n
-- Mathlib/Order/Filter/Prod.lean
theorem Eventually.curry {la : Filter α} {lb : Filter β} {p : α × β → Prop}
    (h : ∀ᶠ x in la ×ˢ lb, p x) : ∀ᶠ x in la, ∀ᶠ y in lb, p (x, y)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α × β → Prop
h✝ : ∀ᶠ (x : α × β) in la ×ˢ lb, p x
pa : α → Prop
ha : ∀ᶠ (x : α) in la, pa x
pb : β → Prop
hb : ∀ᶠ (y : β) in lb, pb y
h : ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)

Tactic:
exact ha.mono fun a ha => hb.mono fun b hb => h ha hb

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α × β → Prop
h : ∀ᶠ (x : α × β) in la ×ˢ lb, p x
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)

Tactic:
rcases eventually_prod_iff.1 h with ⟨pa, ha, pb, hb, h⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α × β → Prop
h✝ : ∀ᶠ (x : α × β) in la ×ˢ lb, p x
pa : α → Prop
ha : ∀ᶠ (x : α) in la, pa x
pb : β → Prop
hb : ∀ᶠ (y : β) in lb, pb y
h : ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_alterKey_self [EquivBEq α] (k : α) (f : Option β → Option β)
    (l : List ((_ : α) × β)) (hl : DistinctKeys l) (hc : containsKey k (alterKey k f l)) :
    haveI hc' : (f (getValue? k l)).isSome

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k (alterKey k f l) = true
⊢ getValue k (alterKey k f l) hc = (f (getValue? k l)).get ⋯

Tactic:
rw [getValue_alterKey _ _ _ _ hl]

Result:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k (alterKey k f l) = true
⊢ (if h : (k == k) = true then (f (getValue? k l)).get ⋯ else getValue k l ⋯) = (f (getValue? k l)).get ⋯

Proof state:
α : Type u
β✝ : α → Type v
γ : α → Type w
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k (alterKey k f l) = true
⊢ (f (getValue? k l)).isSome = true

Tactic:
rwa [containsKey_alterKey hl, BEq.refl] at hc

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k (alterKey k f l) = true
⊢ (if h : (k == k) = true then (f (getValue? k l)).get ⋯ else getValue k l ⋯) = (f (getValue? k l)).get ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem Disjoint.sup_sdiff_cancel_left (h : Disjoint a b) : (a ⊔ b) \ a = b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ (a ⊔ b) \ a = b

Tactic:
rw [sup_sdiff, sdiff_self, bot_sup_eq, h.sdiff_eq_right]

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem not_mem_support_iff {f : SkewMonoidAlgebra k G} {a : G} :
    a ∉ f.support ↔ f.coeff a = 0

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
f : SkewMonoidAlgebra k G
a : G
⊢ a ∉ f.support ↔ f.coeff a = 0

Tactic:
simp only [mem_support_iff, ne_eq, not_not]

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
/-- The singular part of `κ` with respect to `η` is mutually singular with `η`. -/
lemma mutuallySingular_singularPart (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η]
    (a : α) :
    singularPart κ η a ⟂ₘ η a

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (κ.singularPart η) a ⟂ₘ η a

Tactic:
symm

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ η a ⟂ₘ (κ.singularPart η) a

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ η a ⟂ₘ (κ.singularPart η) a

Tactic:
exact ⟨mutuallySingularSetSlice κ η a, measurableSet_mutuallySingularSetSlice κ η a,
  measure_mutuallySingularSetSlice κ η a, singularPart_compl_mutuallySingularSetSlice κ η a⟩

Result:
no goals
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
lemma Odd.gammaFactor_def {χ : DirichletCharacter ℂ N} (hχ : χ.Odd) (s : ℂ) :
    gammaFactor χ s = Gammaℝ (s + 1)

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ.Odd
s : ℂ
⊢ χ.gammaFactor s = (s + 1).Gammaℝ

Tactic:
simp [gammaFactor, hχ.not_even]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem pred_le_pred_iff : pred a ≤ pred b ↔ a ≤ b

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
⊢ pred a ≤ pred b ↔ a ≤ b

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem nnnorm_eq_of_L2 (x : PiLp 2 β) :
    ‖x‖₊ = NNReal.sqrt (∑ i : ι, ‖x i‖₊ ^ 2) :=
  NNReal.eq <| by
    push_cast
    exact norm_eq_of_L2 x

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ = √(∑ x_1 : ι, ‖x x_1‖ ^ 2)

Tactic:
exact norm_eq_of_L2 x

Result:
no goals

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ↑‖x‖₊ = ↑(NNReal.sqrt (∑ i : ι, ‖x i‖₊ ^ 2))

Tactic:
push_cast

Result:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ = √(∑ x_1 : ι, ‖x x_1‖ ^ 2)
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma mem_range_coroot_of_mem_range_coreflection_of_mem_range_coroot
    {r : N ≃ₗ[R] N} {α : N} (hr : r ∈ range P.coreflection) (hα : α ∈ range P.coroot) :
    r • α ∈ range P.coroot

Proof state:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
α : N
hα : α ∈ range ⇑P.coroot
i : ι
⊢ P.coreflection i • α ∈ range ⇑P.coroot

Tactic:
obtain ⟨j, rfl⟩ := hα

Result:
case intro.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.coreflection i • P.coroot j ∈ range ⇑P.coroot

Proof state:
case intro.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.coreflection i • P.coroot j ∈ range ⇑P.coroot

Tactic:
exact ⟨P.reflection_perm i j, P.coroot_reflection_perm i j⟩

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
r : N ≃ₗ[R] N
α : N
hr : r ∈ range P.coreflection
hα : α ∈ range ⇑P.coroot
⊢ r • α ∈ range ⇑P.coroot

Tactic:
obtain ⟨i, rfl⟩ := hr

Result:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
α : N
hα : α ∈ range ⇑P.coroot
i : ι
⊢ P.coreflection i • α ∈ range ⇑P.coroot
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get?_insertMany_list_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (m.insertMany l).get? k' = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v) :=
  Raw₀.get?_insertMany_list_of_mem ⟨m.1, _⟩ m.2 k_beq distinct mem

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Proof state:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals