harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualPairing_nondegenerate (W : Subspace K V₁) : W.dualPairing.Nondegenerate

Proof state:
case right
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
x : ↥W
h : ∀ (x_1 : Dual K V₁ ⧸ dualAnnihilator W), ((Submodule.dualPairing W) x_1) x = 0
⊢ x = 0

Tactic:
rw [← forall_dual_apply_eq_zero_iff K x]

Result:
case right
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
x : ↥W
h : ∀ (x_1 : Dual K V₁ ⧸ dualAnnihilator W), ((Submodule.dualPairing W) x_1) x = 0
⊢ ∀ (φ : Dual K ↥W), φ x = 0

Proof state:
case left
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (Submodule.dualPairing W).SeparatingLeft

Tactic:
rw [LinearMap.separatingLeft_iff_ker_eq_bot, dualPairing_eq]

Result:
case left
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ LinearMap.ker ↑W.quotAnnihilatorEquiv = ⊥

Proof state:
case left
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ LinearMap.ker ↑W.quotAnnihilatorEquiv = ⊥

Tactic:
apply LinearEquiv.ker

Result:
no goals

Proof state:
case right
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
x : ↥W
h : ∀ (x_1 : Dual K V₁ ⧸ dualAnnihilator W), ((Submodule.dualPairing W) x_1) x = 0
φ : Dual K ↥W
⊢ φ x = 0

Tactic:
simpa only [Submodule.dualPairing_apply, dualLift_of_subtype] using
  h (Submodule.Quotient.mk (W.dualLift φ))

Result:
no goals

Proof state:
case right
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
x : ↥W
h : ∀ (x_1 : Dual K V₁ ⧸ dualAnnihilator W), ((Submodule.dualPairing W) x_1) x = 0
⊢ ∀ (φ : Dual K ↥W), φ x = 0

Tactic:
intro φ

Result:
case right
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
x : ↥W
h : ∀ (x_1 : Dual K V₁ ⧸ dualAnnihilator W), ((Submodule.dualPairing W) x_1) x = 0
φ : Dual K ↥W
⊢ φ x = 0

Proof state:
case right
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (Submodule.dualPairing W).SeparatingRight

Tactic:
intro x h

Result:
case right
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
x : ↥W
h : ∀ (x_1 : Dual K V₁ ⧸ dualAnnihilator W), ((Submodule.dualPairing W) x_1) x = 0
⊢ x = 0

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (Submodule.dualPairing W).Nondegenerate

Tactic:
constructor

Result:
case left
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (Submodule.dualPairing W).SeparatingLeft

case right
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (Submodule.dualPairing W).SeparatingRight
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_dirac [MeasurableSpace α] [MeasurableSingletonClass α] (f : α → E) (a : α) :
    ∫ x, f x ∂Measure.dirac a = f a :=
  calc
    ∫ x, f x ∂Measure.dirac a = ∫ _, f a ∂Measure.dirac a := integral_congr_ae <| ae_eq_dirac f
    _ = f a

Proof state:
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → E
a : α
⊢ ∫ (x : α), f a ∂Measure.dirac a = f a

Tactic:
simp [Measure.dirac_apply_of_mem]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem closure_le_normalClosure {s : Set G} : closure s ≤ normalClosure s

Proof state:
G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure s ≤ normalClosure s

Tactic:
simp only [subset_normalClosure, closure_le]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem prod_sUnion {s : Set α} {C : Set (Set β)} : s ×ˢ ⋃₀ C = ⋃₀ ((fun t => s ×ˢ t) '' C)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
C : Set (Set β)
⊢ s ×ˢ ⋃₀ C = ⋃₀ ((fun t => s ×ˢ t) '' C)

Tactic:
simp_rw [sUnion_eq_biUnion, biUnion_image, prod_iUnion₂]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem sInf_apply {m : Set (OuterMeasure α)} {s : Set α} (h : m.Nonempty) :
    sInf m s =
      ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' n, ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), μ (t n)

Proof state:
α : Type u_1
m : Set (OuterMeasure α)
s : Set α
h : m.Nonempty
⊢ (sInf m) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, μ (t n)

