harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Bases.lean
theorem hasBasis_iInf_of_directed {ι : Type*} {ι' : Sort _} [Nonempty ι] {l : ι → Filter α}
    (s : ι → ι' → Set α) (p : ι → ι' → Prop) (hl : ∀ i, (l i).HasBasis (p i) (s i))
    (h : Directed (· ≥ ·) l) :
    (⨅ i, l i).HasBasis (fun ii' : ι × ι' => p ii'.1 ii'.2) fun ii' => s ii'.1 ii'.2

Proof state:
α : Type u_1
ι : Type u_6
ι' : Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 => x1 ≥ x2) l
t : Set α
⊢ t ∈ ⨅ i, l i ↔ ∃ i, p i.1 i.2 ∧ s i.1 i.2 ⊆ t

Tactic:
rw [mem_iInf_of_directed h, Prod.exists]

Result:
α : Type u_1
ι : Type u_6
ι' : Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 => x1 ≥ x2) l
t : Set α
⊢ (∃ i, t ∈ l i) ↔ ∃ a b, p (a, b).1 (a, b).2 ∧ s (a, b).1 (a, b).2 ⊆ t

Proof state:
α : Type u_1
ι : Type u_6
ι' : Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 => x1 ≥ x2) l
⊢ (⨅ i, l i).HasBasis (fun ii' => p ii'.1 ii'.2) fun ii' => s ii'.1 ii'.2

Tactic:
refine ⟨fun t => ?_⟩

Result:
α : Type u_1
ι : Type u_6
ι' : Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 => x1 ≥ x2) l
t : Set α
⊢ t ∈ ⨅ i, l i ↔ ∃ i, p i.1 i.2 ∧ s i.1 i.2 ⊆ t

Proof state:
α : Type u_1
ι : Type u_6
ι' : Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 => x1 ≥ x2) l
t : Set α
⊢ (∃ i, t ∈ l i) ↔ ∃ a b, p (a, b).1 (a, b).2 ∧ s (a, b).1 (a, b).2 ⊆ t

Tactic:
exact exists_congr fun i => (hl i).mem_iff

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙHom_eq_of_continuous_of_map_id [UniqueHom R A]
    (φ : C(σₙ R a, R)₀ →⋆ₙₐ[R] A) (hφ₁ : Continuous φ)
    (hφ₂ : φ ⟨.restrict (σₙ R a) <| .id R, rfl⟩ = a) : cfcₙHom ha = φ :=
  (cfcₙHom ha).ext_continuousMap a φ (cfcₙHom_isClosedEmbedding ha).continuous hφ₁ <| by
    rw [cfcₙHom_id ha, hφ₂]

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
ha : p a
inst✝ : UniqueHom R A
φ : C(↑(σₙ R a), R)₀ →⋆ₙₐ[R] A
hφ₁ : Continuous ⇑φ
hφ₂ : φ { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } = a
⊢ (cfcₙHom ha) { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } =
    φ { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ }

Tactic:
rw [cfcₙHom_id ha, hφ₂]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem zero_add (n : Num) : 0 + n = n

Proof state:
n : Num
⊢ 0 + n = n

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
theorem isIntegral_iff_isIntegral_closure_finite {r : B} :
    IsIntegral R r ↔ ∃ s : Set R, s.Finite ∧ IsIntegral (Subring.closure s) r

Proof state:
case mp
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
hr : IsIntegral R r
⊢ ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r

Tactic:
rcases hr with ⟨p, hmp, hpr⟩

Result:
case mp.intro.intro
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
p : R[X]
hmp : p.Monic
hpr : eval₂ (algebraMap R B) r p = 0
⊢ ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r

Proof state:
case mp.intro.intro
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
p : R[X]
hmp : p.Monic
hpr : eval₂ (algebraMap R B) r p = 0
⊢ ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r

Tactic:
refine ⟨_, Finset.finite_toSet _, p.restriction, monic_restriction.2 hmp, ?_⟩

Result:
case mp.intro.intro
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
p : R[X]
hmp : p.Monic
hpr : eval₂ (algebraMap R B) r p = 0
⊢ eval₂ (algebraMap (↥(Subring.closure ↑p.coeffs)) B) r p.restriction = 0

Proof state:
case mp.intro.intro
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
p : R[X]
hmp : p.Monic
hpr : eval₂ (algebraMap R B) r p = 0
⊢ eval₂ (algebraMap (↥(Subring.closure ↑p.coeffs)) B) r p.restriction = 0

Tactic:
rw [← aeval_def, ← aeval_map_algebraMap R r p.restriction, map_restriction, aeval_def, hpr]

Result:
no goals

Proof state:
case mpr
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
hr : ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r
⊢ IsIntegral R r

Tactic:
rcases hr with ⟨s, _, hsr⟩

Result:
case mpr.intro.intro
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
s : Set R
left✝ : s.Finite
hsr : IsIntegral (↥(Subring.closure s)) r
⊢ IsIntegral R r

Proof state:
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
⊢ IsIntegral R r ↔ ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r

Tactic:
constructor <;> intro hr

Result:
case mp
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
hr : IsIntegral R r
⊢ ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r

case mpr
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
hr : ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r
⊢ IsIntegral R r

Proof state:
case mpr.intro.intro
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
s : Set R
left✝ : s.Finite
hsr : IsIntegral (↥(Subring.closure s)) r
⊢ IsIntegral R r

Tactic:
exact hsr.of_subring _

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem Partrec.dom_re {α β} [Primcodable α] [Primcodable β] {f : α →. β} (h : Partrec f) :
    REPred fun a => (f a).Dom :=
  (h.map (Computable.const ()).to₂).of_eq fun n => Part.ext fun _ => by simp [Part.dom_iff_mem]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α →. β
h : Partrec f
n : α
x✝ : Unit
⊢ x✝ ∈ Part.map (fun b => ()) (f n) ↔ x✝ ∈ Part.assert ((fun a => (f a).Dom) n) fun x => Part.some ()

Tactic:
simp [Part.dom_iff_mem]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem GammaSeq_mul (z : ℂ) {n : ℕ} (hn : n ≠ 0) :
    GammaSeq z n * GammaSeq (1 - z) n =
      n / (n + ↑1 - z) * (↑1 / (z * ∏ j ∈ Finset.range n, (↑1 - z ^ 2 / ((j : ℂ) + 1) ^ 2)))

Proof state:
z : ℂ
n : ℕ
hn : n ≠ 0
a✝ b✝ c✝ d✝ : ℂ
⊢ a✝ * b✝ * (c✝ * d✝) = a✝ * c✝ * (b✝ * d✝)

Tactic:
ring

Result:
no goals

Proof state:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
⊢ ∀ (a b c d : ℂ), a * b * (c * d) = a * (d * (b * c))

Tactic:
intros

Result:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
a✝ b✝ c✝ d✝ : ℂ
⊢ a✝ * b✝ * (c✝ * d✝) = a✝ * (d✝ * (b✝ * c✝))

Proof state:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
j : ℕ
this : ↑j + 1 ≠ 0
⊢ (z + (↑j + 1)) * (1 - z + ↑j) = (↑j + 1) ^ 2 - z ^ 2

Tactic:
ring

Result:
no goals

Proof state:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : ↑n ^ z * ↑n ^ (1 - z) = ↑n
j : ℕ
⊢ ↑j + 1 ≠ 0

Tactic:
rw [← Nat.cast_succ, Nat.cast_ne_zero]

Result:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : ↑n ^ z * ↑n ^ (1 - z) = ↑n
j : ℕ
⊢ j.succ ≠ 0

Proof state:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : ↑n ^ z * ↑n ^ (1 - z) = ↑n
⊢ ↑n ^ z * ↑n ^ (1 - z) * ↑n ! ^ 2 /
      ((∏ j ∈ Finset.range (n + 1), (z + ↑j)) * ∏ j ∈ Finset.range (n + 1), (1 - z + ↑j)) =
    ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))

