harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/Primrec.lean
theorem curry {f : α × β → σ} : Primrec₂ (Function.curry f) ↔ Primrec f

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α × β → σ
⊢ Primrec₂ (Function.curry f) ↔ Primrec f

Tactic:
rw [← uncurry, Function.uncurry_curry]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_reverse' {l : Array α} (i j) (h : i + j + 1 = l.size) : l.reverse[i]? = l[j]?

Proof state:
α : Type u_1
l : Array α
i j : Nat
h : i + j + 1 = l.size
⊢ l.reverse[i]? = l[j]?

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
i j : Nat
l : List α
h : i + j + 1 = { toList := l }.size
⊢ { toList := l }.reverse[i]? = { toList := l }[j]?

Proof state:
case mk
α : Type u_1
i j : Nat
l : List α
h : i + j + 1 = l.length
⊢ { toList := l }.reverse[i]? = { toList := l }[j]?

Tactic:
simp only [List.reverse_toArray, List.getElem?_toArray]

Result:
case mk
α : Type u_1
i j : Nat
l : List α
h : i + j + 1 = l.length
⊢ l.reverse[i]? = l[j]?

Proof state:
case mk
α : Type u_1
i j : Nat
l : List α
h : i + j + 1 = { toList := l }.size
⊢ { toList := l }.reverse[i]? = { toList := l }[j]?

Tactic:
simp at h

Result:
case mk
α : Type u_1
i j : Nat
l : List α
h : i + j + 1 = l.length
⊢ { toList := l }.reverse[i]? = { toList := l }[j]?

Proof state:
case mk
α : Type u_1
i j : Nat
l : List α
h : i + j + 1 = l.length
⊢ l.reverse[i]? = l[j]?

Tactic:
rw [List.getElem?_reverse' (l := l) _ _ h]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Even.lean
theorem even.algHom_ext ⦃f g : even Q →ₐ[R] A⦄ (h : (even.ι Q).compr₂ f = (even.ι Q).compr₂ g) :
    f = g

Proof state:
case H.mk.ι_mul_ι_mul
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x✝ : CliffordAlgebra Q
m₁ m₂ : M
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
ih : f ⟨x, hx⟩ = g ⟨x, hx⟩
this :
  (fun x1 x2 => x1 * x2) ((((ι Q).compr₂ f).bilin m₁) m₂) (f ⟨x, hx⟩) =
    (fun x1 x2 => x1 * x2) ((((ι Q).compr₂ g).bilin m₁) m₂) (g ⟨x, hx⟩)
⊢ f ⟨(CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x, ⋯⟩ =
    g ⟨(CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x, ⋯⟩

Tactic:
exact (map_mul f _ _).trans (this.trans <| (map_mul g _ _).symm)

Result:
no goals

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f g : ↥(even Q) →ₐ[R] A
h : (ι Q).compr₂ f = (ι Q).compr₂ g
⊢ f = g

Tactic:
rw [EvenHom.ext_iff] at h

Result:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
⊢ f = g

Proof state:
case H.mk.add
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x✝ x y : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
hy : y ∈ evenOdd Q 0
ihx : f ⟨x, hx⟩ = g ⟨x, hx⟩
ihy : f ⟨y, hy⟩ = g ⟨y, hy⟩
this : (fun x1 x2 => x1 + x2) (f ⟨x, hx⟩) (f ⟨y, hy⟩) = (fun x1 x2 => x1 + x2) (g ⟨x, hx⟩) (g ⟨y, hy⟩)
⊢ f ⟨x + y, ⋯⟩ = g ⟨x + y, ⋯⟩

Tactic:
exact (map_add f _ _).trans (this.trans <| (map_add g _ _).symm)

Result:
no goals

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
⊢ f = g

Tactic:
ext ⟨x, hx⟩

Result:
case H.mk
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x : CliffordAlgebra Q
hx : x ∈ even Q
⊢ f ⟨x, hx⟩ = g ⟨x, hx⟩

Proof state:
case H.mk.algebraMap
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x : CliffordAlgebra Q
r : R
⊢ f ⟨(algebraMap R (CliffordAlgebra Q)) r, ⋯⟩ = g ⟨(algebraMap R (CliffordAlgebra Q)) r, ⋯⟩

Tactic:
exact (f.commutes r).trans (g.commutes r).symm

Result:
no goals
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem rank_prime_pow_ramificationIdx [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime]
    (hP0 : P ≠ ⊥) (he : e ≠ 0) :
    Module.rank (R ⧸ p) (S ⧸ P ^ e) =
      e •
        @Module.rank (R ⧸ p) (S ⧸ P) _ _
          (@Algebra.toModule _ _ _ _ <|
            @Quotient.algebraQuotientOfRamificationIdxNeZero _ _ _ _ _ _ _ ⟨he⟩)

Proof state:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
this : NeZero e := { out := he }
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)

Tactic:
have := rank_pow_quot p P hP0 0 (Nat.zero_le e)

Result:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ 0)) = (e - 0) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)

