harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
@[reassoc]
lemma homEquiv_comp (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃) :
    (homEquiv V) (f ≫ g) = (λ_ (𝟙_ V)).inv ≫ ((homEquiv V) f ⊗ (homEquiv V) g) ≫
    enrichedComp V F₁ F₂ F₃

Proof state:
case h
V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
⊢ (homEquiv V) (f ≫ g) ≫ end_.π (diagram V F₁ F₃) j =
    ((λ_ (𝟙_ V)).inv ≫ ((homEquiv V) f ⊗ (homEquiv V) g) ≫ enrichedComp V F₁ F₂ F₃) ≫ end_.π (diagram V F₁ F₃) j

Tactic:
simp only [homEquiv_apply_π, NatTrans.comp_app, eHomEquiv_comp, assoc,
  enrichedComp_π, Functor.op_obj, ← tensor_comp_assoc]

Result:
no goals

Proof state:
V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
⊢ (homEquiv V) (f ≫ g) = (λ_ (𝟙_ V)).inv ≫ ((homEquiv V) f ⊗ (homEquiv V) g) ≫ enrichedComp V F₁ F₂ F₃

Tactic:
ext j

Result:
case h
V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
⊢ (homEquiv V) (f ≫ g) ≫ end_.π (diagram V F₁ F₃) j =
    ((λ_ (𝟙_ V)).inv ≫ ((homEquiv V) f ⊗ (homEquiv V) g) ≫ enrichedComp V F₁ F₂ F₃) ≫ end_.π (diagram V F₁ F₃) j
-- Mathlib/Data/Real/Sign.lean
theorem sign_intCast (z : ℤ) : sign (z : ℝ) = ↑(Int.sign z)

Proof state:
case inl
z : ℤ
hn : z < 0
⊢ (↑z).sign = ↑z.sign

Tactic:
rw [sign_of_neg (Int.cast_lt_zero.mpr hn), Int.sign_eq_neg_one_of_neg hn, Int.cast_neg,
  Int.cast_one]

Result:
no goals

Proof state:
case inr.inl

⊢ (↑0).sign = ↑(Int.sign 0)

Tactic:
rw [Int.cast_zero, sign_zero, Int.sign_zero, Int.cast_zero]

Result:
no goals

Proof state:
z : ℤ
⊢ (↑z).sign = ↑z.sign

Tactic:
obtain hn | rfl | hp := lt_trichotomy z (0 : ℤ)

Result:
case inl
z : ℤ
hn : z < 0
⊢ (↑z).sign = ↑z.sign

case inr.inl

⊢ (↑0).sign = ↑(Int.sign 0)

case inr.inr
z : ℤ
hp : 0 < z
⊢ (↑z).sign = ↑z.sign

Proof state:
case inr.inr
z : ℤ
hp : 0 < z
⊢ (↑z).sign = ↑z.sign

Tactic:
rw [sign_of_pos (Int.cast_pos.mpr hp), Int.sign_eq_one_of_pos hp, Int.cast_one]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma supClosure_empty : supClosure (∅ : Set α) = ∅

Proof state:
α : Type u_3
inst✝ : SemilatticeSup α
⊢ supClosure ∅ = ∅

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem _root_.ContinuousMultilinearMap.integral_apply {ι : Type*} [Fintype ι] {M : ι → Type*}
    [∀ i, NormedAddCommGroup (M i)] [∀ i, NormedSpace 𝕜 (M i)]
    {φ : X → ContinuousMultilinearMap 𝕜 M E} (φ_int : Integrable φ μ) (m : ∀ i, M i) :
    (∫ x, φ x ∂μ) m = ∫ x, φ x m ∂μ

Proof state:
case neg
X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace ℝ E
ι : Type u_6
inst✝² : Fintype ι
M : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
hE : ¬CompleteSpace E
⊢ (∫ (x : X), φ x ∂μ) m = ∫ (x : X), (φ x) m ∂μ

Tactic:
by_cases hm : ∀ i, m i ≠ 0

Result:
case pos
X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace ℝ E
ι : Type u_6
inst✝² : Fintype ι
M : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
hE : ¬CompleteSpace E
hm : ∀ (i : ι), m i ≠ 0
⊢ (∫ (x : X), φ x ∂μ) m = ∫ (x : X), (φ x) m ∂μ

