harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem zero_comp (f : NormedAddGroupHom V₁ V₂) : (0 : NormedAddGroupHom V₂ V₃).comp f = 0

Proof state:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
⊢ NormedAddGroupHom.comp 0 f = 0

Tactic:
ext

Result:
case H
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
x✝ : V₁
⊢ (NormedAddGroupHom.comp 0 f) x✝ = 0 x✝

Proof state:
case H
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
x✝ : V₁
⊢ (NormedAddGroupHom.comp 0 f) x✝ = 0 x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Factorization/PrimePow.lean
theorem exists_ordCompl_eq_one_iff_isPrimePow {n : ℕ} (hn : n ≠ 1) :
    IsPrimePow n ↔ ∃ p : ℕ, p.Prime ∧ ordCompl[p] n = 1

Proof state:
case intro.intro
n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rw [← Nat.eq_of_dvd_of_div_eq_one (Nat.ordProj_dvd n p) h] at hn ⊢

Result:
case intro.intro
n p : ℕ
hn : p ^ n.factorization p ≠ 1
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ ∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ n.factorization p

Proof state:
case intro.intro
n p : ℕ
hn : p ^ n.factorization p ≠ 1
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ 0 < n.factorization p

Tactic:
contrapose! hn

Result:
case intro.intro
n p : ℕ
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
hn : n.factorization p ≤ 0
⊢ p ^ n.factorization p = 1

Proof state:
n : ℕ
hn : n ≠ 1
h : ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
⊢ IsPrimePow n

Tactic:
rcases h with ⟨p, pp, h⟩

Result:
case intro.intro
n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ IsPrimePow n

Proof state:
case intro.intro
n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ IsPrimePow n

Tactic:
rw [isPrimePow_nat_iff]

Result:
case intro.intro
n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Proof state:
case intro.intro
n p : ℕ
hn : p ^ n.factorization p ≠ 1
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ ∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ n.factorization p

Tactic:
refine ⟨p, n.factorization p, pp, ?_, by simp⟩

Result:
case intro.intro
n p : ℕ
hn : p ^ n.factorization p ≠ 1
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ 0 < n.factorization p

Proof state:
n : ℕ
hn : n ≠ 1
⊢ IsPrimePow n ↔ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
refine ⟨fun h => IsPrimePow.exists_ordCompl_eq_one h, fun h => ?_⟩

Result:
n : ℕ
hn : n ≠ 1
h : ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
⊢ IsPrimePow n

Proof state:
case intro.intro
n p : ℕ
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
hn : n.factorization p ≤ 0
⊢ p ^ n.factorization p = 1

Tactic:
simp [Nat.le_zero.1 hn]

Result:
no goals

Proof state:
n p : ℕ
hn : p ^ n.factorization p ≠ 1
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ p ^ n.factorization p = p ^ n.factorization p

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/TopologicallyNilpotent.lean
theorem add_of_commute [IsLinearTopology R R] {a b : R}
    (ha : IsTopologicallyNilpotent a) (hb : IsTopologicallyNilpotent b) (h : Commute a b) :
    IsTopologicallyNilpotent (a + b)

Proof state:
case intro
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
ha✝ : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent b
h : Commute a b
I : Ideal R
I_mem_nhds : ↑I ∈ 𝓝 0
na : ℕ
ha : a ^ na ∈ ↑I
⊢ ∃ ia, ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ ↑I

Tactic:
obtain ⟨nb, hb⟩ := hb.exists_pow_mem_of_mem_nhds I_mem_nhds

Result:
case intro.intro
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
ha✝ : IsTopologicallyNilpotent a
hb✝ : IsTopologicallyNilpotent b
h : Commute a b
I : Ideal R
I_mem_nhds : ↑I ∈ 𝓝 0
na : ℕ
ha : a ^ na ∈ ↑I
nb : ℕ
hb : b ^ nb ∈ ↑I
⊢ ∃ ia, ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ ↑I

Proof state:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent b
h : Commute a b
⊢ IsTopologicallyNilpotent (a + b)

