harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β) (l : List α) (init : β) :
    (l.filter p).foldrM g init =
      l.foldrM (fun x y => if p x then g x y else pure y) init

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : α → β → m β
init : β
⊢ foldrM g init (filter p []) = foldrM (fun x y => if p x = true then g x y else pure y) init []

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : α → β → m β
l : List α
init : β
⊢ foldrM g init (filter p l) = foldrM (fun x y => if p x = true then g x y else pure y) init l

Tactic:
induction l generalizing init with
| nil => rfl
| cons a l ih =>
  simp only [filter_cons, foldrM_cons]
  split <;> simp [ih]

Result:
no goals

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : α → β → m β
a : α
l : List α
ih : ∀ (init : β), foldrM g init (filter p l) = foldrM (fun x y => if p x = true then g x y else pure y) init l
init : β
⊢ foldrM g init (filter p (a :: l)) = foldrM (fun x y => if p x = true then g x y else pure y) init (a :: l)

Tactic:
simp only [filter_cons, foldrM_cons]

Result:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : α → β → m β
a : α
l : List α
ih : ∀ (init : β), foldrM g init (filter p l) = foldrM (fun x y => if p x = true then g x y else pure y) init l
init : β
⊢ foldrM g init (if p a = true then a :: filter p l else filter p l) = do
    let y ← foldrM (fun x y => if p x = true then g x y else pure y) init l
    if p a = true then g a y else pure y

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : α → β → m β
a : α
l : List α
ih : ∀ (init : β), foldrM g init (filter p l) = foldrM (fun x y => if p x = true then g x y else pure y) init l
init : β
⊢ foldrM g init (if p a = true then a :: filter p l else filter p l) = do
    let y ← foldrM (fun x y => if p x = true then g x y else pure y) init l
    if p a = true then g a y else pure y

Tactic:
split <;> simp [ih]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Action/Defs.lean
lemma smul_eq_zero_iff_eq (a : α) {x : β} : a • x = 0 ↔ x = 0 :=
  ⟨fun h => by rw [← inv_smul_smul a x, h, smul_zero], fun h => h.symm ▸ smul_zero _⟩

Proof state:
α : Type u_5
β : Type u_6
inst✝² : Group α
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction α β
a : α
x : β
h : a • x = 0
⊢ x = 0

Tactic:
rw [← inv_smul_smul a x, h, smul_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Bimon_.lean
theorem mul_counit (M : Bimon_ C) :
    M.X.mul ≫ M.counit.hom = (M.counit.hom ⊗ M.counit.hom) ≫ (λ_ _).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon_ C
⊢ M.X.mul ≫ M.counit.hom = (M.counit.hom ⊗ M.counit.hom) ≫ (λ_ (𝟙_ (Mon_ C)).X).hom

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addZ_of_Z_eq_zero_right {P Q : Fin 3 → R} (hQz : Q z = 0) :
    addZ P Q = -(Q x * P z) * P z

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hQz : Q z = 0
⊢ P x * 0 ^ 2 - Q x * P z ^ 2 = -(Q x * P z) * P z

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hQz : Q z = 0
⊢ addZ P Q = -(Q x * P z) * P z

Tactic:
rw [addZ, hQz]

Result:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hQz : Q z = 0
⊢ P x * 0 ^ 2 - Q x * P z ^ 2 = -(Q x * P z) * P z
-- Mathlib/Computability/Partrec.lean
theorem bind {f : α →. β} {g : α → β →. σ} (hf : Partrec f) (hg : Partrec₂ g) :
    Partrec fun a => (f a).bind (g a) :=
  (hg.comp (Nat.Partrec.some.pair hf)).of_eq fun n => by
    simp [Seq.seq]; rcases e : decode (α := α) n with - | a <;> simp [e, encodek]

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. β
g : α → β →. σ
hf : Partrec f
hg : Partrec₂ g
n : ℕ
⊢ (((↑(decode n)).bind fun y => map (Nat.pair n) (map encode (f y))).bind fun n =>
      (↑((decode (Nat.unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).2))).bind fun a =>
        map encode (g a.1 a.2)) =
    (↑(decode n)).bind fun a => (f a).bind fun y => map encode (g a y)

Tactic:
rcases e : decode (α := α) n with - | a <;> simp [e, encodek]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. β
g : α → β →. σ
hf : Partrec f
hg : Partrec₂ g
n : ℕ
⊢ (do
      let n ← Nat.pair <$> Part.some n <*> (↑(decode n)).bind fun a => map encode (f a)
      (↑(decode n)).bind fun a => map encode ((fun p => g p.1 p.2) a)) =
    (↑(decode n)).bind fun a => map encode ((fun a => (f a).bind (g a)) a)

Tactic:
simp [Seq.seq]

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. β
g : α → β →. σ
hf : Partrec f
hg : Partrec₂ g
n : ℕ
⊢ (((↑(decode n)).bind fun y => map (Nat.pair n) (map encode (f y))).bind fun n =>
      (↑((decode (Nat.unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).2))).bind fun a =>
        map encode (g a.1 a.2)) =
    (↑(decode n)).bind fun a => (f a).bind fun y => map encode (g a y)
-- Mathlib/Data/Fintype/Card.lean
theorem Finset.card_add_card_compl [DecidableEq α] [Fintype α] (s : Finset α) :
    #s + #sᶜ = Fintype.card α

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ #s + #sᶜ = Fintype.card α

Tactic:
rw [Finset.card_compl, ← Nat.add_sub_assoc (card_le_univ s), Nat.add_sub_cancel_left]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
lemma IsHamiltonianCycle.count_support_self (hp : p.IsHamiltonianCycle) :
    p.support.count a = 2

Proof state:
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
⊢ List.count a p.support = 2

Tactic:
rw [support_eq_cons, List.count_cons_self, ← support_tail _ hp.1.not_nil, hp.isHamiltonian_tail]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem attach_congr {l₁ l₂ : List α} (h : l₁ = l₂) :
    l₁.attach = l₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩)

