harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Monoid.lean
theorem continuous_finprod {f : ι → X → M} (hc : ∀ i, Continuous (f i))
    (hf : LocallyFinite fun i => mulSupport (f i)) : Continuous fun x => ∏ᶠ i, f i x

Proof state:
case intro
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, ∏ᶠ (i : ι), f i y = ∏ i ∈ s, f i y
⊢ ContinuousAt (fun x => ∏ᶠ (i : ι), f i x) x

Tactic:
refine ContinuousAt.congr ?_ (EventuallyEq.symm hs)

Result:
case intro
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, ∏ᶠ (i : ι), f i y = ∏ i ∈ s, f i y
⊢ ContinuousAt (fun x => ∏ i ∈ s, f i x) x

Proof state:
case intro
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, ∏ᶠ (i : ι), f i y = ∏ i ∈ s, f i y
⊢ ContinuousAt (fun x => ∏ i ∈ s, f i x) x

Tactic:
exact tendsto_finset_prod _ fun i _ => (hc i).continuousAt

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
⊢ ContinuousAt (fun x => ∏ᶠ (i : ι), f i x) x

Tactic:
rcases finprod_eventually_eq_prod hf x with ⟨s, hs⟩

Result:
case intro
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, ∏ᶠ (i : ι), f i y = ∏ i ∈ s, f i y
⊢ ContinuousAt (fun x => ∏ᶠ (i : ι), f i x) x

Proof state:
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ Continuous fun x => ∏ᶠ (i : ι), f i x

Tactic:
refine continuous_iff_continuousAt.2 fun x => ?_

Result:
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
⊢ ContinuousAt (fun x => ∏ᶠ (i : ι), f i x) x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem shiftLeft_add {w : Nat} (x : BitVec w) (n m : Nat) :
    x <<< (n + m) = (x <<< n) <<< m

Proof state:
w : Nat
x : BitVec w
n m i : Nat
a✝ : i < w
⊢ i - (n + m) = i - m - n

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n m : Nat
⊢ x <<< (n + m) = x <<< n <<< m

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec w
n m i : Nat
a✝ : i < w
⊢ (x <<< (n + m)).getLsbD i = (x <<< n <<< m).getLsbD i

Proof state:
case pred
w : Nat
x : BitVec w
n m i : Nat
a✝ : i < w
⊢ (x <<< (n + m)).getLsbD i = (x <<< n <<< m).getLsbD i

Tactic:
simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and]

Result:
case pred
w : Nat
x : BitVec w
n m i : Nat
a✝ : i < w
⊢ (decide (i < w) && !decide (i < n + m) && x.getLsbD (i - (n + m))) =
    (decide (i < w) && !decide (i < m) && (decide (i - m < w) && !decide (i - m < n) && x.getLsbD (i - m - n)))

Proof state:
case pred
w : Nat
x : BitVec w
n m i : Nat
a✝ : i < w
⊢ (decide (i < w) && !decide (i < n + m) && x.getLsbD (i - m - n)) =
    (decide (i < w) && !decide (i < m) && (decide (i - m < w) && !decide (i - m < n) && x.getLsbD (i - m - n)))

Tactic:
cases h₂ : decide (i < m) <;>
cases h₃ : decide (i - m < w) <;>
cases h₄ : decide (i - m < n) <;>
cases h₅ : decide (i < n + m) <;>
  simp at * <;> omega

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
n m i : Nat
a✝ : i < w
⊢ (decide (i < w) && !decide (i < n + m) && x.getLsbD (i - (n + m))) =
    (decide (i < w) && !decide (i < m) && (decide (i - m < w) && !decide (i - m < n) && x.getLsbD (i - m - n)))

Tactic:
rw [show i - (n + m) = (i - m - n) by omega]

Result:
case pred
w : Nat
x : BitVec w
n m i : Nat
a✝ : i < w
⊢ (decide (i < w) && !decide (i < n + m) && x.getLsbD (i - m - n)) =
    (decide (i < w) && !decide (i < m) && (decide (i - m < w) && !decide (i - m < n) && x.getLsbD (i - m - n)))
