harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem Eventually.atTop_of_arithmetic {p : ℕ → Prop} {n : ℕ} (hn : n ≠ 0)
    (hp : ∀ k < n, ∀ᶠ a in atTop, p (n * a + k)) : ∀ᶠ a in atTop, p a

Proof state:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun x => n * N x
⊢ p (n * (b / n) + b % n)

Tactic:
have hlt := Nat.mod_lt b hn.bot_lt

Result:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun x => n * N x
hlt : b % n < n
⊢ p (n * (b / n) + b % n)

Proof state:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun x => n * N x
hlt : b % n < n
⊢ b / n ≥ N (b % n)

Tactic:
rw [ge_iff_le, Nat.le_div_iff_mul_le hn.bot_lt, mul_comm]

Result:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun x => n * N x
hlt : b % n < n
⊢ n * N (b % n) ≤ b

Proof state:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ k < n, ∀ᶠ (a : ℕ) in atTop, p (n * a + k)
⊢ ∀ᶠ (a : ℕ) in atTop, p a

Tactic:
simp only [eventually_atTop] at hp ⊢

Result:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ k < n, ∃ a, ∀ b ≥ a, p (n * b + k)
⊢ ∃ a, ∀ b ≥ a, p b

Proof state:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun x => n * N x
hlt : b % n < n
⊢ p (n * (b / n) + b % n)

Tactic:
refine hN _ hlt _ ?_

Result:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun x => n * N x
hlt : b % n < n
⊢ b / n ≥ N (b % n)

Proof state:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ k < n, ∃ a, ∀ b ≥ a, p (n * b + k)
⊢ ∃ a, ∀ b ≥ a, p b

Tactic:
choose! N hN using hp

Result:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
⊢ ∃ a, ∀ b ≥ a, p b

Proof state:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun x => n * N x
⊢ p b

Tactic:
rw [← Nat.div_add_mod b n]

Result:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun x => n * N x
⊢ p (n * (b / n) + b % n)
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_preimage_inter_eq :
    (f.extend I).symm ⁻¹' (s ∩ t) ∩ range I =
      (f.extend I).symm ⁻¹' s ∩ range I ∩ (f.extend I).symm ⁻¹' t

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s t : Set M
⊢ ↑(f.extend I).symm ⁻¹' (s ∩ t) ∩ range ↑I = ↑(f.extend I).symm ⁻¹' s ∩ range ↑I ∩ ↑(f.extend I).symm ⁻¹' t

Tactic:
mfld_set_tac

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_subtype_comap {s : Set α} (hs : MeasurableSet s) (f : α → ℝ≥0∞) :
    ∫⁻ x : s, f x ∂(μ.comap (↑)) = ∫⁻ x in s, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ ∫⁻ (x : ↑s), f ↑x ∂Measure.comap Subtype.val μ = ∫⁻ (x : α) in s, f x ∂μ

Tactic:
rw [← (MeasurableEmbedding.subtype_coe hs).lintegral_map, map_comap_subtype_coe hs]

Result:
no goals
-- Mathlib/Order/Rel/GaloisConnection.lean
theorem gc_leftDual_rightDual : GaloisConnection (toDual ∘ R.leftDual) (R.rightDual ∘ ofDual) :=
  fun _ _ ↦ ⟨fun h _ ha _ hb ↦ h (by simpa) ha, fun h _ hb _ ha ↦ h (by simpa) hb⟩

Proof state:
α : Type u_1
β : Type u_2
R : Rel α β
x✝³ : Set α
x✝² : (Set β)ᵒᵈ
h : (⇑toDual ∘ R.leftDual) x✝³ ≤ x✝²
x✝¹ : α
ha : x✝¹ ∈ x✝³
x✝ : β
hb : x✝ ∈ ofDual x✝²
⊢ x✝ ∈ x✝²

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : Rel α β
x✝³ : Set α
x✝² : (Set β)ᵒᵈ
h : x✝³ ≤ (R.rightDual ∘ ⇑ofDual) x✝²
x✝¹ : β
hb : x✝¹ ∈ x✝²
x✝ : α
ha : x✝ ∈ x✝³
⊢ x✝ ∈ x✝³