case neg
X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace ℝ E
ι : Type u_6
inst✝² : Fintype ι
M : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
hE : ¬CompleteSpace E
hm : ¬∀ (i : ι), m i ≠ 0
⊢ (∫ (x : X), φ x ∂μ) m = ∫ (x : X), (φ x) m ∂μ
-- Mathlib/Data/Multiset/Fintype.lean
theorem toEnumFinset_mono {m₁ m₂ : Multiset α} (h : m₁ ≤ m₂) :
    m₁.toEnumFinset ⊆ m₂.toEnumFinset

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p ∈ m₁.toEnumFinset → p ∈ m₂.toEnumFinset

Tactic:
simp only [Multiset.mem_toEnumFinset]

Result:
α : Type u_1
inst✝ : DecidableEq α
m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p.2 < count p.1 m₁ → p.2 < count p.1 m₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p.2 < count p.1 m₁ → p.2 < count p.1 m₂

Tactic:
exact gt_of_ge_of_gt (Multiset.le_iff_count.mp h p.1)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m₁ m₂ : Multiset α
h : m₁ ≤ m₂
⊢ m₁.toEnumFinset ⊆ m₂.toEnumFinset

Tactic:
intro p

Result:
α : Type u_1
inst✝ : DecidableEq α
m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p ∈ m₁.toEnumFinset → p ∈ m₂.toEnumFinset
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem takeList_eq_takeListTR : @takeList = @takeListTR

Proof state:
α : Type u_1
xs✝ : List α
ns✝ : List Nat
acc : Array (List α)
n : Nat
ns : List Nat
xs : List α
⊢ takeListTR.go (n :: ns) xs acc =
    match xs.takeList (n :: ns) with
    | (l, r) => (acc.toList ++ l, r)

Tactic:
simp [takeListTR.go, takeList, go _ ns]

Result:
no goals

Proof state:
case h.h.h
α : Type u_1
xs : List α
ns : List Nat
⊢ xs.takeList ns = xs.takeListTR ns

Tactic:
simp [takeListTR]

Result:
case h.h.h
α : Type u_1
xs : List α
ns : List Nat
⊢ xs.takeList ns = takeListTR.go ns xs #[]

Proof state:
case h.h.h
α : Type u_1
xs : List α
ns : List Nat
⊢ xs.takeList ns = takeListTR.go ns xs #[]

Tactic:
simp [takeListTR, go]

Result:
no goals

Proof state:
α : Type u_1
xs✝ : List α
ns : List Nat
acc : Array (List α)
xs : List α
⊢ takeListTR.go [] xs acc =
    match xs.takeList [] with
    | (l, r) => (acc.toList ++ l, r)

Tactic:
simp [takeListTR.go, takeList]

Result:
no goals

Proof state:
⊢ @takeList = @takeListTR

Tactic:
funext α xs ns

Result:
case h.h.h
α : Type u_1
xs : List α
ns : List Nat
⊢ xs.takeList ns = xs.takeListTR ns
-- Mathlib/Algebra/CharP/Defs.lean
lemma not_char_dvd (p : ℕ) [CharP R p] (k : ℕ) [h : NeZero (k : R)] : ¬p ∣ k

Proof state:
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
k : ℕ
h : NeZero ↑k
⊢ ¬p ∣ k

Tactic:
rwa [← CharP.cast_eq_zero_iff R p k, ← Ne, ← neZero_iff]

Result:
no goals
-- Mathlib/Data/Rat/Cast/CharZero.lean
@[simp]
lemma cast_divNat (a b : ℕ) : (divNat a b : α) = a / b

Proof state:
case e_a.a
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ ↑(divNat a b) = ↑(↑a / ↑b)

Tactic:
apply Rat.mkRat_eq_div

Result:
no goals

Proof state:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ ↑(divNat a b) = ↑(↑a / ↑b)

Tactic:
congr

Result:
case e_a
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ divNat a b = ↑a / ↑b

Proof state:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ ↑(divNat a b) = ↑a / ↑b

Tactic:
rw [← cast_natCast, ← cast_natCast b, ← cast_div]

Result:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ ↑(divNat a b) = ↑(↑a / ↑b)

Proof state:
case e_a
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ divNat a b = ↑a / ↑b

Tactic:
ext