Tactic:
rw [this, Finset.prod_range_succ', Finset.prod_range_succ, aux, ← Finset.prod_mul_distrib,
  Nat.cast_zero, add_zero, add_comm (1 - z) n, ← add_sub_assoc]

Result:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : ↑n ^ z * ↑n ^ (1 - z) = ↑n
⊢ ↑n * ↑n ! ^ 2 / ((∏ x ∈ Finset.range n, (z + ↑(x + 1)) * (1 - z + ↑x)) * (z * (↑n + 1 - z))) =
    ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
-- Mathlib/Data/Set/Equitable.lean
theorem Subsingleton.equitableOn {s : Set α} (hs : s.Subsingleton) (f : α → β) : s.EquitableOn f :=
  fun i j hi hj => by
  rw [hs hi hj]
  exact le_add_of_nonneg_right zero_le_one

Proof state:
α : Type u_1
β : Type u_2
inst✝ : OrderedSemiring β
s : Set α
hs : s.Subsingleton
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f i ≤ f j + 1

Tactic:
rw [hs hi hj]

Result:
α : Type u_1
β : Type u_2
inst✝ : OrderedSemiring β
s : Set α
hs : s.Subsingleton
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f j ≤ f j + 1

Proof state:
α : Type u_1
β : Type u_2
inst✝ : OrderedSemiring β
s : Set α
hs : s.Subsingleton
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f j ≤ f j + 1