Tactic:
simpa

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean
@[reassoc]
lemma homologySequenceδ_comp :
    F.homologySequenceδ T n₀ n₁ h ≫ (F.shift n₁).map T.mor₁ = 0

Proof state:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ F.homologySequenceδ T n₀ n₁ h ≫ (F.shift n₁).map T.mor₁ = 0

Tactic:
dsimp only [homologySequenceδ]

Result:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map T.mor₁ = 0

Proof state:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map T.mor₁ = 0

Tactic:
rw [← F.shiftMap_comp, comp_distTriang_mor_zero₃₁ _ hT, shiftMap_zero]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem eventually_prod_iff {p : α × β → Prop} :
    (∀ᶠ x in f ×ˢ g, p x) ↔
      ∃ pa : α → Prop, (∀ᶠ x in f, pa x) ∧ ∃ pb : β → Prop, (∀ᶠ y in g, pb y) ∧
        ∀ {x}, pa x → ∀ {y}, pb y → p (x, y)

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔
    ∃ pa, (∀ᶠ (x : α) in f, pa x) ∧ ∃ pb, (∀ᶠ (y : β) in g, pb y) ∧ ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)

Tactic:
simpa only [Set.prod_subset_iff] using @mem_prod_iff α β p f g

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem deleteEdges_deleteEdges (s s' : Set (Sym2 V)) :
    (G'.deleteEdges s).deleteEdges s' = G'.deleteEdges (s ∪ s')

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
⊢ (G'.deleteEdges s).deleteEdges s' = G'.deleteEdges (s ∪ s')

Tactic:
ext <;> simp [and_assoc, not_or]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem ext_getElem {l₁ l₂ : List α} (hl : length l₁ = length l₂)
    (h : ∀ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i]'h₁ = l₂[i]'h₂) : l₁ = l₂ :=
  ext_getElem? fun n =>
    if h₁ : n < length l₁ then by
      simp_all [getElem?_eq_getElem]
    else by
      have h₁ := Nat.le_of_not_lt h₁
      rw [getElem?_eq_none h₁, getElem?_eq_none]; rwa [← hl]

Proof state:
α : Type u_1
l₁ l₂ : List α
hl : l₁.length = l₂.length
h : ∀ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i] = l₂[i]
n : Nat
h₁ : ¬n < l₁.length
⊢ l₁[n]? = l₂[n]?

Tactic:
have h₁ := Nat.le_of_not_lt h₁

Result:
α : Type u_1
l₁ l₂ : List α
hl : l₁.length = l₂.length
h : ∀ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i] = l₂[i]
n : Nat
h₁✝ : ¬n < l₁.length
h₁ : l₁.length ≤ n
⊢ l₁[n]? = l₂[n]?

Proof state:
α : Type u_1
l₁ l₂ : List α
hl : l₁.length = l₂.length
h : ∀ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i] = l₂[i]
n : Nat
h₁✝ : ¬n < l₁.length
h₁ : l₁.length ≤ n
⊢ l₁[n]? = l₂[n]?

Tactic:
rw [getElem?_eq_none h₁, getElem?_eq_none]

Result:
α : Type u_1
l₁ l₂ : List α
hl : l₁.length = l₂.length
h : ∀ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i] = l₂[i]
n : Nat
h₁✝ : ¬n < l₁.length
h₁ : l₁.length ≤ n
⊢ l₂.length ≤ n

Proof state:
α : Type u_1
l₁ l₂ : List α
hl : l₁.length = l₂.length
h : ∀ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i] = l₂[i]
n : Nat
h₁✝ : ¬n < l₁.length
h₁ : l₁.length ≤ n
⊢ l₂.length ≤ n

Tactic:
rwa [← hl]

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
hl : l₁.length = l₂.length
h : ∀ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i] = l₂[i]
n : Nat
h₁ : n < l₁.length
⊢ l₁[n]? = l₂[n]?

