harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/DFinsupp/Defs.lean
theorem erase_eq_sub_single {β : ι → Type*} [∀ i, AddGroup (β i)] (f : Π₀ i, β i) (i : ι) :
    f.erase i = f - single i (f i)

Proof state:
case h
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
⊢ (erase i f) j = (f - single i (f i)) j

Tactic:
rcases eq_or_ne i j with (rfl | h)

Result:
case h.inl
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i : ι
⊢ (erase i f) i = (f - single i (f i)) i

case h.inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
h : i ≠ j
⊢ (erase i f) j = (f - single i (f i)) j

Proof state:
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i : ι
⊢ erase i f = f - single i (f i)

Tactic:
ext j

Result:
case h
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
⊢ (erase i f) j = (f - single i (f i)) j

Proof state:
case h.inl
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i : ι
⊢ (erase i f) i = (f - single i (f i)) i

Tactic:
simp

Result:
no goals

Proof state:
case h.inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
h : i ≠ j
⊢ (erase i f) j = (f - single i (f i)) j

Tactic:
simp [erase_ne h.symm, single_eq_of_ne h, @eq_comm _ j, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Raw.lean
theorem WF.containsThenInsertIfNew [BEq α] [Hashable α] {m : Raw α β} {a : α} {b : β a} (h : m.WF) :
    (m.containsThenInsertIfNew a b).2.WF

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
a : α
b : β a
h : m.WF
⊢ (m.containsThenInsertIfNew a b).snd.WF

Tactic:
simpa [Raw.containsThenInsertIfNew, h.size_buckets_pos] using .containsThenInsertIfNew₀ h

Result:
no goals
-- Mathlib/Dynamics/Ergodic/Conservative.lean
theorem ae_forall_image_mem_imp_frequently_image_mem (hf : Conservative f μ)
    (hs : NullMeasurableSet s μ) : ∀ᵐ x ∂μ, ∀ k, f^[k] x ∈ s → ∃ᶠ n in atTop, f^[n] x ∈ s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
⊢ ∀ᵐ (x : α) ∂μ, ∀ (k : ℕ), f^[k] x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
refine ae_all_iff.2 fun k => ?_

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
⊢ ∀ᵐ (a : α) ∂μ, f^[k] a ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] a ∈ s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
n : ℕ
hn : f^[n] x ∈ f^[k] ⁻¹' s
⊢ f^[n + k] x ∈ s

Tactic:
rwa [add_comm, iterate_add_apply]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
⊢ ∃ᶠ (a : ℕ) in atTop, f^[a + k] x ∈ s

Tactic:
refine (hx hk).mono fun n hn => ?_

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
n : ℕ
hn : f^[n] x ∈ f^[k] ⁻¹' s
⊢ f^[n + k] x ∈ s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
rw [← map_add_atTop_eq_nat k, frequently_map]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
⊢ ∃ᶠ (a : ℕ) in atTop, f^[a + k] x ∈ s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
⊢ ∀ᵐ (a : α) ∂μ, f^[k] a ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] a ∈ s

Tactic:
refine (hf.ae_mem_imp_frequently_image_mem
  (hs.preimage <| hf.toQuasiMeasurePreserving.iterate k)).mono fun x hx hk => ?_

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_apply_left (a : α) : toIocMod hp a a = a + p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a < a + p ∧ ∃ z, a = a + p + z • p

Tactic:
exact ⟨lt_add_of_pos_right _ hp, -1, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ toIocMod hp a a = a + p

Tactic:
rw [toIocMod_eq_iff hp, Set.right_mem_Ioc]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a < a + p ∧ ∃ z, a = a + p + z • p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a = a + p + -1 • p

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem _root_.List.periodic_prod [Add α] [Monoid β] (l : List (α → β))
    (hl : ∀ f ∈ l, Periodic f c) : Periodic l.prod c

Proof state:
case cons
α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : Monoid β
g : α → β
l : List (α → β)
ih : (∀ f ∈ l, Periodic f c) → Periodic l.prod c
hl : ∀ f ∈ g :: l, Periodic f c
⊢ Periodic (g :: l).prod c

Tactic:
rw [List.forall_mem_cons] at hl

Result:
case cons
α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : Monoid β
g : α → β
l : List (α → β)
ih : (∀ f ∈ l, Periodic f c) → Periodic l.prod c
hl : Periodic g c ∧ ∀ x ∈ l, Periodic x c
⊢ Periodic (g :: l).prod c

Proof state:
case cons
α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : Monoid β
g : α → β
l : List (α → β)
ih : (∀ f ∈ l, Periodic f c) → Periodic l.prod c
hl : Periodic g c ∧ ∀ x ∈ l, Periodic x c
⊢ Periodic (g :: l).prod c

