harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem getElem_attach {xs : Vector α n} {i : Nat} (h : i < n) :
    xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
  getElem_attachWith h

Proof state:
α : Type ?u.31839
n : Nat
xs : Vector α n
i : Nat
h : i < n
⊢ i < n

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ico_add_one_right_eq_Icc (a b : α) : Ico a (b + 1) = Icc a b

Proof state:
α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ico a (b + 1) = Icc a b

Tactic:
simpa [succ_eq_add_one] using  Ico_succ_right_eq_Icc a b

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem integrable_cexp_neg_mul_sum_add {ι : Type*} [Fintype ι] (hb : 0 < b.re) (c : ι → ℂ) :
    Integrable (fun (v : ι → ℝ) ↦ cexp (- b * ∑ i, (v i : ℂ) ^ 2 + ∑ i, c i * v i))

Proof state:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ Integrable (fun v => cexp (-∑ i : ι, b * ↑(v i) ^ 2 + ∑ i : ι, c i * ↑(v i))) volume

Tactic:
exact integrable_cexp_neg_sum_mul_add (fun _ ↦ hb) c

Result:
no goals

Proof state:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ Integrable (fun v => cexp (-b * ∑ i : ι, ↑(v i) ^ 2 + ∑ i : ι, c i * ↑(v i))) volume

Tactic:
simp_rw [neg_mul, Finset.mul_sum]

Result:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ Integrable (fun v => cexp (-∑ i : ι, b * ↑(v i) ^ 2 + ∑ i : ι, c i * ↑(v i))) volume
-- Mathlib/Data/Int/Lemmas.lean
theorem natAbs_inj_of_nonneg_of_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) :
    natAbs a = natAbs b ↔ a = b

Proof state:
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a.natAbs = b.natAbs ↔ a = b

