harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/EulerProduct/Basic.lean
/-- Given a (completely) multiplicative function `f : ℕ → F`, where `F` is a normed field,
such that `‖f p‖ < 1` for all primes `p`, we can express the sum of `f n` over all `N`-smooth
positive integers `n` as a product of `(1 - f p)⁻¹` over the primes `p < N`. At the same time,
we show that the sum involved converges absolutely. -/
lemma summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric {f : ℕ →* F}
    (h : ∀ {p : ℕ}, p.Prime → ‖f p‖ < 1) (N : ℕ) :
    Summable (fun m : N.smoothNumbers ↦ ‖f m‖) ∧
      HasSum (fun m : N.smoothNumbers ↦ f m) (∏ p ∈ N.primesBelow, (1 - f p)⁻¹)

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
N : ℕ
⊢ (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) (range N), (1 - f p)⁻¹)

Tactic:
exact summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric h _

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
N : ℕ
⊢ (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ N.primesBelow, (1 - f p)⁻¹)

Tactic:
rw [smoothNumbers_eq_factoredNumbers, primesBelow]

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
N : ℕ
⊢ (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) (range N), (1 - f p)⁻¹)
-- Mathlib/Order/Filter/Basic.lean
theorem mem_biInf_of_directed {f : β → Filter α} {s : Set β} (h : DirectedOn (f ⁻¹'o (· ≥ ·)) s)
    (ne : s.Nonempty) {t : Set α} : (t ∈ ⨅ i ∈ s, f i) ↔ ∃ i ∈ s, t ∈ f i

Proof state:
α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun x1 x2 => x1 ≥ x2) s
ne : s.Nonempty
t : Set α
this : Nonempty ↑s
⊢ t ∈ ⨅ i ∈ s, f i ↔ ∃ i ∈ s, t ∈ f i

Tactic:
simp_rw [iInf_subtype', mem_iInf_of_directed h.directed_val, Subtype.exists, exists_prop]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun x1 x2 => x1 ≥ x2) s
ne : s.Nonempty
t : Set α
⊢ t ∈ ⨅ i ∈ s, f i ↔ ∃ i ∈ s, t ∈ f i

Tactic:
haveI := ne.to_subtype

Result:
α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun x1 x2 => x1 ≥ x2) s
ne : s.Nonempty
t : Set α
this : Nonempty ↑s
⊢ t ∈ ⨅ i ∈ s, f i ↔ ∃ i ∈ s, t ∈ f i
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem differentiableWithinAt_comp_sub (a : E) :
    DifferentiableWithinAt 𝕜 (fun x ↦ f (x - a)) s x ↔
      DifferentiableWithinAt 𝕜 f (-a +ᵥ s) (x - a)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
a : E
⊢ DifferentiableWithinAt 𝕜 (fun x => f (x - a)) s x ↔ DifferentiableWithinAt 𝕜 f (-a +ᵥ s) (x - a)

Tactic:
simp [DifferentiableWithinAt, hasFDerivWithinAt_comp_sub]

Result:
no goals
-- Mathlib/Data/Finset/Disjoint.lean
theorem disjoint_singleton : Disjoint ({a} : Finset α) {b} ↔ a ≠ b

Proof state:
α : Type u_1
a b : α
⊢ Disjoint {a} {b} ↔ a ≠ b

Tactic:
rw [disjoint_singleton_left, mem_singleton]

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/GaussSum.lean
/-- If `gaussSum χ e ≠ 0`, and `d` is such that `e.mulShift d = 1`, then `χ` must factor through
`d`. (This will be used to show that Gauss sums vanish when `χ` is primitive and `e` is not.) -/
lemma factorsThrough_of_gaussSum_ne_zero [IsDomain R] {χ : DirichletCharacter R N} {d : ℕ}
    (hd : d ∣ N) (he : e.mulShift d = 1) (h_ne : gaussSum χ e ≠ 0) :
    χ.FactorsThrough d

Proof state:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
⊢ χ.FactorsThrough d

Tactic:
rw [DirichletCharacter.factorsThrough_iff_ker_unitsMap hd]

Result:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
⊢ (ZMod.unitsMap hd).ker ≤ (MulChar.toUnitHom χ).ker

Proof state:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
u : (ZMod N)ˣ
hu : u ∈ (ZMod.unitsMap hd).ker
⊢ χ ↑u = ↑1

Tactic:
simpa only [Units.val_one, ne_eq, h_ne, not_false_eq_true, mul_eq_right₀] using
  gaussSum_aux_of_mulShift e χ hd he hu

Result:
no goals

Proof state:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
⊢ (ZMod.unitsMap hd).ker ≤ (MulChar.toUnitHom χ).ker

Tactic:
intro u hu

Result:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
u : (ZMod N)ˣ
hu : u ∈ (ZMod.unitsMap hd).ker
⊢ u ∈ (MulChar.toUnitHom χ).ker

Proof state:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
u : (ZMod N)ˣ
hu : u ∈ (ZMod.unitsMap hd).ker
⊢ u ∈ (MulChar.toUnitHom χ).ker

Tactic:
rw [MonoidHom.mem_ker, ← Units.eq_iff, MulChar.coe_toUnitHom]

Result:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
u : (ZMod N)ˣ
hu : u ∈ (ZMod.unitsMap hd).ker
⊢ χ ↑u = ↑1
-- Mathlib/Order/Fin/Tuple.lean
lemma liftFun_vecCons {n : ℕ} (r : α → α → Prop) [IsTrans α r] {f : Fin (n + 1) → α} {a : α} :
    ((· < ·) ⇒ r) (vecCons a f) (vecCons a f) ↔ r a (f 0) ∧ ((· < ·) ⇒ r) f f

Proof state:
α : Type u_1
n : ℕ
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
a : α
⊢ ((fun x1 x2 => x1 < x2) ⇒ r) (vecCons a f) (vecCons a f) ↔ r a (f 0) ∧ ((fun x1 x2 => x1 < x2) ⇒ r) f f

Tactic:
simp only [liftFun_iff_succ r, forall_iff_succ, cons_val_succ, cons_val_zero, ← succ_castSucc,
  castSucc_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/RankNullity.lean
theorem LinearMap.rank_eq_of_surjective {f : M →ₗ[R] M₁} (h : Surjective f) :
    Module.rank R M = Module.rank R M₁ + Module.rank R (LinearMap.ker f)

Proof state:
R : Type u_1
M M₁ : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M₁
h : Surjective ⇑f
⊢ Module.rank R M = Module.rank R M₁ + Module.rank R ↥(ker f)

Tactic:
rw [← rank_range_add_rank_ker f, ← rank_range_of_surjective f h]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem offDiag_eq_empty : s.offDiag = ∅ ↔ s.Subsingleton

Proof state:
α : Type u_1
s : Set α
⊢ s.offDiag = ∅ ↔ s.Subsingleton

Tactic:
rw [← not_nonempty_iff_eq_empty, ← not_nontrivial_iff, offDiag_nonempty.not]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem toSubmodule_eq_bot : (N : Submodule R M) = ⊥ ↔ N = ⊥

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ ↑N = ⊥ ↔ N = ⊥

Tactic:
rw [← toSubmodule_inj, bot_toSubmodule]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem foldRev_eq {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
    l.foldRev f init = l.buckets.foldr (fun l acc => l.foldr (fun a b g => f g a b) acc) init

Proof state:
α : Type u
β : α → Type v
γ : Type w
l : Raw α β
f : γ → (a : α) → β a → γ
init : γ
⊢ Raw.foldRev f init l = Array.foldr (fun l acc => AssocList.foldr (fun a b g => f g a b) acc l) init l.buckets

Tactic:
simp only [Raw.foldRev, Raw.foldRevM, ← Array.foldrM_toList, Array.foldr_toList,
  ← List.foldr_eq_foldrM, Id.run, AssocList.foldr]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem sub_conj (z : ℂ) : z - conj z = (2 * z.im : ℝ) * I :=
  Complex.ext_iff.2 <| by simp [two_mul, sub_eq_add_neg, ofReal]

Proof state:
z : ℂ
⊢ (z - (starRingEnd ℂ) z).re = (↑(2 * z.im) * I).re ∧ (z - (starRingEnd ℂ) z).im = (↑(2 * z.im) * I).im

Tactic:
simp [two_mul, sub_eq_add_neg, ofReal]

Result:
no goals
-- Mathlib/FieldTheory/LinearDisjoint.lean
theorem finrank_sup (H : A.LinearDisjoint B) : finrank F ↥(A ⊔ B) = finrank F A * finrank F B

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
H : A.LinearDisjoint ↥B
⊢ finrank F ↥(A ⊔ B) = finrank F ↥A * finrank F ↥B

Tactic:
simpa only [map_mul] using congr(Cardinal.toNat $(H.rank_sup))

Result:
no goals
-- Mathlib/Order/Heyting/Boundary.lean
theorem hnot_boundary (a : α) : ￢∂ a = ⊤

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢∂ a = ⊤

Tactic:
rw [boundary, hnot_inf_distrib, sup_hnot_self]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma lt_sub_iff_add_lt' : a < c - b ↔ b + a < c

Proof state:
a b c : ℕ
⊢ a < c - b ↔ b + a < c

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_of_injective (e : ι → κ) (he : Injective e) (f : ι → α) (g : κ → α)
    (h' : ∀ i ∉ Set.range e, g i = 1) (h : ∀ i, f i = g (e i)) : ∏ i, f i = ∏ j, g j :=
  prod_of_injOn e he.injOn (by simp) (by simpa using h') (fun i _ ↦ h i)

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝² : Fintype ι
inst✝¹ : Fintype κ
inst✝ : CommMonoid α
e : ι → κ
he : Injective e
f : ι → α
g : κ → α
h' : ∀ i ∉ Set.range e, g i = 1
h : ∀ (i : ι), f i = g (e i)
⊢ ∀ i ∈ univ, i ∉ e '' ↑univ → g i = 1

Tactic:
simpa using h'

Result:
no goals

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝² : Fintype ι
inst✝¹ : Fintype κ
inst✝ : CommMonoid α
e : ι → κ
he : Injective e
f : ι → α
g : κ → α
h' : ∀ i ∉ Set.range e, g i = 1
h : ∀ (i : ι), f i = g (e i)
⊢ Set.MapsTo e ↑univ ↑univ

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem finrank_finsupp_self {ι : Type v} [Fintype ι] : finrank R (ι →₀ R) = card ι

Proof state:
R : Type u
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
ι : Type v
inst✝ : Fintype ι
⊢ finrank R (ι →₀ R) = card ι

Tactic:
rw [finrank, rank_finsupp_self, ← mk_toNat_eq_card, toNat_lift]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallyBijective.lean
lemma W_iff_isLocallyBijective :
    J.W f ↔ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : J.WEqualsLocallyBijective A
X Y : Cᵒᵖ ⥤ A
f : X ⟶ Y
⊢ J.W f ↔ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f

Tactic:
apply WEqualsLocallyBijective.iff

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem one_mul (x : BitVec w) : 1#w * x = x

Proof state:
w : Nat
x : BitVec w
⊢ 1#w * x = x

Tactic:
rw [BitVec.mul_comm, BitVec.mul_one]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
lemma single_tmul {ι : Type*} [DecidableEq ι] {M : ι → Type*} [∀ i, AddCommMonoid (M i)]
    [∀ i, Module R (M i)] (i : ι) (x : N) (m : M i) (j : ι) :
    Pi.single i m j ⊗ₜ[R] x = (Pi.single i (m ⊗ₜ[R] x) : ∀ i, M i ⊗[R] N) j

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_6
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_11
inst✝² : DecidableEq ι
M : ι → Type u_12
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
⊢ Pi.single i m j ⊗ₜ[R] x = Pi.single i (m ⊗ₜ[R] x) j

Tactic:
by_cases h : i = j <;> aesop

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem map_le_map_iff_of_injective {f : G →* N} (hf : Function.Injective f) {H K : Subgroup G} :
    H.map f ≤ K.map f ↔ H ≤ K

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
⊢ map f H ≤ map f K ↔ H ≤ K

Tactic:
rw [map_le_iff_le_comap, comap_map_eq_self_of_injective hf]

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem minpoly_powerBasis_gen_of_monic (hf : f.Monic) (hf' : f ≠ 0 := hf.ne_zero) :
    minpoly K (powerBasis hf').gen = f

Proof state:
K : Type w
inst✝ : Field K
f : K[X]
hf : f.Monic
hf' : optParam (f ≠ 0) ⋯
⊢ minpoly K (powerBasis hf').gen = f

Tactic:
rw [minpoly_powerBasis_gen hf', hf.leadingCoeff, inv_one, C.map_one, mul_one]

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
lemma wInner_const_left (a : 𝕜) (f : ι → 𝕜) :
    ⟪const _ a, f⟫_[𝕜, w] = conj a * ∑ i, w i • f i

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
w : ι → ℝ
a : 𝕜
f : ι → 𝕜
⊢ wInner w (const ι a) f = (starRingEnd 𝕜) a * ∑ i : ι, w i • f i

Tactic:
simp [wInner, const_apply, mul_sum]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_eq_pi_div_two_sub_arccos (x : ℝ) : arcsin x = π / 2 - arccos x

Proof state:
x : ℝ
⊢ arcsin x = π / 2 - arccos x

Tactic:
simp [arccos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatten_flatten {L : List (List (List α))} : flatten (flatten L) = flatten (map flatten L)

Proof state:
α : Type u_1
L : List (List (List α))
⊢ L.flatten.flatten = (map flatten L).flatten

Tactic:
induction L <;> simp_all

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem prod_inf_prod {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} :
    (f₁ ×ˢ g₁) ⊓ (f₂ ×ˢ g₂) = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂)

Proof state:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
⊢ f₁ ×ˢ g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂)

Tactic:
simp only [prod_eq_inf, comap_inf, inf_comm, inf_assoc, inf_left_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem inv_whiskerLeft (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) [IsIso η] :
    inv (f ◁ η) = f ◁ inv η

Proof state:
case hom_inv_id
B : Type u
inst✝¹ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
inst✝ : IsIso η
⊢ f ◁ η ≫ f ◁ inv η = 𝟙 (f ≫ g)

Tactic:
simp only [← whiskerLeft_comp, whiskerLeft_id, IsIso.hom_inv_id]

Result:
no goals

Proof state:
B : Type u
inst✝¹ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
inst✝ : IsIso η
⊢ inv (f ◁ η) = f ◁ inv η

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Result:
case hom_inv_id
B : Type u
inst✝¹ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
inst✝ : IsIso η
⊢ f ◁ η ≫ f ◁ inv η = 𝟙 (f ≫ g)
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ico_diff_Ioo_same (h : a < b) : Ico a b \ Ioo a b = {a}

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a < b
⊢ Ico a b \ Ioo a b = {a}

Tactic:
rw [← Ico_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 <| left_mem_Ico.2 h)]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Opposite.lean
lemma oppositeShiftFunctorZero_hom_app (X : OppositeShift C A) :
    (shiftFunctorZero (OppositeShift C A) A).hom.app X =
      ((shiftFunctorZero C A).inv.app X.unop).op

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
⊢ 𝟙 ((shiftFunctor (OppositeShift C A) 0).obj X) = 𝟙 (Opposite.op ((shiftFunctor C 0).obj (Opposite.unop X)))

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
⊢ (shiftFunctorZero (OppositeShift C A) A).hom.app X = ((shiftFunctorZero C A).inv.app (Opposite.unop X)).op

Tactic:
rw [← cancel_mono ((shiftFunctorZero (OppositeShift C A) A).inv.app X),
  Iso.hom_inv_id_app, oppositeShiftFunctorZero_inv_app, ← op_comp,
  Iso.hom_inv_id_app, op_id]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
⊢ 𝟙 ((shiftFunctor (OppositeShift C A) 0).obj X) = 𝟙 (Opposite.op ((shiftFunctor C 0).obj (Opposite.unop X)))
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem not_squarefree_zero [MonoidWithZero R] [Nontrivial R] : ¬Squarefree (0 : R)

Proof state:
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ ¬(0 * 0 ∣ 0 → IsUnit 0)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ ¬Squarefree 0

Tactic:
erw [not_forall]

Result:
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ ∃ x, ¬(x * x ∣ 0 → IsUnit x)

Proof state:
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ ∃ x, ¬(x * x ∣ 0 → IsUnit x)

Tactic:
exact ⟨0, by simp⟩

Result:
no goals
-- Mathlib/Analysis/Convex/EGauge.lean
lemma egauge_lt_iff : egauge 𝕜 s x < r ↔ ∃ c : 𝕜, x ∈ c • s ∧ ‖c‖ₑ < r

Proof state:
𝕜 : Type u_1
inst✝¹ : NNNorm 𝕜
E : Type u_2
inst✝ : SMul 𝕜 E
s : Set E
x : E
r : ℝ≥0∞
⊢ egauge 𝕜 s x < r ↔ ∃ c, x ∈ c • s ∧ ‖c‖ₑ < r

Tactic:
simp [egauge, iInf_lt_iff]

Result:
no goals
-- Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean
theorem Ideal.minimalPrimes_eq_subsingleton (hI : I.IsPrimary) : I.minimalPrimes = {I.radical}

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ I.minimalPrimes ↔ J ∈ {I.radical}

Tactic:
constructor

Result:
case h.mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ I.minimalPrimes → J ∈ {I.radical}

case h.mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ {I.radical} → J ∈ I.minimalPrimes

Proof state:
case h.mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : I.IsPrimary
⊢ I.radical ∈ I.minimalPrimes

Tactic:
exact ⟨⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩, fun _ H _ => H.1.radical_le_iff.mpr H.2⟩

Result:
no goals

Proof state:
case h.mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ {I.radical} → J ∈ I.minimalPrimes

Tactic:
rintro (rfl : J = I.radical)

Result:
case h.mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : I.IsPrimary
⊢ I.radical ∈ I.minimalPrimes

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : I.IsPrimary
⊢ I.minimalPrimes = {I.radical}

Tactic:
ext J

Result:
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ I.minimalPrimes ↔ J ∈ {I.radical}

Proof state:
case h.mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ I.minimalPrimes → J ∈ {I.radical}

Tactic:
exact fun H =>
  let e := H.1.1.radical_le_iff.mpr H.1.2
  (H.2 ⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩ e).antisymm e

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isSuffix_map_iff {β} {f : α → β} {l₁ : List α} {l₂ : List β} :
    l₂ <:+ l₁.map f ↔ ∃ l, l <:+ l₁ ∧ l₂ = l.map f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l₁ : List α
l₂ : List β
⊢ l₂ <:+ map f l₁ ↔ ∃ l, l <:+ l₁ ∧ l₂ = map f l

Tactic:
rw [← filterMap_eq_map, isSuffix_filterMap_iff]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma InjOn.of_comp (h : InjOn (g ∘ f) s) : InjOn f s :=
  fun _ hx _ hy heq ↦ h hx hy (by simp [heq])

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
f : α → β
g : β → γ
h : InjOn (g ∘ f) s
x✝¹ : α
hx : x✝¹ ∈ s
x✝ : α
hy : x✝ ∈ s
heq : f x✝¹ = f x✝
⊢ (g ∘ f) x✝¹ = (g ∘ f) x✝

Tactic:
simp [heq]

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
lemma wInner_add_left (w : ι → ℝ) (f₁ f₂ g : ∀ i, E i) :
    ⟪f₁ + f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] + ⟪f₂, g⟫_[𝕜, w]

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
w : ι → ℝ
f₁ f₂ g : (i : ι) → E i
⊢ wInner w (f₁ + f₂) g = wInner w f₁ g + wInner w f₂ g

Tactic:
simp [wInner, inner_add_left, smul_add, sum_add_distrib]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem expand_expand (f : R[X]) : expand R p (expand R q f) = expand R (p * q) f :=
  Polynomial.induction_on f (fun r => by simp_rw [expand_C])
    (fun f g ihf ihg => by simp_rw [map_add, ihf, ihg]) fun n r _ => by
    simp_rw [map_mul, expand_C, map_pow, expand_X, map_pow, expand_X, pow_mul]

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
r : R
⊢ (expand R p) ((expand R q) (C r)) = (expand R (p * q)) (C r)

Tactic:
simp_rw [expand_C]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : (expand R p) ((expand R q) (C r * X ^ n)) = (expand R (p * q)) (C r * X ^ n)
⊢ (expand R p) ((expand R q) (C r * X ^ (n + 1))) = (expand R (p * q)) (C r * X ^ (n + 1))

Tactic:
simp_rw [map_mul, expand_C, map_pow, expand_X, map_pow, expand_X, pow_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
f✝ f g : R[X]
ihf : (expand R p) ((expand R q) f) = (expand R (p * q)) f
ihg : (expand R p) ((expand R q) g) = (expand R (p * q)) g
⊢ (expand R p) ((expand R q) (f + g)) = (expand R (p * q)) (f + g)

Tactic:
simp_rw [map_add, ihf, ihg]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean
theorem prod_singleton (a : α) : prod {a} = a

Proof state:
α : Type u_3
inst✝ : CommMonoid α
a : α
⊢ {a}.prod = a

Tactic:
simp only [mul_one, prod_cons, ← cons_zero, eq_self_iff_true, prod_zero]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem isPreconnected_preimage {s : Set Y} (h : X ≃ₜ Y) :
    IsPreconnected (h ⁻¹' s) ↔ IsPreconnected s

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

Tactic:
rw [← image_symm, isPreconnected_image]

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
lemma lt_card_toFinset_of_nth_ne_zero {n : ℕ} (h : nth p n ≠ 0) (hf : (setOf p).Finite) :
    n < #hf.toFinset

Proof state:
p : ℕ → Prop
n : ℕ
h : nth p n ≠ 0
hf : (setOf p).Finite
⊢ n < #hf.toFinset

Tactic:
simp only [ne_eq, nth_eq_zero, not_or, not_exists, not_le] at h

Result:
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
h : ¬(p 0 ∧ n = 0) ∧ ∀ (x : (setOf p).Finite), n < #x.toFinset
⊢ n < #hf.toFinset

Proof state:
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
h : ¬(p 0 ∧ n = 0) ∧ ∀ (x : (setOf p).Finite), n < #x.toFinset
⊢ n < #hf.toFinset

Tactic:
exact h.2 hf

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem IsRegular.cof_omega_eq {o : Ordinal} (H : (ℵ_ o).IsRegular) : (ω_ o).cof = ℵ_ o

Proof state:
o : Ordinal.{u_1}
H : (ℵ_ o).IsRegular
⊢ (ω_ o).cof = ℵ_ o

Tactic:
rw [← ord_aleph, H.cof_eq]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem of_diff {M : Type*} [AddCommGroup M] [TopologicalSpace M] [T2Space M]
    {v : VectorMeasure α M} {A B : Set α} (hA : MeasurableSet A) (hB : MeasurableSet B)
    (h : A ⊆ B) : v (B \ A) = v B - v A

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h : A ⊆ B
⊢ ↑v (B \ A) = ↑v B - ↑v A

Tactic:
rw [← of_add_of_diff hA hB h, add_sub_cancel_left]

Result:
no goals
-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem stereographic_neg_apply (v : sphere (0 : E) 1) :
    stereographic (norm_eq_of_mem_sphere (-v)) v = 0

Proof state:
case h.e'_2.h.e'_6.a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : ↑(sphere 0 1)
⊢ ↑v = ↑(- -v)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2.h.e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : ↑(sphere 0 1)
⊢ v = - -v

Tactic:
ext1

Result:
case h.e'_2.h.e'_6.a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : ↑(sphere 0 1)
⊢ ↑v = ↑(- -v)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : ↑(sphere 0 1)
⊢ ↑(stereographic ⋯) v = 0

Tactic:
convert stereographic_apply_neg (-v)

Result:
case h.e'_2.h.e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : ↑(sphere 0 1)
⊢ v = - -v