Proof state:
α : Type u_1
l₁ : List α
⊢ l₁.attach = map (fun x => ⟨x.val, ⋯⟩) l₁.attach

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
h : l₁ = l₂
⊢ l₁.attach = map (fun x => ⟨x.val, ⋯⟩) l₂.attach

Tactic:
subst h

Result:
α : Type u_1
l₁ : List α
⊢ l₁.attach = map (fun x => ⟨x.val, ⋯⟩) l₁.attach
-- Mathlib/Combinatorics/Quiver/Symmetric.lean
theorem reverse_reverse [h : HasInvolutiveReverse V] {a b : V} (f : a ⟶ b) :
    reverse (reverse f) = f

Proof state:
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f : a ⟶ b
⊢ reverse (reverse f) = f

Tactic:
apply h.inv'

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalWhiskerRightAux_of {f g : C} (η : f ⟶ g) (h : C) :
    η ▷ h = (Iso.refl _).hom ≫ η ▷ h ≫ (Iso.refl _).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g : C
η : f ⟶ g
h : C
⊢ η ▷ h = (Iso.refl (f ⊗ h)).hom ≫ η ▷ h ≫ (Iso.refl (g ⊗ h)).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
lemma closedBall_prod_same (x : α) (y : β) (r : ℝ) :
    closedBall x r ×ˢ closedBall y r = closedBall (x, y) r := ext fun z => by simp [Prod.dist_eq]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α
y : β
r : ℝ
z : α × β
⊢ z ∈ closedBall x r ×ˢ closedBall y r ↔ z ∈ closedBall (x, y) r

Tactic:
simp [Prod.dist_eq]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/SubboxInduction.lean
theorem mem_splitCenter : J ∈ splitCenter I ↔ ∃ s, I.splitCenterBox s = J

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
⊢ J ∈ splitCenter I ↔ ∃ s, I.splitCenterBox s = J

Tactic:
simp [splitCenter]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem Module.comap_annihilator {R₀} [CommSemiring R₀] [Module R₀ M]
    [Algebra R₀ R] [IsScalarTower R₀ R M] :
    (Module.annihilator R M).comap (algebraMap R₀ R) = Module.annihilator R₀ M

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₀ : Type u_4
inst✝³ : CommSemiring R₀
inst✝² : Module R₀ M
inst✝¹ : Algebra R₀ R
inst✝ : IsScalarTower R₀ R M
x : R₀
⊢ x ∈ Ideal.comap (algebraMap R₀ R) (annihilator R M) ↔ x ∈ annihilator R₀ M