Tactic:
rw [← sq_eq_sq₀ ha hb, ← natAbs_eq_iff_sq_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem twoPow_mul_eq_shiftLeft (x : BitVec w) (i : Nat) :
    (twoPow w i) * x = x <<< i

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ twoPow w i * x = x <<< i

Tactic:
rw [BitVec.mul_comm, mul_twoPow_eq_shiftLeft]

Result:
no goals
-- Mathlib/Topology/Constructible.lean
lemma IsLocallyConstructible.finsetInf' {ι : Type*} {s : Finset ι} {hs} {t : ι → Set X}
    (ht : ∀ i ∈ s, IsLocallyConstructible (t i)) : IsLocallyConstructible (s.inf' hs t)

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (s.inf t)

Tactic:
exact .finsetInf ht

Result:
no goals

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (s.inf' hs t)

Tactic:
rw [Finset.inf'_eq_inf]

Result:
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (s.inf t)
-- Mathlib/Algebra/Field/Periodic.lean
theorem Periodic.div_const [DivisionSemiring α] (h : Periodic f c) (a : α) :
    Periodic (fun x => f (x / a)) (c * a)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : DivisionSemiring α
h : Periodic f c
a : α
⊢ Periodic (fun x => f (x / a)) (c * a)

Tactic:
simpa only [div_eq_mul_inv] using h.mul_const_inv a

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertMany_empty_list_cons {k : α} {v : β k}
    {tl : List ((a : α) × (β a))} :
    (insertMany empty (⟨k, v⟩ :: tl)).1 = ((empty.insert k v).insertMany tl).1

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
v : β k
tl : List ((a : α) × β a)
⊢ (empty.insertMany (⟨k, v⟩ :: tl)).val = ((empty.insert k v).insertMany tl).val

Tactic:
rw [insertMany_cons]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_closure_union_closure_eq_closure_union (M : Matroid α) (X Y : Set α) :
    M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)

Proof state:
α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (⋃ i, M.closure (bif i then X else Y)) = M.closure (⋃ b, bif b then M.closure X else M.closure Y)

Tactic:
simp_rw [Bool.cond_eq_ite, apply_ite]

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)

Tactic:
rw [eq_comm, union_eq_iUnion, ← closure_iUnion_closure_eq_closure_iUnion, union_eq_iUnion]

Result:
α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (⋃ i, M.closure (bif i then X else Y)) = M.closure (⋃ b, bif b then M.closure X else M.closure Y)
-- Mathlib/Topology/Basic.lean
theorem isClosed_compl_iff {s : Set X} : IsClosed sᶜ ↔ IsOpen s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed sᶜ ↔ IsOpen s

Tactic:
rw [← isOpen_compl_iff, compl_compl]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem binomial_succ_succ [DecidableEq α] (h : a ≠ b) :
    multinomial {a, b} (Function.update (Function.update f a (f a).succ) b (f b).succ) =
      multinomial {a, b} (Function.update f a (f a).succ) +
      multinomial {a, b} (Function.update f b (f b).succ)

Proof state:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ ((f a).succ + (f b).succ).choose (f a).succ = ((f a).succ + f b).choose (f a).succ + (f a + (f b).succ).choose (f a)

Tactic:
rw [add_succ, choose_succ_succ, succ_add_eq_add_succ]

Result:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ (f a + (f b).succ).choose (f a) + (f a + (f b).succ).choose (f a).succ =
    (f a + (f b).succ).choose (f a).succ + (f a + (f b).succ).choose (f a)

Proof state:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ multinomial {a, b} (Function.update (Function.update f a (f a).succ) b (f b).succ) =
    multinomial {a, b} (Function.update f a (f a).succ) + multinomial {a, b} (Function.update f b (f b).succ)

Tactic:
simp only [binomial_eq_choose, Function.update_apply,
  h, Ne, ite_true, ite_false, not_false_eq_true]

Result:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ ((f a).succ + (f b).succ).choose (f a).succ =
    ((f a).succ + if b = a then (f a).succ else f b).choose (f a).succ + (f a + (f b).succ).choose (f a)

Proof state:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ ((f a).succ + (f b).succ).choose (f a).succ =
    ((f a).succ + if b = a then (f a).succ else f b).choose (f a).succ + (f a + (f b).succ).choose (f a)

Tactic:
rw [if_neg h.symm]

Result:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ ((f a).succ + (f b).succ).choose (f a).succ = ((f a).succ + f b).choose (f a).succ + (f a + (f b).succ).choose (f a)

Proof state:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ (f a + (f b).succ).choose (f a) + (f a + (f b).succ).choose (f a).succ =
    (f a + (f b).succ).choose (f a).succ + (f a + (f b).succ).choose (f a)

Tactic:
ring

Result:
no goals
-- Mathlib/CategoryTheory/Pi/Basic.lean
theorem eqToHom_proj {x x' : ∀ i, C i} (h : x = x') (i : I) :
    (eqToHom h : x ⟶ x') i = eqToHom (funext_iff.mp h i)

Proof state:
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
x : (i : I) → C i
i : I
⊢ eqToHom ⋯ i = eqToHom ⋯

Tactic:
rfl

Result:
no goals

Proof state:
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
x x' : (i : I) → C i
h : x = x'
i : I
⊢ eqToHom h i = eqToHom ⋯

Tactic:
subst h

Result:
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
x : (i : I) → C i
i : I
⊢ eqToHom ⋯ i = eqToHom ⋯
-- Mathlib/Topology/Algebra/Valued/ValuationTopology.lean
theorem hasBasis_nhds_zero :
    (𝓝 (0 : R)).HasBasis (fun _ => True) fun γ : Γ₀ˣ => { x | v x < (γ : Γ₀) }

Proof state:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ (𝓝 0).HasBasis (fun x => True) fun γ => {x | v x < ↑γ}

Tactic:
simp [Filter.hasBasis_iff, is_topological_valuation]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_inf_mul_relrank : A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
⊢ A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C

Tactic:
rw [← inf_relrank_right A (B ⊓ C), ← inf_relrank_right B C, ← inf_relrank_right (A ⊓ B) C,
  inf_assoc, relrank_mul_relrank inf_le_right inf_le_right]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem toMatrix'_comp (Q : QuadraticMap R (m → R) R) (f : (n → R) →ₗ[R] m → R) :
    (Q.comp f).toMatrix' = (LinearMap.toMatrix' f)ᵀ * Q.toMatrix' * (LinearMap.toMatrix' f)

Proof state:
case a
R : Type u_3
n : Type w
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : DecidableEq n
inst✝² : Invertible 2
m : Type w
inst✝¹ : DecidableEq m
inst✝ : Fintype m
Q : QuadraticMap R (m → R) R
f : (n → R) →ₗ[R] m → R
i✝ j✝ : n
⊢ (Q.comp f).toMatrix' i✝ j✝ = ((LinearMap.toMatrix' f)ᵀ * Q.toMatrix' * LinearMap.toMatrix' f) i✝ j✝