-- Mathlib/Data/Set/Sigma.lean
theorem range_sigmaMk (i : ι) : range (Sigma.mk i : α i → Sigma α) = Sigma.fst ⁻¹' {i}

Proof state:
ι : Type u_1
α : ι → Type u_3
i : ι
⊢ range (Sigma.mk i) = Sigma.fst ⁻¹' {i}

Tactic:
apply Subset.antisymm

Result:
case h₁
ι : Type u_1
α : ι → Type u_3
i : ι
⊢ range (Sigma.mk i) ⊆ Sigma.fst ⁻¹' {i}

case h₂
ι : Type u_1
α : ι → Type u_3
i : ι
⊢ Sigma.fst ⁻¹' {i} ⊆ range (Sigma.mk i)

Proof state:
case h₁
ι : Type u_1
α : ι → Type u_3
i : ι
⊢ range (Sigma.mk i) ⊆ Sigma.fst ⁻¹' {i}

Tactic:
rintro _ ⟨b, rfl⟩

Result:
case h₁.intro
ι : Type u_1
α : ι → Type u_3
i : ι
b : α i
⊢ ⟨i, b⟩ ∈ Sigma.fst ⁻¹' {i}

Proof state:
case h₁.intro
ι : Type u_1
α : ι → Type u_3
i : ι
b : α i
⊢ ⟨i, b⟩ ∈ Sigma.fst ⁻¹' {i}

Tactic:
simp

Result:
no goals

Proof state:
case h₂
ι : Type u_1
α : ι → Type u_3
i : ι
⊢ Sigma.fst ⁻¹' {i} ⊆ range (Sigma.mk i)

Tactic:
rintro ⟨x, y⟩ (rfl | _)

Result:
case h₂.mk.refl
ι : Type u_1
α : ι → Type u_3
x : ι
y : α x
⊢ ⟨x, y⟩ ∈ range (Sigma.mk ⟨x, y⟩.fst)

Proof state:
case h₂.mk.refl
ι : Type u_1
α : ι → Type u_3
x : ι
y : α x
⊢ ⟨x, y⟩ ∈ range (Sigma.mk ⟨x, y⟩.fst)

Tactic:
exact mem_range_self y

Result:
no goals
-- Mathlib/Order/Interval/Finset/Defs.lean
@[simp] lemma toFinset_Ioo (a b : α) [Fintype (Ioo a b)] : (Ioo a b).toFinset = Finset.Ioo a b

Proof state:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ioo a b)
⊢ (Ioo a b).toFinset = Finset.Ioo a b

Tactic:
ext

Result:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ioo a b)
a✝ : α
⊢ a✝ ∈ (Ioo a b).toFinset ↔ a✝ ∈ Finset.Ioo a b

Proof state:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ioo a b)
a✝ : α
⊢ a✝ ∈ (Ioo a b).toFinset ↔ a✝ ∈ Finset.Ioo a b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem isUnit_iff : IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a

Proof state:
case mpr.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit {a}

Tactic:
exact ha.finset

Result:
no goals

Proof state:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a

Tactic:
rintro ⟨u, rfl⟩

Result:
case mp.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
⊢ ∃ a, ↑u = {a} ∧ IsUnit a

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ∃ a, ↑u = {a} ∧ IsUnit a

Tactic:
refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ {b * a} = {1}

Proof state:
case mp.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
⊢ ∃ a, ↑u = {a} ∧ IsUnit a

Tactic:
obtain ⟨a, b, ha, hb, h⟩ := Finset.mul_eq_one_iff.1 u.mul_inv

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ∃ a, ↑u = {a} ∧ IsUnit a

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = {1}

Tactic:
exact u.inv_mul

Result:
no goals

Proof state:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s

Tactic:
rintro ⟨a, rfl, ha⟩

Result:
case mpr.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit {a}

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a

Tactic:
constructor

Result:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a

case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ {b * a} = {1}