Tactic:
exact le_add_of_nonneg_right zero_le_one

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem Prime.factorization {p : ℕ} (hp : Prime p) : p.factorization = single p 1

Proof state:
p : ℕ
hp : Prime p
⊢ p.factorization = single p 1

Tactic:
ext q

Result:
case h
p : ℕ
hp : Prime p
q : ℕ
⊢ p.factorization q = (single p 1) q

Proof state:
case h
p : ℕ
hp : Prime p
q : ℕ
⊢ p.factorization q = (single p 1) q

Tactic:
rw [← primeFactorsList_count_eq, primeFactorsList_prime hp, single_apply, count_singleton',
  if_congr eq_comm] <;> rfl

Result:
no goals
-- Mathlib/Probability/StrongLaw.lean
theorem abs_truncation_le_bound (f : α → ℝ) (A : ℝ) (x : α) : |truncation f A x| ≤ |A|

Proof state:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
⊢ |truncation f A x| ≤ |A|

Tactic:
simp only [truncation, Set.indicator, Set.mem_Icc, id, Function.comp_apply]

Result:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
⊢ |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |A|

Proof state:
case neg
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : f x ∉ Set.Ioc (-A) A
⊢ |0| ≤ |A|

Tactic:
simp [abs_nonneg]

Result:
no goals

Proof state:
case pos
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : f x ∈ Set.Ioc (-A) A
⊢ |f x| ≤ |A|

Tactic:
exact abs_le_abs h.2 (neg_le.2 h.1.le)

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
⊢ |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |A|

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : f x ∈ Set.Ioc (-A) A
⊢ |f x| ≤ |A|

case neg
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : f x ∉ Set.Ioc (-A) A
⊢ |0| ≤ |A|
-- Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
lemma ofComplex_apply_of_im_nonpos {w : ℂ} (hw : w.im ≤ 0) :
    ofComplex w = Classical.choice inferInstance

Proof state:
w : ℂ
hw : w.im ≤ 0
⊢ ↑ofComplex w = Classical.choice ⋯