Tactic:
simp only [IsTopologicallyNilpotent, atTop_basis.tendsto_iff IsLinearTopology.hasBasis_ideal,
  true_and]

Result:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent b
h : Commute a b
⊢ ∀ (ib : Ideal R), ↑ib ∈ 𝓝 0 → ∃ ia, ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ ↑ib

Proof state:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent b
h : Commute a b
I : Ideal R
I_mem_nhds : ↑I ∈ 𝓝 0
⊢ ∃ ia, ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ ↑I

Tactic:
obtain ⟨na, ha⟩ := ha.exists_pow_mem_of_mem_nhds I_mem_nhds

Result:
case intro
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
ha✝ : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent b
h : Commute a b
I : Ideal R
I_mem_nhds : ↑I ∈ 𝓝 0
na : ℕ
ha : a ^ na ∈ ↑I
⊢ ∃ ia, ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ ↑I

Proof state:
case intro.intro
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
ha✝ : IsTopologicallyNilpotent a
hb✝ : IsTopologicallyNilpotent b
h : Commute a b
I : Ideal R
I_mem_nhds : ↑I ∈ 𝓝 0
na : ℕ
ha : a ^ na ∈ ↑I
nb : ℕ
hb : b ^ nb ∈ ↑I
⊢ ∃ ia, ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ ↑I

Tactic:
exact ⟨na + nb, fun m hm ↦
  I.add_pow_mem_of_pow_mem_of_le_of_commute ha hb (le_trans hm (Nat.le_add_right _ _)) h⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent b
h : Commute a b
⊢ ∀ (ib : Ideal R), ↑ib ∈ 𝓝 0 → ∃ ia, ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ ↑ib

Tactic:
intro I I_mem_nhds

Result:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent b
h : Commute a b
I : Ideal R
I_mem_nhds : ↑I ∈ 𝓝 0
⊢ ∃ ia, ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ ↑I
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem isSome_attach (o : Option α) : o.attach.isSome = o.isSome

Proof state:
α : Type u_1
o : Option α
⊢ o.attach.isSome = o.isSome

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem sign_eq_zero_iff : sign a = 0 ↔ a = 0

Proof state:
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : sign a = 0
⊢ a = 0

Tactic:
rw [sign_apply] at h

Result:
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = 0
⊢ a = 0

Proof state:
case neg.refl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h_1 : ¬0 < a
h_2 : ¬a < 0
⊢ a = 0

Tactic:
exact (le_of_not_lt h_1).eq_of_not_lt h_2

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h_1 : ¬0 < a
h_2 : ¬a < 0
h : 0 = 0
⊢ a = 0

Tactic:
cases h

Result:
case neg.refl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h_1 : ¬0 < a
h_2 : ¬a < 0
⊢ a = 0

Proof state:
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = 0
⊢ a = 0

Tactic:
split_ifs at h with h_1 h_2

Result:
case neg
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h_1 : ¬0 < a
h_2 : ¬a < 0
h : 0 = 0
⊢ a = 0

Proof state:
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ sign a = 0 ↔ a = 0

Tactic:
refine ⟨fun h => ?_, fun h => h.symm ▸ sign_zero⟩

Result:
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : sign a = 0
⊢ a = 0
-- Mathlib/Computability/Halting.lean
theorem not {p : α → Prop} (hp : ComputablePred p) : ComputablePred fun a => ¬p a

Proof state:
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ DecidablePred fun a => ¬(fun a => f a = true) a

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Primcodable α
p : α → Prop
hp : ComputablePred p
⊢ ComputablePred fun a => ¬p a

Tactic:
obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp

Result:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ ComputablePred fun a => ¬(fun a => f a = true) a

Proof state:
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
⊢ (bif f n then false else true) = decide ((fun a => ¬(fun a => f a = true) a) n)

Tactic:
simp only [Bool.not_eq_true]

Result:
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
⊢ (bif f n then false else true) = decide (f n = false)

Proof state:
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
⊢ (bif f n then false else true) = decide (f n = false)