Tactic:
simp_all [getElem?_eq_getElem]

Result:
no goals
-- Mathlib/Data/List/FinRange.lean
theorem get_finRange {n : ℕ} {i : ℕ} (h) :
    (finRange n).get ⟨i, h⟩ = ⟨i, length_finRange n ▸ h⟩

Proof state:
n i : ℕ
h : i < (finRange n).length
⊢ (finRange n).get ⟨i, h⟩ = ⟨i, ⋯⟩

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
theorem span_mFourierLp_closure_eq_top {p : ℝ≥0∞} [Fact (1 ≤ p)] (hp : p ≠ ∞) :
    (span ℂ (range (@mFourierLp d _ p _))).topologicalClosure = ⊤

Proof state:
d : Type u_1
inst✝¹ : Fintype d
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
⊢ (span ℂ (range (mFourierLp p))).topologicalClosure = ⊤

Tactic:
simpa only [map_span, ContinuousLinearMap.coe_coe, ← range_comp, Function.comp_def] using
  (ContinuousMap.toLp_denseRange ℂ volume ℂ hp).topologicalClosure_map_submodule
    span_mFourier_closure_eq_top

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem ι_of_isLimit {f : J → C} {t : Bicone f} (ht : IsLimit t.toCone) (j : J) :
    t.ι j = ht.lift (Fan.mk _ fun j' => if h : j = j' then eqToHom (congr_arg f h) else 0) :=
  ht.hom_ext fun j' => by
    rw [ht.fac]
    simp [t.ι_π]

Proof state:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsLimit t.toCone
j : J
j' : Discrete J
⊢ t.ι j ≫ t.toCone.π.app j' = ht.lift (Fan.mk (f j) fun j' => if h : j = j' then eqToHom ⋯ else 0) ≫ t.toCone.π.app j'

Tactic:
rw [ht.fac]

Result:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsLimit t.toCone
j : J
j' : Discrete J
⊢ t.ι j ≫ t.toCone.π.app j' = (Fan.mk (f j) fun j' => if h : j = j' then eqToHom ⋯ else 0).π.app j'

Proof state:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsLimit t.toCone
j : J
j' : Discrete J
⊢ t.ι j ≫ t.toCone.π.app j' = (Fan.mk (f j) fun j' => if h : j = j' then eqToHom ⋯ else 0).π.app j'

Tactic:
simp [t.ι_π]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma add_of_Z_eq_zero {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q)
    (hPz : P z = 0) (hQz : Q z = 0) : W.add P Q = P x ^ 2 • ![1, 1, 0]

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ W.add P Q = P x ^ 2 • ![1, 1, 0]

Tactic:
rw [add, if_pos <| equiv_of_Z_eq_zero hP hQ hPz hQz, dblXYZ_of_Z_eq_zero hP.left hPz]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem two_zsmul_oangle_neg_right (x y : V) :
    (2 : ℤ) • o.oangle x (-y) = (2 : ℤ) • o.oangle x y

Proof state:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : y = 0
⊢ 2 • o.oangle x (-y) = 2 • o.oangle x y

Tactic:
simp [hy]

Result:
no goals

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
⊢ 2 • o.oangle x (-y) = 2 • o.oangle x y

Tactic:
by_cases hy : y = 0

Result:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : y = 0
⊢ 2 • o.oangle x (-y) = 2 • o.oangle x y

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ 2 • o.oangle x (-y) = 2 • o.oangle x y

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ 2 • o.oangle x (-y) = 2 • o.oangle x y

Tactic:
simp [o.oangle_neg_right hx hy]

Result:
no goals

Proof state:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x = 0
⊢ 2 • o.oangle x (-y) = 2 • o.oangle x y

Tactic:
simp [hx]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ 2 • o.oangle x (-y) = 2 • o.oangle x y

Tactic:
by_cases hx : x = 0

