harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Nilpotent.lean
theorem nilpotencyClass_pi [Fintype η] [∀ i, IsNilpotent (Gs i)] :
    Group.nilpotencyClass (∀ i, Gs i) = Finset.univ.sup fun i => Group.nilpotencyClass (Gs i)

Proof state:
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Fintype η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
⊢ nilpotencyClass ((i : η) → Gs i) = Finset.univ.sup fun i => nilpotencyClass (Gs i)

Tactic:
apply eq_of_forall_ge_iff

Result:
case H
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Fintype η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
⊢ ∀ (c : ℕ), nilpotencyClass ((i : η) → Gs i) ≤ c ↔ (Finset.univ.sup fun i => nilpotencyClass (Gs i)) ≤ c

Proof state:
case H
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Fintype η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
k : ℕ
⊢ nilpotencyClass ((i : η) → Gs i) ≤ k ↔ (Finset.univ.sup fun i => nilpotencyClass (Gs i)) ≤ k

Tactic:
simp only [Finset.sup_le_iff, ← lowerCentralSeries_eq_bot_iff_nilpotencyClass_le,
  lowerCentralSeries_pi_of_finite, pi_eq_bot_iff, Finset.mem_univ, true_imp_iff]

Result:
no goals

Proof state:
case H
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Fintype η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
⊢ ∀ (c : ℕ), nilpotencyClass ((i : η) → Gs i) ≤ c ↔ (Finset.univ.sup fun i => nilpotencyClass (Gs i)) ≤ c

Tactic:
intro k

Result:
case H
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Fintype η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
k : ℕ
⊢ nilpotencyClass ((i : η) → Gs i) ≤ k ↔ (Finset.univ.sup fun i => nilpotencyClass (Gs i)) ≤ k
-- Mathlib/Data/Real/Archimedean.lean
theorem exists_isLUB (hne : s.Nonempty) (hbdd : BddAbove s) : ∃ x, IsLUB s x

Proof state:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ ↑j
ik : ε⁻¹ ≤ ↑k
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε

Tactic:
have j0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ij)

Result:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ ↑j
ik : ε⁻¹ ≤ ↑k
j0 : 0 < j
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε

Proof state:
case intro.intro.refine_1.intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n => ↑(f n) / ↑n, hg⟩
x : ℝ
xS : x ∈ s
z : ℝ
K n : ℕ
nK : n ≥ K
xz : 0 < x - z
hK : (x - z)⁻¹ ≤ ↑n
n0 : 0 < n
⊢ z ≤ ↑(↑g n)

Tactic:
refine le_trans ?_ (hf₂ _ n0 _ xS).le

Result:
case intro.intro.refine_1.intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n => ↑(f n) / ↑n, hg⟩
x : ℝ
xS : x ∈ s
z : ℝ
K n : ℕ
nK : n ≥ K
xz : 0 < x - z
hK : (x - z)⁻¹ ≤ ↑n
n0 : 0 < n
⊢ z ≤ x - (↑n)⁻¹

Proof state:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ik : k ≥ ⌈ε⁻¹⌉₊
ij : ε⁻¹ ≤ ↑j
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε

Tactic:
replace ik := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ik)

Result:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ ↑j
ik : ε⁻¹ ≤ ↑k
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε
-- Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean
theorem lebesgue_number_lemma_of_metric_sUnion {s : Set α} {c : Set (Set α)} (hs : IsCompact s)
    (hc₁ : ∀ t ∈ c, IsOpen t) (hc₂ : s ⊆ ⋃₀ c) : ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen t
hc₂ : s ⊆ ⋃₀ c
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t

Tactic:
rw [sUnion_eq_iUnion] at hc₂

Result:
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen t
hc₂ : s ⊆ ⋃ i, ↑i
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen t
hc₂ : s ⊆ ⋃ i, ↑i
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t

Tactic:
simpa using lebesgue_number_lemma_of_metric hs (by simpa) hc₂

Result:
no goals

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen t
hc₂ : s ⊆ ⋃ i, ↑i
⊢ ∀ (i : ↑c), IsOpen ↑i

Tactic:
simpa

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/Residual.lean
theorem setOf_liouville_eq_iInter_iUnion :
    { x | Liouville x } =
      ⋂ n : ℕ, ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b),
      ball ((a : ℝ) / b) (1 / (b : ℝ) ^ n) \ {(a : ℝ) / b}

