harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Shift/Basic.lean
@[reassoc]
lemma shiftFunctorAdd_assoc_inv_app (a₁ a₂ a₃ : A) (X : C) :
    ((shiftFunctorAdd C a₁ a₂).inv.app X)⟦a₃⟧' ≫
      (shiftFunctorAdd C (a₁ + a₂) a₃).inv.app X =
    (shiftFunctorAdd C a₂ a₃).inv.app (X⟦a₁⟧) ≫
      (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (add_assoc _ _ _).symm).inv.app X

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).inv.app X) ≫ (shiftFunctorAdd C (a₁ + a₂) a₃).inv.app X =
    (shiftFunctorAdd C a₂ a₃).inv.app ((shiftFunctor C a₁).obj X) ≫
      (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).inv.app X

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.inv (shiftFunctorAdd_assoc C a₁ a₂ a₃)) X

Result:
no goals
-- Mathlib/Tactic/ComputeDegree.lean
theorem degree_eq_of_le_of_coeff_ne_zero' {deg m o : WithBot ℕ} {c : R} {p : R[X]}
    (h_deg_le : degree p ≤ m) (coeff_eq : coeff p (WithBot.unbotD 0 deg) = c)
    (coeff_ne_zero : c ≠ 0) (deg_eq_deg : m = deg) (coeff_eq_deg : o = deg) :
    degree p = deg

Proof state:
case inl
R : Type u_1
inst✝ : Semiring R
p : R[X]
h_deg_le : p.degree ≤ ⊥
coeff_ne_zero : p.coeff (WithBot.unbotD 0 ⊥) ≠ 0
⊢ p.degree = ⊥

Tactic:
exact bot_unique h_deg_le

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝ : Semiring R
m : WithBot ℕ
p : R[X]
h_deg_le : p.degree ≤ m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 m) ≠ 0
hh : m ≠ ⊥
⊢ p.degree = m

Tactic:
obtain ⟨m, rfl⟩ := WithBot.ne_bot_iff_exists.mp hh

Result:
case inr.intro
R : Type u_1
inst✝ : Semiring R
p : R[X]
m : ℕ
h_deg_le : p.degree ≤ ↑m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 ↑m) ≠ 0
hh : ↑m ≠ ⊥
⊢ p.degree = ↑m

Proof state:
case inr.intro
R : Type u_1
inst✝ : Semiring R
p : R[X]
m : ℕ
h_deg_le : p.degree ≤ ↑m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 ↑m) ≠ 0
hh : ↑m ≠ ⊥
⊢ p.degree = ↑m

Tactic:
exact degree_eq_of_le_of_coeff_ne_zero ‹_› ‹_›

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
m : WithBot ℕ
p : R[X]
h_deg_le : p.degree ≤ m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 m) ≠ 0
⊢ p.degree = m

Tactic:
rcases eq_or_ne m ⊥ with rfl|hh

Result:
case inl
R : Type u_1
inst✝ : Semiring R
p : R[X]
h_deg_le : p.degree ≤ ⊥
coeff_ne_zero : p.coeff (WithBot.unbotD 0 ⊥) ≠ 0
⊢ p.degree = ⊥

case inr
R : Type u_1
inst✝ : Semiring R
m : WithBot ℕ
p : R[X]
h_deg_le : p.degree ≤ m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 m) ≠ 0
hh : m ≠ ⊥
⊢ p.degree = m

Proof state:
R : Type u_1
inst✝ : Semiring R
deg m o : WithBot ℕ
c : R
p : R[X]
h_deg_le : p.degree ≤ m
coeff_eq : p.coeff (WithBot.unbotD 0 deg) = c
coeff_ne_zero : c ≠ 0
deg_eq_deg : m = deg
coeff_eq_deg : o = deg
⊢ p.degree = deg

Tactic:
subst coeff_eq coeff_eq_deg deg_eq_deg

