harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
theorem adjointAux_inner (y : T.adjointDomain) (x : T.domain) :
    ⟪adjointAux hT y, x⟫ = ⟪(y : F), T x⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : ↥T.adjointDomain
x : ↥T.domain
⊢ (adjointDomainMkCLMExtend hT y) ↑x = inner (↑y) (↑T x)

Tactic:
rw [adjointDomainMkCLMExtend_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : ↥T.adjointDomain
x : ↥T.domain
⊢ inner ((adjointAux hT) y) ↑x = inner (↑y) (↑T x)

Tactic:
simp only [adjointAux, LinearMap.coe_mk, InnerProductSpace.toDual_symm_apply,
  adjointDomainMkCLMExtend_apply]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : ↥T.adjointDomain
x : ↥T.domain
⊢ inner ({ toFun := fun y => (InnerProductSpace.toDual 𝕜 E).symm (adjointDomainMkCLMExtend hT y), map_add' := ⋯ } y)
      ↑x =
    inner (↑y) (↑T x)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : ↥T.adjointDomain
x : ↥T.domain
⊢ inner ({ toFun := fun y => (InnerProductSpace.toDual 𝕜 E).symm (adjointDomainMkCLMExtend hT y), map_add' := ⋯ } y)
      ↑x =
    inner (↑y) (↑T x)

Tactic:
simp only [AddHom.coe_mk, InnerProductSpace.toDual_symm_apply]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : ↥T.adjointDomain
x : ↥T.domain
⊢ (adjointDomainMkCLMExtend hT y) ↑x = inner (↑y) (↑T x)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
theorem Bool.and_to_and (a b : Bool) : ((a = true) ∧ (b = true)) = ((a && b) = true)

Proof state:
a b : Bool
⊢ (a = true ∧ b = true) = ((a && b) = true)

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- The cardinality of the set of `k`-smooth numbers `≤ N` is bounded by `2^π(k-1) * √N`. -/
lemma smoothNumbersUpTo_card_le (N k : ℕ) :
    (smoothNumbersUpTo N k).card ≤ 2 ^ k.primesBelow.card * N.sqrt

Proof state:
N k : ℕ
⊢ (N.smoothNumbersUpTo k).card ≤ 2 ^ k.primesBelow.card * N.sqrt

Tactic:
convert (Finset.card_le_card <| smoothNumbersUpTo_subset_image N k).trans <|
  Finset.card_image_le

Result:
case h.e'_4
N k : ℕ
⊢ 2 ^ k.primesBelow.card * N.sqrt = (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0).card

Proof state:
case h.e'_4
N k : ℕ
⊢ 2 ^ k.primesBelow.card * N.sqrt = (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0).card

Tactic:
simp only [Finset.card_product, Finset.card_powerset, Finset.mem_range, zero_lt_succ,
  Finset.card_erase_of_mem, Finset.card_range, succ_sub_succ_eq_sub, tsub_zero]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- For `x ≤ 0` the defining sum diverges, so the kernel is 0. -/
lemma evenKernel_undef (a : UnitAddCircle) {x : ℝ} (hx : x ≤ 0) : evenKernel a x = 0

Proof state:
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ (I * ↑x).im ≤ 0

Tactic:
simpa

Result:
no goals

Proof state:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ evenKernel a x = 0

Tactic:
induction a using QuotientAddGroup.induction_on with
| H a' => simp [← ofReal_inj, evenKernel_def, jacobiTheta₂_undef _ (by simpa : (I * ↑x).im ≤ 0)]

Result:
no goals

Proof state:
case H
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ evenKernel (↑a') x = 0

Tactic:
simp [← ofReal_inj, evenKernel_def, jacobiTheta₂_undef _ (by simpa : (I * ↑x).im ≤ 0)]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem gcd_zero_left (i : ℤ) : gcd 0 i = natAbs i

Proof state:
i : ℤ
⊢ gcd 0 i = i.natAbs

Tactic:
simp [gcd]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma cyclesMap'_neg :
    cyclesMap' (-φ) h₁ h₂ = -cyclesMap' φ h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ cyclesMap' (-φ) h₁ h₂ = -cyclesMap' φ h₁ h₂

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ cyclesMap' (-φ) h₁ h₂ = -cyclesMap' φ h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ cyclesMap' (-φ) h₁ h₂ = -cyclesMap' φ h₁ h₂

Tactic:
simp only [γ.cyclesMap'_eq, γ.neg.cyclesMap'_eq, LeftHomologyMapData.neg_φK]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem GoodProducts.linearIndependentAux (μ : Ordinal) : P I μ

Proof state:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ : Ordinal.{u}
⊢ P I μ

Tactic:
refine Ordinal.limitRecOn μ P0 (fun o h ho C hC hsC ↦ ?_)
    (fun o ho h ↦ (GoodProducts.Plimit o ho (fun o' ho' ↦ (h o' ho'))))

Result:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : Order.succ o ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (Order.succ o)
⊢ LinearIndependent ℤ (eval C)

Proof state:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : Order.succ o ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (Order.succ o)
ho' : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ LinearIndependent ℤ (eval C)

Tactic:
rw [linearIndependent_iff_sum C hsC ho']

Result:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : Order.succ o ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (Order.succ o)
ho' : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ LinearIndependent ℤ (SumEval C ho')

Proof state:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : Order.succ o ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (Order.succ o)
ho' : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ LinearIndependent ℤ (SumEval C ho')

Tactic:
refine ModuleCat.linearIndependent_leftExact (succ_exact C hC hsC ho') ?_ ?_ (succ_mono C o)
  (square_commutes C ho')

Result:
case refine_1
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : Order.succ o ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (Order.succ o)
ho' : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ LinearIndependent (ι := ↑(GoodProducts (π C fun x => ord I x < o))) ℤ (eval (π C fun x => ord I x < o))

case refine_2
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : Order.succ o ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (Order.succ o)
ho' : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ LinearIndependent (ι := ↑(MaxProducts C ho')) ℤ
    (⇑(ConcreteCategory.hom (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho')) ⋯).g) ∘
      SumEval C ho' ∘ Sum.inr)
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem mem_map_of_equiv {E : Type*} [EquivLike E R S] [RingEquivClass E R S] (e : E)
    {I : Ideal R} (y : S) : y ∈ map e I ↔ ∃ x ∈ I, e x = y

Proof state:
case mpr
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ (∃ x ∈ I, e x = y) → y ∈ map e I

Tactic:
rintro ⟨x, hx, rfl⟩

Result:
case mpr.intro.intro
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
x : R
hx : x ∈ I
⊢ e x ∈ map e I

Proof state:
case mp
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ y ∈ map e I → ∃ x ∈ I, e x = y

Tactic:
intro h

Result:
case mp
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
h : y ∈ map e I
⊢ ∃ x ∈ I, e x = y

Proof state:
case mpr.intro.intro
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
x : R
hx : x ∈ I
⊢ e x ∈ map e I

Tactic:
exact mem_map_of_mem e hx

Result:
no goals

Proof state:
case mp
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
h : y ∈ comap (↑e).symm I
⊢ ∃ x ∈ I, e x = y

Tactic:
exact ⟨(e : R ≃+* S).symm y, h, (e : R ≃+* S).apply_symm_apply y⟩

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ y ∈ map e I ↔ ∃ x ∈ I, e x = y

Tactic:
constructor

Result:
case mp
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ y ∈ map e I → ∃ x ∈ I, e x = y

case mpr
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ (∃ x ∈ I, e x = y) → y ∈ map e I

Proof state:
case mp
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
h : y ∈ map e I
⊢ ∃ x ∈ I, e x = y

Tactic:
simp_rw [show map e I = _ from map_comap_of_equiv (e : R ≃+* S)] at h

Result:
case mp
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
h : y ∈ comap (↑e).symm I
⊢ ∃ x ∈ I, e x = y
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem deleteVerts_empty : G'.deleteVerts ∅ = G'

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.deleteVerts ∅ = G'

Tactic:
simp [deleteVerts]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Girth.lean
lemma exists_girth_eq_length :
    (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length) ↔ ¬ G.IsAcyclic

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ (∃ a w, w.IsCycle ∧ G.girth = w.length) → ¬G.IsAcyclic

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ (∃ a w, w.IsCycle ∧ G.girth = w.length) ↔ ¬G.IsAcyclic

Tactic:
refine ⟨by tauto, fun h ↦ ?_⟩

Result:
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
⊢ ∃ a w, w.IsCycle ∧ G.girth = w.length

Proof state:
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
⊢ ∃ a w, w.IsCycle ∧ G.girth = w.length

Tactic:
obtain ⟨_, _, _⟩ := exists_egirth_eq_length.mpr h

Result:
case intro.intro
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
w✝¹ : α
w✝ : G.Walk w✝¹ w✝¹
h✝ : w✝.IsCycle ∧ G.egirth = ↑w✝.length
⊢ ∃ a w, w.IsCycle ∧ G.girth = w.length

Proof state:
case intro.intro
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
w✝¹ : α
w✝ : G.Walk w✝¹ w✝¹
h✝ : w✝.IsCycle ∧ G.egirth = ↑w✝.length
⊢ ∃ a w, w.IsCycle ∧ G.girth = w.length

Tactic:
simp_all only [girth, ENat.toNat_coe]

Result:
case intro.intro
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
w✝¹ : α
w✝ : G.Walk w✝¹ w✝¹
h✝ : w✝.IsCycle ∧ G.egirth = ↑w✝.length
⊢ ∃ a w, w.IsCycle ∧ w✝.length = w.length

Proof state:
case intro.intro
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
w✝¹ : α
w✝ : G.Walk w✝¹ w✝¹
h✝ : w✝.IsCycle ∧ G.egirth = ↑w✝.length
⊢ ∃ a w, w.IsCycle ∧ w✝.length = w.length

Tactic:
tauto

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem pure_prod {a : α} {f : Filter β} : pure a ×ˢ f = map (Prod.mk a) f

Proof state:
α : Type u_1
β : Type u_2
a : α
f : Filter β
⊢ pure a ×ˢ f = map (Prod.mk a) f

Tactic:
rw [prod_eq, map_pure, pure_seq_eq_map]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_le_inv_mul₀ (ha : 0 < a) : 1 ≤ a⁻¹ * b ↔ a ≤ b

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : PosMulMono G₀
ha : 0 < a
⊢ 1 ≤ a⁻¹ * b ↔ a ≤ b

Tactic:
rw [le_inv_mul_iff₀ ha, mul_one]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Strong.lean
theorem whiskerLeft_naturality_naturality (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) :
    f ◁ G.map₂ β ▷ θ.app b ≫ f ◁ (θ.naturality h).hom =
      f ◁ (θ.naturality g).hom ≫ f ◁ θ.app a ◁ H.map₂ β

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
G H : OplaxFunctor B C
θ : StrongOplaxNatTrans G H
a b : B
a' : C
f : a' ⟶ G.obj a
g h : a ⟶ b
β : g ⟶ h
⊢ f ◁ G.map₂ β ▷ θ.app b ≫ f ◁ (θ.naturality h).hom = f ◁ (θ.naturality g).hom ≫ f ◁ θ.app a ◁ H.map₂ β

Tactic:
apply θ.toOplax.whiskerLeft_naturality_naturality

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
@[simp]
lemma leadingCoeff_eq_zero (hD : D.Injective) : p.leadingCoeff D = 0 ↔ p = 0

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
h : ¬p = 0
⊢ ¬leadingCoeff D p = 0

Tactic:
rw [leadingCoeff, ← Ne, ← Finsupp.mem_support_iff]

Result:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
h : ¬p = 0
⊢ Function.invFun D (supDegree D p) ∈ p.support

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
h : ¬p = 0
⊢ Function.invFun D (supDegree D p) ∈ p.support

Tactic:
exact supDegree_mem_support hD h

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
⊢ leadingCoeff D p = 0 ↔ p = 0

Tactic:
refine ⟨(fun h => ?_).mtr, fun h => h ▸ leadingCoeff_zero⟩

Result:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
h : ¬p = 0
⊢ ¬leadingCoeff D p = 0
-- Mathlib/Data/Real/Sign.lean
theorem sign_apply_eq (r : ℝ) : sign r = -1 ∨ sign r = 0 ∨ sign r = 1

Proof state:
case inr.inl

⊢ sign 0 = -1 ∨ sign 0 = 0 ∨ sign 0 = 1

Tactic:
exact Or.inr <| Or.inl <| sign_zero

Result:
no goals

Proof state:
r : ℝ
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

Tactic:
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)

Result:
case inl
r : ℝ
hn : r < 0
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

case inr.inl

⊢ sign 0 = -1 ∨ sign 0 = 0 ∨ sign 0 = 1

case inr.inr
r : ℝ
hp : 0 < r
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

Proof state:
case inr.inr
r : ℝ
hp : 0 < r
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

Tactic:
exact Or.inr <| Or.inr <| sign_of_pos hp

Result:
no goals

Proof state:
case inl
r : ℝ
hn : r < 0
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

Tactic:
exact Or.inl <| sign_of_neg hn

Result:
no goals
-- Mathlib/Data/List/Zip.lean
theorem zip_swap : ∀ (l₁ : List α) (l₂ : List β), (zip l₁ l₂).map Prod.swap = zip l₂ l₁
  | [], _ => zip_nil_right.symm
  | l₁, [] => by rw [zip_nil_right]; rfl
  | a :: l₁, b :: l₂ => by
    simp only [zip_cons_cons, map_cons, zip_swap l₁ l₂, Prod.swap_prod_mk]

Proof state:
α : Type u
β : Type u_1
l₁ : List α
⊢ map Prod.swap (l₁.zip []) = [].zip l₁

Tactic:
rw [zip_nil_right]

Result:
α : Type u
β : Type u_1
l₁ : List α
⊢ map Prod.swap [] = [].zip l₁

Proof state:
α : Type u
β : Type u_1
a : α
l₁ : List α
b : β
l₂ : List β
⊢ map Prod.swap ((a :: l₁).zip (b :: l₂)) = (b :: l₂).zip (a :: l₁)

Tactic:
simp only [zip_cons_cons, map_cons, zip_swap l₁ l₂, Prod.swap_prod_mk]

Result:
no goals

Proof state:
α : Type u
β : Type u_1
l₁ : List α
⊢ map Prod.swap [] = [].zip l₁

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/Torsion.lean
theorem not_isTorsionFree_iff : ¬IsTorsionFree G ↔ ∃ g : G, g ≠ 1 ∧ IsOfFinOrder g

Proof state:
G : Type u_1
inst✝ : Monoid G
⊢ ¬IsTorsionFree G ↔ ∃ g, g ≠ 1 ∧ IsOfFinOrder g

Tactic:
simp_rw [IsTorsionFree, Ne, not_forall, Classical.not_not, exists_prop]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem withTopEquiv_top : withTopEquiv ⊤ = ⊤

Proof state:
⊢ withTopEquiv ⊤ = ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem uniformOfFintype_apply (a : α) : uniformOfFintype α a = (Fintype.card α : ℝ≥0∞)⁻¹

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
a : α
⊢ (uniformOfFintype α) a = (↑(Fintype.card α))⁻¹

Tactic:
simp [uniformOfFintype, Finset.mem_univ, if_true, uniformOfFinset_apply]

Result:
no goals
-- Mathlib/GroupTheory/DoubleCoset.lean
theorem left_bot_eq_left_quot (H : Subgroup G) :
    Quotient (⊥ : Subgroup G) (H : Set G) = (G ⧸ H)

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Quotient ↑⊥ ↑H = (G ⧸ H)

Tactic:
unfold Quotient

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ _root_.Quotient (setoid ↑⊥ ↑H) = (G ⧸ H)

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ _root_.Quotient (setoid ↑⊥ ↑H) = (G ⧸ H)

Tactic:
congr

Result:
case e_s
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ setoid ↑⊥ ↑H = QuotientGroup.leftRel H

Proof state:
case e_s.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : G
⊢ (setoid ↑⊥ ↑H) a✝ b✝ ↔ (QuotientGroup.leftRel H) a✝ b✝

Tactic:
simp_rw [← bot_rel_eq_leftRel H]

Result:
no goals

Proof state:
case e_s
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ setoid ↑⊥ ↑H = QuotientGroup.leftRel H

Tactic:
ext

Result:
case e_s.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : G
⊢ (setoid ↑⊥ ↑H) a✝ b✝ ↔ (QuotientGroup.leftRel H) a✝ b✝
-- Mathlib/CategoryTheory/Sites/Sieves.lean
lemma ofArrows_eq_ofObjects {X : C} (hX : IsTerminal X)
    {I : Type*} (Y : I → C) (f : ∀ i, Y i ⟶ X) :
    ofArrows Y f = ofObjects Y X

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
f : (i : I) → Y i ⟶ X
⊢ ofArrows Y f = ofObjects Y X

Tactic:
refine le_antisymm (ofArrows_le_ofObjects Y f) (fun W g => ?_)

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (ofObjects Y X).arrows g → (ofArrows Y f).arrows g

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (ofObjects Y X).arrows g → (ofArrows Y f).arrows g

Tactic:
rw [mem_ofArrows_iff, mem_ofObjects_iff]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (∃ i, Nonempty (W ⟶ Y i)) → ∃ i a, g = a ≫ f i

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (∃ i, Nonempty (W ⟶ Y i)) → ∃ i a, g = a ≫ f i

Tactic:
rintro ⟨i, ⟨h⟩⟩

Result:
case intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
i : I
h : W ⟶ Y i
⊢ ∃ i a, g = a ≫ f i

Proof state:
case intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
i : I
h : W ⟶ Y i
⊢ ∃ i a, g = a ≫ f i

Tactic:
exact ⟨i, h, hX.hom_ext _ _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVec.lean
theorem get_cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (idx : Nat) (hidx : idx < len)
    (hcast : aig1.decls.size ≤ aig2.decls.size) :
    (s.cast hcast).get idx hidx
      =
    (s.get idx hidx).cast hcast

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig1 aig2 : AIG α
s : aig1.RefVec len
idx : Nat
hidx : idx < len
hcast : aig1.decls.size ≤ aig2.decls.size
⊢ (s.cast hcast).get idx hidx = (s.get idx hidx).cast hcast

Tactic:
simp [cast, cast', get]

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

Proof state:
w : Nat
x y : BitVec w
⊢ -x * -y = x * y

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Induced.lean
@[simp]
lemma zero_hom_app_obj (X : C) :
    (zero F s i).hom.app (F.obj X) =
      (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)

Proof state:
C : Type u_5
D : Type u_2
inst✝⁵ : Category.{u_4, u_5} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
h :
  whiskerLeft F (zero F s i).hom =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).hom
⊢ (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).hom.app X =
    (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_5
D : Type u_2
inst✝⁵ : Category.{u_4, u_5} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
h :
  whiskerLeft F (zero F s i).hom =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).hom
⊢ (zero F s i).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)

Tactic:
exact (NatTrans.congr_app h X).trans (by simp)

Result:
no goals

Proof state:
C : Type u_5
D : Type u_2
inst✝⁵ : Category.{u_4, u_5} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
⊢ (zero F s i).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)

Tactic:
have h : whiskerLeft F (zero F s i).hom = _ :=
  ((whiskeringLeft C D D).obj F).map_preimage _

Result:
C : Type u_5
D : Type u_2
inst✝⁵ : Category.{u_4, u_5} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
h :
  whiskerLeft F (zero F s i).hom =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).hom
⊢ (zero F s i).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)