Tactic:
simp only [QuadraticMap.associated_comp, LinearMap.toMatrix₂'_compl₁₂, toMatrix']

Result:
no goals

Proof state:
R : Type u_3
n : Type w
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : DecidableEq n
inst✝² : Invertible 2
m : Type w
inst✝¹ : DecidableEq m
inst✝ : Fintype m
Q : QuadraticMap R (m → R) R
f : (n → R) →ₗ[R] m → R
⊢ (Q.comp f).toMatrix' = (LinearMap.toMatrix' f)ᵀ * Q.toMatrix' * LinearMap.toMatrix' f

Tactic:
ext

Result:
case a
R : Type u_3
n : Type w
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : DecidableEq n
inst✝² : Invertible 2
m : Type w
inst✝¹ : DecidableEq m
inst✝ : Fintype m
Q : QuadraticMap R (m → R) R
f : (n → R) →ₗ[R] m → R
i✝ j✝ : n
⊢ (Q.comp f).toMatrix' i✝ j✝ = ((LinearMap.toMatrix' f)ᵀ * Q.toMatrix' * LinearMap.toMatrix' f) i✝ j✝
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem comap_id' (U : Opens (PrimeSpectrum.Top R)) :
    (comap (RingHom.id R) U U fun p hpU => by rwa [PrimeSpectrum.comap_id]) = RingHom.id _

Proof state:
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
⊢ comap (RingHom.id R) U U ⋯ = RingHom.id ↑((structureSheaf R).val.obj (op U))

Tactic:
rw [comap_id rfl]

Result:
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
⊢ CommRingCat.Hom.hom (eqToHom ⋯) = RingHom.id ↑((structureSheaf R).val.obj (op U))

Proof state:
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
⊢ CommRingCat.Hom.hom (eqToHom ⋯) = RingHom.id ↑((structureSheaf R).val.obj (op U))

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U : Opens ↑(PrimeSpectrum.Top R)
p : ↑(PrimeSpectrum.Top R)
hpU : p ∈ U.carrier
⊢ p ∈ ⇑(PrimeSpectrum.comap (RingHom.id R)) ⁻¹' U.carrier

Tactic:
rwa [PrimeSpectrum.comap_id]

Result:
no goals
-- Mathlib/Algebra/RingQuot.lean
theorem liftAlgHom_unique (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ ⦃x y⦄, s x y → f x = f y)
    (g : RingQuot s →ₐ[S] B) (h : g.comp (mkAlgHom S s) = f) : g = liftAlgHom S ⟨f, w⟩

Proof state:
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
g : RingQuot s →ₐ[S] B
h : g.comp (mkAlgHom S s) = f
⊢ g = (liftAlgHom S) ⟨f, w⟩

Tactic:
ext

Result:
case w.H
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
g : RingQuot s →ₐ[S] B
h : g.comp (mkAlgHom S s) = f
x✝ : A
⊢ (g.comp (mkAlgHom S s)) x✝ = (((liftAlgHom S) ⟨f, w⟩).comp (mkAlgHom S s)) x✝