Tactic:
simp [ofComplex_apply_eq_ite w, hw]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_insertListIfNewUnit_of_contains_eq_false_of_mem [BEq α] [EquivBEq α]
    {l : List ((_ : α) × Unit)} {toInsert : List α}
    {k k' fallback : α} (k_beq : k == k')
    (h : containsKey k l = false)
    (distinct : toInsert.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ toInsert) :
    getKeyD k' (insertListIfNewUnit l toInsert) fallback = k

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' fallback : α
k_beq : (k == k') = true
h : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ getKeyD k' (insertListIfNewUnit l toInsert) fallback = k

Tactic:
rw [getKeyD_eq_getKey?, getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem k_beq h
  distinct mem, Option.getD_some]

Result:
no goals
-- Mathlib/ModelTheory/Fraisse.lean
theorem age.has_representative_as_substructure :
    ∀ C ∈ Quotient.mk' '' L.age M, ∃ V : {V : L.Substructure M // FG V},
      ⟦Bundled.mk V⟧ = C

Proof state:
case intro.intro.intro.intro
L : Language
M : Type w
inst✝ : L.Structure M
C✝ : Quotient equivSetoid
N : Bundled L.Structure
N_eq : Quotient.mk' N = C✝
N_fg : Structure.FG L ↑N
N_incl : ↑N ↪[L] M
⊢ N_incl.toHom.range.FG

Tactic:
exact FG.range N_fg (Embedding.toHom N_incl)

Result:
no goals

Proof state:
case intro.intro.intro.intro
L : Language
M : Type w
inst✝ : L.Structure M
C✝ : Quotient equivSetoid
N : Bundled L.Structure
N_eq : Quotient.mk' N = C✝
N_fg : Structure.FG L ↑N
N_incl : ↑N ↪[L] M
⊢ ∃ V, ⟦{ α := ↥↑V, str := inferInstance }⟧ = C✝

Tactic:
refine N_eq.symm ▸ ⟨⟨N_incl.toHom.range, ?_⟩, Quotient.sound ⟨N_incl.equivRange.symm⟩⟩

Result:
case intro.intro.intro.intro
L : Language
M : Type w
inst✝ : L.Structure M
C✝ : Quotient equivSetoid
N : Bundled L.Structure
N_eq : Quotient.mk' N = C✝
N_fg : Structure.FG L ↑N
N_incl : ↑N ↪[L] M
⊢ N_incl.toHom.range.FG

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
⊢ ∀ C ∈ Quotient.mk' '' L.age M, ∃ V, ⟦{ α := ↥↑V, str := inferInstance }⟧ = C

Tactic:
rintro _ ⟨N, ⟨N_fg, ⟨N_incl⟩⟩, N_eq⟩

Result:
case intro.intro.intro.intro
L : Language
M : Type w
inst✝ : L.Structure M
C✝ : Quotient equivSetoid
N : Bundled L.Structure
N_eq : Quotient.mk' N = C✝
N_fg : Structure.FG L ↑N
N_incl : ↑N ↪[L] M
⊢ ∃ V, ⟦{ α := ↥↑V, str := inferInstance }⟧ = C✝
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem zero_of_comp_mono {X Y Z : C} {f : X ⟶ Y} (g : Y ⟶ Z) [Mono g] (h : f ≫ g = 0) : f = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono g
h : f ≫ g = 0
⊢ f = 0

Tactic:
rw [← zero_comp, cancel_mono] at h

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono g
h✝ : f ≫ g = 0
h : f = 0
⊢ f = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono g
h✝ : f ≫ g = 0
h : f = 0
⊢ f = 0

Tactic:
exact h

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem foldl_ext (f g : α → β → α) (a : α) {l : List β} (H : ∀ a : α, ∀ b ∈ l, f a b = g a b) :
    foldl f a l = foldl g a l

Proof state:
α : Type u
β : Type v
f g : α → β → α
a : α
l : List β
H : ∀ (a : α) (b : β), b ∈ l → f a b = g a b
⊢ foldl f a l = foldl g a l

Tactic:
induction l generalizing a with
| nil => rfl
| cons hd tl ih =>
  unfold foldl
  rw [ih _ fun a b bin => H a b <| mem_cons_of_mem _ bin, H a hd (mem_cons_self _ _)]

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
f g : α → β → α
hd : β
tl : List β
ih : ∀ (a : α), (∀ (a : α) (b : β), b ∈ tl → f a b = g a b) → foldl f a tl = foldl g a tl
a : α
H : ∀ (a : α) (b : β), b ∈ hd :: tl → f a b = g a b
⊢ foldl f (f a hd) tl = foldl g (g a hd) tl

Tactic:
rw [ih _ fun a b bin => H a b <| mem_cons_of_mem _ bin, H a hd (mem_cons_self _ _)]

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
f g : α → β → α
hd : β
tl : List β
ih : ∀ (a : α), (∀ (a : α) (b : β), b ∈ tl → f a b = g a b) → foldl f a tl = foldl g a tl
a : α
H : ∀ (a : α) (b : β), b ∈ hd :: tl → f a b = g a b
⊢ foldl f a (hd :: tl) = foldl g a (hd :: tl)

Tactic:
unfold foldl

Result:
case cons
α : Type u
β : Type v
f g : α → β → α
hd : β
tl : List β
ih : ∀ (a : α), (∀ (a : α) (b : β), b ∈ tl → f a b = g a b) → foldl f a tl = foldl g a tl
a : α
H : ∀ (a : α) (b : β), b ∈ hd :: tl → f a b = g a b
⊢ foldl f (f a hd) tl = foldl g (g a hd) tl

Proof state:
case nil
α : Type u
β : Type v
f g : α → β → α
a : α
H : ∀ (a : α) (b : β), b ∈ [] → f a b = g a b
⊢ foldl f a [] = foldl g a []

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem op_snd {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) :
    c.op.snd = c.inr.op

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ c.op.snd = c.inr.op

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem rfind' {f} (hf : Nat.Partrec f) :
    Nat.Partrec
      (Nat.unpaired fun a m =>
        (Nat.rfind fun n => (fun m => m = 0) <$> f (Nat.pair a (n + m))).map (· + m)) :=
  Partrec₂.unpaired'.2 <| by
    refine
      Partrec.map
        ((@Partrec₂.unpaired' fun a b : ℕ =>
              Nat.rfind fun n => (fun m => m = 0) <$> f (Nat.pair a (n + b))).1
          ?_)
        (Primrec.nat_add.comp Primrec.snd <| Primrec.snd.comp Primrec.fst).to_comp.to₂
    have : Nat.Partrec (fun a => Nat.rfind (fun n => (fun m => decide (m = 0)) <$>
      Nat.unpaired (fun a b => f (Nat.pair (Nat.unpair a).1 (b + (Nat.unpair a).2)))
        (Nat.pair a n))) :=
      rfind
        (Partrec₂.unpaired'.2
          ((Partrec.nat_iff.2 hf).comp
              (Primrec₂.pair.comp (Primrec.fst.comp <| Primrec.unpair.comp Primrec.fst)
                  (Primrec.nat_add.comp Primrec.snd
                    (Primrec.snd.comp <| Primrec.unpair.comp Primrec.fst))).to_comp))
    simpa

Proof state:
f : ℕ →. ℕ
hf : Partrec f
⊢ Partrec (unpaired fun a b => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + b)))