Proof state:
case h
x : ℝ
⊢ x ∈ {x | Liouville x} ↔ x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}

Tactic:
simp only [mem_iInter, mem_iUnion, Liouville, mem_setOf_eq, exists_prop, mem_diff,
  mem_singleton_iff, mem_ball, Real.dist_eq, and_comm]

Result:
no goals

Proof state:
⊢ {x | Liouville x} = ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}

Tactic:
ext x

Result:
case h
x : ℝ
⊢ x ∈ {x | Liouville x} ↔ x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}
-- Mathlib/Analysis/NormedSpace/Real.lean
theorem dist_smul_add_one_sub_smul_le {r : ℝ} {x y : E} (h : r ∈ Icc 0 1) :
    dist (r • x + (1 - r) • y) x ≤ dist y x :=
  calc
    dist (r • x + (1 - r) • y) x = ‖1 - r‖ * ‖x - y‖

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ (1 - r) * dist y x ≤ (1 - 0) * dist y x

Tactic:
gcongr

Result:
case h.h
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ 0 ≤ r

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ dist (r • x + (1 - r) • y) x = ‖1 - r‖ * ‖x - y‖

Tactic:
simp_rw [dist_eq_norm', ← norm_smul, sub_smul, one_smul, smul_sub, ← sub_sub, ← sub_add,
  sub_right_comm]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ (1 - 0) * dist y x = dist y x

Tactic:
rw [sub_zero, one_mul]

Result:
no goals

Proof state:
case h.h
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ 0 ≤ r

Tactic:
exact h.1

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ ‖1 - r‖ * ‖x - y‖ = (1 - r) * dist y x

Tactic:
rw [Real.norm_eq_abs, abs_eq_self.mpr (sub_nonneg.mpr h.2), dist_eq_norm']

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Slope.lean
theorem hasDerivAt_iff_tendsto_slope_zero :
    HasDerivAt f f' x ↔ Tendsto (fun t ↦ t⁻¹ • (f (x + t) - f x)) (𝓝[≠] 0) (𝓝 f')

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
this : 𝓝[≠] x = map (fun t => x + t) (𝓝[≠] 0)
⊢ HasDerivAt f f' x ↔ Tendsto (fun t => t⁻¹ • (f (x + t) - f x)) (𝓝[≠] 0) (𝓝 f')

Tactic:
simp [hasDerivAt_iff_tendsto_slope, this, slope, Function.comp_def]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
⊢ HasDerivAt f f' x ↔ Tendsto (fun t => t⁻¹ • (f (x + t) - f x)) (𝓝[≠] 0) (𝓝 f')

Tactic:
have : 𝓝[≠] x = Filter.map (fun t ↦ x + t) (𝓝[≠] 0) := by
  simp [nhdsWithin, map_add_left_nhds_zero x, Filter.map_inf, add_right_injective x]

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
this : 𝓝[≠] x = map (fun t => x + t) (𝓝[≠] 0)
⊢ HasDerivAt f f' x ↔ Tendsto (fun t => t⁻¹ • (f (x + t) - f x)) (𝓝[≠] 0) (𝓝 f')

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
⊢ 𝓝[≠] x = map (fun t => x + t) (𝓝[≠] 0)

Tactic:
simp [nhdsWithin, map_add_left_nhds_zero x, Filter.map_inf, add_right_injective x]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
/-- RHS form is used, e.g., in the definition of `UniformSpace`. -/
lemma mem_comap_prod_mk {x : α} {s : Set β} {F : Filter (α × β)} :
    s ∈ comap (Prod.mk x) F ↔ {p : α × β | p.fst = x → p.snd ∈ s} ∈ F

Proof state:
α : Type u_1
β : Type u_2
x : α
s : Set β
F : Filter (α × β)
⊢ s ∈ comap (Prod.mk x) F ↔ {p | p.1 = x → p.2 ∈ s} ∈ F