Tactic:
rw [← singleton_mul_singleton, ← ha, ← hb]

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = {1}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem ne_of_beq_false [BEq α] [LawfulBEq α] {a b : α} (h : (a == b) = false) : a ≠ b

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : (a == a) = false
⊢ False

Tactic:
have : true = false := Eq.trans LawfulBEq.rfl.symm h

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : (a == a) = false
this : true = false
⊢ False

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : (a == a) = false
this : true = false
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : (a == b) = false
⊢ a ≠ b

Tactic:
intro h'

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : (a == b) = false
h' : a = b
⊢ False

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : (a == b) = false
h' : a = b
⊢ False

Tactic:
subst h'

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : (a == a) = false
⊢ False
-- Mathlib/Algebra/CharP/Algebra.lean
theorem CharP.dvd_of_ringHom {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A]
    (f : R →+* A) (p q : ℕ) [CharP R p] [CharP A q] : q ∣ p

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring A
f : R →+* A
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP A q
⊢ q ∣ p

Tactic:
refine (CharP.cast_eq_zero_iff A q p).mp ?_

Result:
R : Type u_1
A : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring A
f : R →+* A
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP A q
⊢ ↑p = 0

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring A
f : R →+* A
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP A q
⊢ ↑p = 0

Tactic:
rw [← map_natCast f p, CharP.cast_eq_zero, map_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_filter (l : List α) :
    countP p (filter q l) = countP (fun a => p a && q a) l

Proof state:
α : Type u_1
p q : α → Bool
l : List α
⊢ countP p (filter q l) = countP (fun a => p a && q a) l

Tactic:
simp only [countP_eq_length_filter, filter_filter]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
theorem congr_app {X Y : Scheme} {f g : X ⟶ Y} (e : f = g) (U) :
    f.app U = g.app U ≫ X.presheaf.map (eqToHom (by subst e; rfl)).op

Proof state:
X Y : Scheme
f g : X ⟶ Y
e : f = g
U : Y.Opens
⊢ f ⁻¹ᵁ U = g ⁻¹ᵁ U

Tactic:
subst e

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ⁻¹ᵁ U = f ⁻¹ᵁ U

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Hom.app f U = Hom.app f U ≫ X.presheaf.map (𝟙 (op (f ⁻¹ᵁ U)))

Tactic:
simp

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ⁻¹ᵁ U = f ⁻¹ᵁ U

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Hom.app f U = Hom.app f U ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
dsimp

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Hom.app f U = Hom.app f U ≫ X.presheaf.map (𝟙 (op (f ⁻¹ᵁ U)))

Proof state:
X Y : Scheme
f g : X ⟶ Y
e : f = g
U : Y.Opens
⊢ Hom.app f U = Hom.app g U ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
subst e

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Hom.app f U = Hom.app f U ≫ X.presheaf.map (eqToHom ⋯).op
-- Mathlib/Testing/Plausible/Functions.lean
theorem List.applyId_eq_self [DecidableEq α] {xs ys : List α} (x : α) :
    x ∉ xs → List.applyId.{u} (xs.zip ys) x = x

Proof state:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ ∀ (x_1 : α), (x, x_1) ∉ xs.zip ys

Tactic:
intro y hy

Result:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
y : α
hy : (x, y) ∈ xs.zip ys
⊢ False

Proof state:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
y : α
hy : (x, y) ∈ xs.zip ys
⊢ False

Tactic:
exact h (List.of_mem_zip hy).1

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ applyId (xs.zip ys) x = x

Tactic:
dsimp [List.applyId]

Result:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ (dlookup x (map Prod.toSigma (xs.zip ys))).getD x = x

Proof state:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ x ∉ (map Prod.toSigma (xs.zip ys)).keys

Tactic:
simp only [List.keys, not_exists, Prod.toSigma, exists_and_right, exists_eq_right, List.mem_map,
  Function.comp_apply, List.map_map, Prod.exists]

Result:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ ∀ (x_1 : α), (x, x_1) ∉ xs.zip ys

Proof state:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
⊢ x ∉ xs → applyId (xs.zip ys) x = x

Tactic:
intro h

Result:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ applyId (xs.zip ys) x = x

Proof state:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ (dlookup x (map Prod.toSigma (xs.zip ys))).getD x = x

Tactic:
rw [List.dlookup_eq_none.2]

Result:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ none.getD x = x

α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ x ∉ (map Prod.toSigma (xs.zip ys)).keys

Proof state:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ none.getD x = x

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem FamilyOfElements.comp_of_compatible (S : Sieve X) {x : FamilyOfElements P S}
    (t : x.Compatible) {f : Y ⟶ X} (hf : S f) {Z} (g : Z ⟶ Y) :
    x (g ≫ f) (S.downward_closed hf g) = P.map g.op (x f hf)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
x : FamilyOfElements P S.arrows
t : x.Compatible
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ x (g ≫ f) ⋯ = P.map g.op (x f hf)

Tactic:
simpa using t (𝟙 _) g (S.downward_closed hf g) hf (id_comp _)

Result:
no goals
-- Mathlib/NumberTheory/FermatPsp.lean
theorem frequently_atTop_fermatPsp {b : ℕ} (h : 1 ≤ b) : ∃ᶠ n in Filter.atTop, FermatPsp n b

Proof state:
b : ℕ
h : 1 ≤ b
⊢ ∃ᶠ (n : ℕ) in Filter.atTop, n.FermatPsp b

Tactic:
refine Filter.frequently_atTop.2 fun n => ?_

Result:
b : ℕ
h : 1 ≤ b
n : ℕ
⊢ ∃ b_1 ≥ n, b_1.FermatPsp b

Proof state:
case intro
b : ℕ
h : 1 ≤ b
n p : ℕ
hp : p.FermatPsp b ∧ n ≤ p
⊢ ∃ b_1 ≥ n, b_1.FermatPsp b

Tactic:
exact ⟨p, hp.2, hp.1⟩

Result:
no goals

Proof state:
b : ℕ
h : 1 ≤ b
n : ℕ
⊢ ∃ b_1 ≥ n, b_1.FermatPsp b

Tactic:
obtain ⟨p, hp⟩ := exists_infinite_pseudoprimes h n

Result:
case intro
b : ℕ
h : 1 ≤ b
n p : ℕ
hp : p.FermatPsp b ∧ n ≤ p
⊢ ∃ b_1 ≥ n, b_1.FermatPsp b
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem iSupIndep_iff_forall_dfinsupp (p : ι → Submodule R N) :
    iSupIndep p ↔
      ∀ (i) (x : p i) (v : Π₀ i : ι, ↥(p i)),
        lsum ℕ (M := fun i ↦ ↥(p i)) (fun i => (p i).subtype) (erase i v) = x → x = 0

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
⊢ (∀ (i : ι), ∀ x ∈ p i, ∀ (x_1 : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i x_1) = x → x = 0) ↔
    ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0

Tactic:
refine forall_congr' fun i => Subtype.forall'.trans ?_

Result:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
i : ι
⊢ (∀ (x : ↥(p i)) (x_1 : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i x_1) = ↑x → ↑x = 0) ↔
    ∀ (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
⊢ iSupIndep p ↔
    ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0

Tactic:
simp_rw [iSupIndep_def, Submodule.disjoint_def,
  Submodule.mem_biSup_iff_exists_dfinsupp, exists_imp, filter_ne_eq_erase]

Result:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
⊢ (∀ (i : ι), ∀ x ∈ p i, ∀ (x_1 : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i x_1) = x → x = 0) ↔
    ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
i : ι
⊢ (∀ (x : ↥(p i)) (x_1 : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i x_1) = ↑x → ↑x = 0) ↔
    ∀ (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0

Tactic:
simp_rw [Submodule.coe_eq_zero]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_add : (p + q).eval₂ f g = p.eval₂ f g + q.eval₂ f g

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ a ∈ p.support ∪ q.support, (f 0 * a.prod fun n e => g n ^ e) = 0

Tactic:
simp [f.map_zero]

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ eval₂ f g (p + q) = eval₂ f g p + eval₂ f g q

Tactic:
classical exact Finsupp.sum_add_index (by simp [f.map_zero]) (by simp [add_mul, f.map_add])

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ eval₂ f g (p + q) = eval₂ f g p + eval₂ f g q

Tactic:
exact Finsupp.sum_add_index (by simp [f.map_zero]) (by simp [add_mul, f.map_add])

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ a ∈ p.support ∪ q.support,
    ∀ (b₁ b₂ : R),
      (f (b₁ + b₂) * a.prod fun n e => g n ^ e) = (f b₁ * a.prod fun n e => g n ^ e) + f b₂ * a.prod fun n e => g n ^ e

Tactic:
simp [add_mul, f.map_add]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem IsReal.coe_embedding_apply {φ : K →+* ℂ} (hφ : IsReal φ) (x : K) :
    (hφ.embedding x : ℂ) = φ x

Proof state:
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (↑(hφ.embedding x)).re = (φ x).re

Tactic:
rfl

Result:
no goals

Proof state:
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (↑(hφ.embedding x)).im = (φ x).im

Tactic:
rw [ofReal_im, eq_comm, ← Complex.conj_eq_iff_im]

Result:
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (starRingEnd ℂ) (φ x) = φ x

Proof state:
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (starRingEnd ℂ) (φ x) = φ x

Tactic:
exact RingHom.congr_fun hφ x

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ ↑(hφ.embedding x) = φ x

Tactic:
apply Complex.ext

Result:
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (↑(hφ.embedding x)).re = (φ x).re

case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (↑(hφ.embedding x)).im = (φ x).im
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_le_rpow_of_nonpos (hx : 0 < x) (hxy : x ≤ y) (hz : z ≤ 0) : y ^ z ≤ x ^ z

Proof state:
case hb
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < y ^ z

Tactic:
positivity

Result:
no goals

Proof state:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
⊢ y ^ z ≤ x ^ z

Tactic:
have := hx.trans_le hxy

Result:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ y ^ z ≤ x ^ z

Proof state:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x

case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ y

case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x

case ha
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < x ^ z

case hb
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < y ^ z

Tactic:
all_goals positivity

Result:
no goals

Proof state:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ x ^ (-z) ≤ y ^ (-z)

case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ y

case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x

case ha
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < x ^ z

case hb
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < y ^ z

Tactic:
on_goal 1 => refine rpow_le_rpow ?_ hxy (neg_nonneg.2 hz)

Result:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x

case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ y

case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x

case ha
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < x ^ z

case hb
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < y ^ z

Proof state:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ y ^ z ≤ x ^ z

Tactic:
rw [← inv_le_inv₀, ← rpow_neg, ← rpow_neg]

Result:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ x ^ (-z) ≤ y ^ (-z)

case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ y

case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x

case ha
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < x ^ z

case hb
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < y ^ z

Proof state:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ x ^ (-z) ≤ y ^ (-z)

Tactic:
refine rpow_le_rpow ?_ hxy (neg_nonneg.2 hz)

Result:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x
-- Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
theorem strongMono_comp [StrongMono f] [StrongMono g] : StrongMono (f ≫ g) :=
  { mono := mono_comp _ _
    rlp

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝² : StrongMono f
inst✝¹ : StrongMono g
X✝ Y✝ : C
z✝ : X✝ ⟶ Y✝
inst✝ : Epi z✝
⊢ HasLiftingProperty z✝ (f ≫ g)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono f
inst✝ : StrongMono g
⊢ ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [inst : Epi z], HasLiftingProperty z (f ≫ g)

Tactic:
intros

Result:
C : Type u
inst✝³ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝² : StrongMono f
inst✝¹ : StrongMono g
X✝ Y✝ : C
z✝ : X✝ ⟶ Y✝
inst✝ : Epi z✝
⊢ HasLiftingProperty z✝ (f ≫ g)