Tactic:
have : Nat.Partrec (fun a => Nat.rfind (fun n => (fun m => decide (m = 0)) <$>
  Nat.unpaired (fun a b => f (Nat.pair (Nat.unpair a).1 (b + (Nat.unpair a).2)))
    (Nat.pair a n))) :=
  rfind
    (Partrec₂.unpaired'.2
      ((Partrec.nat_iff.2 hf).comp
          (Primrec₂.pair.comp (Primrec.fst.comp <| Primrec.unpair.comp Primrec.fst)
              (Primrec.nat_add.comp Primrec.snd
                (Primrec.snd.comp <| Primrec.unpair.comp Primrec.fst))).to_comp))

Result:
f : ℕ →. ℕ
hf : Partrec f
this :
  Partrec fun a =>
    Nat.rfind fun n =>
      (fun m => decide (m = 0)) <$> unpaired (fun a b => f (Nat.pair (unpair a).1 (b + (unpair a).2))) (Nat.pair a n)
⊢ Partrec (unpaired fun a b => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + b)))

Proof state:
f : ℕ →. ℕ
hf : Partrec f
this :
  Partrec fun a =>
    Nat.rfind fun n =>
      (fun m => decide (m = 0)) <$> unpaired (fun a b => f (Nat.pair (unpair a).1 (b + (unpair a).2))) (Nat.pair a n)