Proof state:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)

Tactic:
letI : NeZero e := ⟨he⟩

Result:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
this : NeZero e := { out := he }
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)

Proof state:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ 0)) = (e - 0) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)

Tactic:
rw [pow_zero, Nat.sub_zero, Ideal.one_eq_top, Ideal.map_top] at this

Result:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Module.rank (R ⧸ p) ↥⊤ = e • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)

Proof state:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Module.rank (R ⧸ p) ↥⊤ = e • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)

Tactic:
exact (rank_top (R ⧸ p) _).symm.trans this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem getElem?_range' (s step) :
    ∀ {m n : Nat}, m < n → (range' s n step)[m]? = some (s + step * m)
  | 0, n + 1, _ => by simp [range'_succ]
  | m + 1, n + 1, h => by
    simp only [range'_succ, getElem?_cons_succ]
    exact (getElem?_range' (s + step) step (by exact succ_lt_succ_iff.mp h)).trans <| by
      simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]

Proof state:
s step m n : Nat
h : m + 1 < n + 1
⊢ m < n

Tactic:
exact succ_lt_succ_iff.mp h

Result:
no goals

Proof state:
s step n : Nat
x✝ : 0 < n + 1
⊢ (range' s (n + 1) step)[0]? = some (s + step * 0)

Tactic:
simp [range'_succ]

Result:
no goals

Proof state:
s step m n : Nat
h : m + 1 < n + 1
⊢ some (s + step + step * m) = some (s + step * (m + 1))

Tactic:
simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]

Result:
no goals

Proof state:
s step m n : Nat
h : m + 1 < n + 1
⊢ (range' s (n + 1) step)[m + 1]? = some (s + step * (m + 1))

Tactic:
simp only [range'_succ, getElem?_cons_succ]

Result:
s step m n : Nat
h : m + 1 < n + 1
⊢ (range' (s + step) n step)[m]? = some (s + step * (m + 1))

Proof state:
s step m n : Nat
h : m + 1 < n + 1
⊢ (range' (s + step) n step)[m]? = some (s + step * (m + 1))

Tactic:
exact (getElem?_range' (s + step) step (by exact succ_lt_succ_iff.mp h)).trans <| by
  simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem closedBall_add_closedBall [ProperSpace E] (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (a b : E) :
    closedBall a ε + closedBall b δ = closedBall (a + b) (ε + δ)

Proof state:
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
δ ε : ℝ
inst✝ : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)

Tactic:
rw [(isCompact_closedBall _ _).add_closedBall hδ b, cthickening_closedBall hδ hε a,
  Metric.vadd_closedBall, vadd_eq_add, add_comm, add_comm δ]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem nonempty_sInter {c : Set (Set α)} : (⋂₀ c).Nonempty ↔ ∃ a, ∀ b ∈ c, a ∈ b

Proof state:
α : Type u_1
c : Set (Set α)
⊢ (⋂₀ c).Nonempty ↔ ∃ a, ∀ b ∈ c, a ∈ b

Tactic:
simp [nonempty_iff_ne_empty, sInter_eq_empty_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basis.lean
theorem _root_.LinearMap.BilinMap.toQuadraticMap_surjective [Module.Free R M] :
    Function.Surjective (LinearMap.BilinMap.toQuadraticMap : LinearMap.BilinMap R M N → _)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module.Free R M
⊢ Function.Surjective BilinMap.toQuadraticMap

Tactic:
intro Q

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module.Free R M
Q : QuadraticMap R M N
⊢ ∃ a, a.toQuadraticMap = Q

Proof state:
case intro.mk
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module.Free R M
Q : QuadraticMap R M N
ι : Type u_2
b : Basis ι R M
this : LinearOrder ι := IsWellOrder.linearOrder WellOrderingRel
⊢ ∃ a, a.toQuadraticMap = Q

Tactic:
exact ⟨_, toQuadraticMap_toBilin _ b⟩

Result:
no goals

Proof state:
case intro.mk
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module.Free R M
Q : QuadraticMap R M N
ι : Type u_2
b : Basis ι R M
⊢ ∃ a, a.toQuadraticMap = Q

Tactic:
letI : LinearOrder ι := IsWellOrder.linearOrder WellOrderingRel

Result:
case intro.mk
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module.Free R M
Q : QuadraticMap R M N
ι : Type u_2
b : Basis ι R M
this : LinearOrder ι := IsWellOrder.linearOrder WellOrderingRel
⊢ ∃ a, a.toQuadraticMap = Q

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module.Free R M
Q : QuadraticMap R M N
⊢ ∃ a, a.toQuadraticMap = Q

Tactic:
obtain ⟨ι, b⟩ := Module.Free.exists_basis (R := R) (M := M)

Result:
case intro.mk
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module.Free R M
Q : QuadraticMap R M N
ι : Type u_2
b : Basis ι R M
⊢ ∃ a, a.toQuadraticMap = Q
-- Mathlib/Data/Nat/Choose/Cast.lean
theorem cast_choose {a b : ℕ} (h : a ≤ b) : (b.choose a : K) = b ! / (a ! * (b - a)!)

Proof state:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ ↑(b.choose a) = ↑b ! / (↑a ! * ↑(b - a)!)

Tactic:
rw [eq_div_iff_mul_eq (mul_ne_zero this this)]

Result:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ ↑(b.choose a) * (↑a ! * ↑(b - a)!) = ↑b !

Proof state:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
⊢ ↑(b.choose a) = ↑b ! / (↑a ! * ↑(b - a)!)

Tactic:
have : ∀ {n : ℕ}, (n ! : K) ≠ 0 := Nat.cast_ne_zero.2 (factorial_ne_zero _)

Result:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ ↑(b.choose a) = ↑b ! / (↑a ! * ↑(b - a)!)

Proof state:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ ↑(b.choose a) * (↑a ! * ↑(b - a)!) = ↑b !

Tactic:
rw_mod_cast [← mul_assoc, choose_mul_factorial_mul_factorial h]

Result:
no goals
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_eq_zero {x : PGame} :
    birthday x = 0 ↔ IsEmpty x.LeftMoves ∧ IsEmpty x.RightMoves

Proof state:
x : PGame
⊢ x.birthday = 0 ↔ IsEmpty x.LeftMoves ∧ IsEmpty x.RightMoves

Tactic:
rw [birthday_def, max_eq_zero, lsub_eq_zero_iff, lsub_eq_zero_iff]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
theorem cauchySeq_iff_tendsto_dist_atTop_0 [Nonempty β] [SemilatticeSup β] {u : β → α} :
    CauchySeq u ↔ Tendsto (fun n : β × β => dist (u n.1) (u n.2)) atTop (𝓝 0)

Proof state:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ CauchySeq u ↔ Tendsto (fun n => dist (u n.1) (u n.2)) atTop (𝓝 0)

Tactic:
rw [cauchySeq_iff_tendsto, Metric.uniformity_eq_comap_nhds_zero, tendsto_comap_iff,
  Function.comp_def]

Result:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto (fun x => dist (Prod.map u u x).1 (Prod.map u u x).2) atTop (𝓝 0) ↔
    Tendsto (fun n => dist (u n.1) (u n.2)) atTop (𝓝 0)

Proof state:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto (fun x => dist (Prod.map u u x).1 (Prod.map u u x).2) atTop (𝓝 0) ↔
    Tendsto (fun n => dist (u n.1) (u n.2)) atTop (𝓝 0)

Tactic:
simp_rw [Prod.map_fst, Prod.map_snd]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem hasFiniteIntegral_of_dominated_convergence {F : ℕ → α → β} {f : α → β} {bound : α → ℝ}
    (bound_hasFiniteIntegral : HasFiniteIntegral bound μ)
    (h_bound : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a)
    (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))) : HasFiniteIntegral f μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ HasFiniteIntegral f μ

Tactic:
rw [hasFiniteIntegral_iff_norm]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ⊤

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ 0 ≤ᶠ[ae μ] bound

Tactic:
exact (h_bound 0).mono fun a h => le_trans (norm_nonneg _) h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ HasFiniteIntegral bound μ

Tactic:
exact bound_hasFiniteIntegral

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ⊤

Tactic:
rw [← hasFiniteIntegral_iff_ofReal]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ HasFiniteIntegral bound μ

α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ 0 ≤ᶠ[ae μ] bound
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem diam_pair : diam ({x, y} : Set α) = dist x y

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ diam {x, y} = dist x y

Tactic:
simp only [diam, EMetric.diam_pair, dist_edist]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_le_tsub_iff_right (h : c ≤ b) : a - c ≤ b - c ↔ a ≤ b

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : c ≤ b
⊢ a - c ≤ b - c ↔ a ≤ b

Tactic:
rw [tsub_le_iff_right, tsub_add_cancel_of_le h]

Result:
no goals
-- Mathlib/Algebra/Homology/ExactSequence.lean
lemma Exact.δ₀ {S : ComposableArrows C (n + 2)} (hS : S.Exact) :
    S.δ₀.Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
hS : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact ∧ S.δ₀.Exact
⊢ S.δ₀.Exact

Tactic:
exact hS.2

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
hS : S.Exact
⊢ S.δ₀.Exact

Tactic:
rw [exact_iff_δ₀] at hS

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
hS : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact ∧ S.δ₀.Exact
⊢ S.δ₀.Exact
-- Mathlib/Data/Seq/WSeq.lean
theorem liftRel_flatten {R : α → β → Prop} {c1 : Computation (WSeq α)} {c2 : Computation (WSeq β)}
    (h : c1.LiftRel (LiftRel R) c2) : LiftRel R (flatten c1) (flatten c2) :=
  let S s t := ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
  ⟨S, ⟨c1, c2, rfl, rfl, h⟩, fun {s t} h =>
    match s, t, h with
    | _, _, ⟨c1, c2, rfl, rfl, h⟩ => by
      simp only [destruct_flatten]; apply liftRel_bind _ _ h
      intro a b ab; apply Computation.LiftRel.imp _ _ _ (liftRel_destruct ab)
      intro a b; apply LiftRelO.imp_right
      intro s t h; refine ⟨Computation.pure s, Computation.pure t, ?_, ?_, ?_⟩ <;>
        -- Porting note: These 2 theorems should be excluded.
        simp [h, -liftRel_pure_left, -liftRel_pure_right]⟩

Proof state:
α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop :=
  fun s t => ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a✝ : WSeq α
b✝ : WSeq β
ab : LiftRel R a✝ b✝
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ LiftRelO R (LiftRel R) a b → LiftRelO R S a b

Tactic:
apply LiftRelO.imp_right

Result:
case H
α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop :=
  fun s t => ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a✝ : WSeq α
b✝ : WSeq β
ab : LiftRel R a✝ b✝
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ ∀ (s : WSeq α) (t : WSeq β), LiftRel R s t → S s t
-- Mathlib/Data/Option/Basic.lean
theorem map_injective' : Function.Injective (@Option.map α β) := fun f g h ↦
  funext fun x ↦ some_injective _ <| by simp only [← map_some', h]

Proof state:
α : Type u_1
β : Type u_2
f g : α → β
h : Option.map f = Option.map g
x : α
⊢ some (f x) = some (g x)

Tactic:
simp only [← map_some', h]

Result:
no goals
-- Mathlib/Order/Filter/Cofinite.lean
theorem cofinite_eq_bot_iff : @cofinite α = ⊥ ↔ Finite α

Proof state:
α : Type u_2
⊢ cofinite = ⊥ ↔ Finite α

Tactic:
simp [← empty_mem_iff_bot, finite_univ_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem max_min_distrib_right (a b c : Nat) :
    max (min a b) c = min (max a c) (max b c)

Proof state:
a b c : Nat
⊢ max (min a b) c = min (max a c) (max b c)

Tactic:
repeat rw [Nat.max_comm _ c]

Result:
a b c : Nat
⊢ max c (min a b) = min (max c a) (max c b)

Proof state:
a b c : Nat
⊢ max c (min a b) = min (max c a) (max c b)

Tactic:
exact Nat.max_min_distrib_left ..

Result:
no goals

Proof state:
a b c : Nat
⊢ max c (min a b) = min (max c a) (max b c)

Tactic:
rw [Nat.max_comm _ c]

Result:
a b c : Nat
⊢ max c (min a b) = min (max c a) (max c b)
-- Mathlib/Data/Finsupp/Weight.lean
theorem nonTorsionWeight_of [NoZeroSMulDivisors R M] (hw : ∀ i : σ, w i ≠ 0) :
    NonTorsionWeight R w where
  eq_zero_of_smul_eq_zero {n s} h

Proof state:
σ : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Semiring R
w : σ → M
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
hw : ∀ (i : σ), w i ≠ 0
n : R
s : σ
h : n • w s = 0
⊢ n = 0

Tactic:
rw [smul_eq_zero, or_iff_not_imp_right] at h

Result:
σ : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Semiring R
w : σ → M
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
hw : ∀ (i : σ), w i ≠ 0
n : R
s : σ
h : ¬w s = 0 → n = 0
⊢ n = 0

Proof state:
σ : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Semiring R
w : σ → M
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
hw : ∀ (i : σ), w i ≠ 0
n : R
s : σ
h : ¬w s = 0 → n = 0
⊢ n = 0

Tactic:
exact h (hw s)

Result:
no goals