harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/Ideal.lean
theorem stdBasisMatrix_mem_jacobson_matricesOver (I : Ideal R) :
    ∀ x ∈ I.jacobson, ∀ (i j : n), stdBasisMatrix i j x ∈ (I.matricesOver n).jacobson

Proof state:
case h.inl
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
i : n
⊢ (N * M * stdBasisMatrix p q x + N - 1) i q ∈ I

Tactic:
by_cases iq : i = q

Result:
case pos
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
i : n
iq : i = q
⊢ (N * M * stdBasisMatrix p q x + N - 1) i q ∈ I

case neg
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
i : n
iq : ¬i = q
⊢ (N * M * stdBasisMatrix p q x + N - 1) i q ∈ I

Proof state:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
⊢ ∀ x ∈ I.jacobson, ∀ (i j : n), stdBasisMatrix i j x ∈ (matricesOver n I).jacobson

Tactic:
simp_rw [Ideal.mem_jacobson_iff]

Result:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
⊢ ∀ (x : R),
    (∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I) →
      ∀ (i j : n) (y : Matrix n n R), ∃ z, z * y * stdBasisMatrix i j x + z - 1 ∈ matricesOver n I

Proof state:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
⊢ ∃ z, z * M * stdBasisMatrix p q x + z - 1 ∈ matricesOver n I

Tactic:
let N : Matrix n n R := 1 - ∑ i, stdBasisMatrix i q (if i = q then 1 - z else (M i p)*x*z)

Result:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
⊢ ∃ z, z * M * stdBasisMatrix p q x + z - 1 ∈ matricesOver n I
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_mul_one : Principal (· * ·) 1

Proof state:
⊢ 0 * 0 = 0

Tactic:
exact zero_mul _

Result:
no goals

Proof state:
⊢ Principal (fun x1 x2 => x1 * x2) 1

Tactic:
rw [principal_one_iff]

Result:
⊢ 0 * 0 = 0
-- Mathlib/Data/Nat/Basic.lean
lemma pow_left_injective (hn : n ≠ 0) : Injective (fun a : ℕ ↦ a ^ n)

Proof state:
n : ℕ
hn : n ≠ 0
⊢ Injective fun a => a ^ n

Tactic:
simp [Injective, le_antisymm_iff, Nat.pow_le_pow_iff_left hn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_flatten (f : α → β) (L : Vector (Vector α n) m) :
    (flatten L).map f = (map (map f) L).flatten

Proof state:
case of
α : Type u_1
β : Type u_2
n m : Nat
f : α → β
xss : Array (Array α)
h₁ : xss.size = m
h₂ : ∀ (xs : Array α), xs ∈ xss → xs.size = n
⊢ map f
      {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
              xss.attach,
          size_toArray := ⋯ }.flatten =
    (map (map f)
        {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
              xss.attach,
          size_toArray := ⋯ }).flatten

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n m : Nat
f : α → β
L : Vector (Vector α n) m
⊢ map f L.flatten = (map (map f) L).flatten

Tactic:
induction L using vector₂_induction with
| of xss h₁ h₂ => simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integrableOn_Ioi_of_intervalIntegral_norm_bounded (I a : ℝ)
    (hfi : ∀ i, IntegrableOn f (Ioc a (b i)) μ) (hb : Tendsto b l atTop)
    (h : ∀ᶠ i in l, (∫ x in a..b i, ‖f x‖ ∂μ) ≤ I) : IntegrableOn f (Ioi a) μ

Proof state:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun i => Iic (b i)
i : ι
⊢ IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))

Tactic:
rw [IntegrableOn, Measure.restrict_restrict (hφ.measurableSet i), inter_comm]

Result:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun i => Iic (b i)
i : ι
⊢ Integrable f (μ.restrict (Ioi a ∩ Iic (b i)))
-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem Gamma_mul_Gamma_one_sub (z : ℂ) : Gamma z * Gamma (1 - z) = π / sin (π * z)

Proof state:
case h.e'_3
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ (fun n => ↑n / (↑n + 1 - z)) = fun n => ↑n / (↑n + (1 - z))

Tactic:
ext1 n