Proof state:
case w.H
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
g : RingQuot s →ₐ[S] B
h : g.comp (mkAlgHom S s) = f
x✝ : A
⊢ (g.comp (mkAlgHom S s)) x✝ = (((liftAlgHom S) ⟨f, w⟩).comp (mkAlgHom S s)) x✝

Tactic:
simp [h]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
lemma range_mapIncl_mono {p p' : Submodule R P} {q q' : Submodule R Q} (hp : p ≤ p') (hq : q ≤ q') :
    LinearMap.range (mapIncl p q) ≤ LinearMap.range (mapIncl p' q')

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_7
Q : Type u_8
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
inst✝ : Module R P
p p' : Submodule R P
q q' : Submodule R Q
hp : p ≤ p'
hq : q ≤ q'
⊢ range (mapIncl p q) ≤ range (mapIncl p' q')

Tactic:
simp_rw [range_mapIncl]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_7
Q : Type u_8
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
inst✝ : Module R P
p p' : Submodule R P
q q' : Submodule R Q
hp : p ≤ p'
hq : q ≤ q'
⊢ Submodule.span R (Set.image2 (fun x1 x2 => x1 ⊗ₜ[R] x2) ↑p ↑q) ≤
    Submodule.span R (Set.image2 (fun x1 x2 => x1 ⊗ₜ[R] x2) ↑p' ↑q')

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_7
Q : Type u_8
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
inst✝ : Module R P
p p' : Submodule R P
q q' : Submodule R Q
hp : p ≤ p'
hq : q ≤ q'
⊢ Submodule.span R (Set.image2 (fun x1 x2 => x1 ⊗ₜ[R] x2) ↑p ↑q) ≤
    Submodule.span R (Set.image2 (fun x1 x2 => x1 ⊗ₜ[R] x2) ↑p' ↑q')

Tactic:
exact Submodule.span_mono (Set.image2_subset hp hq)

Result:
no goals
-- Mathlib/Topology/PartitionOfUnity.lean
theorem exists_isSubordinate_hasCompactSupport_of_locallyFinite_t2space [LocallyCompactSpace X]
    [T2Space X]
    (hs : IsCompact s) (U : ι → Set X) (ho : ∀ i, IsOpen (U i)) (hf : LocallyFinite U)
    (hU : s ⊆ ⋃ i, U i) :
    ∃ f : BumpCovering ι X s, f.IsSubordinate U ∧ ∀ i, HasCompactSupport (f i)

Proof state:
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ i, U i
⊢ ∃ f, f.IsSubordinate U ∧ ∀ (i : ι), HasCompactSupport ⇑(f i)