Tactic:
simp [mem_annihilator]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₀ : Type u_4
inst✝³ : CommSemiring R₀
inst✝² : Module R₀ M
inst✝¹ : Algebra R₀ R
inst✝ : IsScalarTower R₀ R M
⊢ Ideal.comap (algebraMap R₀ R) (annihilator R M) = annihilator R₀ M

Tactic:
ext x

Result:
case h
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₀ : Type u_4
inst✝³ : CommSemiring R₀
inst✝² : Module R₀ M
inst✝¹ : Algebra R₀ R
inst✝ : IsScalarTower R₀ R M
x : R₀
⊢ x ∈ Ideal.comap (algebraMap R₀ R) (annihilator R M) ↔ x ∈ annihilator R₀ M
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem bne_eq_decide_not_eq {_ : BEq α} [LawfulBEq α] [DecidableEq α] (a b : α) : (a != b) = (decide (¬ a = b))

Proof state:
α : Type u_1
x✝ : BEq α
inst✝¹ : LawfulBEq α
inst✝ : DecidableEq α
a b : α
⊢ (a != b) = decide ¬a = b

Tactic:
by_cases a = b <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem whiskerLeft_rightUnitor (f : a ⟶ b) (g : b ⟶ c) :
    f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom

Tactic:
rw [← whiskerRight_iff, comp_whiskerRight, ← cancel_epi (α_ _ _ _).inv, ←
    cancel_epi (f ◁ (α_ _ _ _).inv), pentagon_inv_assoc, triangle_assoc_comp_right, ←
    associator_inv_naturality_middle, ← whiskerLeft_comp_assoc, triangle_assoc_comp_right,
    associator_inv_naturality_right]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
@[simp] lemma ofNat_le_cast : ofNat(n) ≤ (p : K) ↔ OfNat.ofNat n ≤ p

Proof state:
K : Type u_5
inst✝¹ : LinearOrderedSemifield K
p : ℚ≥0
n : ℕ
inst✝ : n.AtLeastTwo
⊢ OfNat.ofNat n ≤ ↑p ↔ OfNat.ofNat n ≤ p

Tactic:
simp [← cast_le (K := K)]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Degree.lean
theorem intDegree_one : intDegree (1 : RatFunc K) = 0

Proof state:
K : Type u
inst✝ : Field K
⊢ intDegree 1 = 0

Tactic:
rw [intDegree, num_one, denom_one, sub_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem reverse_range' (s n : Nat) : reverse (range' s n) = map (s + n - 1 - ·) (range n)