Result:
R : Type u_1
inst✝ : Semiring R
m : WithBot ℕ
p : R[X]
h_deg_le : p.degree ≤ m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 m) ≠ 0
⊢ p.degree = m
-- Mathlib/NumberTheory/Pell.lean
theorem mul_inv_y_nonneg {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : 1 < a.x)
    (hay : 0 < a.y) : 0 ≤ (a * a₁⁻¹).y

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ 0 ≤ (a * a₁⁻¹).y

Tactic:
simpa only [y_inv, mul_neg, y_mul, le_neg_add_iff_add_le, add_zero] using
  h.x_mul_y_le_y_mul_x hax hay

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
lemma nontrivial_of_ediam_ne_zero (h : G.ediam ≠ 0) : Nontrivial α

Proof state:
α : Type u_1
G : SimpleGraph α
h : ¬Nontrivial α
⊢ G.ediam = 0

Tactic:
rw [not_nontrivial_iff_subsingleton] at h

Result:
α : Type u_1
G : SimpleGraph α
h : Subsingleton α
⊢ G.ediam = 0

Proof state:
α : Type u_1
G : SimpleGraph α
h : G.ediam ≠ 0
⊢ Nontrivial α

Tactic:
contrapose! h

Result:
α : Type u_1
G : SimpleGraph α
h : ¬Nontrivial α
⊢ G.ediam = 0

Proof state:
α : Type u_1
G : SimpleGraph α
h : Subsingleton α
⊢ G.ediam = 0

Tactic:
exact ediam_eq_zero_of_subsingleton

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_empty {a : α} {c : Nat} : (empty c : Raw₀ α β).contains a = false

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
c : Nat
⊢ (empty c).contains a = false

Tactic:
simp [contains]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem coordinate_eval_1 : (coordinate 1).eval (.ofList (a0 :: a1 :: t)) = a1

Proof state:
a0 a1 : Int
t : List Int
⊢ (coordinate 1).eval (Coeffs.ofList (a0 :: a1 :: t)) = a1

Tactic:
simp

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem Ici_iSup (f : ι → α) : Ici (⨆ i, f i) = ⨆ i, Ici (f i) :=
  SetLike.ext fun c => by simp only [mem_Ici_iff, mem_iSup_iff, iSup_le_iff]

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
c : α
⊢ c ∈ Ici (⨆ i, f i) ↔ c ∈ ⨆ i, Ici (f i)

Tactic:
simp only [mem_Ici_iff, mem_iSup_iff, iSup_le_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/WithTop.lean
lemma coe_mul_eq_bind {a : α} (ha : a ≠ 0) : ∀ b, (a * b : WithTop α) = b.bind fun b ↦ ↑(a * b)
  | ⊤ => by simp [top_mul, ha]; rfl
  | (b : α) => rfl

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : α
ha : a ≠ 0
⊢ ⊤ = Option.bind ⊤ fun b => Option.some (a * b)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : α
ha : a ≠ 0
⊢ ↑a * ⊤ = Option.bind ⊤ fun b => Option.some (a * b)

Tactic:
simp [top_mul, ha]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : α
ha : a ≠ 0
⊢ ⊤ = Option.bind ⊤ fun b => Option.some (a * b)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem choice_isSome_iff_nonempty {α : Type _} : (choice α).isSome ↔ Nonempty α :=
  ⟨fun h => ⟨(choice α).get h⟩, fun h => by simp only [choice, dif_pos h, isSome_some]⟩

Proof state:
α : Type u_1
h : Nonempty α
⊢ (choice α).isSome = true

Tactic:
simp only [choice, dif_pos h, isSome_some]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
@[simp]
lemma coeff_Ψ₂Sq : W.Ψ₂Sq.coeff 3 = 4

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆).coeff 3 = 4

Tactic:
compute_degree!

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Ψ₂Sq.coeff 3 = 4