Tactic:
simpa only [List.prod_cons] using hl.1.mul (ih hl.2)

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : Monoid β
hl : ∀ f ∈ [], Periodic f c
⊢ Periodic [].prod c

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : Monoid β
l : List (α → β)
hl : ∀ f ∈ l, Periodic f c
⊢ Periodic l.prod c

Tactic:
induction l with
| nil => simp
| cons g l ih =>
  rw [List.forall_mem_cons] at hl
  simpa only [List.prod_cons] using hl.1.mul (ih hl.2)

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCoseparating_proj_preimage {𝒢 : Set C} (h𝒢 : IsCoseparating 𝒢) :
    IsCoseparating ((proj S T).obj ⁻¹' 𝒢)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
⊢ IsCoseparating ((proj S T).obj ⁻¹' 𝒢)

Tactic:
refine fun X Y f g hfg => ext _ _ (h𝒢 _ _ fun G hG h => ?_)

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : StructuredArrow S T
f g : X ⟶ Y
hfg : ∀ G ∈ (proj S T).obj ⁻¹' 𝒢, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : C
hG : G ∈ 𝒢
h : Y.right ⟶ G
⊢ f.right ≫ h = g.right ≫ h

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : StructuredArrow S T
f g : X ⟶ Y
hfg : ∀ G ∈ (proj S T).obj ⁻¹' 𝒢, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : C
hG : G ∈ 𝒢
h : Y.right ⟶ G
⊢ f.right ≫ h = g.right ≫ h

Tactic:
exact congr_arg CommaMorphism.right (hfg (mk (Y.hom ≫ T.map h)) hG (homMk h rfl))

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem eq_zero_of_constant_mem_of_maximal (hR : IsField R) (I : Ideal R[X]) [hI : I.IsMaximal]
    (x : R) (hx : C x ∈ I) : x = 0

Proof state:
R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
⊢ x = 0

Tactic:
refine Classical.by_contradiction fun hx0 => hI.ne_top ((eq_top_iff_one I).2 ?_)

Result:
R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
⊢ 1 ∈ I

Proof state:
case h.e'_5
R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 = C y * C x

Tactic:
rw [← C.map_mul, hR.mul_comm y x, hy, RingHom.map_one]

Result:
no goals

Proof state:
case intro
R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 ∈ I

Tactic:
convert I.mul_mem_left (C y) hx

Result:
case h.e'_5
R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 = C y * C x

Proof state:
R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
⊢ 1 ∈ I

Tactic:
obtain ⟨y, hy⟩ := hR.mul_inv_cancel hx0

Result:
case intro
R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 ∈ I
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem monotone_ite
    {α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β]
    (c : Prop) [Decidable c]
    (k₁ : α → β) (k₂ : α → β)
    (hmono₁ : monotone k₁) (hmono₂ : monotone k₂) :
  monotone fun x => if c then k₁ x else k₂ x

Proof state:
α : Sort u
β : Sort v
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
c : Prop
inst✝ : Decidable c
k₁ k₂ : α → β
hmono₁ : monotone k₁
hmono₂ : monotone k₂
⊢ monotone fun x => if c then k₁ x else k₂ x

Tactic:
split

Result:
case isTrue
α : Sort u
β : Sort v
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
c : Prop
inst✝ : Decidable c
k₁ k₂ : α → β
hmono₁ : monotone k₁
hmono₂ : monotone k₂
h✝ : c
⊢ monotone fun x => k₁ x

case isFalse
α : Sort u
β : Sort v
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
c : Prop
inst✝ : Decidable c
k₁ k₂ : α → β
hmono₁ : monotone k₁
hmono₂ : monotone k₂
h✝ : ¬c
⊢ monotone fun x => k₂ x

Proof state:
case isTrue
α : Sort u
β : Sort v
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
c : Prop
inst✝ : Decidable c
k₁ k₂ : α → β
hmono₁ : monotone k₁
hmono₂ : monotone k₂
h✝ : c
⊢ monotone fun x => k₁ x

Tactic:
apply hmono₁

Result:
no goals

Proof state:
case isFalse
α : Sort u
β : Sort v
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
c : Prop
inst✝ : Decidable c
k₁ k₂ : α → β
hmono₁ : monotone k₁
hmono₂ : monotone k₂
h✝ : ¬c
⊢ monotone fun x => k₂ x

Tactic:
apply hmono₂

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem IsSuccLimit.ne_bot [OrderBot α] (h : IsSuccLimit a) : a ≠ ⊥

Proof state:
α : Type u_1
a : α
inst✝¹ : Preorder α
inst✝ : OrderBot α
h : IsSuccLimit a
⊢ a ≠ ⊥

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderBot α
h : IsSuccLimit ⊥
⊢ False

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderBot α
h : IsSuccLimit ⊥
⊢ False

Tactic:
exact not_isSuccLimit_bot h

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
lemma disjoint_biUnion_left (s : Finset α) (f : α → Finset β) (t : Finset β) :
    Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Finset β
t : Finset β
i : α
s : Finset α
his : i ∉ s
ih : Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t
⊢ Disjoint ((insert i s).biUnion f) t ↔ ∀ i_1 ∈ insert i s, Disjoint (f i_1) t

Tactic:
simp only [disjoint_union_left, biUnion_insert, his, forall_mem_insert, ih]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    a ∉ s →
      (Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t) →
        (Disjoint ((insert a s).biUnion f) t ↔ ∀ i ∈ insert a s, Disjoint (f i) t)

Tactic:
intro i s his ih

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Finset β
t : Finset β
i : α
s : Finset α
his : i ∉ s
ih : Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t
⊢ Disjoint ((insert i s).biUnion f) t ↔ ∀ i_1 ∈ insert i s, Disjoint (f i_1) t

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ Disjoint (∅.biUnion f) t ↔ ∀ i ∈ ∅, Disjoint (f i) t

Tactic:
simp only [forall_mem_empty_iff, biUnion_empty, disjoint_empty_left]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t

Tactic:
refine s.induction ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ Disjoint (∅.biUnion f) t ↔ ∀ i ∈ ∅, Disjoint (f i) t

case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    a ∉ s →
      (Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t) →
        (Disjoint ((insert a s).biUnion f) t ↔ ∀ i ∈ insert a s, Disjoint (f i) t)
-- Mathlib/Topology/Algebra/Ring/Basic.lean
theorem toTopologicalSpace_injective :
    Injective (toTopologicalSpace : RingTopology α → TopologicalSpace α)

Proof state:
α : Type u_1
inst✝ : Ring α
f g : RingTopology α
a✝ : f.toTopologicalSpace = g.toTopologicalSpace
⊢ f = g

Tactic:
cases f

Result:
case mk
α : Type u_1
inst✝ : Ring α
g : RingTopology α
toTopologicalSpace✝ : TopologicalSpace α
toIsTopologicalRing✝ : IsTopologicalRing α
a✝ :
  { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ }.toTopologicalSpace =
    g.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ } = g

Proof state:
α : Type u_1
inst✝ : Ring α
⊢ Injective toTopologicalSpace

Tactic:
intro f g _

Result:
α : Type u_1
inst✝ : Ring α
f g : RingTopology α
a✝ : f.toTopologicalSpace = g.toTopologicalSpace
⊢ f = g

Proof state:
case mk
α : Type u_1
inst✝ : Ring α
g : RingTopology α
toTopologicalSpace✝ : TopologicalSpace α
toIsTopologicalRing✝ : IsTopologicalRing α
a✝ :
  { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ }.toTopologicalSpace =
    g.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ } = g