Tactic:
simp_rw [mem_comap', Prod.ext_iff, and_imp, @forall_swap β (_ = _), forall_eq, eq_comm]

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem BlankExtends.trans {Γ} [Inhabited Γ] {l₁ l₂ l₃ : List Γ} :
    BlankExtends l₁ l₂ → BlankExtends l₂ l₃ → BlankExtends l₁ l₃

Proof state:
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ : List Γ
i j : ℕ
⊢ BlankExtends l₁ (l₁ ++ List.replicate i default ++ List.replicate j default)

Tactic:
exact ⟨i + j, by simp⟩

Result:
no goals

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
⊢ BlankExtends l₁ l₂ → BlankExtends l₂ l₃ → BlankExtends l₁ l₃

Tactic:
rintro ⟨i, rfl⟩ ⟨j, rfl⟩

Result:
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ : List Γ
i j : ℕ
⊢ BlankExtends l₁ (l₁ ++ List.replicate i default ++ List.replicate j default)

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ : List Γ
i j : ℕ
⊢ l₁ ++ List.replicate i default ++ List.replicate j default = l₁ ++ List.replicate (i + j) default

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_pi_div_eight : sin (π / 8) = √(2 - √2) / 2

Proof state:
⊢ sin (π / 8) = sin (π / 2 ^ 3)

Tactic:
congr

Result:
case e_x.e_a

⊢ 8 = 2 ^ 3

Proof state:
case e_x.e_a

⊢ 8 = 2 ^ 3

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ sin (π / 2 ^ 3) = √(2 - √2) / 2

Tactic:
simp

Result:
no goals

Proof state:
⊢ sin (π / 8) = √(2 - √2) / 2

Tactic:
trans sin (π / 2 ^ 3)

Result:
⊢ sin (π / 8) = sin (π / 2 ^ 3)


⊢ sin (π / 2 ^ 3) = √(2 - √2) / 2
-- Mathlib/CategoryTheory/Sites/Coherent/ExtensiveTopology.lean
lemma extensiveTopology.mem_sieves_iff_contains_colimit_cofan {X : C} (S : Sieve X) :
    S ∈ (extensiveTopology C) X ↔
      (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → (Y a ⟶ X)),
        Nonempty (IsColimit (Cofan.mk X π)) ∧ (∀ a : α, (S.arrows) (π a)))

Proof state:
case mp.top
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S : Sieve X✝
X : C
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), ⊤.arrows (π a)

Tactic:
refine ⟨Unit, inferInstance, fun _ => X, fun _ => (𝟙 X), ⟨?_⟩, by simp⟩

Result:
case mp.top
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S : Sieve X✝
X : C
⊢ IsColimit (Cofan.mk X fun x => 𝟙 X)

Proof state:
case mp.of.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Sieve.generate S).arrows (π a)

Tactic:
refine ⟨α, inferInstance, Y, π, ?_, fun a ↦ ?_⟩

Result:
case mp.of.intro.intro.intro.intro.intro.refine_1
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
⊢ Nonempty (IsColimit (Cofan.mk X π))