Tactic:
simpa using
  exists_isSubordinate_of_locallyFinite_of_prop_t2space (fun _ => True)
    (fun _ _ ht hs hd =>
      (exists_continuous_zero_one_of_isCompact' hs ht hd.symm).imp fun _ hf => ⟨trivial, hf⟩)
    hs U ho hf hU

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem erase_val [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} :
    m.val.erase a = m.erase a

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
⊢ m.val.erase a = (m.erase a).val

Tactic:
simp [Raw.erase, m.2]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem dlookup_map₁ {β : Type v} (l : List (Σ _ : α, β))
    {f : α → α'} (hf : Function.Injective f) (a : α) :
    (l.map fun x => ⟨f x.1, x.2⟩ : List (Σ _ : α', β)).dlookup (f a) = l.dlookup a

Proof state:
α : Type u
α' : Type u'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
β : Type v
l : List ((_ : α) × β)
f : α → α'
hf : Function.Injective f
a : α
⊢ dlookup (f a) (map (fun x => ⟨f x.fst, x.snd⟩) l) = dlookup a l

Tactic:
rw [dlookup_map (β' := fun _ => β) l hf (fun _ x => x) a, Option.map_id']

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
protected lemma map_mul (g h : GL n R) : map f (g * h) = map f g * map f h

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g h : GL n R
⊢ (map f) (g * h) = (map f) g * (map f) h

Tactic:
ext

Result:
case a.a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g h : GL n R
i✝ j✝ : n
⊢ ↑((map f) (g * h)) i✝ j✝ = ↑((map f) g * (map f) h) i✝ j✝

Proof state:
case a.a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g h : GL n R
i✝ j✝ : n
⊢ ↑((map f) (g * h)) i✝ j✝ = ↑((map f) g * (map f) h) i✝ j✝

Tactic:
simp only [_root_.map_mul, Units.val_mul]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_diff_left : Icc a b \ {a} = Ioc a b :=
  ext fun x => by simp [lt_iff_le_and_ne, eq_comm, and_right_comm]

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b x : α
⊢ x ∈ Icc a b \ {a} ↔ x ∈ Ioc a b

Tactic:
simp [lt_iff_le_and_ne, eq_comm, and_right_comm]

Result:
no goals
-- Mathlib/Algebra/Ring/Divisibility/Basic.lean
theorem dvd_sub_comm : a ∣ b - c ↔ a ∣ c - b

Proof state:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
⊢ a ∣ b - c ↔ a ∣ c - b

Tactic:
rw [← dvd_neg, neg_sub]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem kernelSubobject_arrow' :
    (kernelSubobjectIso f).inv ≫ (kernelSubobject f).arrow = kernel.ι f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ (kernelSubobjectIso f).inv ≫ (kernelSubobject f).arrow = kernel.ι f

Tactic:
simp [kernelSubobjectIso]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem getCastD_eq [BEq α] [LawfulBEq α] {l : AssocList α β} {a : α} {fallback : β a} :
    l.getCastD a fallback = getValueCastD a l.toList fallback

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
fallback : β a
⊢ getCastD a fallback nil = getValueCastD a nil.toList fallback

Tactic:
simp [getCastD, List.getValueCastD]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
fallback : β a
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : getCastD a fallback tail✝ = getValueCastD a tail✝.toList fallback
⊢ getCastD a fallback (cons key✝ value✝ tail✝) = getValueCastD a (cons key✝ value✝ tail✝).toList fallback

Tactic:
simp_all [getCastD, List.getValueCastD, List.getValueCastD, List.getValueCast?_cons,
  apply_dite (fun x => Option.getD x fallback)]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : AssocList α β
a : α
fallback : β a
⊢ getCastD a fallback l = getValueCastD a l.toList fallback

Tactic:
induction l

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
fallback : β a
⊢ getCastD a fallback nil = getValueCastD a nil.toList fallback

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
fallback : β a
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : getCastD a fallback tail✝ = getValueCastD a tail✝.toList fallback
⊢ getCastD a fallback (cons key✝ value✝ tail✝) = getValueCastD a (cons key✝ value✝ tail✝).toList fallback
-- Mathlib/Data/Fintype/Pi.lean
theorem piFinset_singleton (f : ∀ i, δ i) : piFinset (fun i => {f i} : ∀ i, Finset (δ i)) = {f} :=
  ext fun _ => by simp only [funext_iff, Fintype.mem_piFinset, mem_singleton]

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
f x✝ : (a : α) → δ a
⊢ (x✝ ∈ piFinset fun i => {f i}) ↔ x✝ ∈ {f}

Tactic:
simp only [funext_iff, Fintype.mem_piFinset, mem_singleton]

Result:
no goals
-- Mathlib/Data/Set/Countable.lean
theorem subset_range_enumerate {s : Set α} (h : s.Countable) (default : α) :
    s ⊆ range (enumerateCountable h default) := fun x hx =>
  ⟨@Encodable.encode s h.toEncodable ⟨x, hx⟩, by
    letI := h.toEncodable
    simp [enumerateCountable, Encodable.encodek]⟩

Proof state:
α : Type u
s : Set α
h : s.Countable
default x : α
hx : x ∈ s
this : Encodable ↑s := h.toEncodable
⊢ enumerateCountable h default (encode ⟨x, hx⟩) = x

Tactic:
simp [enumerateCountable, Encodable.encodek]

Result:
no goals

Proof state:
α : Type u
s : Set α
h : s.Countable
default x : α
hx : x ∈ s
⊢ enumerateCountable h default (encode ⟨x, hx⟩) = x

Tactic:
letI := h.toEncodable

Result:
α : Type u
s : Set α
h : s.Countable
default x : α
hx : x ∈ s
this : Encodable ↑s := h.toEncodable
⊢ enumerateCountable h default (encode ⟨x, hx⟩) = x
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_preimage_smul {r : ℝ} (hr : r ≠ 0) (s : Set E) :
    μ ((r • ·) ⁻¹' s) = ENNReal.ofReal (abs (r ^ finrank ℝ E)⁻¹) * μ s :=
  calc
    μ ((r • ·) ⁻¹' s) = Measure.map (r • ·) μ s :=
      ((Homeomorph.smul (isUnit_iff_ne_zero.2 hr).unit).toMeasurableEquiv.map_apply s).symm
    _ = ENNReal.ofReal (abs (r ^ finrank ℝ E)⁻¹) * μ s

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
s : Set E
⊢ (map (fun x => r • x) μ) s = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| * μ s

Tactic:
rw [map_addHaar_smul μ hr, coe_smul, Pi.smul_apply, smul_eq_mul]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Basic.lean
theorem mk_apply_of_mem {s : Finset ι} {f : ∀ i : (↑s : Set ι), β i.val} {n : ι} (hn : n ∈ s) :
    mk β s f n = f ⟨n, hn⟩

Proof state:
ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
s : Finset ι
f : (i : ↑↑s) → β ↑i
n : ι
hn : n ∈ s
⊢ (if H : n ∈ s then f ⟨n, H⟩ else 0) = f ⟨n, hn⟩

Tactic:
rw [dif_pos hn]

Result:
no goals

Proof state:
ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
s : Finset ι
f : (i : ↑↑s) → β ↑i
n : ι
hn : n ∈ s
⊢ ((mk β s) f) n = f ⟨n, hn⟩

Tactic:
dsimp only [Finset.coe_sort_coe, mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk, DFinsupp.mk_apply]

Result:
ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
s : Finset ι
f : (i : ↑↑s) → β ↑i
n : ι
hn : n ∈ s
⊢ (if H : n ∈ s then f ⟨n, H⟩ else 0) = f ⟨n, hn⟩
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem yn_one : yn a1 1 = 1

Proof state:
a : ℕ
a1 : 1 < a
⊢ yn a1 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
lemma cycles_ext_iff {A : C} (f₁ f₂ : A ⟶ S.cycles) :
    f₁ = f₂ ↔ f₁ ≫ S.iCycles = f₂ ≫ S.iCycles

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
A : C
f₁ f₂ : A ⟶ S.cycles
⊢ f₁ = f₂ ↔ f₁ ≫ S.iCycles = f₂ ≫ S.iCycles

Tactic:
rw [cancel_mono]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem IntegrableOn.integrable_of_ae_not_mem_eq_zero (hf : IntegrableOn f s μ)
    (h't : ∀ᵐ x ∂μ, x ∉ s → f x = 0) : Integrable f μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
⊢ Integrable f μ

Tactic:
rw [← integrableOn_univ]

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
⊢ IntegrableOn f univ μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ \ s → f x = 0

Tactic:
filter_upwards [h't] with x hx h'x using hx h'x.2

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
⊢ IntegrableOn f univ μ

Tactic:
apply hf.of_ae_diff_eq_zero nullMeasurableSet_univ

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ \ s → f x = 0
-- Mathlib/Algebra/Polynomial/Sequence.lean
/-- `S i` has strictly monotone natural degree. -/
lemma natDegree_strictMono : StrictMono <| natDegree ∘ S := fun _ _  ↦ by simp

Proof state:
R : Type u_1
inst✝ : Semiring R
S : Sequence R
x✝¹ x✝ : ℕ
⊢ x✝¹ < x✝ → (natDegree ∘ ↑S) x✝¹ < (natDegree ∘ ↑S) x✝

Tactic:
simp

Result:
no goals