harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/Primrec.lean
theorem dom_fintype [Finite α] (f : α → σ) : Primrec f :=
  let ⟨l, _, m⟩ := Finite.exists_univ_list α
  option_some_iff.1 <| by
    haveI := decidableEqOfEncodable α
    refine ((list_get?₁ (l.map f)).comp (list_idxOf₁ l)).of_eq fun a => ?_
    rw [List.get?_eq_getElem?, List.getElem?_map, List.getElem?_idxOf (m a), Option.map_some']

Proof state:
α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
inst✝ : Finite α
f : α → σ
l : List α
left✝ : l.Nodup
m : ∀ (x : α), x ∈ l
⊢ Primrec fun a => some (f a)

Tactic:
haveI := decidableEqOfEncodable α

Result:
α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
inst✝ : Finite α
f : α → σ
l : List α
left✝ : l.Nodup
m : ∀ (x : α), x ∈ l
this : DecidableEq α
⊢ Primrec fun a => some (f a)

Proof state:
α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
inst✝ : Finite α
f : α → σ
l : List α
left✝ : l.Nodup
m : ∀ (x : α), x ∈ l
this : DecidableEq α
a : α
⊢ (List.map f l).get? (List.idxOf a l) = some (f a)

Tactic:
rw [List.get?_eq_getElem?, List.getElem?_map, List.getElem?_idxOf (m a), Option.map_some']

Result:
no goals

Proof state:
α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
inst✝ : Finite α
f : α → σ
l : List α
left✝ : l.Nodup
m : ∀ (x : α), x ∈ l
this : DecidableEq α
⊢ Primrec fun a => some (f a)

Tactic:
refine ((list_get?₁ (l.map f)).comp (list_idxOf₁ l)).of_eq fun a => ?_

Result:
α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
inst✝ : Finite α
f : α → σ
l : List α
left✝ : l.Nodup
m : ∀ (x : α), x ∈ l
this : DecidableEq α
a : α
⊢ (List.map f l).get? (List.idxOf a l) = some (f a)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sin_eq_zero_iff {θ : Angle} : sin θ = 0 ↔ θ = 0 ∨ θ = π

Proof state:
θ : Angle
⊢ θ.sin = 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
nth_rw 1 [← sin_zero]

Result:
θ : Angle
⊢ θ.sin = sin 0 ↔ θ = 0 ∨ θ = ↑π

Proof state:
θ : Angle
⊢ θ.sin = sin 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
rw [sin_eq_iff_eq_or_add_eq_pi]

Result:
θ : Angle
⊢ θ = 0 ∨ θ + 0 = ↑π ↔ θ = 0 ∨ θ = ↑π

Proof state:
θ : Angle
⊢ θ = 0 ∨ θ + 0 = ↑π ↔ θ = 0 ∨ θ = ↑π

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_nsmul_eq_pi_iff {θ : Angle} : (2 : ℕ) • θ = π ↔ θ = (π / 2 : ℝ) ∨ θ = (-π / 2 : ℝ)

Proof state:
θ : Angle
⊢ 2 • θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
have h : (π : Angle) = ((2 : ℕ) • (π / 2 : ℝ):) := by rw [two_nsmul, add_halves]

Result:
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ 2 • θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Proof state:
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ 2 • θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
nth_rw 1 [h]

Result:
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ 2 • θ = ↑(2 • (π / 2)) ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Proof state:
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ 2 • θ = ↑(2 • (π / 2)) ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
rw [coe_nsmul, two_nsmul_eq_iff]

Result:
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ θ = ↑(π / 2) ∨ θ = ↑(π / 2) + ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Proof state:
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ θ = ↑(π / 2) ∨ θ = ↑(π / 2) + ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
convert Iff.rfl

Result:
case h.e'_2.h.e'_2.h.e'_3
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ ↑(-π / 2) = ↑(π / 2) + ↑π

Proof state:
θ : Angle
⊢ ↑π = ↑(2 • (π / 2))

Tactic:
rw [two_nsmul, add_halves]

Result:
no goals

Proof state:
case h.e'_2.h.e'_2.h.e'_3
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ ↑(-π / 2) = ↑(π / 2) + ↑π

Tactic:
rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, ← neg_sub, sub_neg_eq_add, add_assoc,
  add_halves, ← two_mul, coe_neg, coe_two_pi, neg_zero]

Result:
no goals
-- Mathlib/Data/Set/Finite/Powerset.lean
theorem Finite.finite_subsets {α : Type u} {a : Set α} (h : a.Finite) : { b | b ⊆ a }.Finite

Proof state:
α : Type u
a : Set α
h : a.Finite
⊢ {b | b ⊆ a}.Finite

Tactic:
convert ((Finset.powerset h.toFinset).map Finset.coeEmb.1).finite_toSet

Result:
case h.e'_2
α : Type u
a : Set α
h : a.Finite
⊢ {b | b ⊆ a} = ↑(Finset.map Finset.coeEmb.toEmbedding h.toFinset.powerset)

Proof state:
case h.e'_2.h
α : Type u
a : Set α
h : a.Finite
s : Set α
⊢ s ∈ {b | b ⊆ a} ↔ s ∈ ↑(Finset.map Finset.coeEmb.toEmbedding h.toFinset.powerset)

Tactic:
simpa [← @exists_finite_iff_finset α fun t => t ⊆ a ∧ t = s, Finite.subset_toFinset,
  ← and_assoc, Finset.coeEmb] using h.subset

Result:
no goals

Proof state:
case h.e'_2
α : Type u
a : Set α
h : a.Finite
⊢ {b | b ⊆ a} = ↑(Finset.map Finset.coeEmb.toEmbedding h.toFinset.powerset)

Tactic:
ext s

Result:
case h.e'_2.h
α : Type u
a : Set α
h : a.Finite
s : Set α
⊢ s ∈ {b | b ⊆ a} ↔ s ∈ ↑(Finset.map Finset.coeEmb.toEmbedding h.toFinset.powerset)
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigOWith_const_const (c : E) {c' : F''} (hc' : c' ≠ 0) (l : Filter α) :
    IsBigOWith (‖c‖ / ‖c'‖) l (fun _x : α => c) fun _x => c'

Proof state:
case h
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
⊢ ∀ (a : α), a ∈ {x | (fun x => ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖) x}

Tactic:
intro x

Result:
case h
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
x : α
⊢ x ∈ {x | (fun x => ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖) x}

Proof state:
case h
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
x : α
⊢ x ∈ {x | (fun x => ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖) x}

Tactic:
rw [mem_setOf, div_mul_cancel₀ _ (norm_ne_zero_iff.mpr hc')]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
⊢ IsBigOWith (‖c‖ / ‖c'‖) l (fun _x => c) fun _x => c'

Tactic:
simp only [IsBigOWith_def]

Result:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
⊢ ∀ᶠ (x : α) in l, ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖

Proof state:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
⊢ ∀ᶠ (x : α) in l, ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖

Tactic:
apply univ_mem'

Result:
case h
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
⊢ ∀ (a : α), a ∈ {x | (fun x => ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖) x}
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem coeff_toSubring' {n : ℕ} : (coeff (toSubring p T hp) n).1 = coeff p n

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
⊢ ↑((p.toSubring T hp).coeff n) = p.coeff n

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
theorem map'_id {M : ModuleCat.{v} R} : map' f (𝟙 M) = 𝟙 _

Proof state:
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
⊢ map' f (𝟙 M) = 𝟙 (obj' f M)

Tactic:
ext x

Result:
case hf.h
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
x : ↑(obj' f M)
⊢ (Hom.hom (map' f (𝟙 M))) x = (Hom.hom (𝟙 (obj' f M))) x

Proof state:
case hf.h
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
x : ↑(obj' f M)
⊢ (Hom.hom (map' f (𝟙 M))) x = (Hom.hom (𝟙 (obj' f M))) x

Tactic:
simp [map', obj']

Result:
no goals
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem compl_erase : (s.erase a)ᶜ = insert a sᶜ

Proof state:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ (s.erase a)ᶜ = insert a sᶜ

Tactic:
ext

Result:
case h
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ (s.erase a)ᶜ ↔ a✝ ∈ insert a sᶜ

Proof state:
case h
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ (s.erase a)ᶜ ↔ a✝ ∈ insert a sᶜ

Tactic:
simp only [or_iff_not_imp_left, mem_insert, not_and, mem_compl, mem_erase]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem product_union [DecidableEq α] [DecidableEq β] : s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t'

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t'

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t ∪ t') ↔ (x, y) ∈ s ×ˢ t ∪ s ×ˢ t'

Proof state:
case h.mk
α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t ∪ t') ↔ (x, y) ∈ s ×ˢ t ∪ s ×ˢ t'

Tactic:
simp only [and_or_left, mem_union, mem_product]

Result:
no goals
-- Mathlib/Algebra/Group/Nat/Range.lean
theorem range_add (a b : ℕ) : range (a + b) = range a ∪ (range b).map (addLeftEmbedding a)

Proof state:
a b : ℕ
⊢ (range (a + b)).val = (range a).val ∪ (map (addLeftEmbedding a) (range b)).val

Tactic:
exact Multiset.range_add_eq_union a b

Result:
no goals

Proof state:
a b : ℕ
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)

Tactic:
rw [← val_inj, union_val]

Result:
a b : ℕ
⊢ (range (a + b)).val = (range a).val ∪ (map (addLeftEmbedding a) (range b)).val
-- Mathlib/Data/Complex/Norm.lean
theorem abs_re_le_norm (z : ℂ) : |z.re| ≤ ‖z‖

Proof state:
z : ℂ
⊢ z.re * z.re ≤ normSq z

Tactic:
apply re_sq_le_normSq

Result:
no goals

Proof state:
z : ℂ
⊢ |z.re| ≤ ‖z‖

Tactic:
rw [mul_self_le_mul_self_iff (abs_nonneg z.re) (norm_nonneg _), abs_mul_abs_self,
  norm_mul_self_eq_normSq]

Result:
z : ℂ
⊢ z.re * z.re ≤ normSq z
-- Mathlib/Probability/Distributions/Gaussian.lean
/-- If `X` is a real random variable with Gaussian law with mean `μ` and variance `v`, then `X + y`
has Gaussian law with mean `μ + y` and variance `v`. -/
lemma gaussianReal_add_const {X : Ω → ℝ} (hX : Measure.map X ℙ = gaussianReal μ v) (y : ℝ) :
    Measure.map (fun ω ↦ X ω + y) ℙ = gaussianReal (μ + y) v

Proof state:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
y : ℝ
⊢ Measure.map (fun ω => X ω + y) ℙ = gaussianReal (μ + y) v

Tactic:
have hXm : AEMeasurable X := aemeasurable_of_map_neZero (by rw [hX]; infer_instance)

Result:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
y : ℝ
hXm : AEMeasurable X ℙ
⊢ Measure.map (fun ω => X ω + y) ℙ = gaussianReal (μ + y) v

Proof state:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
y : ℝ
hXm : AEMeasurable X ℙ
⊢ Measure.map (fun ω => X ω + y) ℙ = gaussianReal (μ + y) v

Tactic:
change Measure.map ((fun ω ↦ ω + y) ∘ X) ℙ = gaussianReal (μ + y) v

Result:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
y : ℝ
hXm : AEMeasurable X ℙ
⊢ Measure.map ((fun ω => ω + y) ∘ X) ℙ = gaussianReal (μ + y) v

Proof state:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
y : ℝ
hXm : AEMeasurable X ℙ
⊢ Measure.map ((fun ω => ω + y) ∘ X) ℙ = gaussianReal (μ + y) v

Tactic:
rw [← AEMeasurable.map_map_of_aemeasurable (measurable_id'.add_const _).aemeasurable hXm, hX,
  gaussianReal_map_add_const y]

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
y : ℝ
⊢ NeZero (Measure.map X ℙ)

Tactic:
rw [hX]

Result:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
y : ℝ
⊢ NeZero (gaussianReal μ v)

Proof state:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
y : ℝ
⊢ NeZero (gaussianReal μ v)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
lemma comp_id (C : VariableChange R) : comp C id = C

Proof state:
R : Type u
inst✝ : CommRing R
C : VariableChange R
⊢ C.comp id = C

Tactic:
simp only [comp, id, add_zero, mul_zero, one_mul, mul_one, one_pow, Units.val_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem lt_of_getLsb?_eq_some (x : BitVec w) (i : Nat) : x[i]? = some b → i < w

Proof state:
case some
w : Nat
b : Bool
x : BitVec w
i : Nat
val✝ : Bool
h : x[i]? = some val✝
⊢ some val✝ = some b → i < w

Tactic:
by_cases i < w <;> simp_all

Result:
no goals

Proof state:
case none
w : Nat
b : Bool
x : BitVec w
i : Nat
h : x[i]? = none
⊢ none = some b → i < w

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
b : Bool
x : BitVec w
i : Nat
⊢ x[i]? = some b → i < w

Tactic:
cases h : x[i]? with
| none => simp
| some => by_cases i < w <;> simp_all

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem biInf_congr' {p : ι → Prop} {f g : (i : ι) → p i → α}
    (h : ∀ i (hi : p i), f i hi = g i hi) :
    ⨅ i, ⨅ (hi : p i), f i hi = ⨅ i, ⨅ (hi : p i), g i hi

Proof state:
case e_s
α : Type u_1
ι : Sort u_4
inst✝ : InfSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
⊢ (fun i => ⨅ (hi : p i), f i hi) = fun i => ⨅ (hi : p i), g i hi

Tactic:
ext i

Result:
case e_s.h
α : Type u_1
ι : Sort u_4
inst✝ : InfSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
i : ι
⊢ ⨅ (hi : p i), f i hi = ⨅ (hi : p i), g i hi

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : InfSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
⊢ ⨅ i, ⨅ (hi : p i), f i hi = ⨅ i, ⨅ (hi : p i), g i hi

Tactic:
congr

Result:
case e_s
α : Type u_1
ι : Sort u_4
inst✝ : InfSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
⊢ (fun i => ⨅ (hi : p i), f i hi) = fun i => ⨅ (hi : p i), g i hi

Proof state:
case e_s.h
α : Type u_1
ι : Sort u_4
inst✝ : InfSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
i : ι
⊢ ⨅ (hi : p i), f i hi = ⨅ (hi : p i), g i hi

Tactic:
congr

Result:
case e_s.h.e_s
α : Type u_1
ι : Sort u_4
inst✝ : InfSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
i : ι
⊢ (fun hi => f i hi) = fun hi => g i hi

Proof state:
case e_s.h.e_s.h
α : Type u_1
ι : Sort u_4
inst✝ : InfSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
i : ι
hi : p i
⊢ f i hi = g i hi

Tactic:
exact h i hi

Result:
no goals

Proof state:
case e_s.h.e_s
α : Type u_1
ι : Sort u_4
inst✝ : InfSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
i : ι
⊢ (fun hi => f i hi) = fun hi => g i hi

Tactic:
ext hi

Result:
case e_s.h.e_s.h
α : Type u_1
ι : Sort u_4
inst✝ : InfSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
i : ι
hi : p i
⊢ f i hi = g i hi
-- Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean
theorem hasBasis_nhds_adic (I : Ideal R) (x : R) :
    HasBasis (@nhds R I.adicTopology x) (fun _n : ℕ => True) fun n =>
      (fun y => x + y) '' (I ^ n : Ideal R)

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x : R
⊢ (𝓝 x).HasBasis (fun _n => True) fun n => (fun y => x + y) '' ↑(I ^ n)

Tactic:
letI := I.adicTopology

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x : R
this : TopologicalSpace R := I.adicTopology
⊢ (𝓝 x).HasBasis (fun _n => True) fun n => (fun y => x + y) '' ↑(I ^ n)

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x : R
this✝ : TopologicalSpace R := I.adicTopology
this : (Filter.map (fun y => x + y) (𝓝 0)).HasBasis (fun _n => True) fun i => (fun y => x + y) '' ↑(I ^ i)
⊢ (𝓝 x).HasBasis (fun _n => True) fun n => (fun y => x + y) '' ↑(I ^ n)

Tactic:
rwa [map_add_left_nhds_zero x] at this

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x : R
this : TopologicalSpace R := I.adicTopology
⊢ (𝓝 x).HasBasis (fun _n => True) fun n => (fun y => x + y) '' ↑(I ^ n)

Tactic:
have := I.hasBasis_nhds_zero_adic.map fun y => x + y

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x : R
this✝ : TopologicalSpace R := I.adicTopology
this : (Filter.map (fun y => x + y) (𝓝 0)).HasBasis (fun _n => True) fun i => (fun y => x + y) '' ↑(I ^ i)
⊢ (𝓝 x).HasBasis (fun _n => True) fun n => (fun y => x + y) '' ↑(I ^ n)
-- Mathlib/Data/Set/Image.lean
theorem image_eq_range (f : α → β) (s : Set α) : f '' s = range fun x : s => f x

Proof state:
case h.mpr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
⊢ (x✝ ∈ range fun x => f ↑x) → x✝ ∈ f '' s

Tactic:
rintro ⟨⟨x, h1⟩, h2⟩

Result:
case h.mpr.intro.mk
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
x : α
h1 : x ∈ s
h2 : (fun x => f ↑x) ⟨x, h1⟩ = x✝
⊢ x✝ ∈ f '' s

Proof state:
case h.mp.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
x : α
h1 : x ∈ s
h2 : f x = x✝
⊢ x✝ ∈ range fun x => f ↑x

Tactic:
exact ⟨⟨x, h1⟩, h2⟩

Result:
no goals

Proof state:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
⊢ x✝ ∈ f '' s → x✝ ∈ range fun x => f ↑x

Tactic:
rintro ⟨x, h1, h2⟩

Result:
case h.mp.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
x : α
h1 : x ∈ s
h2 : f x = x✝
⊢ x✝ ∈ range fun x => f ↑x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s = range fun x => f ↑x

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
⊢ x✝ ∈ f '' s ↔ x✝ ∈ range fun x => f ↑x

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
⊢ x✝ ∈ f '' s ↔ x✝ ∈ range fun x => f ↑x

Tactic:
constructor

Result:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
⊢ x✝ ∈ f '' s → x✝ ∈ range fun x => f ↑x

case h.mpr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
⊢ (x✝ ∈ range fun x => f ↑x) → x✝ ∈ f '' s

Proof state:
case h.mpr.intro.mk
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
x : α
h1 : x ∈ s
h2 : (fun x => f ↑x) ⟨x, h1⟩ = x✝
⊢ x✝ ∈ f '' s

Tactic:
exact ⟨x, h1, h2⟩

Result:
no goals
-- Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean
theorem exists_mem_of_not_isUnit_aeval_prod [IsDomain R] {p : R[X]} {a : A}
    (h : ¬IsUnit (aeval a (Multiset.map (fun x : R => X - C x) p.roots).prod)) :
    ∃ k : R, k ∈ σ a ∧ eval k p = 0

Proof state:
case intro.intro
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ p.roots
r_nu : ¬IsUnit (a - ↑ₐ r)
⊢ ∃ k ∈ σ a, eval k p = 0

Tactic:
exact ⟨r, by rwa [mem_iff, ← IsUnit.sub_iff], (mem_roots'.1 r_mem).2⟩

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ∃ a_1 ∈ p.roots, ¬IsUnit (a - ↑ₐ a_1)
⊢ ∃ k ∈ σ a, eval k p = 0

Tactic:
rcases h with ⟨r, r_mem, r_nu⟩

Result:
case intro.intro
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ p.roots
r_nu : ¬IsUnit (a - ↑ₐ r)
⊢ ∃ k ∈ σ a, eval k p = 0

Proof state:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit ((aeval a) (Multiset.map (fun x => X - C x) p.roots).prod)
⊢ ∃ k ∈ σ a, eval k p = 0

Tactic:
rw [← Multiset.prod_toList, map_list_prod] at h

Result:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit (List.map (⇑(aeval a)) (Multiset.map (fun x => X - C x) p.roots).toList).prod
⊢ ∃ k ∈ σ a, eval k p = 0

Proof state:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬∀ m ∈ List.map (⇑(aeval a)) (Multiset.map (fun x => X - C x) p.roots).toList, IsUnit m
⊢ ∃ k ∈ σ a, eval k p = 0

Tactic:
simp only [not_forall, exists_prop, aeval_C, Multiset.mem_toList, List.mem_map, aeval_X,
  exists_exists_and_eq_and, Multiset.mem_map, map_sub] at h

Result:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ∃ a_1 ∈ p.roots, ¬IsUnit (a - ↑ₐ a_1)
⊢ ∃ k ∈ σ a, eval k p = 0

Proof state:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit (List.map (⇑(aeval a)) (Multiset.map (fun x => X - C x) p.roots).toList).prod
⊢ ∃ k ∈ σ a, eval k p = 0

Tactic:
replace h := mt List.prod_isUnit h

Result:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬∀ m ∈ List.map (⇑(aeval a)) (Multiset.map (fun x => X - C x) p.roots).toList, IsUnit m
⊢ ∃ k ∈ σ a, eval k p = 0

Proof state:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ p.roots
r_nu : ¬IsUnit (a - ↑ₐ r)
⊢ r ∈ σ a

Tactic:
rwa [mem_iff, ← IsUnit.sub_iff]

Result:
no goals
-- Mathlib/Analysis/Convolution.lean
theorem ConvolutionExistsAt.add_distrib {x : G} (hfg : ConvolutionExistsAt f g x L μ)
    (hfg' : ConvolutionExistsAt f' g x L μ) :
    ((f + f') ⋆[L, μ] g) x = (f ⋆[L, μ] g) x + (f' ⋆[L, μ] g) x

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f f' : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x : G
hfg : ConvolutionExistsAt f g x L μ
hfg' : ConvolutionExistsAt f' g x L μ
⊢ ((f + f') ⋆[L, μ] g) x = (f ⋆[L, μ] g) x + (f' ⋆[L, μ] g) x

Tactic:
simp only [convolution_def, L.map_add₂, Pi.add_apply, integral_add hfg hfg']

Result:
no goals
-- Mathlib/RingTheory/Ideal/AssociatedPrime.lean
theorem not_isAssociatedPrime_of_subsingleton [Subsingleton M] : ¬IsAssociatedPrime I M

Proof state:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
⊢ ¬IsAssociatedPrime I M

Tactic:
rintro ⟨hI, x, hx⟩

Result:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
hI : I.IsPrime
x : M
hx : I = ker (toSpanSingleton R M x)
⊢ False

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
hI : I.IsPrime
x : M
hx : I = ker (toSpanSingleton R M x)
⊢ False

Tactic:
apply hI.ne_top

Result:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
hI : I.IsPrime
x : M
hx : I = ker (toSpanSingleton R M x)
⊢ I = ⊤

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
hI : I.IsPrime
x : M
hx : I = ker (toSpanSingleton R M x)
⊢ I = ⊤

Tactic:
simpa [Subsingleton.elim x 0] using hx

Result:
no goals