harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/PushoutI.lean
theorem base_smul_def (h : H) (w : NormalWord d) :
    base φ h • w = { w with head := h * w.head }

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
h : H
w : NormalWord d
⊢ MulAction.toEndHom h w = { toWord := w.toWord, head := h * w.head, normalized := ⋯ }

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
h : H
w : NormalWord d
⊢ (base φ) h • w = { toWord := w.toWord, head := h * w.head, normalized := ⋯ }

Tactic:
dsimp [NormalWord.mulAction, instHSMul, SMul.smul]

Result:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
h : H
w : NormalWord d
⊢ (lift (fun x => MulAction.toEndHom) MulAction.toEndHom ⋯) ((base φ) h) w =
    { toWord := w.toWord, head := h * w.head, normalized := ⋯ }

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
h : H
w : NormalWord d
⊢ (lift (fun x => MulAction.toEndHom) MulAction.toEndHom ⋯) ((base φ) h) w =
    { toWord := w.toWord, head := h * w.head, normalized := ⋯ }

Tactic:
rw [lift_base]

Result:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
h : H
w : NormalWord d
⊢ MulAction.toEndHom h w = { toWord := w.toWord, head := h * w.head, normalized := ⋯ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem zipWith_eq_zipWith_take_min : ∀ (l₁ : List α) (l₂ : List β),
    zipWith f l₁ l₂ = zipWith f (l₁.take (min l₁.length l₂.length)) (l₂.take (min l₁.length l₂.length))
  | [], _ => by simp
  | _, [] => by simp
  | a :: l₁, b :: l₂ => by simp [succ_min_succ, zipWith_eq_zipWith_take_min l₁ l₂]

Proof state:
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
x✝ : List α
⊢ zipWith f x✝ [] = zipWith f (take (min x✝.length [].length) x✝) (take (min x✝.length [].length) [])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
a : α
l₁ : List α
b : β
l₂ : List β
⊢ zipWith f (a :: l₁) (b :: l₂) =
    zipWith f (take (min (a :: l₁).length (b :: l₂).length) (a :: l₁))
      (take (min (a :: l₁).length (b :: l₂).length) (b :: l₂))

Tactic:
simp [succ_min_succ, zipWith_eq_zipWith_take_min l₁ l₂]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
x✝ : List β
⊢ zipWith f [] x✝ = zipWith f (take (min [].length x✝.length) []) (take (min [].length x✝.length) x✝)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/LowerUpperTopology.lean
/-- A function `f : β → α` with lower topology in the codomain is continuous
if and only if the preimage of every interval `Set.Ici a` is a closed set.
-/
lemma continuous_iff_Ici [TopologicalSpace β] {f : β → α} :
    Continuous f ↔ ∀ a, IsClosed (f ⁻¹' (Ici a))

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace β
f : β → α
inst✝ : IsLower α
⊢ Continuous f ↔ ∀ (a : α), IsClosed (f ⁻¹' Ici a)

Tactic:
simp [continuous_generateFrom_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : TopologicalSpace α
inst✝¹ : IsLower α
inst✝ : TopologicalSpace β
f : β → α
⊢ Continuous f ↔ ∀ (a : α), IsClosed (f ⁻¹' Ici a)

Tactic:
obtain rfl := IsLower.topology_eq α

Result:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace β
f : β → α
inst✝ : IsLower α
⊢ Continuous f ↔ ∀ (a : α), IsClosed (f ⁻¹' Ici a)
-- Mathlib/Data/Rat/Defs.lean
protected lemma neg_add_cancel : -a + a = 0

Proof state:
a : ℚ
⊢ -a + a = 0

Tactic:
simp [add_def, normalize_eq_mkRat, Int.neg_mul, Int.add_comm, ← Int.sub_eq_add_neg]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_eq_empty_iff : Icc a b = ∅ ↔ ¬a ≤ b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Icc a b = ∅ ↔ ¬a ≤ b

Tactic:
rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Icc]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Finite.lean
theorem card_map_of_injective {H : Type*} [Group H] {K : Subgroup G} {f : G →* H}
    (hf : Function.Injective f) :
    Nat.card (map f K) = Nat.card K

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_3
inst✝ : Group H
K : Subgroup G
f : G →* H
hf : Function.Injective ⇑f
⊢ Nat.card ↥(map f K) = Nat.card ↥K

Tactic:
apply Nat.card_image_of_injective hf

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem μ_natural {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :
    (F.map f ⊗ F.map g) ≫ μ F Y Y' = μ F X X' ≫ F.map (f ⊗ g)

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 Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (F.map f ⊗ F.map g) ≫ μ F Y Y' = μ F X X' ≫ F.map (f ⊗ g)

Tactic:
simp [tensorHom_def]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem bot_lt_add_iff {x y : EReal} : ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y

Proof state:
x y : EReal
⊢ ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y

Tactic:
simp [bot_lt_iff_ne_bot]

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem Int.coe_nat_two_pow_pred (p : ℕ) : ((2 ^ p - 1 : ℕ) : ℤ) = (2 ^ p - 1 : ℤ) :=
  Int.natCast_pow_pred 2 p (by decide)

Proof state:
p : ℕ
⊢ 0 < 2

Tactic:
decide

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc (attr := simp)]
lemma whiskerLeft_ε_η (T : D) : T ◁ ε F ≫ T ◁ η F = 𝟙 _

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.Monoidal
T : D
⊢ T ◁ ε F ≫ T ◁ η F = 𝟙 (T ⊗ 𝟙_ D)

Tactic:
rw [← MonoidalCategory.whiskerLeft_comp, ε_η, MonoidalCategory.whiskerLeft_id]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
@[simp]
lemma id_comp {ι₂ M₂ N₂ : Type*}
    [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
    (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : Hom P Q) :
    comp f (id P) = f

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Hom Q
⊢ f.comp (id P) = f

Tactic:
ext x <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem mkMetric_mono {m₁ m₂ : ℝ≥0∞ → ℝ≥0∞} (hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂) :
    (mkMetric m₁ : OuterMeasure X) ≤ mkMetric m₂

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂
⊢ mkMetric m₁ ≤ mkMetric m₂

Tactic:
convert @mkMetric_mono_smul X _ _ m₂ _ ENNReal.one_ne_top one_ne_zero _ <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Control/Lawful/MonadLift.lean
theorem lift_pure (a : α) : OptionT.lift (pure a : m α) = pure a

Proof state:
m : Type u_1 → Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
a : α
⊢ OptionT.lift (pure a) = pure a

Tactic:
simp only [OptionT.lift, OptionT.mk, bind_pure_comp, map_pure, pure, OptionT.pure]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem _root_.List.attach_toArray {l : List α} :
    l.toArray.attach = (l.attachWith (· ∈ l.toArray) (by simp)).toArray

Proof state:
α : Type ?u.1226
l : List α
⊢ ∀ (x : α), x ∈ l → (fun x => x ∈ l.toArray) x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ l.toArray.attach = (l.attachWith (fun x => x ∈ l.toArray) ⋯).toArray

Tactic:
simp [attach]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem preimage_coe_mem_nhds_subtype {s t : Set α} {a : s} : (↑) ⁻¹' t ∈ 𝓝 a ↔ t ∈ 𝓝[s] ↑a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
a : ↑s
⊢ Subtype.val ⁻¹' t ∈ 𝓝 a ↔ t ∈ 𝓝[s] ↑a

Tactic:
rw [← map_nhds_subtype_val, mem_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.xor_right_inj' (a b c : BitVec w) : (c ^^^ a == b ^^^ c) = (a == b)

Proof state:
w : Nat
a b c : BitVec w
⊢ (a ^^^ c == b ^^^ c) = true ↔ (a == b) = true

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
a b c : BitVec w
⊢ (c ^^^ a == b ^^^ c) = (a == b)

Tactic:
rw [Bool.eq_iff_iff, BitVec.xor_comm c]

Result:
w : Nat
a b c : BitVec w
⊢ (a ^^^ c == b ^^^ c) = true ↔ (a == b) = true
-- Mathlib/LinearAlgebra/Dual.lean
theorem flip_injective_iff₂ [FiniteDimensional K V₂] : Injective B.flip ↔ Surjective B

Proof state:
K : Type uK
inst✝⁵ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₂
⊢ Injective ⇑B.flip ↔ Surjective ⇑B

Tactic:
rw [← dualMap_injective_iff]

Result:
K : Type uK
inst✝⁵ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₂
⊢ Injective ⇑B.flip ↔ Injective ⇑B.dualMap

Proof state:
K : Type uK
inst✝⁵ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₂
⊢ Injective ⇑B.flip ↔ Injective ⇑B.dualMap

Tactic:
exact (evalEquiv K V₂).toEquiv.injective_comp B.dualMap

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_emod_left (a b : Int) : (a * b) % b = 0

Proof state:
a b : Int
⊢ a * b % b = 0

Tactic:
rw [← Int.zero_add (a * b), Int.add_mul_emod_self, Int.zero_emod]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findSome?_append {l₁ : Vector α n₁} {l₂ : Vector α n₂} : (l₁ ++ l₂).findSome? f = (l₁.findSome? f).or (l₂.findSome? f)

Proof state:
case mk.mk
α : Type u_1
n₁ n₂ : Nat
α✝ : Type u_2
f : α → Option α✝
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n₁
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n₂
⊢ findSome? f
      ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
        { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    (findSome? f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }).or
      (findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ })

Tactic:
simp [Array.findSome?_append]

Result:
no goals

Proof state:
α : Type u_1
n₁ n₂ : Nat
α✝ : Type u_2
f : α → Option α✝
l₁ : Vector α n₁
l₂ : Vector α n₂
⊢ findSome? f (l₁ ++ l₂) = (findSome? f l₁).or (findSome? f l₂)

Tactic:
cases l₁

Result:
case mk
α : Type u_1
n₁ n₂ : Nat
α✝ : Type u_2
f : α → Option α✝
l₂ : Vector α n₂
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n₁
⊢ findSome? f ({ toArray := toArray✝, size_toArray := size_toArray✝ } ++ l₂) =
    (findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ }).or (findSome? f l₂)

Proof state:
case mk
α : Type u_1
n₁ n₂ : Nat
α✝ : Type u_2
f : α → Option α✝
l₂ : Vector α n₂
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n₁
⊢ findSome? f ({ toArray := toArray✝, size_toArray := size_toArray✝ } ++ l₂) =
    (findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ }).or (findSome? f l₂)

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
n₁ n₂ : Nat
α✝ : Type u_2
f : α → Option α✝
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n₁
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n₂
⊢ findSome? f
      ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
        { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    (findSome? f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }).or
      (findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ })
-- Mathlib/Combinatorics/Pigeonhole.lean
theorem exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum
    (hf : ∀ y ∉ t, ∑ x ∈ s with f x = y, w x ≤ 0) (ht : t.Nonempty)
    (hb : #t • b ≤ ∑ x ∈ s, w x) : ∃ y ∈ t, b ≤ ∑ x ∈ s with f x = y, w x :=
  exists_le_of_sum_le ht <|
    calc
      ∑ _y ∈ t, b ≤ ∑ x ∈ s, w x

Proof state:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
inst✝ : LinearOrderedCancelAddCommMonoid M
hf : ∀ y ∉ t, ∑ x ∈ filter (fun x => f x = y) s, w x ≤ 0
ht : t.Nonempty
hb : #t • b ≤ ∑ x ∈ s, w x
⊢ ∑ _y ∈ t, b ≤ ∑ x ∈ s, w x

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
    (H : ∀ (a : α), a ∈ xs → P a) (p : β → Bool) :
    (xs.pmap f H).find? p = (xs.attach.find? (fun ⟨a, m⟩ => p (f a (H a m)))).map fun ⟨a, m⟩ => f a (H a m)

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : Array α
H : ∀ (a : α), a ∈ xs → P a
p : β → Bool
⊢ find? p (pmap f xs H) =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      (find?
        (fun x =>
          match x with
          | ⟨a, m⟩ => p (f a ⋯))
        xs.attach)

Tactic:
simp only [pmap_eq_map_attach, find?_map]

Result:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : Array α
H : ∀ (a : α), a ∈ xs → P a
p : β → Bool
⊢ Option.map (fun x => f x.val ⋯) (find? (p ∘ fun x => f x.val ⋯) xs.attach) =
    Option.map (fun x => f x.val ⋯) (find? (fun x => p (f x.val ⋯)) xs.attach)

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : Array α
H : ∀ (a : α), a ∈ xs → P a
p : β → Bool
⊢ Option.map (fun x => f x.val ⋯) (find? (p ∘ fun x => f x.val ⋯) xs.attach) =
    Option.map (fun x => f x.val ⋯) (find? (fun x => p (f x.val ⋯)) xs.attach)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem whisker_assoc_symm (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) :
    f ◁ η ▷ h = (α_ f g h).inv ≫ (f ◁ η) ▷ h ≫ (α_ f g' h).hom

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ f ◁ η ▷ h = (α_ f g h).inv ≫ (f ◁ η) ▷ h ≫ (α_ f g' h).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
lemma nmem_nonZeroDivisorsRight_iff :
    x ∉ nonZeroDivisorsRight M₀ ↔ {y | x * y = 0 ∧ y ≠ 0}.Nonempty

Proof state:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
x : M₀
⊢ x ∉ nonZeroDivisorsRight M₀ ↔ {y | x * y = 0 ∧ y ≠ 0}.Nonempty

Tactic:
simpa [mem_nonZeroDivisorsRight_iff] using Set.nonempty_def.symm

Result:
no goals
-- Mathlib/Data/Multiset/Sym.lean
theorem dedup_sym2 [DecidableEq α] (m : Multiset α) : m.sym2.dedup = m.dedup.sym2 :=
  m.inductionOn fun xs => by simp [List.dedup_sym2]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
xs : List α
⊢ (Multiset.sym2 ⟦xs⟧).dedup = (dedup ⟦xs⟧).sym2

Tactic:
simp [List.dedup_sym2]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem conePointsIsoOfNatIso_hom_comp {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s)
    (Q : IsLimit t) (w : F ≅ G) (j : J) :
    (conePointsIsoOfNatIso P Q w).hom ≫ t.π.app j = s.π.app j ≫ w.hom.app j

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F G : J ⥤ C
s : Cone F
t : Cone G
P : IsLimit s
Q : IsLimit t
w : F ≅ G
j : J
⊢ (P.conePointsIsoOfNatIso Q w).hom ≫ t.π.app j = s.π.app j ≫ w.hom.app j

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
theorem limitObjIsoLimitCompEvaluation_inv_limit_map [HasLimitsOfShape J C] {i j : K}
    (F : J ⥤ K ⥤ C) (f : i ⟶ j) : (limitObjIsoLimitCompEvaluation _ _).inv ≫ (limit F).map f =
    limMap (whiskerLeft _ ((evaluation _ _).map f)) ≫ (limitObjIsoLimitCompEvaluation _ _).inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
⊢ (limitObjIsoLimitCompEvaluation F i).inv ≫ (limit F).map f =
    limMap (whiskerLeft F ((evaluation K C).map f)) ≫ (limitObjIsoLimitCompEvaluation F j).inv

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv,
  limit_map_limitObjIsoLimitCompEvaluation_hom]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem inter_ae_eq_left_of_ae_eq_univ (h : t =ᵐ[μ] univ) : (s ∩ t : Set α) =ᵐ[μ] s

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
⊢ s ∩ t =ᶠ[ae μ] s

Tactic:
convert ae_eq_set_inter (ae_eq_refl s) h

Result:
case h.e'_5
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
⊢ s = s ∩ univ

Proof state:
case h.e'_5
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
⊢ s = s ∩ univ

Tactic:
rw [inter_univ]

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
lemma ringChar_zero_iff_CharZero : ringChar R = 0 ↔ CharZero R

Proof state:
R : Type u_1
inst✝ : NonAssocRing R
⊢ ringChar R = 0 ↔ CharZero R

Tactic:
rw [ringChar.eq_iff, charP_zero_iff_charZero]

Result:
no goals
-- Mathlib/Analysis/Complex/Hadamard.lean
/-- A bound to the norm of `f` on the line `z.re = u` induces a bound to the norm of `scale f l u z`
  on the line `z.re = 1`. -/
lemma scale_bound_right {f : ℂ → E} {l u b : ℝ} (hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b) :
    ∀ z ∈ re ⁻¹' {1}, ‖scale f l u z‖ ≤ b

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
z : ℂ
hz : z.re = 1
⊢ ‖f (↑l + z * (↑u - ↑l))‖ ≤ b

Tactic:
exact hb (↑l + z * (↑u - ↑l)) (by simp [hz])

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
⊢ ∀ (z : ℂ), z.re = 1 → ‖f (↑l + z * (↑u - ↑l))‖ ≤ b

Tactic:
intro z hz

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
z : ℂ
hz : z.re = 1
⊢ ‖f (↑l + z * (↑u - ↑l))‖ ≤ b

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
⊢ ∀ z ∈ re ⁻¹' {1}, ‖scale f l u z‖ ≤ b

Tactic:
simp only [scale, mem_preimage, mem_singleton_iff, smul_eq_mul]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
⊢ ∀ (z : ℂ), z.re = 1 → ‖f (↑l + z * (↑u - ↑l))‖ ≤ b

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
z : ℂ
hz : z.re = 1
⊢ ↑l + z * (↑u - ↑l) ∈ re ⁻¹' {u}

Tactic:
simp [hz]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Girth.lean
lemma egirth_anti : Antitone (egirth : SimpleGraph α → ℕ∞) :=
  fun G H h ↦ iInf_mono fun a ↦ iInf₂_mono' fun w hw ↦ ⟨w.mapLe h, hw.mapLe _, by simp⟩

Proof state:
α : Type u_1
G H : SimpleGraph α
h : G ≤ H
a : α
w : G.Walk a a
hw : w.IsCycle
⊢ ↑(Walk.mapLe h w).length ≤ ↑w.length

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (a == ·)

Proof state:
α : Type u_1
inst✝ : BEq α
l : List α
a : α
⊢ l.contains a = l.any fun x => a == x

Tactic:
induction l with simp | cons b l => cases b == a <;> simp [*]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
a b : α
l : List α
tail_ih✝ : l.contains a = l.any fun x => a == x
⊢ (a == b || l.contains a) = (a == b || l.any fun x => a == x)

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

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_lt_top {a b : α} : emultiplicity a b < ⊤ ↔ FiniteMultiplicity a b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
⊢ emultiplicity a b < ⊤ ↔ FiniteMultiplicity a b

Tactic:
simp [lt_top_iff_ne_top, emultiplicity_eq_top]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_polynomialY : (W'.baseChange B).toProjective.polynomialY =
    MvPolynomial.map f (W'.baseChange A).toProjective.polynomialY

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (baseChange W' B).toProjective.polynomialY = (MvPolynomial.map ↑f) (baseChange W' A).toProjective.polynomialY

Tactic:
rw [← map_polynomialY, map_baseChange]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_eq_add_fract_mul (a b : α) :
    toIcoMod hp a b = a + Int.fract ((b - a) / p) * p

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - ↑⌊(b - a) / p⌋ * p = a + (b - a - p * ↑⌊(b - a) / p⌋)

Tactic:
ring

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - ⌊(b - a) / p⌋ • p = a + ((b - a) / p - ↑⌊(b - a) / p⌋) * p

Tactic:
field_simp

Result:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - ↑⌊(b - a) / p⌋ * p = a + (b - a - p * ↑⌊(b - a) / p⌋)

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b = a + Int.fract ((b - a) / p) * p

Tactic:
rw [toIcoMod, toIcoDiv_eq_floor, Int.fract]

Result:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - ⌊(b - a) / p⌋ • p = a + ((b - a) / p - ↑⌊(b - a) / p⌋) * p
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseIdx_zero (l : List α) : eraseIdx l 0 = tail l

Proof state:
α : Type u_1
l : List α
⊢ l.eraseIdx 0 = l.tail

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Topology/Bornology/Absorbs.lean
@[simp] lemma of_boundedSpace [BoundedSpace M] : Absorbs M s t

Proof state:
M : Type u_1
α : Type u_2
inst✝² : Bornology M
inst✝¹ : SMul M α
s t : Set α
inst✝ : BoundedSpace M
⊢ Absorbs M s t

Tactic:
simp [Absorbs]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Localization.lean
lemma isLocalization_C_mk' (a : R) (m : M) :
    C (IsLocalization.mk' S a m) = IsLocalization.mk' (MvPolynomial σ S) (C (σ := σ) a)
      ⟨C m, Submonoid.mem_map_of_mem C m.property⟩

Proof state:
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
m : ↥M
⊢ C (IsLocalization.mk' S a m) = IsLocalization.mk' (MvPolynomial σ S) (C a) ⟨C ↑m, ⋯⟩

Tactic:
simp_rw [IsLocalization.eq_mk'_iff_mul_eq, algebraMap_def, map_C, ← map_mul,
  IsLocalization.mk'_spec]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Module.lean
theorem linearEquivFunOnFintype_symm_coe [Fintype ι] (f : ⨁ i, M i) :
    (linearEquivFunOnFintype R ι M).symm f = f

Proof state:
R : Type u
inst✝³ : Semiring R
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
f : ⨁ (i : ι), M i
⊢ (linearEquivFunOnFintype R ι M).symm ⇑f = f

Tactic:
simp [linearEquivFunOnFintype]

Result:
no goals