harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean
theorem liftAlternating_one (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) :
    liftAlternating (R := R) (M := M) (N := N) f (1 : ExteriorAlgebra R M) = f 0 0

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (liftAlternating f) 1 = (f 0) 0

Tactic:
dsimp [liftAlternating]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) f) 1 0) 0 = (f 0) 0

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) f) 1 0) 0 = (f 0) 0

Tactic:
rw [foldl_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem mem_of_mem_eraseIdx {l : Array α} {i : Nat} {h} {a : α} (h : a ∈ l.eraseIdx i) : a ∈ l

Proof state:
case mk
α : Type u_1
i : Nat
a : α
l : List α
h✝ : i < { toList := l }.size
h : a ∈ { toList := l }.eraseIdx i h✝
⊢ a ∈ { toList := l }

Tactic:
simpa using List.mem_of_mem_eraseIdx (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
l : Array α
i : Nat
h✝ : i < l.size
a : α
h : a ∈ l.eraseIdx i h✝
⊢ a ∈ l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
i : Nat
a : α
l : List α
h✝ : i < { toList := l }.size
h : a ∈ { toList := l }.eraseIdx i h✝
⊢ a ∈ { toList := l }

Proof state:
α : Type u_1
i : Nat
a : α
l : List α
h✝ : i < { toList := l }.size
h : a ∈ { toList := l }.eraseIdx i h✝
⊢ a ∈ l.eraseIdx ?m.54667

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem neg_coe_pi : -(π : Angle) = π

Proof state:
⊢ -↑π = ↑π

Tactic:
rw [← coe_neg, angle_eq_iff_two_pi_dvd_sub]

Result:
⊢ ∃ k, -π - π = 2 * π * ↑k

Proof state:
⊢ ∃ k, -π - π = 2 * π * ↑k

Tactic:
use -1

Result:
case h

⊢ -π - π = 2 * π * ↑(-1)

Proof state:
case h

⊢ -π - π = 2 * π * ↑(-1)

Tactic:
simp [two_mul, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma ZModModule.char_ne_one [Nontrivial G] : n ≠ 1

Proof state:
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Nontrivial G
inst✝ : Module (ZMod 1) G
⊢ False

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : G)

Result:
case intro
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Nontrivial G
inst✝ : Module (ZMod 1) G
x : G
hx : x ≠ 0
⊢ False

Proof state:
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Nontrivial G
inst✝ : Module (ZMod 1) G
x : G
hx : x ≠ 0
⊢ x = 0

Tactic:
simpa using char_nsmul_eq_zero 1 x

Result:
no goals

Proof state:
case intro
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Nontrivial G
inst✝ : Module (ZMod 1) G
x : G
hx : x ≠ 0
⊢ False

Tactic:
exact hx <| by simpa using char_nsmul_eq_zero 1 x

Result:
no goals

Proof state:
n : ℕ
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Module (ZMod n) G
inst✝ : Nontrivial G
⊢ n ≠ 1

Tactic:
rintro rfl

Result:
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Nontrivial G
inst✝ : Module (ZMod 1) G
⊢ False
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem map_add (v w : VectorMeasure α M) (f : α → β) : (v + w).map f = v.map f + w.map f

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : Measurable f
⊢ (v + w).map f = v.map f + w.map f

Tactic:
ext i hi

Result:
case pos.h
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ ↑((v + w).map f) i = ↑(v.map f + w.map f) i

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
⊢ (v + w).map f = v.map f + w.map f

Tactic:
by_cases hf : Measurable f

Result:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : Measurable f
⊢ (v + w).map f = v.map f + w.map f

case neg
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : ¬Measurable f
⊢ (v + w).map f = v.map f + w.map f

Proof state:
case pos.h
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ ↑((v + w).map f) i = ↑(v.map f + w.map f) i

Tactic:
simp [map_apply _ hf hi]

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : ¬Measurable f
⊢ (v + w).map f = v.map f + w.map f

Tactic:
simp [map, dif_neg hf]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivAtFilter.comp_hasFDerivAtFilter_of_eq
    {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) {L'' : Filter E}
    (hh₂ : HasDerivAtFilter h₂ h₂' y L') (hf : HasFDerivAtFilter f f' x L'')
    (hL : Tendsto f L'' L') (hy : y = f x) : HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L''

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
L' : Filter 𝕜'
y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
L'' : Filter E
hh₂ : HasDerivAtFilter h₂ h₂' y L'
hf : HasFDerivAtFilter f f' x L''
hL : Tendsto f L'' L'
hy : y = f x
⊢ HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L''

Tactic:
rw [hy] at hh₂

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
L' : Filter 𝕜'
y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
L'' : Filter E
hh₂ : HasDerivAtFilter h₂ h₂' (f x) L'
hf : HasFDerivAtFilter f f' x L''
hL : Tendsto f L'' L'
hy : y = f x
⊢ HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L''

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
L' : Filter 𝕜'
y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
L'' : Filter E
hh₂ : HasDerivAtFilter h₂ h₂' (f x) L'
hf : HasFDerivAtFilter f f' x L''
hL : Tendsto f L'' L'
hy : y = f x
⊢ HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L''

Tactic:
exact hh₂.comp_hasFDerivAtFilter x hf hL

Result:
no goals
-- Mathlib/Analysis/Complex/AbelLimit.lean
theorem nhdsWithin_lt_le_nhdsWithin_stolzSet {M : ℝ} (hM : 1 < M) :
    (𝓝[<] 1).map ofReal ≤ 𝓝[stolzSet M] 1

Proof state:
M : ℝ
hM : 1 < M
⊢ Tendsto id (Filter.map ofReal (𝓝[<] 1)) (𝓝[stolzSet M] 1)

Tactic:
refine tendsto_map' <| tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within ofReal
  (tendsto_nhdsWithin_of_tendsto_nhds <| ofRealCLM.continuous.tendsto' 1 1 rfl) ?_

Result:
M : ℝ
hM : 1 < M
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, ↑x ∈ stolzSet M

Proof state:
M : ℝ
hM : 1 < M
x : ℝ
hx : x ∈ Set.Ioo 0 2 ∩ Set.Iio 1
⊢ x ∈ {x | ↑x ∈ stolzSet M}

Tactic:
simp only [Set.mem_inter_iff, Set.mem_Ioo, Set.mem_Iio] at hx

Result:
M : ℝ
hM : 1 < M
x : ℝ
hx : (0 < x ∧ x < 2) ∧ x < 1
⊢ x ∈ {x | ↑x ∈ stolzSet M}

Proof state:
M : ℝ
hM : 1 < M
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, ↑x ∈ stolzSet M

Tactic:
simp only [eventually_iff, mem_nhdsWithin]

Result:
M : ℝ
hM : 1 < M
⊢ ∃ u, IsOpen u ∧ 1 ∈ u ∧ u ∩ Set.Iio 1 ⊆ {x | ↑x ∈ stolzSet M}

Proof state:
M : ℝ
hM : 1 < M
⊢ 1 ∈ Set.Ioo 0 2

Tactic:
norm_num

Result:
no goals

Proof state:
M : ℝ
hM : 1 < M
⊢ ∃ u, IsOpen u ∧ 1 ∈ u ∧ u ∩ Set.Iio 1 ⊆ {x | ↑x ∈ stolzSet M}

Tactic:
refine ⟨Set.Ioo 0 2, isOpen_Ioo, by norm_num, fun x hx ↦ ?_⟩

Result:
M : ℝ
hM : 1 < M
x : ℝ
hx : x ∈ Set.Ioo 0 2 ∩ Set.Iio 1
⊢ x ∈ {x | ↑x ∈ stolzSet M}

Proof state:
M : ℝ
hM : 1 < M
x : ℝ
hx : (0 < x ∧ x < 2) ∧ x < 1
⊢ x < 1 ∧ 1 - x < M * (1 - x)

Tactic:
exact ⟨hx.2, lt_mul_left (sub_pos.mpr hx.2) hM⟩

Result:
no goals

Proof state:
M : ℝ
hM : 1 < M
⊢ Filter.map ofReal (𝓝[<] 1) ≤ 𝓝[stolzSet M] 1

Tactic:
rw [← tendsto_id']

Result:
M : ℝ
hM : 1 < M
⊢ Tendsto id (Filter.map ofReal (𝓝[<] 1)) (𝓝[stolzSet M] 1)

Proof state:
M : ℝ
hM : 1 < M
x : ℝ
hx : (0 < x ∧ x < 2) ∧ x < 1
⊢ x ∈ {x | ↑x ∈ stolzSet M}

Tactic:
simp only [Set.mem_setOf_eq, stolzSet, ← ofReal_one, ← ofReal_sub, norm_real,
  norm_of_nonneg hx.1.1.le, norm_of_nonneg <| (sub_pos.mpr hx.2).le]

Result:
M : ℝ
hM : 1 < M
x : ℝ
hx : (0 < x ∧ x < 2) ∧ x < 1
⊢ x < 1 ∧ 1 - x < M * (1 - x)
-- Mathlib/NumberTheory/Cyclotomic/Three.lean
theorem eq_one_or_neg_one_of_unit_of_congruent
    [NumberField K] [IsCyclotomicExtension {3} ℚ K] (hcong : ∃ n : ℤ, λ ^ 2 ∣ (u - n : 𝓞 K)) :
    u = 1 ∨ u = -1

Proof state:
case «3».intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit) - ↑n = 3 * x
⊢ ∃ n, ↑↑3 ∣ hζ.toInteger - ↑n

Tactic:
rw [sub_eq_iff_eq_add] at hx

Result:
case «3».intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit) = 3 * x + ↑n
⊢ ∃ n, ↑↑3 ∣ hζ.toInteger - ↑n

Proof state:
case «5».intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit ^ 2) - ↑n = 3 * x
⊢ ⋯.toInteger = ↑↑3 * -x + ↑(-n)

Tactic:
have : (hζ.pow_of_coprime 2 (by decide)).toInteger = hζ.toInteger ^ 2 := by ext; simp

Result:
case «5».intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit ^ 2) - ↑n = 3 * x
this : ⋯.toInteger = hζ.toInteger ^ 2
⊢ ⋯.toInteger = ↑↑3 * -x + ↑(-n)

Proof state:
case «3»
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑(-⋯.unit) - ↑n
⊢ False

Tactic:
apply hζ.not_exists_int_prime_dvd_sub_of_prime_ne_two' (by decide)

Result:
case «3»
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑(-⋯.unit) - ↑n
⊢ ∃ n, ↑↑3 ∣ hζ.toInteger - ↑n

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑(⋯.unit ^ 2) - ↑n
⊢ Nat.Coprime 2 ↑3

Tactic:
decide

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
lemma unreduced_edges_subset :
    (A ×ˢ A).filter (fun (x, y) ↦ G.Adj x y ∧ ¬ (G.regularityReduced P (ε/8) (ε/4)).Adj x y) ⊆
      (P.nonUniforms G (ε/8)).biUnion (fun (U, V) ↦ U ×ˢ V) ∪ P.parts.biUnion offDiag ∪
        (P.sparsePairs G (ε/4)).biUnion fun (U, V) ↦ G.interedges U V

Proof state:
case mk.intro.intro
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx✝ : x ∈ A
hy : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

Tactic:
obtain ⟨V, hV, hy⟩ := P.exists_mem hy

Result:
case mk.intro.intro.intro.intro
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx✝ : x ∈ A
hy✝ : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
-- Mathlib/NumberTheory/Divisors.lean
theorem prod_divisorsAntidiagonal {M : Type*} [CommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} :
    ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f i (n / i)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x ∈ n.divisors,
      f ({ toFun := fun d => (d, n / d), inj' := ⋯ } x).1 ({ toFun := fun d => (d, n / d), inj' := ⋯ } x).2 =
    ∏ i ∈ n.divisors, f i (n / i)

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f i (n / i)

Tactic:
rw [← map_div_right_divisors, Finset.prod_map]

Result:
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x ∈ n.divisors,
      f ({ toFun := fun d => (d, n / d), inj' := ⋯ } x).1 ({ toFun := fun d => (d, n / d), inj' := ⋯ } x).2 =
    ∏ i ∈ n.divisors, f i (n / i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem lex_empty [BEq α] {lt : α → α → Bool} (l : Array α) : l.lex #[] lt = false

Proof state:
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
l : Array α
⊢ l.lex #[] lt = false

Tactic:
simp [lex, Id.run]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_zero_singleton : (R ∙ (0 : M)) = ⊥

Proof state:
case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ x✝ ∈ span R {0} ↔ x✝ ∈ ⊥

Tactic:
simp [mem_span_singleton, eq_comm]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ span R {0} = ⊥

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ x✝ ∈ span R {0} ↔ x✝ ∈ ⊥
-- Mathlib/AlgebraicGeometry/Limits.lean
@[simp]
lemma coprodMk_inl (x : X) :
    coprodMk X Y (.inl x) = (coprod.inl : X ⟶ X ⨿ Y).base x

Proof state:
case e_a.e_a
X Y : Scheme
x : ↑↑X.toPresheafedSpace
⊢ colimit.ι (pair ↑X.toPresheafedSpace ↑Y.toPresheafedSpace) { as := WalkingPair.left } ≫
      (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom =
    Scheme.forgetToTop.map coprod.inl

Tactic:
exact coprodComparison_inl Scheme.forgetToTop

Result:
no goals

Proof state:
case e_a.e_a
X Y : Scheme
x : ↑↑X.toPresheafedSpace
⊢ ((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inl ≫
      (colimit.isoColimitCocone
            { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
              isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
        (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom =
    Scheme.forgetToTop.map coprod.inl

Tactic:
refine (colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.binaryCofanIsColimit _ _⟩ _ _).trans ?_

Result:
case e_a.e_a
X Y : Scheme
x : ↑↑X.toPresheafedSpace
⊢ colimit.ι (pair ↑X.toPresheafedSpace ↑Y.toPresheafedSpace) { as := WalkingPair.left } ≫
      (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom =
    Scheme.forgetToTop.map coprod.inl

Proof state:
X Y : Scheme
x : ↑↑X.toPresheafedSpace
⊢ (coprodMk X Y) (Sum.inl x) = (ConcreteCategory.hom coprod.inl.base) x

Tactic:
show ((TopCat.binaryCofan X Y).inl ≫
  (colimit.isoColimitCocone ⟨_, TopCat.binaryCofanIsColimit _ _⟩).inv ≫ _) x =
    Scheme.forgetToTop.map coprod.inl x

Result:
X Y : Scheme
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom
        (((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inl ≫
          (colimit.isoColimitCocone
                { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
                  isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
            (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom))
      x =
    (ConcreteCategory.hom (Scheme.forgetToTop.map coprod.inl)) x

Proof state:
X Y : Scheme
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom
        (((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inl ≫
          (colimit.isoColimitCocone
                { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
                  isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
            (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom))
      x =
    (ConcreteCategory.hom (Scheme.forgetToTop.map coprod.inl)) x

Tactic:
congr 2

Result:
case e_a.e_a
X Y : Scheme
x : ↑↑X.toPresheafedSpace
⊢ ((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inl ≫
      (colimit.isoColimitCocone
            { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
              isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
        (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom =
    Scheme.forgetToTop.map coprod.inl
-- Mathlib/Topology/UniformSpace/Cauchy.lean
/-- A finite indexed union is totally bounded
if and only if each set of the family is totally bounded. -/
@[simp]
lemma totallyBounded_iUnion {ι : Sort*} [Finite ι] {s : ι → Set α} :
    TotallyBounded (⋃ i, s i) ↔ ∀ i, TotallyBounded (s i)

Proof state:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
s : ι → Set α
h : ∀ (i : ι), TotallyBounded (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), s x ⊆ ⋃ y ∈ t x, {x | (x, y) ∈ U}
⊢ ∃ t, t.Finite ∧ ⋃ i, s i ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Tactic:
refine ⟨⋃ i, t i, finite_iUnion htf, ?_⟩

Result:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
s : ι → Set α
h : ∀ (i : ι), TotallyBounded (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), s x ⊆ ⋃ y ∈ t x, {x | (x, y) ∈ U}
⊢ ⋃ i, s i ⊆ ⋃ y ∈ ⋃ i, t i, {x | (x, y) ∈ U}

Proof state:
case h
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
s : ι → Set α
h : ∀ (i : ι), TotallyBounded (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), s x ⊆ ⋃ y ∈ t x, {x | (x, y) ∈ U}
i✝ : ι
⊢ s i✝ ⊆ ⋃ x ∈ t i✝, {x_1 | (x_1, x) ∈ U}

Tactic:
apply ht

Result:
no goals

Proof state:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
s : ι → Set α
h : ∀ (i : ι), TotallyBounded (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), s x ⊆ ⋃ y ∈ t x, {x | (x, y) ∈ U}
⊢ ⋃ i, s i ⊆ ⋃ y ∈ ⋃ i, t i, {x | (x, y) ∈ U}

Tactic:
rw [biUnion_iUnion]

Result:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
s : ι → Set α
h : ∀ (i : ι), TotallyBounded (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), s x ⊆ ⋃ y ∈ t x, {x | (x, y) ∈ U}
⊢ ⋃ i, s i ⊆ ⋃ i, ⋃ x ∈ t i, {x_1 | (x_1, x) ∈ U}

Proof state:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
s : ι → Set α
⊢ TotallyBounded (⋃ i, s i) ↔ ∀ (i : ι), TotallyBounded (s i)

Tactic:
refine ⟨fun h i ↦ h.subset (subset_iUnion _ _), fun h U hU ↦ ?_⟩

Result:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
s : ι → Set α
h : ∀ (i : ι), TotallyBounded (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ t, t.Finite ∧ ⋃ i, s i ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Proof state:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
s : ι → Set α
h : ∀ (i : ι), TotallyBounded (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), s x ⊆ ⋃ y ∈ t x, {x | (x, y) ∈ U}
⊢ ⋃ i, s i ⊆ ⋃ i, ⋃ x ∈ t i, {x_1 | (x_1, x) ∈ U}

Tactic:
gcongr

Result:
case h
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
s : ι → Set α
h : ∀ (i : ι), TotallyBounded (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), s x ⊆ ⋃ y ∈ t x, {x | (x, y) ∈ U}
i✝ : ι
⊢ s i✝ ⊆ ⋃ x ∈ t i✝, {x_1 | (x_1, x) ∈ U}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zipWithAll_replicate {a : α} {b : β} {n : Nat} :
    zipWithAll f (replicate n a) (replicate n b) = replicate n (f a b)

Proof state:
case zero
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : Option α → Option β → α✝
a : α
b : β
⊢ zipWithAll f (replicate 0 a) (replicate 0 b) = replicate 0 (f (some a) (some b))

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : Option α → Option β → α✝
a : α
b : β
n : Nat
ih : zipWithAll f (replicate n a) (replicate n b) = replicate n (f (some a) (some b))
⊢ zipWithAll f (replicate (n + 1) a) (replicate (n + 1) b) = replicate (n + 1) (f (some a) (some b))

Tactic:
simp [replicate_succ, ih]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : Option α → Option β → α✝
a : α
b : β
n : Nat
⊢ zipWithAll f (replicate n a) (replicate n b) = replicate n (f (some a) (some b))

Tactic:
induction n with
| zero => rfl
| succ n ih => simp [replicate_succ, ih]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem map_monomial {n a} : (monomial n a).map f = monomial n (f a)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
⊢ (C.comp f) a * X ^ n = C (f a) * X ^ n

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
⊢ eval₂ (C.comp f) X ((monomial n) a) = (monomial n) (f a)

Tactic:
rw [eval₂_monomial, ← C_mul_X_pow_eq_monomial]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
⊢ (C.comp f) a * X ^ n = C (f a) * X ^ n

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
⊢ map f ((monomial n) a) = (monomial n) (f a)

Tactic:
dsimp only [map]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
⊢ eval₂ (C.comp f) X ((monomial n) a) = (monomial n) (f a)