Result:
case h.e'_3.h
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
n : ℕ
⊢ ↑n / (↑n + 1 - z) = ↑n / (↑n + (1 - z))

Proof state:
case neg.convert_4.convert_5
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ Tendsto (fun n => (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ↑π) atTop (𝓝 (sin (↑π * z)))

Tactic:
convert tendsto_euler_sin_prod z using 1

Result:
case h.e'_3
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ (fun n => (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ↑π) = fun n =>
    ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)

Proof state:
case neg.convert_3
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ Tendsto (fun n => ↑n / (↑n + 1 - z)) atTop (𝓝 1)

Tactic:
convert tendsto_natCast_div_add_atTop (1 - z) using 1

Result:
case h.e'_3
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ (fun n => ↑n / (↑n + 1 - z)) = fun n => ↑n / (↑n + (1 - z))

Proof state:
case h.e'_3.h
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
n : ℕ
⊢ ↑n / (↑n + 1 - z) = ↑n / (↑n + (1 - z))

Tactic:
rw [add_sub_assoc]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem C_natAbs (n : ℤ) : C R n.natAbs = C R n

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ C R ↑n.natAbs = C R n

Tactic:
obtain h | h := Int.natAbs_eq n <;> nth_rw 2 [h]

Result:
case inr
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : n = -↑n.natAbs
⊢ C R ↑n.natAbs = C R (-↑n.natAbs)

Proof state:
case inr
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : n = -↑n.natAbs
⊢ C R ↑n.natAbs = C R (-↑n.natAbs)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem map_comp_map (g : β → γ) (f : α → β) : map g ∘ map f = map (g ∘ f)

Proof state:
case h.h.a
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
l : List α
i✝ : ℕ
a✝ : γ
⊢ a✝ ∈ ((map g ∘ map f) l)[i✝]? ↔ a✝ ∈ (map (g ∘ f) l)[i✝]?

Tactic:
rw [comp_map, Function.comp_apply]

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ map g ∘ map f = map (g ∘ f)

Tactic:
ext l

Result:
case h.h.a
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
l : List α
i✝ : ℕ
a✝ : γ
⊢ a✝ ∈ ((map g ∘ map f) l)[i✝]? ↔ a✝ ∈ (map (g ∘ f) l)[i✝]?
-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.inf {t₁ t₂ : TopologicalSpace β} {B₁ B₂ : Set (Set β)}
    (h₁ : IsTopologicalBasis (t := t₁) B₁) (h₂ : IsTopologicalBasis (t := t₂) B₂) :
    IsTopologicalBasis (t := t₁ ⊓ t₂) (image2 (· ∩ ·) B₁ B₂)

Proof state:
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
⊢ IsTopologicalBasis (image2 (fun x1 x2 => x1 ∩ x2) B₁ B₂)

Tactic:
refine .of_hasBasis_nhds (t := ?_) fun a ↦ ?_

Result:
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : β
⊢ (𝓝 a).HasBasis (fun t => t ∈ image2 (fun x1 x2 => x1 ∩ x2) B₁ B₂ ∧ a ∈ t) id

Proof state:
case h.e'_4.h.a
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : β
x✝ : Set β
⊢ x✝ ∈ image2 (fun x1 x2 => x1 ∩ x2) B₁ B₂ ∧ a ∈ x✝ ↔
    x✝ ∈ (fun i => i.1 ∩ i.2) '' {i | (i.1 ∈ B₁ ∧ a ∈ i.1) ∧ i.2 ∈ B₂ ∧ a ∈ i.2}

Tactic:
aesop

Result:
no goals

Proof state:
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : β
⊢ (𝓝 a ⊓ 𝓝 a).HasBasis (fun t => t ∈ image2 (fun x1 x2 => x1 ∩ x2) B₁ B₂ ∧ a ∈ t) id

Tactic:
convert ((h₁.nhds_hasBasis (t := t₁)).inf (h₂.nhds_hasBasis (t := t₂))).to_image_id

Result:
case h.e'_4.h.a
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : β
x✝ : Set β
⊢ x✝ ∈ image2 (fun x1 x2 => x1 ∩ x2) B₁ B₂ ∧ a ∈ x✝ ↔
    x✝ ∈ (fun i => i.1 ∩ i.2) '' {i | (i.1 ∈ B₁ ∧ a ∈ i.1) ∧ i.2 ∈ B₂ ∧ a ∈ i.2}

Proof state:
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : β
⊢ (𝓝 a).HasBasis (fun t => t ∈ image2 (fun x1 x2 => x1 ∩ x2) B₁ B₂ ∧ a ∈ t) id

Tactic:
rw [nhds_inf (t₁ := t₁)]

Result:
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : β
⊢ (𝓝 a ⊓ 𝓝 a).HasBasis (fun t => t ∈ image2 (fun x1 x2 => x1 ∩ x2) B₁ B₂ ∧ a ∈ t) id
-- Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
theorem eq_of_locally_eq' (V : Opens X) (iUV : ∀ i : ι, U i ⟶ V) (hcover : V ≤ iSup U)
    (s t : ToType (F.1.obj (op V))) (h : ∀ i, F.1.map (iUV i).op s = F.1.map (iUV i).op t) :
    s = t

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.val.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = (ConcreteCategory.hom (F.val.map (iUV i).op)) t
⊢ s = t

Tactic:
have V_eq_supr_U : V = iSup U := le_antisymm hcover (iSup_le fun i => (iUV i).le)

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.val.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = (ConcreteCategory.hom (F.val.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
⊢ s = t

Proof state:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.val.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = (ConcreteCategory.hom (F.val.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
i : ι
⊢ (ConcreteCategory.hom (F.val.map ((eqToHom ⋯).op ≫ (leSupr U i).op))) s =
    (ConcreteCategory.hom (F.val.map ((eqToHom ⋯).op ≫ (leSupr U i).op))) t

Tactic:
exact h i

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem re_inner_adjoint_mul_self_nonneg (T : E →ₗ[𝕜] E) (x : E) :
    0 ≤ re ⟪x, (LinearMap.adjoint T * T) x⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ 0 ≤ re ⟪x, (adjoint T * T) x⟫_𝕜

Tactic:
simp only [mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ 0 ≤ re (↑‖T x‖ ^ 2)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ 0 ≤ re (↑‖T x‖ ^ 2)

Tactic:
norm_cast

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ 0 ≤ ‖T x‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ 0 ≤ ‖T x‖ ^ 2

Tactic:
exact sq_nonneg _

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem not_mem_top {n m : ℕ} : m ∉ Ico n m

Proof state:
n m : ℕ
⊢ ¬m ∈ Ico n m

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem pmul [CommSemiring R] {f g : ArithmeticFunction R} (hf : f.IsMultiplicative)
    (hg : g.IsMultiplicative) : IsMultiplicative (f.pmul g) :=
  ⟨by simp [hf, hg], fun {m n} cop => by
    simp only [pmul_apply, hf.map_mul_of_coprime cop, hg.map_mul_of_coprime cop]
    ring⟩

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ (f.pmul g) (m * n) = (f.pmul g) m * (f.pmul g) n

Tactic:
simp only [pmul_apply, hf.map_mul_of_coprime cop, hg.map_mul_of_coprime cop]

Result:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ f m * f n * (g m * g n) = f m * g m * (f n * g n)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ f m * f n * (g m * g n) = f m * g m * (f n * g n)

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
⊢ (f.pmul g) 1 = 1

Tactic:
simp [hf, hg]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem le_mk_iff_exists_subset {c : Cardinal} {α : Type u} {s : Set α} :
    c ≤ #s ↔ ∃ p : Set α, p ⊆ s ∧ #p = c

Proof state:
c : Cardinal.{u}
α : Type u
s : Set α
⊢ c ≤ #↑s ↔ ∃ p ⊆ s, #↑p = c

Tactic:
rw [le_mk_iff_exists_set, ← Subtype.exists_set_subtype]

Result:
c : Cardinal.{u}
α : Type u
s : Set α
⊢ (∃ p, #↑p = c) ↔ ∃ s_1, #↑(Subtype.val '' s_1) = c

Proof state:
case h
c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ #↑t = c ↔ #↑(Subtype.val '' t) = c

Tactic:
rw [mk_image_eq]

Result:
case h
c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ Injective Subtype.val

Proof state:
case h
c : Cardinal.{u}
α : Type u
s : Set α
⊢ ∀ (a : Set ↑s), #↑a = c ↔ #↑(Subtype.val '' a) = c

Tactic:
intro t

Result:
case h
c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ #↑t = c ↔ #↑(Subtype.val '' t) = c

Proof state:
case h
c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ Injective Subtype.val

Tactic:
apply Subtype.val_injective

Result:
no goals

Proof state:
c : Cardinal.{u}
α : Type u
s : Set α
⊢ (∃ p, #↑p = c) ↔ ∃ s_1, #↑(Subtype.val '' s_1) = c

Tactic:
apply exists_congr

Result:
case h
c : Cardinal.{u}
α : Type u
s : Set α
⊢ ∀ (a : Set ↑s), #↑a = c ↔ #↑(Subtype.val '' a) = c
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem smul (h : IsFundamentalDomain G s μ) (g : G) : IsFundamentalDomain G (g • s) μ :=
  h.image_of_equiv (MulAction.toPerm g) (measurePreserving_smul _ _).quasiMeasurePreserving
    ⟨fun g' => g⁻¹ * g' * g, fun g' => g * g' * g⁻¹, fun g' => by simp [mul_assoc], fun g' => by
      simp [mul_assoc]⟩
    fun g' x => by simp [smul_smul, mul_assoc]

Proof state:
G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
h : IsFundamentalDomain G s μ
g g' : G
x : α
⊢ (MulAction.toPerm g)
      ((fun x =>
          { toFun := fun g' => g⁻¹ * g' * g, invFun := fun g' => g * g' * g⁻¹, left_inv := ⋯, right_inv := ⋯ } g' • x)
        x) =
    (fun x => g' • x) ((MulAction.toPerm g) x)

Tactic:
simp [smul_smul, mul_assoc]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
h : IsFundamentalDomain G s μ
g g' : G
⊢ (fun g' => g * g' * g⁻¹) ((fun g' => g⁻¹ * g' * g) g') = g'

Tactic:
simp [mul_assoc]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
h : IsFundamentalDomain G s μ
g g' : G
⊢ (fun g' => g⁻¹ * g' * g) ((fun g' => g * g' * g⁻¹) g') = g'

Tactic:
simp [mul_assoc]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Differentials.lean
lemma comm₁₂ : pres.toExtension.cotangentComplex.comp (hom₁ pres) =
    pres.cotangentSpaceBasis.repr.symm.comp (differentialsRelations pres).map

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
⊢ pres.toExtension.cotangentComplex ∘ₗ hom₁ pres =
    ↑pres.cotangentSpaceBasis.repr.symm ∘ₗ pres.differentialsRelations.map

Tactic:
ext r

Result:
case h.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
r : pres.rels
⊢ ((pres.toExtension.cotangentComplex ∘ₗ hom₁ pres) ∘ₗ Finsupp.lsingle r) 1 =
    ((↑pres.cotangentSpaceBasis.repr.symm ∘ₗ pres.differentialsRelations.map) ∘ₗ Finsupp.lsingle r) 1

Proof state:
case h.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
r : pres.rels
this : ∀ (r : pres.rels), pres.differentialsRelations.map (Finsupp.single r 1) = pres.differentialsRelations.relation r
⊢ pres.toExtension.cotangentComplex ((hom₁ pres) (Finsupp.single r 1)) =
    pres.cotangentSpaceBasis.repr.symm (pres.differentialsRelations.map (Finsupp.single r 1))

Tactic:
rw [comm₁₂_single, this]

Result:
no goals

Proof state:
case h.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
r : pres.rels
⊢ ((pres.toExtension.cotangentComplex ∘ₗ hom₁ pres) ∘ₗ Finsupp.lsingle r) 1 =
    ((↑pres.cotangentSpaceBasis.repr.symm ∘ₗ pres.differentialsRelations.map) ∘ₗ Finsupp.lsingle r) 1

Tactic:
have := (differentialsRelations pres).map_single

Result:
case h.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
r : pres.rels
this :
  ∀ (r : pres.differentialsRelations.R),
    pres.differentialsRelations.map (Finsupp.single r 1) = pres.differentialsRelations.relation r
⊢ ((pres.toExtension.cotangentComplex ∘ₗ hom₁ pres) ∘ₗ Finsupp.lsingle r) 1 =
    ((↑pres.cotangentSpaceBasis.repr.symm ∘ₗ pres.differentialsRelations.map) ∘ₗ Finsupp.lsingle r) 1

Proof state:
case h.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
r : pres.rels
this :
  ∀ (r : pres.differentialsRelations.R),
    pres.differentialsRelations.map (Finsupp.single r 1) = pres.differentialsRelations.relation r
⊢ ((pres.toExtension.cotangentComplex ∘ₗ hom₁ pres) ∘ₗ Finsupp.lsingle r) 1 =
    ((↑pres.cotangentSpaceBasis.repr.symm ∘ₗ pres.differentialsRelations.map) ∘ₗ Finsupp.lsingle r) 1

Tactic:
dsimp at this ⊢

Result:
case h.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
r : pres.rels
this : ∀ (r : pres.rels), pres.differentialsRelations.map (Finsupp.single r 1) = pres.differentialsRelations.relation r
⊢ pres.toExtension.cotangentComplex ((hom₁ pres) (Finsupp.single r 1)) =
    pres.cotangentSpaceBasis.repr.symm (pres.differentialsRelations.map (Finsupp.single r 1))
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0∞} (hr : r < 1) :
    Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0)

Proof state:
case intro.intro
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ Tendsto (fun n => ↑r ^ n) atTop (𝓝 0)

Tactic:
rw [← ENNReal.coe_zero]

Result:
case intro.intro
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ Tendsto (fun n => ↑r ^ n) atTop (𝓝 ↑0)

Proof state:
case intro.intro
r : ℝ≥0
hr' hr : r < 1
⊢ Tendsto (HPow.hPow r) atTop (𝓝 0)

Tactic:
apply NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one hr

Result:
no goals

Proof state:
case intro.intro
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ Tendsto (fun n => ↑r ^ n) atTop (𝓝 ↑0)

Tactic:
norm_cast at *

Result:
case intro.intro
r : ℝ≥0
hr' hr : r < 1
⊢ Tendsto (HPow.hPow r) atTop (𝓝 0)

Proof state:
r : ℝ≥0∞
hr : r < 1
⊢ Tendsto (fun n => r ^ n) atTop (𝓝 0)

Tactic:
rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩

Result:
case intro.intro
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ Tendsto (fun n => ↑r ^ n) atTop (𝓝 0)
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
lemma isZero₁_of_isZero₂₃ (h₂ : IsZero T.obj₂) (h₃ : IsZero T.obj₃) : IsZero T.obj₁

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₂ : IsZero T.obj₂
h₃ : IsZero T.obj₃
⊢ T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
exact ⟨h₂.eq_of_tgt _ _, h₃.eq_of_src _ _⟩

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₂ : IsZero T.obj₂
h₃ : IsZero T.obj₃
⊢ IsZero T.obj₁

Tactic:
rw [T.isZero₁_iff hT]

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₂ : IsZero T.obj₂
h₃ : IsZero T.obj₃
⊢ T.mor₁ = 0 ∧ T.mor₃ = 0
-- Mathlib/Data/ENNReal/Real.lean
theorem toNNReal_le_toNNReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toNNReal ≤ b.toNNReal ↔ a ≤ b :=
  ⟨fun h => by rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_le_coe], toNNReal_mono hb⟩

Proof state:
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ ⊤
h : a.toNNReal ≤ b.toNNReal
⊢ a ≤ b

Tactic:
rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_le_coe]

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem chain_map (f : β → α) {b : β} {l : List β} :
    Chain R (f b) (map f l) ↔ Chain (fun a b : β => R (f a) (f b)) b l

Proof state:
α : Type u
β : Type v
R : α → α → Prop
f : β → α
b : β
l : List β
⊢ Chain R (f b) (map f l) ↔ Chain (fun a b => R (f a) (f b)) b l

Tactic:
induction l generalizing b <;> simp only [map, Chain.nil, chain_cons, *]

Result:
no goals