Tactic:
rw [Ψ₂Sq]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆).coeff 3 = 4
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
lemma map_polynomialZ :
    (W'.map f).toProjective.polynomialZ = MvPolynomial.map f W'.polynomialZ

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ (map W' f).toProjective.polynomialZ = (MvPolynomial.map f) W'.polynomialZ

Tactic:
simp only [polynomialZ, map_polynomial, pderiv_map]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean
@[reassoc (attr := simp)]
lemma whiskerLeft_app_fst (F₁ : J ⥤ C) {F₂ F₂' : J ⥤ C} (g : F₂ ⟶ F₂') (j : J) :
    (F₁ ◁ g).app j ≫ fst _ _ = fst _ _ :=
  (tensorHom_app_fst (𝟙 F₁) g j).trans (by simp)

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₂' : J ⥤ C
g : F₂ ⟶ F₂'
j : J
⊢ fst (F₁.obj j) (F₂.obj j) ≫ (𝟙 F₁).app j = fst (F₁.obj j) (F₂.obj j)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive] lemma inv_mabs_le_inv (a : α) : |a|ₘ⁻¹ ≤ a⁻¹

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ (mabs a)⁻¹ ≤ a⁻¹

Tactic:
simpa using inv_mabs_le a⁻¹

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem ite_inter_closure_compl_eq_of_inter_frontier_eq
    (ht : s ∩ frontier t = s' ∩ frontier t) : t.ite s s' ∩ closure tᶜ = s' ∩ closure tᶜ

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ t.ite s s' ∩ closure tᶜ = s' ∩ closure tᶜ

Tactic:
rw [← ite_compl, ite_inter_closure_eq_of_inter_frontier_eq]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ s' ∩ frontier tᶜ = s ∩ frontier tᶜ

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ s' ∩ frontier tᶜ = s ∩ frontier tᶜ

Tactic:
rwa [frontier_compl, eq_comm]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive (attr := simp) smul_dite]
lemma dite_pow (p : Prop) [Decidable p] (a : p → α) (b : ¬ p → α) (c : β) :
    (if h : p then a h else b h) ^ c = if h : p then a h ^ c else b h ^ c

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
c : β
⊢ (if h : p then a h else b h) ^ c = if h : p then a h ^ c else b h ^ c

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem orderTop_add_eq_right {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R}
    (hxy : y.orderTop < x.orderTop) : (x + y).orderTop = y.orderTop

Proof state:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : y.orderTop < x.orderTop
⊢ (x + y).orderTop = y.orderTop

Tactic:
simpa [← map_add, ← AddOpposite.op_add, hxy] using orderTop_add_eq_left
  (x := addOppositeEquiv.symm (.op y))
  (y := addOppositeEquiv.symm (.op x))

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem gcd_mul_right (i j k : ℤ) : gcd (i * j) (k * j) = gcd i k * natAbs j

Proof state:
i j k : ℤ
⊢ (i * j).gcd (k * j) = i.gcd k * j.natAbs

Tactic:
rw [Int.gcd, Int.gcd, natAbs_mul, natAbs_mul]

Result:
i j k : ℤ
⊢ (i.natAbs * j.natAbs).gcd (k.natAbs * j.natAbs) = i.natAbs.gcd k.natAbs * j.natAbs

Proof state:
i j k : ℤ
⊢ (i.natAbs * j.natAbs).gcd (k.natAbs * j.natAbs) = i.natAbs.gcd k.natAbs * j.natAbs

Tactic:
apply Nat.gcd_mul_right

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem _root_.quasispectrum.isCompact (a : B) : IsCompact (quasispectrum 𝕜 a)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NormedField 𝕜
B : Type u_3
inst✝⁵ : NonUnitalNormedRing B
inst✝⁴ : NormedSpace 𝕜 B
inst✝³ : CompleteSpace B
inst✝² : IsScalarTower 𝕜 B B
inst✝¹ : SMulCommClass 𝕜 B B
inst✝ : ProperSpace 𝕜
a : B
⊢ IsCompact (quasispectrum 𝕜 a)

Tactic:
rw [Unitization.quasispectrum_eq_spectrum_inr' 𝕜 𝕜,
  ← AlgEquiv.spectrum_eq (WithLp.unitizationAlgEquiv 𝕜).symm (a : Unitization 𝕜 B)]

Result:
𝕜 : Type u_1
inst✝⁶ : NormedField 𝕜
B : Type u_3
inst✝⁵ : NonUnitalNormedRing B
inst✝⁴ : NormedSpace 𝕜 B
inst✝³ : CompleteSpace B
inst✝² : IsScalarTower 𝕜 B B
inst✝¹ : SMulCommClass 𝕜 B B
inst✝ : ProperSpace 𝕜
a : B
⊢ IsCompact (σ ((WithLp.unitizationAlgEquiv 𝕜).symm ↑a))

Proof state:
𝕜 : Type u_1
inst✝⁶ : NormedField 𝕜
B : Type u_3
inst✝⁵ : NonUnitalNormedRing B
inst✝⁴ : NormedSpace 𝕜 B
inst✝³ : CompleteSpace B
inst✝² : IsScalarTower 𝕜 B B
inst✝¹ : SMulCommClass 𝕜 B B
inst✝ : ProperSpace 𝕜
a : B
⊢ IsCompact (σ ((WithLp.unitizationAlgEquiv 𝕜).symm ↑a))

Tactic:
exact spectrum.isCompact _

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem adjoin_image (f : A →ₐ[R] B) (s : Set A) : adjoin R (f '' s) = (adjoin R s).map f :=
  le_antisymm (adjoin_le <| Set.image_subset _ subset_adjoin) <|
    Subalgebra.map_le.2 <| adjoin_le <| Set.image_subset_iff.1 <| by
      -- Porting note: I don't understand how this worked in Lean 3 with just `subset_adjoin`
      simp only [Set.image_id', coe_carrier_toSubmonoid, Subalgebra.coe_toSubsemiring,
        Subalgebra.coe_comap]
      exact fun x hx => subset_adjoin ⟨x, hx, rfl⟩

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
s : Set A
⊢ (fun x => x) '' s ⊆ (Subalgebra.comap f (adjoin R (⇑f '' s))).carrier

Tactic:
simp only [Set.image_id', coe_carrier_toSubmonoid, Subalgebra.coe_toSubsemiring,
  Subalgebra.coe_comap]

Result:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
s : Set A
⊢ s ⊆ ⇑f ⁻¹' ↑(adjoin R (⇑f '' s))

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
s : Set A
⊢ s ⊆ ⇑f ⁻¹' ↑(adjoin R (⇑f '' s))

Tactic:
exact fun x hx => subset_adjoin ⟨x, hx, rfl⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem reverse_concat (l : List α) (a : α) : (l ++ [a]).reverse = a :: l.reverse

Proof state:
α : Type u_1
l : List α
a : α
⊢ [a].reverse ++ l.reverse = a :: l.reverse

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
l : List α
a : α
⊢ (l ++ [a]).reverse = a :: l.reverse

Tactic:
rw [reverse_append]

Result:
α : Type u_1
l : List α
a : α
⊢ [a].reverse ++ l.reverse = a :: l.reverse
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
lemma support_mul_subset_left (f g : ι → M₀) : support (fun x ↦ f x * g x) ⊆ support f :=
  fun x hfg hf ↦ hfg <| by simp only [hf, zero_mul]

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
f g : ι → M₀
x : ι
hfg : x ∈ support fun x => f x * g x
hf : f x = 0
⊢ (fun x => f x * g x) x = 0

Tactic:
simp only [hf, zero_mul]

Result:
no goals
-- Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean
theorem nonarchimedean (hB : SubmodulesBasis B) : @NonarchimedeanAddGroup M _ hB.topology

Proof state:
case is_nonarchimedean
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := hB.topology
⊢ ∀ U ∈ 𝓝 0, ∃ V, ↑V ⊆ U

Tactic:
intro U hU

Result:
case is_nonarchimedean
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := hB.topology
U : Set M
hU : U ∈ 𝓝 0
⊢ ∃ V, ↑V ⊆ U

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ NonarchimedeanAddGroup M

Tactic:
letI := hB.topology

Result:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := hB.topology
⊢ NonarchimedeanAddGroup M

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := hB.topology
⊢ NonarchimedeanAddGroup M

Tactic:
constructor

Result:
case is_nonarchimedean
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := hB.topology
⊢ ∀ U ∈ 𝓝 0, ∃ V, ↑V ⊆ U

Proof state:
case is_nonarchimedean.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := hB.topology
U : Set M
hU : U ∈ 𝓝 0
i : ι
hi : ↑(B i) ⊆ U
⊢ ∃ V, ↑V ⊆ U

Tactic:
exact ⟨hB.openAddSubgroup i, hi⟩

Result:
no goals

Proof state:
case is_nonarchimedean
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := hB.topology
U : Set M
hU : U ∈ 𝓝 0
⊢ ∃ V, ↑V ⊆ U

Tactic:
obtain ⟨-, ⟨i, rfl⟩, hi : (B i : Set M) ⊆ U⟩ :=
  hB.toModuleFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff.mp hU

Result:
case is_nonarchimedean.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := hB.topology
U : Set M
hU : U ∈ 𝓝 0
i : ι
hi : ↑(B i) ⊆ U
⊢ ∃ V, ↑V ⊆ U
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
lemma mul_nonpos_iff_neg_imp_nonneg [PosMulStrictMono α] [MulPosStrictMono α]
    [AddLeftMono α] [AddLeftReflectLE α] :
    a * b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Proof state:
α : Type u
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
a b : α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
⊢ a * b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
rw [← neg_nonneg, ← neg_mul, mul_nonneg_iff_pos_imp_nonneg (α := α)]

Result:
α : Type u
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
a b : α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
⊢ (0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Proof state:
α : Type u
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
a b : α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
⊢ (0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
simp only [neg_pos, neg_nonneg]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Comap.lean
theorem le_comap_apply (f : α → β) (μ : Measure β) (hfi : Injective f)
    (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ) (s : Set α) :
    μ (f '' s) ≤ comap f μ s

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
⊢ μ (f '' s) ≤ (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯) s

Tactic:
exact le_toMeasure_apply _ _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
⊢ μ (f '' s) ≤ (comap f μ) s

Tactic:
rw [comap, dif_pos (And.intro hfi hf)]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
⊢ μ (f '' s) ≤ (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯) s
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem interior_setOf_le_im (a : ℝ) : interior { z : ℂ | a ≤ z.im } = { z | a < z.im }

Proof state:
a : ℝ
⊢ interior {z | a ≤ z.im} = {z | a < z.im}

Tactic:
simpa only [interior_Ici] using interior_preimage_im (Ici a)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem natAbs_pos : 0 < natAbs a ↔ a ≠ 0

Proof state:
a : Int
⊢ 0 < a.natAbs ↔ a ≠ 0

Tactic:
rw [Nat.pos_iff_ne_zero, Ne, natAbs_eq_zero]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma cosZeta_neg (a : UnitAddCircle) (s : ℂ) :
    cosZeta (-a) s = cosZeta a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ cosZeta (-a) s = cosZeta a s

Tactic:
simp [cosZeta]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem mem_nhdsWithin_prod_iff {x : X} {y : Y} {s : Set (X × Y)} {tx : Set X} {ty : Set Y} :
    s ∈ 𝓝[tx ×ˢ ty] (x, y) ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
tx : Set X
ty : Set Y
⊢ s ∈ 𝓝[tx ×ˢ ty] (x, y) ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s

Tactic:
rw [nhdsWithin_prod_eq, mem_prod_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Basic.lean
lemma Triangle.eqToHom_hom₂ {A B : Triangle C} (h : A = B) :
    (eqToHom h).hom₂ = eqToHom (by subst h; rfl)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A B : Triangle C
h : A = B
⊢ A.obj₂ = B.obj₂

Tactic:
subst h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A : Triangle C
⊢ A.obj₂ = A.obj₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A : Triangle C
⊢ A.obj₂ = A.obj₂

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
h : A = B
⊢ (eqToHom h).hom₂ = eqToHom ⋯

Tactic:
subst h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A : Triangle C
⊢ (eqToHom ⋯).hom₂ = eqToHom ⋯

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A : Triangle C
⊢ (eqToHom ⋯).hom₂ = eqToHom ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
@[simp 1100, norm_cast]
lemma nnnorm_nnratCast (q : ℚ≥0) : ‖(q : ℂ)‖₊ = q

Proof state:
q : ℚ≥0
⊢ ‖↑q‖₊ = ↑q

Tactic:
simp [nnnorm]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem mem_range_embedding (j : Fin n) : j ∈ Set.range (c.embedding (c.index j))

Proof state:
n : ℕ
c : Composition n
j : Fin n
⊢ j ∈ Set.range ⇑(c.embedding (c.index j))

Tactic:
have : c.embedding (c.index j) (c.invEmbedding j) ∈ Set.range (c.embedding (c.index j)) :=
  Set.mem_range_self _

Result:
n : ℕ
c : Composition n
j : Fin n
this : (c.embedding (c.index j)) (c.invEmbedding j) ∈ Set.range ⇑(c.embedding (c.index j))
⊢ j ∈ Set.range ⇑(c.embedding (c.index j))

Proof state:
n : ℕ
c : Composition n
j : Fin n
this : (c.embedding (c.index j)) (c.invEmbedding j) ∈ Set.range ⇑(c.embedding (c.index j))
⊢ j ∈ Set.range ⇑(c.embedding (c.index j))

Tactic:
rwa [c.embedding_comp_inv j] at this

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem foldl (f) (init : α) : ∀ {s}, ValidFor l m r s → s.foldl f init = m.foldl f init
  | _, ⟨⟩ => by simp [-List.append_assoc, Substring.foldl, foldlAux_of_valid]

Proof state:
α : Type u_1
l m r : List Char
f : α → Char → α
init : α
⊢ Substring.foldl f init
      { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
        stopPos := { byteIdx := utf8Len l + utf8Len m } } =
    List.foldl f init m

Tactic:
simp [-List.append_assoc, Substring.foldl, foldlAux_of_valid]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem restrict_empty (m : OuterMeasure α) : restrict ∅ m = 0 :=
  ext fun s => by simp

Proof state:
α : Type u_1
m : OuterMeasure α
s : Set α
⊢ ((restrict ∅) m) s = 0 s

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
@[simp]
lemma Gammaℝ_one : Gammaℝ 1 = 1

Proof state:
⊢ Gammaℝ 1 = 1

Tactic:
rw [Gammaℝ_def, Complex.Gamma_one_half_eq]

Result:
⊢ ↑π ^ (-1 / 2) * ↑π ^ (1 / 2) = 1

Proof state:
⊢ ↑π ^ (-1 / 2) * ↑π ^ (1 / 2) = 1

Tactic:
simp [neg_div, cpow_neg, inv_mul_cancel, pi_ne_zero]

Result:
no goals
-- Mathlib/Data/Finset/Interval.lean
theorem card_Ioo_finset (h : s ⊆ t) : (Ioo s t).card = 2 ^ (t.card - s.card) - 2

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ #(Ioo s t) = 2 ^ (#t - #s) - 2

Tactic:
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc_finset h]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem graph_zero : graph (0 : α →₀ M) = ∅

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
⊢ graph 0 = ∅

Tactic:
simp [graph]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_div {L : Type*} [RCLike L] (r : L) (f : α → L) :
    ∫ a, f a / r ∂μ = (∫ a, f a ∂μ) / r

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
L : Type u_6
inst✝ : RCLike L
r : L
f : α → L
⊢ ∫ (a : α), f a / r ∂μ = (∫ (a : α), f a ∂μ) / r

Tactic:
simpa only [← div_eq_mul_inv] using integral_mul_right r⁻¹ f

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tan_periodic : Function.Periodic tan π

Proof state:
⊢ Function.Periodic tan π

Tactic:
simpa only [Function.Periodic, tan_eq_sin_div_cos] using sin_antiperiodic.div cos_antiperiodic

Result:
no goals