Result:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x = 0
⊢ 2 • o.oangle x (-y) = 2 • o.oangle x y

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
⊢ 2 • o.oangle x (-y) = 2 • o.oangle x y
-- Mathlib/RingTheory/Idempotents.lean
lemma OrthogonalIdempotents.mul_sum_of_not_mem (he : OrthogonalIdempotents e)
    {i : I} {s : Finset I} (h : i ∉ s) : e i * ∑ j ∈ s, e j = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
i : I
s : Finset I
h : i ∉ s
⊢ e i * ∑ j ∈ s, e j = 0

Tactic:
simp [Finset.mul_sum, he.mul_eq, h]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
i : I
s : Finset I
h : i ∉ s
⊢ e i * ∑ j ∈ s, e j = 0

Tactic:
classical
simp [Finset.mul_sum, he.mul_eq, h]

Result:
no goals
-- Mathlib/Control/Traversable/Basic.lean
theorem ext ⦃η η' : ApplicativeTransformation F G⦄ (h : ∀ (α : Type u) (x : F α), η x = η' x) :
    η = η'

Proof state:
F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
η η' : ApplicativeTransformation F G
h : ∀ (α : Type u) (x : F α), (fun {α} => η.app α) x = (fun {α} => η'.app α) x
⊢ η = η'

Tactic:
apply coe_inj

Result:
case h
F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
η η' : ApplicativeTransformation F G
h : ∀ (α : Type u) (x : F α), (fun {α} => η.app α) x = (fun {α} => η'.app α) x
⊢ (fun {α} => η.app α) = fun {α} => η'.app α

Proof state:
case h
F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
η η' : ApplicativeTransformation F G
h : ∀ (α : Type u) (x : F α), (fun {α} => η.app α) x = (fun {α} => η'.app α) x
⊢ (fun {α} => η.app α) = fun {α} => η'.app α

Tactic:
ext1 α

Result:
case h.h
F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
η η' : ApplicativeTransformation F G
h : ∀ (α : Type u) (x : F α), (fun {α} => η.app α) x = (fun {α} => η'.app α) x
α : Type u
⊢ η.app α = η'.app α

Proof state:
case h.h
F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
η η' : ApplicativeTransformation F G
h : ∀ (α : Type u) (x : F α), (fun {α} => η.app α) x = (fun {α} => η'.app α) x
α : Type u
⊢ η.app α = η'.app α

Tactic:
exact funext (h α)

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma HasFPowerSeriesOnBall.prod {e : E} {f : E → F} {g : E → G} {r s : ℝ≥0∞}
    {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
    (hf : HasFPowerSeriesOnBall f p e r) (hg : HasFPowerSeriesOnBall g q e s) :
    HasFPowerSeriesOnBall (fun x ↦ (f x, g x)) (p.prod q) e (min r s)

Proof state:
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p Set.univ e r
hg : HasFPowerSeriesWithinOnBall g q Set.univ e s
⊢ HasFPowerSeriesWithinOnBall (fun x => (f x, g x)) (p.prod q) Set.univ e (r ⊓ s)

Tactic:
exact hf.prod hg

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesOnBall f p e r
hg : HasFPowerSeriesOnBall g q e s
⊢ HasFPowerSeriesOnBall (fun x => (f x, g x)) (p.prod q) e (r ⊓ s)

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf hg ⊢

Result:
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p Set.univ e r
hg : HasFPowerSeriesWithinOnBall g q Set.univ e s
⊢ HasFPowerSeriesWithinOnBall (fun x => (f x, g x)) (p.prod q) Set.univ e (r ⊓ s)
-- Mathlib/Topology/Homeomorph.lean
theorem isCompact_preimage {s : Set Y} (h : X ≃ₜ Y) : IsCompact (h ⁻¹' s) ↔ IsCompact s

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsCompact (⇑h.symm '' s) ↔ IsCompact s

Tactic:
exact h.symm.isCompact_image

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsCompact (⇑h ⁻¹' s) ↔ IsCompact s

Tactic:
rw [← image_symm]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsCompact (⇑h.symm '' s) ↔ IsCompact s
-- Mathlib/Data/List/Scan.lean
theorem length_scanl : ∀ a l, length (scanl f a l) = l.length + 1
  | _, [] => rfl
  | a, x :: l => by
    rw [scanl, length_cons, length_cons, ← succ_eq_add_one, congr_arg succ]
    exact length_scanl _ _

Proof state:
α : Type u_1
β : Type u_2
f : β → α → β
a : β
x : α
l : List α
⊢ (scanl f a (x :: l)).length = (x :: l).length + 1

Tactic:
rw [scanl, length_cons, length_cons, ← succ_eq_add_one, congr_arg succ]

Result:
α : Type u_1
β : Type u_2
f : β → α → β
a : β
x : α
l : List α
⊢ (scanl f (f a x) l).length = l.length + 1

Proof state:
α : Type u_1
β : Type u_2
f : β → α → β
a : β
x : α
l : List α
⊢ (scanl f (f a x) l).length = l.length + 1

Tactic:
exact length_scanl _ _

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Support.lean
theorem mem_span_support' (f : k[G]) :
    f ∈ Submodule.span k (of' k G '' (f.support : Set G))

Proof state:
k : Type u₁
G : Type u₂
inst✝ : Semiring k
f : k[G]
⊢ f ∈ Submodule.span k (of' k G '' ↑f.support)

Tactic:
delta of'

Result:
k : Type u₁
G : Type u₂
inst✝ : Semiring k
f : k[G]
⊢ f ∈ Submodule.span k ((fun a => single a 1) '' ↑f.support)

Proof state:
k : Type u₁
G : Type u₂
inst✝ : Semiring k
f : k[G]
⊢ f ∈ Submodule.span k ((fun a => single a 1) '' ↑f.support)

Tactic:
rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported]

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem mem_iInf {ι : Sort*} {S : ι → NonUnitalSubsemiring R} {x : R} :
    (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_1
S : ι → NonUnitalSubsemiring R
x : R
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem prime_mk {p : M} : Prime (Associates.mk p) ↔ Prime p

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
⊢ Prime (Associates.mk p) ↔ Prime p

Tactic:
rw [Prime, _root_.Prime, forall_associated]

Result:
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
⊢ (Associates.mk p ≠ 0 ∧
      ¬IsUnit (Associates.mk p) ∧
        ∀ (a : M) (b : Associates M),
          Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : M), p ∣ a * b → p ∣ a ∨ p ∣ b

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
⊢ (Associates.mk p ≠ 0 ∧
      ¬IsUnit (Associates.mk p) ∧
        ∀ (a : M) (b : Associates M),
          Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : M), p ∣ a * b → p ∣ a ∨ p ∣ b

Tactic:
simp only [forall_associated, mk_ne_zero, isUnit_mk, mk_mul_mk, mk_dvd_mk]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Gcd.lean
theorem one_gcd {a : Int} : gcd 1 a = 1

Proof state:
a : Int
⊢ gcd 1 a = 1

Tactic:
simp [gcd]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_ofReal_le_lintegral_enorm (f : α → ℝ) :
    ∫⁻ x, ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ x, ‖f x‖ₑ ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Tactic:
simp_rw [← ofReal_norm_eq_enorm]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
x : α
⊢ f x ≤ |f x|

Tactic:
exact le_abs_self (f x)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ

Tactic:
refine lintegral_mono fun x => ENNReal.ofReal_le_ofReal ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
x : α
⊢ f x ≤ ‖f x‖

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
x : α
⊢ f x ≤ ‖f x‖

Tactic:
rw [Real.norm_eq_abs]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
x : α
⊢ f x ≤ |f x|
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k a : α}
    {v : β k} :
    getKey! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then k else getKey! m a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ ¬k ∈ m then k else m.getKey! a

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ m.contains k = false then k else m.getKey! a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ m.contains k = false then k else m.getKey! a

Tactic:
simp_to_raw using Raw₀.getKey!_insertIfNew

Result:
no goals