Proof state:
s n : Nat
⊢ (range' s n).reverse = map (fun x => s + n - 1 - x) (range n)

Tactic:
simp [← toList_inj, List.reverse_range']

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem norm_nonneg (x : ℤ[i]) : 0 ≤ norm x :=
  Zsqrtd.norm_nonneg (by norm_num) _

Proof state:
x : ℤ[i]
⊢ -1 ≤ 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem isSome_map {x : Option α} : (f <$> x).isSome = x.isSome

Proof state:
α α✝ : Type u_1
f : α → α✝
x : Option α
⊢ (f <$> x).isSome = x.isSome

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Filtered.lean
/-- A functor preserving larger cofiltered limits also preserves smaller cofiltered limits. -/
lemma preservesCofilteredLimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}]
    [UnivLE.{w₂, w₂'}] [PreservesCofilteredLimitsOfSize.{w', w₂'} F] :
      PreservesCofilteredLimitsOfSize.{w, w₂} F where
  preserves_cofiltered_limits J _ _

Proof state:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesCofilteredLimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
⊢ PreservesLimitsOfShape J F

Tactic:
let e := ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm

Result:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesCofilteredLimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
⊢ PreservesLimitsOfShape J F

Proof state:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesCofilteredLimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
⊢ PreservesLimitsOfShape J F

Tactic:
haveI := IsCofiltered.of_equivalence e.symm

Result:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesCofilteredLimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
this : IsCofiltered (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ PreservesLimitsOfShape J F

Proof state:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesCofilteredLimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
this : IsCofiltered (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ PreservesLimitsOfShape J F

Tactic:
exact preservesLimitsOfShape_of_equiv e F

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[simp, reassoc]
lemma right_unitality (X : C) :
    (ρ_ (F.obj X)).hom = F.obj X ◁ ε F ≫ μ F X (𝟙_ C) ≫ F.map (ρ_ X).hom

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
⊢ (ρ_ (F.obj X)).hom = F.obj X ◁ ε F ≫ μ F X (𝟙_ C) ≫ F.map (ρ_ X).hom

Tactic:
apply right_unitality'

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem map_extChartAt_nhdsWithin' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    map (extChartAt I x) (𝓝[s] y) = 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x y :=
  map_extend_nhdsWithin _ <| by rwa [← extChartAt_source I]

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x y : M
hy : y ∈ (extChartAt I x).source
⊢ y ∈ (chartAt H x).source

Tactic:
rwa [← extChartAt_source I]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem _root_.Wbtw.oangle_eq_right {p₁ p₂ p₃ p₃' : P} (h : Wbtw ℝ p₂ p₃ p₃') (hp₃p₂ : p₃ ≠ p₂) :
    ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃'

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₃' : P
h : Wbtw ℝ p₂ p₃ p₃'
hp₃p₂ : p₃ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃'

Tactic:
rw [oangle_rev, h.oangle_eq_left hp₃p₂, ← oangle_rev]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem CovBy.nhdsLE (H : a ⋖ b) : 𝓝[≤] b = pure b

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a b : α
H : a ⋖ b
⊢ 𝓝[≤] b = pure b

Tactic:
rw [← Iio_insert, nhdsWithin_insert, H.nhdsLT, sup_bot_eq]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioi_subset_Ici_self : Ioi a ⊆ Ici a

Proof state:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ioi a ⊆ Ici a

Tactic:
simpa [← coe_subset] using Set.Ioi_subset_Ici_self

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalHom.lean
theorem coe_mulHom_mk (f : A →ₛₙₐ[φ] B) (h₁ h₂ h₃ h₄) :
    ((⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₛₙₐ[φ] B) : A →ₙ* B) = ⟨f, h₄⟩

Proof state:
R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f : A →ₛₙₐ[φ] B
h₁ : ∀ (m : R) (x : A), f (m • x) = φ m • f x
h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y
h₄ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) =
      { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x *
        { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y
⊢ ↑{ toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = { toFun := ⇑f, map_mul' := h₄ }

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem restrict_range (f : G →* N) : (f.restrict K).range = K.map f

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
K : Subgroup G
f : G →* N
⊢ (f.restrict K).range = map f K

Tactic:
simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists,
  exists_prop, forall_const]

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
/-- `M.restrictSubtype X` is isomorphic to `M ↾ X`. -/
@[simp] lemma map_val_restrictSubtype_eq (M : Matroid α) (X : Set α) :
    (M.restrictSubtype X).map (↑) Subtype.val_injective.injOn = M ↾ X

Proof state:
α : Type u_1
M : Matroid α
X : Set α
⊢ (M.restrictSubtype X).map Subtype.val ⋯ = M ↾ X

Tactic:
simp [restrictSubtype, map_comap, Subset.rfl]

Result:
no goals
-- Mathlib/Topology/Instances/Discrete.lean
theorem LinearOrder.bot_topologicalSpace_eq_generateFrom {α} [LinearOrder α] [PredOrder α]
    [SuccOrder α] : (⊥ : TopologicalSpace α) = generateFrom { s | ∃ a, s = Ioi a ∨ s = Iio a }

Proof state:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
⊢ ⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}

Tactic:
let _ := Preorder.topology α

Result:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
x✝ : TopologicalSpace α := Preorder.topology α
⊢ ⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}

Proof state:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ ⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}

Tactic:
exact DiscreteTopology.of_predOrder_succOrder.eq_bot.symm

Result:
no goals

Proof state:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
x✝ : TopologicalSpace α := Preorder.topology α
⊢ ⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}

Tactic:
have : OrderTopology α := ⟨rfl⟩

Result:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ ⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
@[reassoc (attr := simp), elementwise (attr := simp)]
lemma groupCohomologyπ_comp_isoH2_hom  :
    groupCohomologyπ A 2 ≫ (isoH2 A).hom = (isoTwoCocycles A).hom ≫ H2π A

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ groupCohomologyπ A 2 ≫ (isoH2 A).hom = (isoTwoCocycles A).hom ≫ H2π A

Tactic:
simp [isoH2, isoTwoCocycles]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem zpow_eq_zpow_emod {x : G} (m : ℤ) {n : ℤ} (h : x ^ n = 1) :
    x ^ m = x ^ (m % n) :=
  calc
    x ^ m = x ^ (m % n + n * (m / n))

Proof state:
G : Type u_3
inst✝ : Group G
x : G
m n : ℤ
h : x ^ n = 1
⊢ x ^ m = x ^ (m % n + n * (m / n))

Tactic:
rw [Int.emod_add_ediv]

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
x : G
m n : ℤ
h : x ^ n = 1
⊢ x ^ (m % n + n * (m / n)) = x ^ (m % n)

Tactic:
simp [zpow_add, zpow_mul, h]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
lemma neg_mem_divisorsAntidiag : -xy ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

Proof state:
xy : ℤ × ℤ
z : ℤ
⊢ -xy ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

Tactic:
simp

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
@[simp] lemma himp_eq_left : x ⇨ y = x ↔ x = ⊤ ∧ y = ⊤

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⇨ y = x ↔ x = ⊤ ∧ y = ⊤

Tactic:
rw [codisjoint_himp_self_left.eq_iff]

Result:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⇨ y = ⊤ ∧ x = ⊤ ↔ x = ⊤ ∧ y = ⊤

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⇨ y = ⊤ ∧ x = ⊤ ↔ x = ⊤ ∧ y = ⊤

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
@[simp] lemma sq_lt_one_iff_abs_lt_one (a : α) : a ^ 2 < 1 ↔ |a| < 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a : α
⊢ a ^ 2 < 1 ↔ |a| < 1

Tactic:
simpa only [one_pow, abs_one] using @sq_lt_sq _ _ a 1

Result:
no goals
-- Mathlib/Algebra/Group/Translate.lean
/-- See `translate_add` -/
lemma translate_add' (a b : G) (f : G → α) : τ (a + b) f = τ b (τ a f)

Proof state:
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
⊢ τ (a + b) f = τ b (τ a f)

Tactic:
rw [add_comm, translate_add]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem continuousWithinAt_diff_singleton [TopologicalSpace Y] [T1Space X]
    {x y : X} {s : Set X} {f : X → Y} :
    ContinuousWithinAt f (s \ {y}) x ↔ ContinuousWithinAt f s x

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x y : X
s : Set X
f : X → Y
⊢ ContinuousWithinAt f (s \ {y}) x ↔ ContinuousWithinAt f s x

Tactic:
rw [← continuousWithinAt_insert, insert_diff_singleton, continuousWithinAt_insert]

Result:
no goals
-- Mathlib/Algebra/Algebra/Hom.lean
theorem comp_ofId (φ : A →ₐ[R] B) : φ.comp (Algebra.ofId R A) = Algebra.ofId R B

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
φ : A →ₐ[R] B
⊢ φ.comp (ofId R A) = ofId R B

Tactic:
ext

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem injective_or_eq_zero [IsSimpleModule R M] (f : M →ₗ[R] N) :
    Function.Injective f ∨ f = 0

Proof state:
R : Type u_2
inst✝⁵ : Ring R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
f : M →ₗ[R] N
⊢ Function.Injective ⇑f ∨ f = 0

Tactic:
rw [← ker_eq_bot, ← ker_eq_top]

Result:
R : Type u_2
inst✝⁵ : Ring R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
f : M →ₗ[R] N
⊢ ker f = ⊥ ∨ ker f = ⊤

Proof state:
R : Type u_2
inst✝⁵ : Ring R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
f : M →ₗ[R] N
⊢ ker f = ⊥ ∨ ker f = ⊤

Tactic:
apply eq_bot_or_eq_top

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem Disjoint.symm : Disjoint f g → Disjoint g f

Proof state:
α : Type u_1
f g : Perm α
⊢ f.Disjoint g → g.Disjoint f

Tactic:
simp only [Disjoint, or_comm, imp_self]

Result:
no goals