Tactic:
cases g

Result:
case mk.mk
α : Type u_1
inst✝ : Ring α
toTopologicalSpace✝¹ : TopologicalSpace α
toIsTopologicalRing✝¹ : IsTopologicalRing α
toTopologicalSpace✝ : TopologicalSpace α
toIsTopologicalRing✝ : IsTopologicalRing α
a✝ :
  { toTopologicalSpace := toTopologicalSpace✝¹, toIsTopologicalRing := toIsTopologicalRing✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, toIsTopologicalRing := toIsTopologicalRing✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ }

Proof state:
case mk.mk
α : Type u_1
inst✝ : Ring α
toTopologicalSpace✝¹ : TopologicalSpace α
toIsTopologicalRing✝¹ : IsTopologicalRing α
toTopologicalSpace✝ : TopologicalSpace α
toIsTopologicalRing✝ : IsTopologicalRing α
a✝ :
  { toTopologicalSpace := toTopologicalSpace✝¹, toIsTopologicalRing := toIsTopologicalRing✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, toIsTopologicalRing := toIsTopologicalRing✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem foldrM_toArray' [Monad m] (f : α → β → m β) (init : β) (l : List α)
    (h : start = l.toArray.size) :
    l.toArray.foldrM f init start 0 = l.foldrM f init

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
start : Nat
inst✝ : Monad m
f : α → β → m β
init : β
l : List α
h : start = l.toArray.size
⊢ Array.foldrM f init l.toArray start = foldrM f init l

Tactic:
subst h

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
l : List α
⊢ Array.foldrM f init l.toArray = foldrM f init l

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
l : List α
⊢ Array.foldrM f init l.toArray = foldrM f init l

Tactic:
rw [foldrM_eq_reverse_foldlM_toList]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
l : List α
⊢ List.foldlM (fun x y => f y x) init l.toArray.toList.reverse = foldrM f init l

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
l : List α
⊢ List.foldlM (fun x y => f y x) init l.toArray.toList.reverse = foldrM f init l

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
lemma cardFactors_zero : Ω 0 = 0

Proof state:
⊢ Ω 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem pow_one (a : R) : a ^ nat_lit 1 = a

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a ^ 1 = a

Tactic:
simp

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem FG.finite [L.IsRelational] {S : L.Substructure M} (h : S.FG) : Finite S

Proof state:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.IsRelational
s : Finset M
⊢ Finite ↥((closure L).toFun ↑s)

Tactic:
have hs := s.finite_toSet

Result:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.IsRelational
s : Finset M
hs : (↑s).Finite
⊢ Finite ↥((closure L).toFun ↑s)

Proof state:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.IsRelational
s : Finset M
hs : (↑((closure L).toFun ↑s)).Finite
⊢ Finite ↥((closure L).toFun ↑s)

Tactic:
exact hs

Result:
no goals

Proof state:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.IsRelational
s : Finset M
hs : (↑s).Finite
⊢ Finite ↥((closure L).toFun ↑s)

Tactic:
rw [← closure_eq_of_isRelational L (s : Set M)] at hs

Result:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.IsRelational
s : Finset M
hs : (↑((closure L).toFun ↑s)).Finite
⊢ Finite ↥((closure L).toFun ↑s)

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.IsRelational
S : L.Substructure M
h : S.FG
⊢ Finite ↥S

Tactic:
obtain ⟨s, rfl⟩ := h

Result:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.IsRelational
s : Finset M
⊢ Finite ↥((closure L).toFun ↑s)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma smul_basis_eq_zero {p q : R[X]} (hpq : p • (1 : W.CoordinateRing) + q • mk W Y = 0) :
    p = 0 ∧ q = 0

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
hpq : p • 1 + q • (mk W) Y = 0
h : ∑ i : Fin 2, ![p, q] i • (CoordinateRing.basis W) i = 0 → ∀ (i : Fin 2), ![p, q] i = 0
⊢ p = 0 ∧ q = 0

Tactic:
rw [Fin.sum_univ_succ, basis_zero, Fin.sum_univ_one, Fin.succ_zero_eq_one, basis_one] at h

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
hpq : p • 1 + q • (mk W) Y = 0
h : ![p, q] 0 • 1 + ![p, q] 1 • (mk W) Y = 0 → ∀ (i : Fin 2), ![p, q] i = 0
⊢ p = 0 ∧ q = 0

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
hpq : p • 1 + q • (mk W) Y = 0
h : ![p, q] 0 • 1 + ![p, q] 1 • (mk W) Y = 0 → ∀ (i : Fin 2), ![p, q] i = 0
⊢ p = 0 ∧ q = 0

Tactic:
exact ⟨h hpq 0, h hpq 1⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
hpq : p • 1 + q • (mk W) Y = 0
⊢ p = 0 ∧ q = 0

Tactic:
have h := Fintype.linearIndependent_iff.mp (CoordinateRing.basis W).linearIndependent ![p, q]

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
hpq : p • 1 + q • (mk W) Y = 0
h : ∑ i : Fin 2, ![p, q] i • (CoordinateRing.basis W) i = 0 → ∀ (i : Fin 2), ![p, q] i = 0
⊢ p = 0 ∧ q = 0
-- Mathlib/Data/Nat/Bits.lean
theorem zero_bits : bits 0 = []

Proof state:
⊢ bits 0 = []

Tactic:
simp [Nat.bits]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `lt_div_iff₀'` for a version with multiplication on the other side. -/
lemma lt_div_iff₀ (hc : 0 < c) : a < b / c ↔ a * c < b

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosStrictMono G₀
hc : 0 < c
⊢ a < b / c ↔ a * c < b

Tactic:
rw [div_eq_mul_inv, lt_mul_inv_iff₀ hc]

Result:
no goals
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem mem_perpBisector_iff_inner_eq :
    c ∈ perpBisector p₁ p₂ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = (dist p₁ p₂) ^ 2 / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ c ∈ perpBisector p₁ p₂ ↔ inner (c -ᵥ p₁) (p₂ -ᵥ p₁) = dist p₁ p₂ ^ 2 / 2

Tactic:
rw [mem_perpBisector_iff_inner_eq_zero, ← vsub_sub_vsub_cancel_right _ _ p₁, inner_sub_left,
  sub_eq_zero, midpoint_vsub_left, invOf_eq_inv, real_inner_smul_left, real_inner_self_eq_norm_sq,
  dist_eq_norm_vsub' V, div_eq_inv_mul]

Result:
no goals