Result:
case e_a.a
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ ↑(divNat a b) = ↑(↑a / ↑b)
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.congr (hf : ConvexOn 𝕜 s f) (hfg : EqOn f g s) : ConvexOn 𝕜 s g :=
  ⟨hf.1, fun x hx y hy a b ha hb hab => by
    simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha hb hab)] using hf.2 hx hy ha hb hab⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hfg : EqOn f g s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ g (a • x + b • y) ≤ a • g x + b • g y

Tactic:
simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha hb hab)] using hf.2 hx hy ha hb hab

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_inj_right {f : α → β} (w : ∀ x y, f x = f y → x = y) : map f l = map f l' ↔ l = l'

Proof state:
α : Type u_1
β : Type u_2
n✝ : Nat
l l' : Vector α n✝
f : α → β
w : ∀ (x y : α), f x = f y → x = y
⊢ map f l = map f l' ↔ l = l'

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
n✝ : Nat
l' : Vector α n✝
f : α → β
w : ∀ (x y : α), f x = f y → x = y
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n✝
⊢ map f { toArray := toArray✝, size_toArray := size_toArray✝ } = map f l' ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } = l'

Proof state:
case mk
α : Type u_1
β : Type u_2
n✝ : Nat
l' : Vector α n✝
f : α → β
w : ∀ (x y : α), f x = f y → x = y
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n✝
⊢ map f { toArray := toArray✝, size_toArray := size_toArray✝ } = map f l' ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } = l'

Tactic:
cases l'