Tactic:
cases f n <;> rfl

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ ComputablePred fun a => ¬(fun a => f a = true) a

Tactic:
exact
  ⟨by infer_instance,
    (cond hf (const false) (const true)).of_eq fun n => by
      simp only [Bool.not_eq_true]
      cases f n <;> rfl⟩

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem pow {M : Type*} [Monoid M] (c : Con M) :
    ∀ (n : ℕ) {w x}, c w x → c (w ^ n) (x ^ n)
  | 0, w, x, _ => by simpa using c.refl _
  | Nat.succ n, w, x, h => by simpa [pow_succ] using c.mul (Con.pow c n h) h

Proof state:
M : Type u_4
inst✝ : Monoid M
c : Con M
n : ℕ
w x : M
h : c w x
⊢ c (w ^ n.succ) (x ^ n.succ)

Tactic:
simpa [pow_succ] using c.mul (Con.pow c n h) h

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
c : Con M
w x : M
x✝ : c w x
⊢ c (w ^ 0) (x ^ 0)

Tactic:
simpa using c.refl _

Result:
no goals
-- Mathlib/Analysis/Calculus/ParametricIntegral.lean
theorem hasFDerivAt_integral_of_dominated_loc_of_lip {F' : α → H →L[𝕜] E}
    (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) μ)
    (hF_int : Integrable (F x₀) μ) (hF'_meas : AEStronglyMeasurable F' μ)
    (h_lip : ∀ᵐ a ∂μ, LipschitzOnWith (Real.nnabs <| bound a) (F · a) (ball x₀ ε))
    (bound_integrable : Integrable (bound : α → ℝ) μ)
    (h_diff : ∀ᵐ a ∂μ, HasFDerivAt (F · a) (F' a) x₀) :
    Integrable F' μ ∧ HasFDerivAt (fun x ↦ ∫ a, F x a ∂μ) (∫ a, F' a ∂μ) x₀

Proof state:
case intro.intro
α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
ε : ℝ
F' : α → H →L[𝕜] E
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lip : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀
δ : ℝ
δ_pos : δ > 0
hδ_meas : ∀ x ∈ ball x₀ δ, AEStronglyMeasurable (F x) μ
hδε : ∀ x ∈ ball x₀ δ, x ∈ ball x₀ ε
⊢ Integrable F' μ ∧ HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
replace h_lip : ∀ᵐ a : α ∂μ, ∀ x ∈ ball x₀ δ, ‖F x a - F x₀ a‖ ≤ |bound a| * ‖x - x₀‖ :=
  h_lip.mono fun a lip x hx ↦ lip.norm_sub_le (hδε x hx) (mem_ball_self ε_pos)

Result:
case intro.intro
α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
ε : ℝ
F' : α → H →L[𝕜] E
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀
δ : ℝ
δ_pos : δ > 0
hδ_meas : ∀ x ∈ ball x₀ δ, AEStronglyMeasurable (F x) μ
hδε : ∀ x ∈ ball x₀ δ, x ∈ ball x₀ ε
h_lip : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ δ, ‖F x a - F x₀ a‖ ≤ |bound a| * ‖x - x₀‖
⊢ Integrable F' μ ∧ HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isPrefixOf_length_pos_nil {L : List α} (h : 0 < L.length) : isPrefixOf L [] = false

Proof state:
α : Type u_1
inst✝ : BEq α
L : List α
h : 0 < L.length
⊢ L.isPrefixOf [] = false

Tactic:
cases L <;> simp_all [isPrefixOf]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem disjoint_append_right : Disjoint l (l₁ ++ l₂) ↔ Disjoint l l₁ ∧ Disjoint l l₂ :=
  disjoint_comm.trans <| by rw [disjoint_append_left]; simp [disjoint_comm]

Proof state:
α✝ : Type u_1
l l₁ l₂ : List α✝
⊢ l₁.Disjoint l ∧ l₂.Disjoint l ↔ l.Disjoint l₁ ∧ l.Disjoint l₂

Tactic:
simp [disjoint_comm]

Result:
no goals

Proof state:
α✝ : Type u_1
l l₁ l₂ : List α✝
⊢ (l₁ ++ l₂).Disjoint l ↔ l.Disjoint l₁ ∧ l.Disjoint l₂

Tactic:
rw [disjoint_append_left]

Result:
α✝ : Type u_1
l l₁ l₂ : List α✝
⊢ l₁.Disjoint l ∧ l₂.Disjoint l ↔ l.Disjoint l₁ ∧ l.Disjoint l₂
-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
/-- As `x` approaches `1` from the right along the real axis, the L-series of
`ArithmeticFunction.vonMangoldt.residueClass` is bounded below by `(q.totient)⁻¹/(x-1) - C`. -/
lemma LSeries_residueClass_lower_bound (ha : IsUnit a) :
    ∃ C : ℝ, ∀ {x : ℝ} (_ : x ∈ Set.Ioc 1 2),
      (q.totient : ℝ)⁻¹ / (x - 1) - C ≤ ∑' n, residueClass a n / (n : ℝ) ^ x

Proof state:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H :
  ∀ {x : ℝ},
    1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x = (LFunctionResidueClassAux a ↑x).re + (↑q.totient)⁻¹ / (x - 1)
⊢ ∃ C, ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x

Tactic:
have : ContinuousOn (fun x : ℝ ↦ (LFunctionResidueClassAux a x).re) (Set.Icc 1 2) :=
  continuous_re.continuousOn.comp (t := Set.univ) (continuousOn_LFunctionResidueClassAux a)
    (fun ⦃x⦄ a ↦ trivial) |>.comp continuous_ofReal.continuousOn fun x hx ↦ by
      simpa only [Set.mem_setOf_eq, ofReal_re] using hx.1

Result:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H :
  ∀ {x : ℝ},
    1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x = (LFunctionResidueClassAux a ↑x).re + (↑q.totient)⁻¹ / (x - 1)
this : ContinuousOn (fun x => (LFunctionResidueClassAux a ↑x).re) (Set.Icc 1 2)
⊢ ∃ C, ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x

Proof state:
case pos
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
n : ℕ
hn : n = 0
⊢ ↑(residueClass a n) / ↑n ^ ↑x = 0

Tactic:
simp only [hn, residueClass_apply_zero, ofReal_zero, zero_div]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_neg_one (x : ℝ≥0∞) : x ^ (-1 : ℝ) = x⁻¹

Proof state:
x : ℝ≥0∞
⊢ x ^ (-1) = x⁻¹

Tactic:
simp [rpow_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_singleton (a b : α) : count a #[b] = if b == a then 1 else 0

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
⊢ count a #[b] = if (b == a) = true then 1 else 0

Tactic:
simp [count_eq_countP]

Result:
no goals
-- Mathlib/Data/Int/Interval.lean
theorem card_fintype_Icc : Fintype.card (Set.Icc a b) = (b + 1 - a).toNat

Proof state:
a b : ℤ
⊢ Fintype.card ↑(Set.Icc a b) = (b + 1 - a).toNat

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
@[reassoc]
lemma triangle_aux₁ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε}
    (i₁ : X₁ ≅ Y₁) (i₂ : X₂ ≅ Y₂) (i₃ : X₃ ≅ Y₃) :
    ((i₁.hom ⊗ i₂.hom) ⊗ i₃.hom) ≫ (α_ Y₁ Y₂ Y₃).hom ≫ (i₁.inv ⊗ i₂.inv ⊗ i₃.inv) =
      (α_ X₁ X₂ X₃).hom

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
i₁ : X₁ ≅ Y₁
i₂ : X₂ ≅ Y₂
i₃ : X₃ ≅ Y₃
⊢ ((i₁.hom ⊗ i₂.hom) ⊗ i₃.hom) ≫ (α_ Y₁ Y₂ Y₃).hom ≫ (i₁.inv ⊗ i₂.inv ⊗ i₃.inv) = (α_ X₁ X₂ X₃).hom

Tactic:
simp only [associator_naturality_assoc, ← tensor_comp, Iso.hom_inv_id, id_tensorHom,
  whiskerLeft_id, comp_id]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem arctan_add {x y : ℝ} (h : x * y < 1) :
    arctan x + arctan y = arctan ((x + y) / (1 - x * y))

Proof state:
case hx₁
x y : ℝ
h : x * y < 1
⊢ -(π / 2) < arctan x + arctan y

Tactic:
rw [neg_lt, neg_add, ← arctan_neg, ← arctan_neg]

Result:
case hx₁
x y : ℝ
h : x * y < 1
⊢ arctan (-x) + arctan (-y) < π / 2

Proof state:
case hx₁
x y : ℝ
h : -x * -y < 1
⊢ arctan (-x) + arctan (-y) < π / 2

Tactic:
exact arctan_add_arctan_lt_pi_div_two h

Result:
no goals

Proof state:
case e_x
x y : ℝ
h : x * y < 1
⊢ tan (arctan x + arctan y) = (x + y) / (1 - x * y)

Tactic:
conv_rhs => rw [← tan_arctan x, ← tan_arctan y]

Result:
case e_x
x y : ℝ
h : x * y < 1
⊢ tan (arctan x + arctan y) = (tan (arctan x) + tan (arctan y)) / (1 - tan (arctan x) * tan (arctan y))

Proof state:
case e_x
x y : ℝ
h : x * y < 1
⊢ tan (arctan x + arctan y) = (tan (arctan x) + tan (arctan y)) / (1 - tan (arctan x) * tan (arctan y))

Tactic:
exact tan_add' ⟨arctan_ne_mul_pi_div_two, arctan_ne_mul_pi_div_two⟩

Result:
no goals

Proof state:
case hx₁
x y : ℝ
h : x * y < 1
⊢ arctan (-x) + arctan (-y) < π / 2

Tactic:
rw [← neg_mul_neg] at h

Result:
case hx₁
x y : ℝ
h : -x * -y < 1
⊢ arctan (-x) + arctan (-y) < π / 2

Proof state:
case hx₂
x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y < π / 2

Tactic:
exact arctan_add_arctan_lt_pi_div_two h

Result:
no goals

Proof state:
x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y))