Tactic:
simp_rw [sInf_eq_boundedBy_sInfGen, boundedBy_apply, iSup_sInfGen_nonempty h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_flatMap (f : β → γ) (g : α → List β) :
    ∀ l : List α, (l.flatMap g).map f = l.flatMap fun a => (g a).map f
  | [] => rfl
  | a::l => by simp only [flatMap_cons, map_append, map_flatMap _ _ l]

Proof state:
β : Type u_1
γ : Type u_2
α : Type u_3
f : β → γ
g : α → List β
a : α
l : List α
⊢ map f (flatMap g (a :: l)) = flatMap (fun a => map f (g a)) (a :: l)

Tactic:
simp only [flatMap_cons, map_append, map_flatMap _ _ l]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem one_le_iff_ne_zero {o : Ordinal} : 1 ≤ o ↔ o ≠ 0

Proof state:
o : Ordinal.{u_1}
⊢ 1 ≤ o ↔ o ≠ 0

Tactic:
rw [Order.one_le_iff_pos, Ordinal.pos_iff_ne_zero]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Multiset.lean
lemma dvd_sum : (∀ x ∈ s, a ∣ x) → a ∣ s.sum :=
  Multiset.induction_on s (fun _ ↦ dvd_zero _) fun x s ih h ↦ by
    rw [sum_cons]
    exact dvd_add (h _ (mem_cons_self _ _)) (ih fun y hy ↦ h _ <| mem_cons.2 <| Or.inr hy)

Proof state:
α : Type u_2
inst✝ : NonUnitalSemiring α
s✝ : Multiset α
a x : α
s : Multiset α
ih : (∀ x ∈ s, a ∣ x) → a ∣ s.sum
h : ∀ x_1 ∈ x ::ₘ s, a ∣ x_1
⊢ a ∣ x + s.sum

Tactic:
exact dvd_add (h _ (mem_cons_self _ _)) (ih fun y hy ↦ h _ <| mem_cons.2 <| Or.inr hy)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : NonUnitalSemiring α
s✝ : Multiset α
a x : α
s : Multiset α
ih : (∀ x ∈ s, a ∣ x) → a ∣ s.sum
h : ∀ x_1 ∈ x ::ₘ s, a ∣ x_1
⊢ a ∣ (x ::ₘ s).sum

Tactic:
rw [sum_cons]

Result:
α : Type u_2
inst✝ : NonUnitalSemiring α
s✝ : Multiset α
a x : α
s : Multiset α
ih : (∀ x ∈ s, a ∣ x) → a ∣ s.sum
h : ∀ x_1 ∈ x ::ₘ s, a ∣ x_1
⊢ a ∣ x + s.sum
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
lemma arg_mul_eq_add_arg_iff {x y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) :
    (x * y).arg = x.arg + y.arg ↔ arg x + arg y ∈ Set.Ioc (-π) π

Proof state:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ (x * y).arg = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π

Tactic:
rw [← arg_coe_angle_toReal_eq_arg, arg_mul_coe_angle hx₀ hy₀, ← Real.Angle.coe_add,
    Real.Angle.toReal_coe_eq_self_iff_mem_Ioc]

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem WCovBy.image (f : α ↪o β) (hab : a ⩿ b) (h : (range f).OrdConnected) : f a ⩿ f b

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : (range ⇑f).OrdConnected
c : α
ha : a < c
hb : c < b
⊢ False

Tactic:
exact hab.2 ha hb

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : (range ⇑f).OrdConnected
c : α
ha : f a < f c
hb : f c < f b
⊢ False

Tactic:
rw [f.lt_iff_lt] at ha hb

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : (range ⇑f).OrdConnected
c : α
ha : a < c
hb : c < b
⊢ False

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : (range ⇑f).OrdConnected
⊢ f a ⩿ f b

Tactic:
refine ⟨f.monotone hab.le, fun c ha hb => ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : (range ⇑f).OrdConnected
c : β
ha : f a < c
hb : c < f b
⊢ False

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : (range ⇑f).OrdConnected
c : β
ha : f a < c
hb : c < f b
⊢ False

Tactic:
obtain ⟨c, rfl⟩ := h.out (mem_range_self _) (mem_range_self _) ⟨ha.le, hb.le⟩

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : (range ⇑f).OrdConnected
c : α
ha : f a < f c
hb : f c < f b
⊢ False
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem dvd_count_pow [Nontrivial α] {a : Associates α} (ha : a ≠ 0)
    {p : Associates α} (hp : Irreducible p) (k : ℕ) : k ∣ count p (a ^ k).factors

Proof state:
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
k : ℕ
⊢ k ∣ p.count (a ^ k).factors

Tactic:
rw [count_pow ha hp]

Result:
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
k : ℕ
⊢ k ∣ k * p.count a.factors

Proof state:
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
k : ℕ
⊢ k ∣ k * p.count a.factors

Tactic:
apply dvd_mul_right

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
@[reassoc]
lemma XIsoOfEq_hom_naturality {K L : HomologicalComplex V c} (φ : K ⟶ L) {n n' : ι} (h : n = n') :
    φ.f n ≫ (L.XIsoOfEq h).hom = (K.XIsoOfEq h).hom ≫ φ.f n'

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
n : ι
⊢ φ.f n ≫ (L.XIsoOfEq ⋯).hom = (K.XIsoOfEq ⋯).hom ≫ φ.f n

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
n n' : ι
h : n = n'
⊢ φ.f n ≫ (L.XIsoOfEq h).hom = (K.XIsoOfEq h).hom ≫ φ.f n'

Tactic:
subst h

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
n : ι
⊢ φ.f n ≫ (L.XIsoOfEq ⋯).hom = (K.XIsoOfEq ⋯).hom ≫ φ.f n
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma Localization.Hom.mk_surjective {X Y : C} (f : Localization.Hom W X Y) :
    ∃ (z : W.LeftFraction X Y), f = mk z

Proof state:
case mk
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
f : Hom W X Y
z : W.LeftFraction X Y
⊢ ∃ z_1, Quot.mk LeftFractionRel z = mk z_1

Tactic:
exact ⟨z, rfl⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
f : Hom W X Y
⊢ ∃ z, f = mk z

Tactic:
obtain ⟨z⟩ := f

Result:
case mk
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
f : Hom W X Y
z : W.LeftFraction X Y
⊢ ∃ z_1, Quot.mk LeftFractionRel z = mk z_1
-- Mathlib/Data/List/Cycle.lean
theorem chain_singleton (r : α → α → Prop) (a : α) : Chain r [a] ↔ r a a

Proof state:
α : Type u_1
r : α → α → Prop
a : α
⊢ Chain r ↑[a] ↔ r a a

Tactic:
rw [chain_coe_cons, nil_append, List.chain_singleton]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
theorem integrableOn_Ioi_deriv_ofReal_cpow {s : ℂ} {t : ℝ} (ht : 0 < t) (hs : s.re < 0) :
    IntegrableOn (deriv fun x : ℝ ↦ (x : ℂ) ^ s) (Set.Ioi t)

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
⊢ IntegrableOn (fun x => s * ↑x ^ (s - 1)) (Ioi t) volume

Tactic:
refine (integrableOn_Ioi_cpow_of_lt ?_ ht).const_mul _

Result:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
⊢ (s - 1).re < -1

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
h : IntegrableOn (fun x => s * ↑x ^ (s - 1)) (Ioi t) volume
⊢ IntegrableOn (deriv fun x => ↑x ^ s) (Ioi t) volume

Tactic:
refine h.congr_fun (fun x hx ↦ ?_) measurableSet_Ioi

Result:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
h : IntegrableOn (fun x => s * ↑x ^ (s - 1)) (Ioi t) volume
x : ℝ
hx : x ∈ Ioi t
⊢ s * ↑x ^ (s - 1) = deriv (fun x => ↑x ^ s) x

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
h : IntegrableOn (fun x => s * ↑x ^ (s - 1)) (Ioi t) volume
x : ℝ
hx : x ∈ Ioi t
⊢ s * ↑x ^ (s - 1) = deriv (fun x => ↑x ^ s) x

Tactic:
rw [Complex.deriv_ofReal_cpow_const (ht.trans hx).ne' (fun h ↦ (Complex.zero_re ▸ h ▸ hs).false)]

Result:
no goals

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
⊢ (s - 1).re < -1

Tactic:
rwa [Complex.sub_re, Complex.one_re, sub_lt_iff_lt_add, neg_add_cancel]

Result:
no goals

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
⊢ IntegrableOn (deriv fun x => ↑x ^ s) (Ioi t) volume

Tactic:
have h : IntegrableOn (fun x : ℝ ↦ s * x ^ (s - 1)) (Set.Ioi t) := by
  refine (integrableOn_Ioi_cpow_of_lt ?_ ht).const_mul _
  rwa [Complex.sub_re, Complex.one_re, sub_lt_iff_lt_add, neg_add_cancel]

Result:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
h : IntegrableOn (fun x => s * ↑x ^ (s - 1)) (Ioi t) volume
⊢ IntegrableOn (deriv fun x => ↑x ^ s) (Ioi t) volume
-- Mathlib/Topology/Homotopy/Contractible.lean
theorem hequiv [ContractibleSpace X] [ContractibleSpace Y] :
    Nonempty (X ≃ₕ Y)

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
h : X ≃ₕ Unit
h' : Y ≃ₕ Unit
⊢ Nonempty (X ≃ₕ Y)

Tactic:
exact ⟨h.trans h'.symm⟩

Result:
no goals

Proof state:
case intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
h : X ≃ₕ Unit
⊢ Nonempty (X ≃ₕ Y)

Tactic:
rcases ContractibleSpace.hequiv_unit' (X := Y) with ⟨h'⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
h : X ≃ₕ Unit
h' : Y ≃ₕ Unit
⊢ Nonempty (X ≃ₕ Y)

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
⊢ Nonempty (X ≃ₕ Y)

Tactic:
rcases ContractibleSpace.hequiv_unit' (X := X) with ⟨h⟩

Result:
case intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
h : X ≃ₕ Unit
⊢ Nonempty (X ≃ₕ Y)
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem archimedean_iff_rat_lt : Archimedean α ↔ ∀ x : α, ∃ q : ℚ, x < q where
  mp _ x :=
    let ⟨n, h⟩ := exists_nat_gt x
    ⟨n, by rwa [Rat.cast_natCast]⟩
  mpr H := archimedean_iff_nat_lt.2 fun x ↦
    let ⟨q, h⟩ := H x; ⟨⌈q⌉₊, lt_of_lt_of_le h <| mod_cast Nat.le_ceil _⟩

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
x✝ : Archimedean α
x : α
n : ℕ
h : x < ↑n
⊢ x < ↑↑n

Tactic:
rwa [Rat.cast_natCast]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem leftUnitor_inv_whiskerRight (f : a ⟶ b) (g : b ⟶ c) :
    (λ_ f).inv ▷ g = (λ_ (f ≫ g)).inv ≫ (α_ (𝟙 a) f g).inv :=
  eq_of_inv_eq_inv (by simp)

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

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Pi.lean
lemma map_nsmul_piAntidiag_univ [Fintype ι] (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
    (piAntidiag (univ : Finset ι) m).map
        ⟨(n • ·), fun _ _ h ↦ funext fun i ↦ mul_right_injective₀ hn (congr_fun h i)⟩ =
      (piAntidiag univ (n * m)).filter fun f : ι → ℕ ↦ ∀ i, n ∣ f i

Proof state:
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m n : ℕ
hn : n ≠ 0
⊢ map { toFun := fun x => n • x, inj' := ⋯ } (univ.piAntidiag m) =
    filter (fun f => ∀ (i : ι), n ∣ f i) (univ.piAntidiag (n * m))

Tactic:
simpa using map_nsmul_piAntidiag (univ : Finset ι) m hn

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
@[simp]
lemma rpow_eq_zero (hx : 0 ≤ x) (hy : y ≠ 0) : x ^ y = 0 ↔ x = 0

Proof state:
x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
⊢ x ^ y = 0 ↔ x = 0

Tactic:
simp [rpow_eq_zero_iff_of_nonneg, *]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem disjoint_cocompact_right (f : Filter X) :
    Disjoint f (Filter.cocompact X) ↔ ∃ K ∈ f, IsCompact K

Proof state:
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ Disjoint f (cocompact X) ↔ ∃ K ∈ f, IsCompact K

Tactic:
simp_rw [hasBasis_cocompact.disjoint_iff_right, compl_compl]

Result:
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ (∃ i, IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K

Proof state:
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ (∃ i, IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K

Tactic:
tauto

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Assoc.lean
theorem inl_inr_pushoutAssoc_inv [HasPushout (g₃ ≫ (pushout.inr _ _ : X₂ ⟶ Y₁)) g₄]
    [HasPushout g₁ (g₂ ≫ (pushout.inl _ _ : X₂ ⟶ Y₂))] :
    pushout.inl _ _ ≫ pushout.inr _ _ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv =
      pushout.inr _ _ ≫ pushout.inl _ _

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄) ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv =
    pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄

Tactic:
rw [← Category.assoc, Iso.comp_inv_eq, Category.assoc, inr_inl_pushoutAssoc_hom]

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem star_mem_star_iff (S : NonUnitalSubalgebra R A) (x : A) : star x ∈ star S ↔ x ∈ S

Proof state:
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : NonUnitalSemiring A
inst✝² : StarRing A
inst✝¹ : Module R A
inst✝ : StarModule R A
S : NonUnitalSubalgebra R A
x : A
⊢ star x ∈ star S ↔ x ∈ S

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem or_self (x : Nat) : x ||| x = x

Proof state:
x : Nat
⊢ x ||| x = x

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
x : Nat
⊢ ∀ (i : Nat), (x ||| x).testBit i = x.testBit i

Proof state:
case pred
x : Nat
⊢ ∀ (i : Nat), (x ||| x).testBit i = x.testBit i

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_univ_two [CommMonoid β] (f : Fin 2 → β) : ∏ i, f i = f 0 * f 1

Proof state:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 2 → β
⊢ ∏ i : Fin 2, f i = f 0 * f 1

Tactic:
simp [prod_univ_succ]

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_smul_non_comm [Star R] [Star α] [SMul R α] [SMul Rᵐᵒᵖ α] (c : R)
    (M : Matrix m n α) (h : ∀ (r : R) (a : α), star (r • a) = MulOpposite.op (star r) • star a) :
    (c • M)ᴴ = MulOpposite.op (star c) • Mᴴ :=
  Matrix.ext <| by simp [h]

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : Star R
inst✝² : Star α
inst✝¹ : SMul R α
inst✝ : SMul Rᵐᵒᵖ α
c : R
M : Matrix m n α
h : ∀ (r : R) (a : α), star (r • a) = MulOpposite.op (star r) • star a
⊢ ∀ (i : n) (j : m), (c • M)ᴴ i j = (MulOpposite.op (star c) • Mᴴ) i j

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem swap_eq_gt {o : Ordering} : o.swap = .gt ↔ o = .lt

Proof state:
o : Ordering
⊢ o.swap = gt ↔ o = lt

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousOn_singleton (f : α → β) (a : α) : ContinuousOn f {a} :=
  forall_eq.2 <| by
    simpa only [ContinuousWithinAt, nhdsWithin_singleton, tendsto_pure_left] using fun s =>
      mem_of_mem_nhds

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
a : α
⊢ ContinuousWithinAt f {a} a

Tactic:
simpa only [ContinuousWithinAt, nhdsWithin_singleton, tendsto_pure_left] using fun s =>
  mem_of_mem_nhds

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
/-- While in many cases `finCongr` is better than `Equiv.cast`/`cast`, sometimes we want to apply
a generic theorem about `cast`. -/
lemma _root_.finCongr_eq_equivCast (h : n = m) : finCongr h = .cast (h ▸ rfl)

Proof state:
n : ℕ
⊢ finCongr ⋯ = Equiv.cast ⋯

Tactic:
simp

Result:
no goals

Proof state:
n m : ℕ
h : n = m
⊢ finCongr h = Equiv.cast ⋯

Tactic:
subst h

Result:
n : ℕ
⊢ finCongr ⋯ = Equiv.cast ⋯
-- Mathlib/.lake/packages/batteries/Batteries/Data/ByteArray.lean
theorem get_extract_aux {a : ByteArray} {start stop} (h : i < (a.extract start stop).size) :
    start + i < a.size

Proof state:
case a
i : Nat
a : ByteArray
start stop : Nat
h : i < (a.extract start stop).size
⊢ min (stop - start) (a.size - start) ≤ a.size - start

Tactic:
exact Nat.min_le_right ..

Result:
no goals

Proof state:
case a
i : Nat
a : ByteArray
start stop : Nat
h : i < (a.extract start stop).size
⊢ (a.extract start stop).size ≤ a.size - start

Tactic:
rw [size_extract, ← Nat.sub_min_sub_right]

Result:
case a
i : Nat
a : ByteArray
start stop : Nat
h : i < (a.extract start stop).size
⊢ min (stop - start) (a.size - start) ≤ a.size - start

Proof state:
case a
i : Nat
a : ByteArray
start stop : Nat
h : i < (a.extract start stop).size
⊢ i < a.size - start

Tactic:
apply Nat.lt_of_lt_of_le h

Result:
case a
i : Nat
a : ByteArray
start stop : Nat
h : i < (a.extract start stop).size
⊢ (a.extract start stop).size ≤ a.size - start

Proof state:
i : Nat
a : ByteArray
start stop : Nat
h : i < (a.extract start stop).size
⊢ start + i < a.size

Tactic:
apply Nat.add_lt_of_lt_sub'

Result:
case a
i : Nat
a : ByteArray
start stop : Nat
h : i < (a.extract start stop).size
⊢ i < a.size - start