Result:
case mk.mk
α : Type u_1
β : Type u_2
n✝ : Nat
f : α → β
w : ∀ (x y : α), f x = f y → x = y
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n✝
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n✝
⊢ map f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } =
      map f { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
n✝ : Nat
f : α → β
w : ∀ (x y : α), f x = f y → x = y
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n✝
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n✝
⊢ map f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } =
      map f { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp [Array.map_inj_right w]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem mem_rootSet_of_injective [CommRing S] {p : S[X]} [Algebra S R]
    (h : Function.Injective (algebraMap S R)) {x : R} (hp : p ≠ 0) :
    x ∈ p.rootSet R ↔ aeval x p = 0

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
p : S[X]
inst✝ : Algebra S R
h : Function.Injective ⇑(algebraMap S R)
x : R
hp : p ≠ 0
⊢ x ∈ p.rootSet R ↔ (aeval x) p = 0

Tactic:
classical
exact Multiset.mem_toFinset.trans (mem_roots_map_of_injective h hp)

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
p : S[X]
inst✝ : Algebra S R
h : Function.Injective ⇑(algebraMap S R)
x : R
hp : p ≠ 0
⊢ x ∈ p.rootSet R ↔ (aeval x) p = 0

Tactic:
exact Multiset.mem_toFinset.trans (mem_roots_map_of_injective h hp)

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem shiftLeft_coe_nat (m n : ℕ) : (m : ℤ) <<< (n : ℤ) = ↑(m <<< n)

Proof state:
m n : ℕ
⊢ (match ↑m, ↑n with
    | ofNat m, ofNat n => ↑(Nat.shiftLeft' false m n)
    | ofNat m, -[n+1] => ↑(m.shiftRight n.succ)
    | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    ↑(m.shiftLeft n)

Tactic:
simp

Result:
no goals

Proof state:
m n : ℕ
⊢ ↑m <<< ↑n = ↑(m <<< n)

Tactic:
unfold_projs

Result:
m n : ℕ
⊢ (match ↑m, ↑n with
    | ofNat m, ofNat n => ↑(Nat.shiftLeft' false m n)
    | ofNat m, -[n+1] => ↑(m.shiftRight n.succ)
    | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    ↑(m.shiftLeft n)
-- Mathlib/RingTheory/Binomial.lean
theorem choose_zero_right [NatPowAssoc R] (r : R) : choose r 0 = 1

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
⊢ choose r 0 = 1

Tactic:
rw [choose_zero_right', npow_zero]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_mul {p a b : α} (hp : Prime p) :
    emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Tactic:
by_cases hfin : FiniteMultiplicity p (a * b)

Result:
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Proof state:
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Tactic:
exact multiplicity_mul hp hfin

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ ¬FiniteMultiplicity p a ∨ ¬FiniteMultiplicity p b

Tactic:
simpa only [FiniteMultiplicity.mul_iff hp, not_and_or] using hfin

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Tactic:
rw [emultiplicity_eq_top.2 hfin, eq_comm, WithTop.add_eq_top, emultiplicity_eq_top,
  emultiplicity_eq_top]

Result:
case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ ¬FiniteMultiplicity p a ∨ ¬FiniteMultiplicity p b

Proof state:
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Tactic:
rw [hfin.emultiplicity_eq_multiplicity, hfin.mul_left.emultiplicity_eq_multiplicity,
  hfin.mul_right.emultiplicity_eq_multiplicity]

Result:
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ ↑(multiplicity p (a * b)) = ↑(multiplicity p a) + ↑(multiplicity p b)

Proof state:
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ ↑(multiplicity p (a * b)) = ↑(multiplicity p a) + ↑(multiplicity p b)

Tactic:
norm_cast

Result:
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lTensor_refl_apply : (refl R N).lTensor M x = x

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
⊢ (lTensor M (refl R N)) x = x

Tactic:
rw [lTensor_refl, refl_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.of_le_eq_false (u v : Nat) : ((u ≤ v) = False) → v + 1 ≤ u

Proof state:
u v : Nat
⊢ v < u → v + 1 ≤ u

Tactic:
omega

Result:
no goals

Proof state:
u v : Nat
⊢ (u ≤ v) = False → v + 1 ≤ u

Tactic:
simp

Result:
u v : Nat
⊢ v < u → v + 1 ≤ u
-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem fst_isEmbedding_of_right {X Y S : TopCat} (f : X ⟶ S) {g : Y ⟶ S}
    (H : IsEmbedding g) : IsEmbedding <| ⇑(pullback.fst f g)

Proof state:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom g)
⊢ g ≫ 𝟙 S = g ≫ 𝟙 S

Tactic:
simp

Result:
no goals

Proof state:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom g)
⊢ IsEmbedding ⇑(ConcreteCategory.hom (pullback.fst f g))

Tactic:
convert (homeoOfIso (asIso (pullback.fst f (𝟙 S)))).isEmbedding.comp
    (pullback_map_isEmbedding (i₁ := 𝟙 X)
      f g f (𝟙 _) (homeoOfIso (Iso.refl _)).isEmbedding H (𝟙 _) rfl (by simp))

Result:
case h.e'_5
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom g)
⊢ ⇑(ConcreteCategory.hom (pullback.fst f g)) =
    ⇑(homeoOfIso (asIso (pullback.fst f (𝟙 S)))) ∘ ⇑(ConcreteCategory.hom (pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) ⋯ ⋯))

Proof state:
case h.e'_5
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom g)
⊢ ⇑(ConcreteCategory.hom (pullback.fst f g)) =
    ⇑(homeoOfIso (asIso (pullback.fst f (𝟙 S)))) ∘ ⇑(ConcreteCategory.hom (pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) ⋯ ⋯))

Tactic:
simp [homeoOfIso, ← coe_comp]

Result:
no goals
-- Mathlib/Order/PrimeIdeal.lean
theorem IsPrime.mem_or_mem (hI : IsPrime I) {x y : P} : x ⊓ y ∈ I → x ∈ I ∨ y ∈ I

Proof state:
P : Type u_1
inst✝ : SemilatticeInf P
I : Ideal P
hI : I.IsPrime
x y : P
⊢ x ⊓ y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
contrapose!

Result:
P : Type u_1
inst✝ : SemilatticeInf P
I : Ideal P
hI : I.IsPrime
x y : P
⊢ x ∉ I ∧ y ∉ I → x ⊓ y ∉ I

Proof state:
P : Type u_1
inst✝ : SemilatticeInf P
I : Ideal P
hI : I.IsPrime
x y : P
⊢ x ∉ I ∧ y ∉ I → x ⊓ y ∉ I

Tactic:
let F := hI.compl_filter.toPFilter

Result:
P : Type u_1
inst✝ : SemilatticeInf P
I : Ideal P
hI : I.IsPrime
x y : P
F : PFilter P := ⋯.toPFilter
⊢ x ∉ I ∧ y ∉ I → x ⊓ y ∉ I

Proof state:
P : Type u_1
inst✝ : SemilatticeInf P
I : Ideal P
hI : I.IsPrime
x y : P
F : PFilter P := ⋯.toPFilter
⊢ x ∉ I ∧ y ∉ I → x ⊓ y ∉ I

Tactic:
show x ∈ F ∧ y ∈ F → x ⊓ y ∈ F

Result:
P : Type u_1
inst✝ : SemilatticeInf P
I : Ideal P
hI : I.IsPrime
x y : P
F : PFilter P := ⋯.toPFilter
⊢ x ∈ F ∧ y ∈ F → x ⊓ y ∈ F

Proof state:
P : Type u_1
inst✝ : SemilatticeInf P
I : Ideal P
hI : I.IsPrime
x y : P
F : PFilter P := ⋯.toPFilter
⊢ x ∈ F ∧ y ∈ F → x ⊓ y ∈ F

Tactic:
exact fun h => inf_mem h.1 h.2

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem lt_add_one_iff_of_not_isMax (hy : ¬ IsMax y) : x < y + 1 ↔ x ≤ y

Proof state:
α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hy : ¬IsMax y
⊢ x < y + 1 ↔ x ≤ y

Tactic:
rw [← succ_eq_add_one, lt_succ_iff_of_not_isMax hy]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem le_limsup_iff {α β} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β}
    (h₁ : f.IsCoboundedUnder (· ≤ ·) u

Proof state:
case pos
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ z, y < z ∧ z < x
y : β
y_x : y < x
⊢ y < limsup u f

Tactic:
rcases h' y y_x with ⟨z, y_z, z_x⟩

Result:
case pos.intro.intro
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ z, y < z ∧ z < x
y : β
y_x : y < x
z : β
y_z : y < z
z_x : z < x
⊢ y < limsup u f
-- Mathlib/Algebra/Group/Action/Defs.lean
lemma smul_inv (g : G) (a : H) : (g • a)⁻¹ = g⁻¹ • a⁻¹ :=
  inv_eq_of_mul_eq_one_right <| by rw [smul_mul_smul_comm, mul_inv_cancel, mul_inv_cancel, one_smul]

Proof state:
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
⊢ g • a * g⁻¹ • a⁻¹ = 1

Tactic:
rw [smul_mul_smul_comm, mul_inv_cancel, mul_inv_cancel, one_smul]

Result:
no goals
-- Mathlib/Order/Filter/Cofinite.lean
theorem Nat.cofinite_eq_atTop : @cofinite ℕ = atTop

Proof state:
⊢ cofinite ≤ atTop

Tactic:
refine atTop_basis.ge_iff.2 fun N _ => ?_

Result:
N : ℕ
x✝ : True
⊢ Ici N ∈ cofinite

Proof state:
⊢ cofinite = atTop

Tactic:
refine le_antisymm ?_ atTop_le_cofinite

Result:
⊢ cofinite ≤ atTop

Proof state:
N : ℕ
x✝ : True
⊢ Ici N ∈ cofinite

Tactic:
simpa only [mem_cofinite, compl_Ici] using finite_lt_nat N

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem norm_sub_eq_abs_sub_norm_of_angle_eq_zero {x y : V} (h : angle x y = 0) :
    ‖x - y‖ = |‖x‖ - ‖y‖|

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ‖x - y‖ = |‖x‖ - ‖y‖|

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg (x - y)) (abs_nonneg (‖x‖ - ‖y‖)), norm_sub_pow_two_real,
  inner_eq_mul_norm_of_angle_eq_zero h, sq_abs (‖x‖ - ‖y‖)]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ‖x‖ ^ 2 - 2 * (‖x‖ * ‖y‖) + ‖y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ‖x‖ ^ 2 - 2 * (‖x‖ * ‖y‖) + ‖y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2

Tactic:
ring

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem uniformEquicontinuous_iInf_dom {u : κ → UniformSpace β'} {F : ι → β' → α}
    {k : κ} (hk : UniformEquicontinuous (uβ := u k) F) :
    UniformEquicontinuous (uβ := ⨅ k, u k) F

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
k : κ
hk : UniformEquicontinuous F
⊢ UniformEquicontinuous F

Tactic:
simp_rw [uniformEquicontinuous_iff_uniformContinuous (uβ := _)] at hk ⊢

Result:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
k : κ
hk : UniformContinuous (⇑ofFun ∘ swap F)
⊢ UniformContinuous (⇑ofFun ∘ swap F)

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
k : κ
hk : UniformContinuous (⇑ofFun ∘ swap F)
⊢ UniformContinuous (⇑ofFun ∘ swap F)

Tactic:
exact uniformContinuous_iInf_dom hk

Result:
no goals