⊢ Partrec (unpaired fun a b => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + b)))

Tactic:
simpa

Result:
no goals

Proof state:
f : ℕ →. ℕ
hf : Partrec f
⊢ Partrec₂ fun a m =>
    Part.map (fun x => x + m) (Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + m)))

Tactic:
refine
  Partrec.map
    ((@Partrec₂.unpaired' fun a b : ℕ =>
          Nat.rfind fun n => (fun m => m = 0) <$> f (Nat.pair a (n + b))).1
      ?_)
    (Primrec.nat_add.comp Primrec.snd <| Primrec.snd.comp Primrec.fst).to_comp.to₂

Result:
f : ℕ →. ℕ
hf : Partrec f
⊢ Partrec (unpaired fun a b => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + b)))
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isDetector_iff_reflectsIsomorphisms_coyoneda_obj (G : C) :
    IsDetector G ↔ (coyoneda.obj (op G)).ReflectsIsomorphisms

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (coyoneda.obj (op G)).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f

Tactic:
suffices IsIso ((coyoneda.obj (op G)).map f) by
  exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (coyoneda.obj (op G)) _ h

Result:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (coyoneda.obj (op G)).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso ((coyoneda.obj (op G)).map f)

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (coyoneda.obj (op G)).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso ((coyoneda.obj (op G)).map f)

Tactic:
rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]

Result:
no goals

Proof state:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsDetector G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso ((coyoneda.obj (op G)).map f)
h : G ⟶ B✝
⊢ ∃! h', h' ≫ f = h

Tactic:
rw [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf

Result:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsDetector G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : ∀ (b : (coyoneda.obj (op G)).obj B✝), ∃! a, (coyoneda.obj (op G)).map f a = b
h : G ⟶ B✝
⊢ ∃! h', h' ≫ f = h

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (coyoneda.obj (op G)).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
this : IsIso ((coyoneda.obj (op G)).map f)
⊢ IsIso f

Tactic:
exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (coyoneda.obj (op G)) _ h

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ IsDetector G ↔ (coyoneda.obj (op G)).ReflectsIsomorphisms

Tactic:
refine
  ⟨fun hG => ⟨fun f hf => hG.def _ fun h => ?_⟩, fun h =>
    (isDetector_def _).2 fun X Y f hf => ?_⟩

Result:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsDetector G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso ((coyoneda.obj (op G)).map f)
h : G ⟶ B✝
⊢ ∃! h', h' ≫ f = h

case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (coyoneda.obj (op G)).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f

Proof state:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsDetector G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : ∀ (b : (coyoneda.obj (op G)).obj B✝), ∃! a, (coyoneda.obj (op G)).map f a = b
h : G ⟶ B✝
⊢ ∃! h', h' ≫ f = h

Tactic:
exact hf h

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem μ_bddBelow (s : ℕ → ℕ) {x : R} (ψ : ℕ → ℕ) :
    BddBelow {a : ℝ |
      ∀ᶠ n : ℝ in map (fun n : ℕ => μ x ^ (↑(s (ψ n)) * (1 / (ψ n : ℝ)))) atTop, n ≤ a}

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
⊢ BddBelow {a | ∀ᶠ (n : ℝ) in map (fun n => μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a}

Tactic:
use 0

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
⊢ 0 ∈ lowerBounds {a | ∀ᶠ (n : ℝ) in map (fun n => μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a}

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
⊢ ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → 0 ≤ x_1

Tactic:
intro r m hm

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
r : ℝ
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ r
⊢ 0 ≤ r

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
⊢ 0 ∈ lowerBounds {a | ∀ᶠ (n : ℝ) in map (fun n => μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a}

Tactic:
simp only [mem_lowerBounds, eventually_map, eventually_atTop, ge_iff_le, Set.mem_setOf_eq,
  forall_exists_index]

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
⊢ ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → 0 ≤ x_1

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
r : ℝ
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ r
⊢ 0 ≤ r

Tactic:
exact le_trans (rpow_nonneg (apply_nonneg μ _) _) (hm m (le_refl _))

Result:
no goals