Tactic:
rw [← arctan_tan (x := _ + _)]

Result:
x y : ℝ
h : x * y < 1
⊢ arctan (tan (arctan x + arctan y)) = arctan ((x + y) / (1 - x * y))

case hx₁
x y : ℝ
h : x * y < 1
⊢ -(π / 2) < arctan x + arctan y

case hx₂
x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y < π / 2

Proof state:
x y : ℝ
h : x * y < 1
⊢ arctan (tan (arctan x + arctan y)) = arctan ((x + y) / (1 - x * y))

Tactic:
congr

Result:
case e_x
x y : ℝ
h : x * y < 1
⊢ tan (arctan x + arctan y) = (x + y) / (1 - x * y)
-- Mathlib/.lake/packages/batteries/Batteries/Data/DList/Lemmas.lean
theorem toList_push (x : α) (l : DList α) : toList (push l x) = toList l ++ [x]

Proof state:
α : Type u_1
x : α
l : DList α
⊢ l.apply [x] = l.apply [] ++ [x]

Tactic:
rw [invariant]

Result:
no goals

Proof state:
α : Type u_1
x : α
l : DList α
⊢ (l.push x).toList = l.toList ++ [x]

Tactic:
simp only [toList, push]

Result:
α : Type u_1
x : α
l : DList α
⊢ l.apply [x] = l.apply [] ++ [x]
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesWithinAt.isBigO_sub_partialSum_pow
    (hf : HasFPowerSeriesWithinAt f p s x) (n : ℕ) :
    (fun y : E => f (x + y) - p.partialSum n y)
      =O[𝓝[(x + ·)⁻¹' insert x s] 0] fun y => ‖y‖ ^ n

Proof state:
case intro.intro.intro.intro.intro.intro.intro
𝕜 : 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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
a C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
⊢ ∀ᶠ (x_1 : E) in 𝓝[(fun x_1 => x + x_1) ⁻¹' insert x s] 0,
    ‖f (x + x_1) - p.partialSum n x_1‖ ≤ C * (a / ↑r') ^ n * ‖‖x_1‖ ^ n‖

Tactic:
replace r'0 : 0 < (r' : ℝ) := mod_cast r'0

Result:
case intro.intro.intro.intro.intro.intro.intro
𝕜 : 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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
h : ↑r' < r
a C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
r'0 : 0 < ↑r'
⊢ ∀ᶠ (x_1 : E) in 𝓝[(fun x_1 => x + x_1) ⁻¹' insert x s] 0,
    ‖f (x + x_1) - p.partialSum n x_1‖ ≤ C * (a / ↑r') ^ n * ‖‖x_1‖ ^ n‖
-- Mathlib/RingTheory/HopfAlgebra/MonoidAlgebra.lean
@[simp]
lemma antipode_single (g : G) (a : A) :
    antipode (R := R) (single g a) = single (-g) (antipode (R := R) a)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : HopfAlgebra R A
G : Type u_3
inst✝ : AddGroup G
g : G
a : A
⊢ antipode (single g a) = single (-g) (antipode a)

Tactic:
simp [AddMonoidAlgebra, antipode]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem conj_cpow_eq_ite (x : ℂ) (n : ℂ) :
    conj x ^ n = if x.arg = π then x ^ n else conj (x ^ conj n)

Proof state:
x n : ℂ
⊢ (starRingEnd ℂ) x ^ n = if x.arg = π then x ^ n else (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)

Tactic:
simp_rw [cpow_def, map_eq_zero, apply_ite conj, map_one, map_zero, ← exp_conj, map_mul, conj_conj,
  log_conj_eq_ite]

Result:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0 else cexp ((if x.arg = π then log x else (starRingEnd ℂ) (log x)) * n)) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n)
    else if x = 0 then if n = 0 then 1 else 0 else cexp ((starRingEnd ℂ) (log x) * n)

Proof state:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0 else cexp ((if x.arg = π then log x else (starRingEnd ℂ) (log x)) * n)) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n)
    else if x = 0 then if n = 0 then 1 else 0 else cexp ((starRingEnd ℂ) (log x) * n)

Tactic:
split_ifs with hcx hn hx <;> rfl

Result:
no goals
-- Mathlib/RingTheory/Coalgebra/Basic.lean
theorem counit_comp_lsingle (i : ι) : counit ∘ₗ (lsingle i : A i →ₗ[R] _) = counit

Proof state:
case h
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i : ι
x✝ : A i
⊢ (counit ∘ₗ lsingle i) x✝ = counit x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i : ι
⊢ counit ∘ₗ lsingle i = counit

Tactic:
ext

Result:
case h
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i : ι
x✝ : A i
⊢ (counit ∘ₗ lsingle i) x✝ = counit x✝
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem set_mul_normal_comm (s : Set G) (N : Subgroup G) [hN : N.Normal] :
    s * (N : Set G) = (N : Set G) * s

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
N : Subgroup G
hN : N.Normal
⊢ s * ↑N = ↑N * s

Tactic:
rw [← iUnion_mul_left_image, ← iUnion_mul_right_image]

Result:
G : Type u_2
inst✝ : Group G
s : Set G
N : Subgroup G
hN : N.Normal
⊢ ⋃ a ∈ s, (fun x => a * x) '' ↑N = ⋃ a ∈ s, (fun x => x * a) '' ↑N

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
N : Subgroup G
hN : N.Normal
⊢ ⋃ a ∈ s, (fun x => a * x) '' ↑N = ⋃ a ∈ s, (fun x => x * a) '' ↑N

Tactic:
simp only [image_mul_left, image_mul_right, Set.preimage, SetLike.mem_coe, hN.mem_comm_iff]

Result:
no goals