harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
    (h : m.1.WF) {l : List α}
    {k k' : α} (k_beq : k == k') {h'} :
    m.contains k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
      getKey (insertManyIfNewUnit m l).1 k' h' = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
k k' : α
k_beq : (k == k') = true
h' : (insertManyIfNewUnit m l).val.contains k' = true
⊢ m.contains k = false →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).val.getKey k' h' = k

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.getKey_insertListIfNewUnit_of_contains_eq_false_of_mem

Result:
no goals
-- Mathlib/RingTheory/Localization/AtPrime.lean
theorem localRingHom_comp {S : Type*} [CommSemiring S] (J : Ideal S) [hJ : J.IsPrime] (K : Ideal P)
    [hK : K.IsPrime] (f : R →+* S) (hIJ : I = J.comap f) (g : S →+* P) (hJK : J = K.comap g) :
    localRingHom I K (g.comp f) (by rw [hIJ, hJK, Ideal.comap_comap f g]) =
      (localRingHom J K g hJK).comp (localRingHom I J f hIJ) :=
  localRingHom_unique _ _ _ _ fun r => by
    simp only [Function.comp_apply, RingHom.coe_comp, localRingHom_to_map]

Proof state:
R : Type u_1
inst✝² : CommSemiring R
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
S : Type u_4
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
K : Ideal P
hK : K.IsPrime
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
r : R
⊢ ((localRingHom J K g hJK).comp (localRingHom I J f hIJ)) ((algebraMap R (Localization.AtPrime I)) r) =
    (algebraMap P (Localization.AtPrime K)) ((g.comp f) r)

Tactic:
simp only [Function.comp_apply, RingHom.coe_comp, localRingHom_to_map]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
S✝ : Type u_2
inst✝³ : CommSemiring S✝
inst✝² : Algebra R S✝
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
S : Type u_4
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
K : Ideal P
hK : K.IsPrime
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
⊢ I = Ideal.comap (g.comp f) K

Tactic:
rw [hIJ, hJK, Ideal.comap_comap f g]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
    (h : m.1.WF) {l : List α} {k k' : α} (k_beq : k == k') :
    m.contains k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
      getKey? (insertManyIfNewUnit m l).1 k' = some k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
k k' : α
k_beq : (k == k') = true
⊢ m.contains k = false →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).val.getKey? k' = some k

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem opNNNorm_le_iff {f : ContinuousMultilinearMap 𝕜 E G} {C : ℝ≥0} :
    ‖f‖₊ ≤ C ↔ ∀ m, ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
C : ℝ≥0
⊢ ↑‖f‖₊ ≤ ↑C ↔ ∀ (m : (i : ι) → E i), ↑‖f m‖₊ ≤ ↑(C * ∏ i : ι, ‖m i‖₊)

Tactic:
simp [opNorm_le_iff C.coe_nonneg, NNReal.coe_prod]

Result:
no goals

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
C : ℝ≥0
⊢ ‖f‖₊ ≤ C ↔ ∀ (m : (i : ι) → E i), ‖f m‖₊ ≤ C * ∏ i : ι, ‖m i‖₊

Tactic:
simp only [← NNReal.coe_le_coe]

Result:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
C : ℝ≥0
⊢ ↑‖f‖₊ ≤ ↑C ↔ ∀ (m : (i : ι) → E i), ↑‖f m‖₊ ≤ ↑(C * ∏ i : ι, ‖m i‖₊)
-- Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
theorem widePullback_ext' {B : C} {ι : Type w} [Nonempty ι] {X : ι → C}
    (f : ∀ j : ι, X j ⟶ B) [HasWidePullback.{w} B X f]
    [PreservesLimit (wideCospan B X f) (forget C)] (x y : ToType (widePullback B X f))
    (h : ∀ j, π f j x = π f j y) : x = y

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : ToType (widePullback B X f)
h : ∀ (j : ι), (ConcreteCategory.hom (π f j)) x = (ConcreteCategory.hom (π f j)) y
⊢ (ConcreteCategory.hom (base f)) x = (ConcreteCategory.hom (base f)) y

Tactic:
inhabit ι

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : ToType (widePullback B X f)
h : ∀ (j : ι), (ConcreteCategory.hom (π f j)) x = (ConcreteCategory.hom (π f j)) y
inhabited_h : Inhabited ι
⊢ (ConcreteCategory.hom (base f)) x = (ConcreteCategory.hom (base f)) y

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : ToType (widePullback B X f)
h : ∀ (j : ι), (ConcreteCategory.hom (π f j)) x = (ConcreteCategory.hom (π f j)) y
inhabited_h : Inhabited ι
⊢ (ConcreteCategory.hom (base f)) x = (ConcreteCategory.hom (base f)) y

Tactic:
simp only [← π_arrow f default, ConcreteCategory.comp_apply, h]

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : ToType (widePullback B X f)
h : ∀ (j : ι), (ConcreteCategory.hom (π f j)) x = (ConcreteCategory.hom (π f j)) y
⊢ x = y

Tactic:
apply Concrete.widePullback_ext _ _ _ _ h

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : ToType (widePullback B X f)
h : ∀ (j : ι), (ConcreteCategory.hom (π f j)) x = (ConcreteCategory.hom (π f j)) y
⊢ (ConcreteCategory.hom (base f)) x = (ConcreteCategory.hom (base f)) y
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma image_pow [MonoidHomClass F α β] (f : F) (s : Finset α) : ∀ n, (s ^ n).image f = s.image f ^ n
  | 0 => by simp [singleton_one]
  | n + 1 => image_pow_of_ne_zero n.succ_ne_zero ..

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq β
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Finset α
⊢ image (⇑f) (s ^ 0) = image (⇑f) s ^ 0

Tactic:
simp [singleton_one]

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
lemma adjoin_le_centralizer_centralizer (s : Set A) :
    adjoin R s ≤ centralizer R (centralizer R s)

Proof state:
case h.e'_4.h.e'_8
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ ↑(centralizer R s) ∪ star ↑(centralizer R s) = ↑(NonUnitalSubalgebra.centralizer R (s ∪ star s))

Tactic:
rw [StarMemClass.star_coe_eq]

Result:
case h.e'_4.h.e'_8
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ ↑(centralizer R s) ∪ ↑(centralizer R s) = ↑(NonUnitalSubalgebra.centralizer R (s ∪ star s))

Proof state:
case h.e'_4.h.e'_8
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ ↑(centralizer R s) ∪ ↑(centralizer R s) = ↑(NonUnitalSubalgebra.centralizer R (s ∪ star s))

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ NonUnitalAlgebra.adjoin R (s ∪ star s) ≤
    NonUnitalSubalgebra.centralizer R (↑(centralizer R s) ∪ star ↑(centralizer R s))

Tactic:
convert NonUnitalAlgebra.adjoin_le_centralizer_centralizer R (s ∪ star s)

Result:
case h.e'_4.h.e'_8
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ ↑(centralizer R s) ∪ star ↑(centralizer R s) = ↑(NonUnitalSubalgebra.centralizer R (s ∪ star s))

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ adjoin R s ≤ centralizer R ↑(centralizer R s)

Tactic:
rw [← toNonUnitalSubalgebra_le_iff, centralizer_toNonUnitalSubalgebra,
  adjoin_toNonUnitalSubalgebra]

Result:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ NonUnitalAlgebra.adjoin R (s ∪ star s) ≤
    NonUnitalSubalgebra.centralizer R (↑(centralizer R s) ∪ star ↑(centralizer R s))
-- Mathlib/Analysis/MeanInequalities.lean
theorem young_inequality_of_nonneg {a b p q : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b)
    (hpq : p.IsConjExponent q) : a * b ≤ a ^ p / p + b ^ q / q

Proof state:
a b p q : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hpq : p.IsConjExponent q
⊢ a * b ≤ a ^ p / p + b ^ q / q

Tactic:
simpa [← rpow_mul, ha, hb, hpq.ne_zero, hpq.symm.ne_zero, _root_.div_eq_inv_mul] using
  geom_mean_le_arith_mean2_weighted hpq.inv_nonneg hpq.symm.inv_nonneg
    (rpow_nonneg ha p) (rpow_nonneg hb q) hpq.inv_add_inv_conj

Result:
no goals
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem pow_dvd_of_squarefree_of_pow_succ_dvd_mul_left {k : ℕ}
    (hy : Squarefree y) (hp : Prime p) (h : p ^ (k + 1) ∣ x * y) :
    p ^ k ∣ x

Proof state:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x y p : R
k : ℕ
hy : Squarefree y
hp : Prime p
h : p ^ (k + 1) ∣ y * x
⊢ p ^ k ∣ x

Tactic:
exact pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right hy hp h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x y p : R
k : ℕ
hy : Squarefree y
hp : Prime p
h : p ^ (k + 1) ∣ x * y
⊢ p ^ k ∣ x

Tactic:
rw [mul_comm] at h

Result:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x y p : R
k : ℕ
hy : Squarefree y
hp : Prime p
h : p ^ (k + 1) ∣ y * x
⊢ p ^ k ∣ x
-- Mathlib/Data/ZMod/Coprime.lean
theorem eq_zero_iff_gcd_ne_one {a : ℤ} {p : ℕ} [pp : Fact p.Prime] :
    (a : ZMod p) = 0 ↔ a.gcd p ≠ 1

Proof state:
a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
⊢ ↑a = 0 ↔ a.gcd ↑p ≠ 1

Tactic:
rw [Ne, Int.gcd_comm, ← Int.isCoprime_iff_gcd_eq_one,
  (Nat.prime_iff_prime_int.1 pp.1).coprime_iff_not_dvd, Classical.not_not,
  intCast_zmod_eq_zero_iff_dvd]

Result:
no goals
-- Mathlib/Algebra/Homology/Opposite.lean
@[simp]
lemma quasiIsoAt_unopFunctor_map_iff
    {K L : HomologicalComplex Vᵒᵖ c} (φ : K ⟶ L) (i : ι)
    [K.HasHomology i] [L.HasHomology i] :
    QuasiIsoAt ((unopFunctor _ _).map φ.op) i ↔ QuasiIsoAt φ i

Proof state:
ι : Type u_1
V : Type u_2
inst✝³ : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝² : HasZeroMorphisms V
K L : HomologicalComplex Vᵒᵖ c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt ((unopFunctor V c).map φ.op) i ↔ QuasiIsoAt φ i

Tactic:
rw [← quasiIsoAt_opFunctor_map_iff]

Result:
ι : Type u_1
V : Type u_2
inst✝³ : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝² : HasZeroMorphisms V
K L : HomologicalComplex Vᵒᵖ c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt ((opFunctor V c.symm).map ((unopFunctor V c).map φ.op).op) i ↔ QuasiIsoAt φ i

Proof state:
ι : Type u_1
V : Type u_2
inst✝³ : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝² : HasZeroMorphisms V
K L : HomologicalComplex Vᵒᵖ c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt ((opFunctor V c.symm).map ((unopFunctor V c).map φ.op).op) i ↔ QuasiIsoAt φ i

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma mem_mutuallySingularSetSlice (κ η : Kernel α γ) (a : α) (x : γ) :
    x ∈ mutuallySingularSetSlice κ η a ↔ 1 ≤ rnDerivAux κ (κ + η) a x

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ x ∈ {x | 1 ≤ κ.rnDerivAux (κ + η) a x} ↔ 1 ≤ κ.rnDerivAux (κ + η) a x

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ x ∈ κ.mutuallySingularSetSlice η a ↔ 1 ≤ κ.rnDerivAux (κ + η) a x

Tactic:
rw [mutuallySingularSetSlice]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ x ∈ {x | 1 ≤ κ.rnDerivAux (κ + η) a x} ↔ 1 ≤ κ.rnDerivAux (κ + η) a x
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem MeasureTheory.Measure.map_mono_of_aemeasurable {f : α → δ} (h : μ ≤ ν)
    (hf : AEMeasurable f ν) : μ.map f ≤ ν.map f :=
  le_iff.2 fun s hs ↦ by simpa [hf, hs, hf.mono_measure h] using h (f ⁻¹' s)

Proof state:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ ν : Measure α
f : α → δ
h : μ ≤ ν
hf : AEMeasurable f ν
s : Set δ
hs : MeasurableSet s
⊢ (map f μ) s ≤ (map f ν) s

Tactic:
simpa [hf, hs, hf.mono_measure h] using h (f ⁻¹' s)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem diff_append (l₁ l₂ l₃ : List α) : l₁.diff (l₂ ++ l₃) = (l₁.diff l₂).diff l₃

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ l₃ : List α
⊢ l₁.diff (l₂ ++ l₃) = (l₁.diff l₂).diff l₃

Tactic:
simp only [diff_eq_foldl, foldl_append]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
theorem IsInitial.mono_from [InitialMonoClass C] {I} {X : C} (hI : IsInitial I) (f : I ⟶ X) :
    Mono f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : InitialMonoClass C
I X : C
hI : IsInitial I
f : I ⟶ X
⊢ Mono f

Tactic:
rw [hI.hom_ext f (hI.to X)]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : InitialMonoClass C
I X : C
hI : IsInitial I
f : I ⟶ X
⊢ Mono (hI.to X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : InitialMonoClass C
I X : C
hI : IsInitial I
f : I ⟶ X
⊢ Mono (hI.to X)

Tactic:
apply InitialMonoClass.isInitial_mono_from

Result:
no goals
-- Mathlib/Data/Multiset/Fintype.lean
@[simp] lemma toEnumFinset_filter_eq (m : Multiset α) (a : α) :
    m.toEnumFinset.filter (·.1 = a) = {a} ×ˢ Finset.range (m.count a)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
a : α
⊢ Finset.filter (fun x => x.1 = a) m.toEnumFinset = {a} ×ˢ Finset.range (count a m)

Tactic:
aesop

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_apply₀' (hs : NullMeasurableSet s μ) : μ.restrict s t = μ (t ∩ s)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
⊢ (μ.restrict s) t = μ (t ∩ s)

Tactic:
rw [← restrict_congr_set hs.toMeasurable_ae_eq,
  restrict_apply' (measurableSet_toMeasurable _ _),
  measure_congr ((ae_eq_refl t).inter hs.toMeasurable_ae_eq)]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma exists_abs_lt {α : Type*} [LinearOrderedRing α] (a : α) : ∃ b > 0, |a| < b :=
  ⟨|a| + 1, lt_of_lt_of_le zero_lt_one <| by simp, lt_add_one |a|⟩

Proof state:
α : Type u_2
inst✝ : LinearOrderedRing α
a : α
⊢ 1 ≤ |a| + 1

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.ι_matrix (m : ∀ j k, f j ⟶ g k) (j : J) :
    biproduct.ι f j ≫ biproduct.matrix m = biproduct.lift fun k => m j k

Proof state:
case w
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
j : J
j✝ : K
⊢ (ι f j ≫ matrix m) ≫ π g j✝ = (lift fun k => m j k) ≫ π g j✝

Tactic:
simp [biproduct.matrix]

Result:
no goals

Proof state:
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
j : J
⊢ ι f j ≫ matrix m = lift fun k => m j k

Tactic:
ext

Result:
case w
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
j : J
j✝ : K
⊢ (ι f j ≫ matrix m) ≫ π g j✝ = (lift fun k => m j k) ≫ π g j✝
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean
theorem eisSummand_SL2_apply (k : ℤ) (i : (Fin 2 → ℤ)) (A : SL(2, ℤ)) (z : ℍ) :
    eisSummand k i (A • z) = (z.denom A) ^ k * eisSummand k (i ᵥ* A) z

Proof state:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
⊢ (↑(i 0) * ↑(A • z) + ↑(i 1)) ^ (-k) =
    denom (↑A) z ^ k *
      ((↑(i 0) * ↑(↑A 0 0) + ↑(i 1) * ↑(↑A 1 0)) * ↑z + (↑(i 0) * ↑(↑A 0 1) + ↑(i 1) * ↑(↑A 1 1))) ^ (-k)

Tactic:
have h (a b c d u v : ℂ) (hc : c * z + d ≠ 0) : (u * ((a * z + b) / (c * z + d)) + v) ^ (-k) =
    (c * z + d) ^ k * ((u * a + v * c) * z + (u * b + v * d)) ^ (-k) := by
  field_simp [hc]
  ring_nf

Result:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
h :
  ∀ (a b c d u v : ℂ),
    c * ↑z + d ≠ 0 →
      (u * ((a * ↑z + b) / (c * ↑z + d)) + v) ^ (-k) =
        (c * ↑z + d) ^ k * ((u * a + v * c) * ↑z + (u * b + v * d)) ^ (-k)
⊢ (↑(i 0) * ↑(A • z) + ↑(i 1)) ^ (-k) =
    denom (↑A) z ^ k *
      ((↑(i 0) * ↑(↑A 0 0) + ↑(i 1) * ↑(↑A 1 0)) * ↑z + (↑(i 0) * ↑(↑A 0 1) + ↑(i 1) * ↑(↑A 1 1))) ^ (-k)

Proof state:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
⊢ eisSummand k i (A • z) = denom (↑A) z ^ k * eisSummand k (i ᵥ* ↑A) z

Tactic:
simp only [eisSummand, vecMul, vec2_dotProduct]

Result:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
⊢ (↑(i 0) * ↑(A • z) + ↑(i 1)) ^ (-k) =
    denom (↑A) z ^ k * (↑(i 0 * ↑A 0 0 + i 1 * ↑A 1 0) * ↑z + ↑(i 0 * ↑A 0 1 + i 1 * ↑A 1 1)) ^ (-k)

Proof state:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : c * ↑z + d ≠ 0
⊢ (u * ((a * ↑z + b) / (c * ↑z + d)) + v) ^ (-k) = (c * ↑z + d) ^ k * ((u * a + v * c) * ↑z + (u * b + v * d)) ^ (-k)

Tactic:
field_simp [hc]

Result:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : c * ↑z + d ≠ 0
⊢ (c * ↑z + d) ^ k / (u * (a * ↑z + b) + v * (c * ↑z + d)) ^ k =
    (c * ↑z + d) ^ k / ((u * a + v * c) * ↑z + (u * b + v * d)) ^ k

Proof state:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
h :
  ∀ (a b c d u v : ℂ),
    c * ↑z + d ≠ 0 →
      (u * ((a * ↑z + b) / (c * ↑z + d)) + v) ^ (-k) =
        (c * ↑z + d) ^ k * ((u * a + v * c) * ↑z + (u * b + v * d)) ^ (-k)
⊢ (↑(i 0) * ↑(A • z) + ↑(i 1)) ^ (-k) =
    denom (↑A) z ^ k *
      ((↑(i 0) * ↑(↑A 0 0) + ↑(i 1) * ↑(↑A 1 0)) * ↑z + (↑(i 0) * ↑(↑A 0 1) + ↑(i 1) * ↑(↑A 1 1))) ^ (-k)

Tactic:
apply h (hc := z.denom_ne_zero A)

Result:
no goals

Proof state:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
⊢ (↑(i 0) * ↑(A • z) + ↑(i 1)) ^ (-k) =
    denom (↑A) z ^ k * (↑(i 0 * ↑A 0 0 + i 1 * ↑A 1 0) * ↑z + ↑(i 0 * ↑A 0 1 + i 1 * ↑A 1 1)) ^ (-k)

Tactic:
push_cast

Result:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
⊢ (↑(i 0) * ↑(A • z) + ↑(i 1)) ^ (-k) =
    denom (↑A) z ^ k *
      ((↑(i 0) * ↑(↑A 0 0) + ↑(i 1) * ↑(↑A 1 0)) * ↑z + (↑(i 0) * ↑(↑A 0 1) + ↑(i 1) * ↑(↑A 1 1))) ^ (-k)

Proof state:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : c * ↑z + d ≠ 0
⊢ (c * ↑z + d) ^ k / (u * (a * ↑z + b) + v * (c * ↑z + d)) ^ k =
    (c * ↑z + d) ^ k / ((u * a + v * c) * ↑z + (u * b + v * d)) ^ k

Tactic:
ring_nf

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem Associated.of_pow_associated_of_prime [CancelCommMonoidWithZero M] {p₁ p₂ : M} {k₁ k₂ : ℕ}
    (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₁ : 0 < k₁) (h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂) : p₁ ~ᵤ p₂

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
this : p₁ ∣ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂

Tactic:
rw [← hp₁.dvd_prime_iff_associated hp₂]

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
this : p₁ ∣ p₂ ^ k₂
⊢ p₁ ∣ p₂

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ∣ p₂ ^ k₂

Tactic:
rw [← h.dvd_iff_dvd_right]

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ∣ p₁ ^ k₁

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
this : p₁ ∣ p₂ ^ k₂
⊢ p₁ ∣ p₂

Tactic:
exact hp₁.dvd_of_dvd_pow this

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ∣ p₁ ^ k₁

Tactic:
apply dvd_pow_self _ hk₁.ne'

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂

Tactic:
have : p₁ ∣ p₂ ^ k₂ := by
  rw [← h.dvd_iff_dvd_right]
  apply dvd_pow_self _ hk₁.ne'

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
this : p₁ ∣ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma restrictSubtype_ground : (M.restrictSubtype X).E = univ

Proof state:
α : Type u_1
X : Set α
M : Matroid α
⊢ (M.restrictSubtype X).E = univ

Tactic:
simp [restrictSubtype]

Result:
no goals