case mp.of.intro.intro.intro.intro.intro.refine_2
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
a : α
⊢ (Sieve.generate S).arrows (π a)
-- Mathlib/Algebra/Homology/BifunctorAssociator.lean
@[reassoc]
lemma mapBifunctorAssociatorX_hom_D₁ (j j' : ι₄) :
    (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom ≫
      mapBifunctor₂₃.D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j' =
        mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' ≫
        (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom

Proof state:
case pos
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝³³ : Category.{u_16, u_1} C₁
inst✝³² : Category.{u_17, u_2} C₂
inst✝³¹ : Category.{u_15, u_5} C₃
inst✝³⁰ : Category.{u_13, u_6} C₄
inst✝²⁹ : Category.{u_14, u_3} C₁₂
inst✝²⁸ : Category.{u_18, u_4} C₂₃
inst✝²⁷ : HasZeroMorphisms C₁
inst✝²⁶ : HasZeroMorphisms C₂
inst✝²⁵ : HasZeroMorphisms C₃
inst✝²⁴ : Preadditive C₁₂
inst✝²³ : Preadditive C₂₃
inst✝²² : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝²¹ : F₁₂.PreservesZeroMorphisms
inst✝²⁰ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝¹⁹ : G.Additive
inst✝¹⁸ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
inst✝¹⁷ : G₂₃.PreservesZeroMorphisms
inst✝¹⁶ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁵ : F.PreservesZeroMorphisms
inst✝¹⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝¹³ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝¹² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹¹ : TotalComplexShape c₁₂ c₃ c₄
inst✝¹⁰ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁹ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁸ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝⁷ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝⁶ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝⁵ : DecidableEq ι₁₂
inst✝⁴ : DecidableEq ι₂₃
inst✝³ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
inst✝² : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝¹ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : c₁.Rel i₁ (c₁.next i₁)
this :
  (G.map ((F₁₂.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂))).app (K₃.X i₃) ≫
      ((associator.hom.app (K₁.X (c₁.next i₁))).app (K₂.X i₂)).app (K₃.X i₃) =
    ((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃) ≫
      (F.map (K₁.d i₁ (c₁.next i₁))).app ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃))
⊢ ((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃) ≫
      mapBifunctor₂₃.d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j' =
    mapBifunctor₁₂.d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j' ≫
      (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom

Tactic:
rw [mapBifunctor₁₂.d₁_eq _ _ _ _ _ _ _ h₁, mapBifunctor₂₃.d₁_eq _ _ _ _ _ _ _ _ h₁,
  Linear.comp_units_smul, Linear.units_smul_comp, assoc,
    ComplexShape.associative_ε₁_eq_mul c₁ c₂ c₃ c₁₂ c₂₃ c₄,
  ιOrZero_mapBifunctorAssociatorX_hom, smul_left_cancel_iff,
  reassoc_of% this]

Result:
no goals
-- Mathlib/Analysis/Analytic/ChangeOrigin.lean
theorem changeOriginSeries_summable_aux₃ {r : ℝ≥0} (hr : ↑r < p.radius) (k : ℕ) :
    Summable fun l : ℕ => ‖p.changeOriginSeries k l‖₊ * r ^ l

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : ↑r < p.radius
k : ℕ
⊢ Summable fun l => ‖p.changeOriginSeries k l‖₊ * r ^ l

Tactic:
refine NNReal.summable_of_le
  (fun n => ?_) (NNReal.summable_sigma.1 <| p.changeOriginSeries_summable_aux₂ hr k).2

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : ↑r < p.radius
k n : ℕ
⊢ ‖p.changeOriginSeries k n‖₊ * r ^ n ≤ ∑' (y : { s // s.card = n }), ‖p (k + ⟨n, y⟩.fst)‖₊ * r ^ ⟨n, y⟩.fst

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : ↑r < p.radius
k n : ℕ
⊢ ‖p.changeOriginSeries k n‖₊ * r ^ n ≤ (∑' (x : { s // s.card = n }), ‖p (k + n)‖₊) * r ^ n

Tactic:
exact mul_le_mul' (p.nnnorm_changeOriginSeries_le_tsum _ _) le_rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : ↑r < p.radius
k n : ℕ
⊢ ‖p.changeOriginSeries k n‖₊ * r ^ n ≤ ∑' (y : { s // s.card = n }), ‖p (k + ⟨n, y⟩.fst)‖₊ * r ^ ⟨n, y⟩.fst

Tactic:
simp only [NNReal.tsum_mul_right]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : ↑r < p.radius
k n : ℕ
⊢ ‖p.changeOriginSeries k n‖₊ * r ^ n ≤ (∑' (x : { s // s.card = n }), ‖p (k + n)‖₊) * r ^ n
-- Mathlib/Analysis/CStarAlgebra/Hom.lean
lemma IsSelfAdjoint.map_spectrum_real {F A B : Type*} [CStarAlgebra A] [CStarAlgebra B]
    [FunLike F A B] [AlgHomClass F ℂ A B] [StarHomClass F A B]
    {a : A} (ha : IsSelfAdjoint a) (φ : F) (hφ : Function.Injective φ) :
    spectrum ℝ (φ a) = spectrum ℝ a

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CStarAlgebra A
inst✝³ : CStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective ⇑φ
h_spec : spectrum ℝ ((StarAlgHom.restrictScalars ℝ ↑φ) a) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum ℝ (φ a)
⊢ Disjoint (spectrum ℝ (φ a)) {x}

Tactic:
simpa

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma nonsingular_iff (x y : R) : W'.Nonsingular x y ↔ W'.Equation x y ∧
    (W'.a₁ * y ≠ 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ∨ y ≠ -y - W'.a₁ * x - W'.a₃)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Nonsingular x y ↔ W'.Equation x y ∧ (W'.a₁ * y ≠ 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ∨ y ≠ -y - W'.a₁ * x - W'.a₃)

Tactic:
rw [nonsingular_iff', sub_ne_zero, ← sub_ne_zero (a := y)]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Equation x y ∧ (W'.a₁ * y ≠ 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ∨ 2 * y + W'.a₁ * x + W'.a₃ ≠ 0) ↔
    W'.Equation x y ∧ (W'.a₁ * y ≠ 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ∨ y - (-y - W'.a₁ * x - W'.a₃) ≠ 0)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Equation x y ∧ (W'.a₁ * y ≠ 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ∨ 2 * y + W'.a₁ * x + W'.a₃ ≠ 0) ↔
    W'.Equation x y ∧ (W'.a₁ * y ≠ 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ∨ y - (-y - W'.a₁ * x - W'.a₃) ≠ 0)

Tactic:
congr! 3

Result:
case a.h.e'_2.h.e'_2.h.e'_2
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ 2 * y + W'.a₁ * x + W'.a₃ = y - (-y - W'.a₁ * x - W'.a₃)

Proof state:
case a.h.e'_2.h.e'_2.h.e'_2
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ 2 * y + W'.a₁ * x + W'.a₃ = y - (-y - W'.a₁ * x - W'.a₃)

Tactic:
ring1

Result:
no goals
-- Mathlib/Data/Nat/Hyperoperation.lean
theorem hyperoperation_one : hyperoperation 1 = (· + ·)

Proof state:
case h.h.succ
m bn : ℕ
bih : hyperoperation 1 m bn = m + bn
⊢ (m + bn).succ = m + (bn + 1)

Tactic:
exact Nat.add_assoc m bn 1

Result:
no goals

Proof state:
case h.h
m k : ℕ
⊢ hyperoperation 1 m k = m + k

Tactic:
induction' k with bn bih

Result:
case h.h.zero
m : ℕ
⊢ hyperoperation 1 m 0 = m + 0

case h.h.succ
m bn : ℕ
bih : hyperoperation 1 m bn = m + bn
⊢ hyperoperation 1 m (bn + 1) = m + (bn + 1)

Proof state:
case h.h.succ
m bn : ℕ
bih : hyperoperation 1 m bn = m + bn
⊢ hyperoperation 1 m (bn + 1) = m + (bn + 1)

Tactic:
rw [hyperoperation_recursion, bih, hyperoperation_zero]

Result:
case h.h.succ
m bn : ℕ
bih : hyperoperation 1 m bn = m + bn
⊢ (m + bn).succ = m + (bn + 1)

Proof state:
case h.h.zero
m : ℕ
⊢ hyperoperation 1 m 0 = m + 0

Tactic:
rw [Nat.add_zero m, hyperoperation]

Result:
no goals

Proof state:
⊢ hyperoperation 1 = fun x1 x2 => x1 + x2

Tactic:
ext m k

Result:
case h.h
m k : ℕ
⊢ hyperoperation 1 m k = m + k
-- Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean
theorem precoherent_isSheaf_iff (e : C ≌ D) (F : Cᵒᵖ ⥤ A) : haveI := e.precoherent
    IsSheaf (coherentTopology C) F ↔ IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Precoherent C
A : Type u_3
inst✝ : Category.{u_6, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (coherentTopology C) F

Tactic:
rw [isSheaf_of_iso_iff (P' := e.functor.op ⋙ e.inverse.op ⋙ F)]

Result:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Precoherent C
A : Type u_3
inst✝ : Category.{u_6, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (coherentTopology C) (e.functor.op ⋙ e.inverse.op ⋙ F)

C : Type u_1
inst✝³ : Category.{u_4, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Precoherent C
A : Type u_3
inst✝ : Category.{u_6, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)
⊢ F ≅ e.functor.op ⋙ e.inverse.op ⋙ F

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Precoherent C
A : Type u_3
inst✝ : Category.{u_6, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (coherentTopology C) (e.functor.op ⋙ e.inverse.op ⋙ F)

Tactic:
exact (e.sheafCongrPrecoherent A).inverse.obj ⟨e.inverse.op ⋙ F, hF⟩ |>.cond

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Precoherent C
A : Type u_3
inst✝ : Category.{u_6, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)
⊢ F ≅ e.functor.op ⋙ e.inverse.op ⋙ F

Tactic:
exact isoWhiskerRight e.op.unitIso F

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Precoherent C
A : Type u_3
inst✝ : Category.{u_6, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
⊢ IsSheaf (coherentTopology C) F ↔ IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)

Tactic:
refine ⟨fun hF ↦ ((e.sheafCongrPrecoherent A).functor.obj ⟨F, hF⟩).cond, fun hF ↦ ?_⟩

Result:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Precoherent C
A : Type u_3
inst✝ : Category.{u_6, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (coherentTopology C) F