harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_iUnion_congr (Xs Ys : ι → Set α) (h : ∀ i, M.closure (Xs i) = M.closure (Ys i)) :
    M.closure (⋃ i, Xs i) = M.closure (⋃ i, Ys i)

Proof state:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs Ys : ι → Set α
h : ∀ (i : ι), M.closure (Xs i) = M.closure (Ys i)
⊢ M.closure (⋃ i, Xs i) = M.closure (⋃ i, Ys i)

Tactic:
simp [h, ← M.closure_iUnion_closure_eq_closure_iUnion]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc (attr := simp)]
lemma inr_f_desc_f (p : ℤ) :
    (inr φ).f p ≫ (desc φ α β eq).f p = β.f p

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
p : ℤ
⊢ (inr φ).f p ≫ (desc φ α β eq).f p = β.f p

Tactic:
simp [desc]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Module.lean
theorem linearEquivFunOnFintype_lof [Fintype ι] (i : ι) (m : M i) :
    (linearEquivFunOnFintype R ι M) (lof R ι M i m) = Pi.single i m

Proof state:
case h
R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : M i
a : ι
⊢ (linearEquivFunOnFintype R ι M) ((lof R ι M i) m) a = Pi.single i m a

Tactic:
change (DFinsupp.equivFunOnFintype (lof R ι M i m)) a = _

Result:
case h
R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : M i
a : ι
⊢ DFinsupp.equivFunOnFintype ((lof R ι M i) m) a = Pi.single i m a

Proof state:
case h
R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : M i
a : ι
⊢ DFinsupp.equivFunOnFintype ((lof R ι M i) m) a = Pi.single i m a

Tactic:
convert _root_.congr_fun (DFinsupp.equivFunOnFintype_single i m) a

Result:
no goals

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✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : M i
⊢ (linearEquivFunOnFintype R ι M) ((lof R ι M i) m) = Pi.single i m

Tactic:
ext a

Result:
case h
R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : M i
a : ι
⊢ (linearEquivFunOnFintype R ι M) ((lof R ι M i) m) a = Pi.single i m a
-- Mathlib/Data/Vector/Basic.lean
theorem mOfFn_pure {m} [Monad m] [LawfulMonad m] {α} :
    ∀ {n} (f : Fin n → α), (@mOfFn m _ _ _ fun i => pure (f i)) = pure (ofFn f)
  | 0, _ => rfl
  | n + 1, f => by
    rw [mOfFn, @mOfFn_pure m _ _ _ n _, ofFn]
    simp

Proof state:
m : Type u_6 → Type u_7
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
⊢ (do
      let a ← pure (f 0)
      let v ← pure (ofFn fun i => f i.succ)
      pure (a ::ᵥ v)) =
    pure (f 0 ::ᵥ ofFn fun i => f i.succ)

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_6 → Type u_7
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
⊢ (mOfFn fun i => pure (f i)) = pure (ofFn f)

Tactic:
rw [mOfFn, @mOfFn_pure m _ _ _ n _, ofFn]

Result:
m : Type u_6 → Type u_7
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
⊢ (do
      let a ← pure (f 0)
      let v ← pure (ofFn fun i => f i.succ)
      pure (a ::ᵥ v)) =
    pure (f 0 ::ᵥ ofFn fun i => f i.succ)
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem dist_triangle_right (x y z : α) : dist x y ≤ dist x z + dist y z

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist x z + dist z y

Tactic:
apply dist_triangle

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist x z + dist y z

Tactic:
rw [dist_comm y]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist x z + dist z y
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
@[to_additive (attr := simp)]
lemma closure_singleton_inv (x : G) : closure {x⁻¹} = closure {x}

Proof state:
G : Type u_2
inst✝ : Group G
x : G
⊢ closure {x⁻¹} = closure {x}

Tactic:
rw [← Set.inv_singleton, closure_inv]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem inv_eq_zero {a : G₀} : a⁻¹ = 0 ↔ a = 0

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a⁻¹ = 0 ↔ a = 0

Tactic:
rw [inv_eq_iff_eq_inv, inv_zero]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem parent'_lt (self : UnionFind) (i : Nat) (h) : self.arr[i].parent < self.size

Proof state:
self : UnionFind
i : Nat
h : i < self.arr.size
⊢ self.arr[i].parent < self.size

Tactic:
simp [← parentD_eq, parentD_lt, Fin.is_lt, Array.length_toList, h]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem idealFactorsEquivOfQuotEquiv_is_dvd_iso {L M : Ideal R} (hL : L ∣ I) (hM : M ∣ I) :
    (idealFactorsEquivOfQuotEquiv f ⟨L, hL⟩ : Ideal A) ∣ idealFactorsEquivOfQuotEquiv f ⟨M, hM⟩ ↔
      L ∣ M

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
this : (idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩ ≤ (idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩ ↔ ⟨M, hM⟩ ≤ ⟨L, hL⟩
⊢ ↑((idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩) ∣ ↑((idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩) ↔ L ∣ M

Tactic:
rw [dvd_iff_le, dvd_iff_le, Subtype.coe_le_coe, this, Subtype.mk_le_mk]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
⊢ (idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩ ≤ (idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩ ↔ ⟨M, hM⟩ ≤ ⟨L, hL⟩

Tactic:
exact (idealFactorsEquivOfQuotEquiv f).le_iff_le

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
⊢ ↑((idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩) ∣ ↑((idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩) ↔ L ∣ M

Tactic:
suffices
  idealFactorsEquivOfQuotEquiv f ⟨M, hM⟩ ≤ idealFactorsEquivOfQuotEquiv f ⟨L, hL⟩ ↔
    (⟨M, hM⟩ : { p : Ideal R | p ∣ I }) ≤ ⟨L, hL⟩
  by rw [dvd_iff_le, dvd_iff_le, Subtype.coe_le_coe, this, Subtype.mk_le_mk]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
⊢ (idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩ ≤ (idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩ ↔ ⟨M, hM⟩ ≤ ⟨L, hL⟩
-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem one_sub_K_ne_top : (1 : ℝ≥0∞) - K ≠ ∞

Proof state:
K : ℝ≥0
⊢ ¬↑(1 - K) = ⊤

Tactic:
exact ENNReal.coe_ne_top

Result:
no goals

Proof state:
K : ℝ≥0
⊢ 1 - ↑K ≠ ⊤

Tactic:
norm_cast

Result:
K : ℝ≥0
⊢ ¬↑(1 - K) = ⊤
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc (attr := simp)]
lemma inr_f_descCochain_v (p₁ p₂ : ℤ) (h₁₂ : p₁ + n = p₂) :
    (inr φ).f p₁ ≫ (descCochain φ α β h).v p₁ p₂ h₁₂ = β.v p₁ p₂ h₁₂

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ (inr φ).f p₁ ≫ (descCochain φ α β h).v p₁ p₂ h₁₂ = β.v p₁ p₂ h₁₂

Tactic:
simpa only [Cochain.comp_v _ _ (zero_add n) p₁ p₁ p₂ (add_zero p₁) h₁₂, Cochain.ofHom_v]
  using Cochain.congr_v (inr_descCochain φ α β h) p₁ p₂ (by omega)

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ p₁ + n = p₂

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/FiberBundle/Basic.lean
theorem isOpen_source (e : Pretrivialization F (π F E)) :
    IsOpen[a.totalSpaceTopology] e.source

Proof state:
case h.mk
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
x : B × F
hx : x ∈ e'.target
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' e.target ↔ ⟨x, hx⟩ ∈ e'.setSymm ⁻¹' e.source

Tactic:
simp only [mem_preimage, Pretrivialization.setSymm, restrict, e.mem_target, e.mem_source,
  e'.proj_symm_apply hx]

Result:
no goals

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
⊢ IsOpen e.source

Tactic:
refine isOpen_iSup_iff.mpr fun e' => isOpen_iSup_iff.mpr fun _ => ?_

Result:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
⊢ IsOpen e.source

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
⊢ IsOpen e.source

Tactic:
refine isOpen_coinduced.mpr (isOpen_induced_iff.mpr ⟨e.target, e.open_target, ?_⟩)

Result:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
⊢ Subtype.val ⁻¹' e.target = e'.setSymm ⁻¹' e.source

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
⊢ Subtype.val ⁻¹' e.target = e'.setSymm ⁻¹' e.source

Tactic:
ext ⟨x, hx⟩

Result:
case h.mk
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
x : B × F
hx : x ∈ e'.target
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' e.target ↔ ⟨x, hx⟩ ∈ e'.setSymm ⁻¹' e.source
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem norm_eq_zero {x : ℤ[i]} : norm x = 0 ↔ x = 0

Proof state:
x : ℤ[i]
⊢ norm x = 0 ↔ x = 0

Tactic:
rw [← @Int.cast_inj ℝ _ _ _]

Result:
x : ℤ[i]
⊢ ↑(norm x) = ↑0 ↔ x = 0

Proof state:
x : ℤ[i]
⊢ ↑(norm x) = ↑0 ↔ x = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
theorem ContinuousMultilinearMap.uncurry0_curry0 (f : G[×0]→L[𝕜] G') :
    ContinuousMultilinearMap.uncurry0 𝕜 G f.curry0 = f

Proof state:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
⊢ uncurry0 𝕜 G f.curry0 = f

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_le_size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List ((a : α) × β a)} :
    m.size ≤ (m.insertMany l).size

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List ((a : α) × β a)
⊢ m.size ≤ (m.insertMany l).size

Tactic:
simp_to_raw using Raw₀.size_le_size_insertMany_list ⟨m, _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem add_sat (w₁ : c₁.sat x₁) (w₂ : c₂.sat x₂) : (add c₁ c₂).sat (x₁ + x₂)

Proof state:
case mk.some.some.mk.some.some.right
x₁ x₂ l₁ u₁ l₂ u₂ : Int
w₁ : l₁ ≤ x₁ ∧ x₁ ≤ u₁
w₂ : l₂ ≤ x₂ ∧ x₂ ≤ u₂
⊢ x₁ + x₂ ≤ u₁ + u₂

Tactic:
exact Int.add_le_add w₁.2 w₂.2

Result:
no goals

Proof state:
case mk.some.some.mk.some.some.left
x₁ x₂ l₁ u₁ l₂ u₂ : Int
w₁ : l₁ ≤ x₁ ∧ x₁ ≤ u₁
w₂ : l₂ ≤ x₂ ∧ x₂ ≤ u₂
⊢ l₁ + l₂ ≤ x₁ + x₂

Tactic:
exact Int.add_le_add w₁.1 w₂.1

Result:
no goals

Proof state:
case mk.some.some.mk.none.some
x₁ x₂ l₁ u₁ u₂ : Int
w₁ : l₁ ≤ x₁ ∧ x₁ ≤ u₁
w₂ : x₂ ≤ u₂
⊢ x₁ + x₂ ≤ u₁ + u₂

Tactic:
exact Int.add_le_add w₁.2 w₂

Result:
no goals

Proof state:
case mk.none.some.mk.some.some
x₁ x₂ u₁ l₂ u₂ : Int
w₁ : x₁ ≤ u₁
w₂ : l₂ ≤ x₂ ∧ x₂ ≤ u₂
⊢ x₁ + x₂ ≤ u₁ + u₂

Tactic:
exact Int.add_le_add w₁ w₂.2

Result:
no goals

Proof state:
case mk.none.some.mk.none.some
x₁ x₂ u₁ u₂ : Int
w₁ : x₁ ≤ u₁
w₂ : x₂ ≤ u₂
⊢ x₁ + x₂ ≤ u₁ + u₂

Tactic:
exact Int.add_le_add w₁ w₂

Result:
no goals

Proof state:
case mk.some.none.mk.some.none
x₁ x₂ l₁ l₂ : Int
w₁ : l₁ ≤ x₁
w₂ : l₂ ≤ x₂
⊢ l₁ + l₂ ≤ x₁ + x₂

Tactic:
exact Int.add_le_add w₁ w₂

Result:
no goals

Proof state:
case mk.some.some.mk.some.none
x₁ x₂ l₁ u₁ l₂ : Int
w₁ : l₁ ≤ x₁ ∧ x₁ ≤ u₁
w₂ : l₂ ≤ x₂
⊢ l₁ + l₂ ≤ x₁ + x₂

Tactic:
exact Int.add_le_add w₁.1 w₂

Result:
no goals

Proof state:
case mk.some.none.mk.some.some
x₁ x₂ l₁ l₂ u₂ : Int
w₁ : l₁ ≤ x₁
w₂ : l₂ ≤ x₂ ∧ x₂ ≤ u₂
⊢ l₁ + l₂ ≤ x₁ + x₂

Tactic:
exact Int.add_le_add w₁ w₂.1

Result:
no goals

Proof state:
case mk.some.some.mk.some.some
x₁ x₂ l₁ u₁ l₂ u₂ : Int
w₁ : l₁ ≤ x₁ ∧ x₁ ≤ u₁
w₂ : l₂ ≤ x₂ ∧ x₂ ≤ u₂
⊢ l₁ + l₂ ≤ x₁ + x₂ ∧ x₁ + x₂ ≤ u₁ + u₂

Tactic:
constructor

Result:
case mk.some.some.mk.some.some.left
x₁ x₂ l₁ u₁ l₂ u₂ : Int
w₁ : l₁ ≤ x₁ ∧ x₁ ≤ u₁
w₂ : l₂ ≤ x₂ ∧ x₂ ≤ u₂
⊢ l₁ + l₂ ≤ x₁ + x₂

case mk.some.some.mk.some.some.right
x₁ x₂ l₁ u₁ l₂ u₂ : Int
w₁ : l₁ ≤ x₁ ∧ x₁ ≤ u₁
w₂ : l₂ ≤ x₂ ∧ x₂ ≤ u₂
⊢ x₁ + x₂ ≤ u₁ + u₂

Proof state:
c₁ c₂ : Constraint
x₁ x₂ : Int
w₁ : c₁.sat x₁ = true
w₂ : c₂.sat x₂ = true
⊢ (c₁.add c₂).sat (x₁ + x₂) = true

Tactic:
rcases c₁ with ⟨_ | l₁, _ | u₁⟩ <;> rcases c₂ with ⟨_ | l₂, _ | u₂⟩
  <;> simp [sat, LowerBound.sat, UpperBound.sat, add] at *

Result:
case mk.none.some.mk.none.some
x₁ x₂ u₁ u₂ : Int
w₁ : x₁ ≤ u₁
w₂ : x₂ ≤ u₂
⊢ x₁ + x₂ ≤ u₁ + u₂

case mk.none.some.mk.some.some
x₁ x₂ u₁ l₂ u₂ : Int
w₁ : x₁ ≤ u₁
w₂ : l₂ ≤ x₂ ∧ x₂ ≤ u₂
⊢ x₁ + x₂ ≤ u₁ + u₂

case mk.some.none.mk.some.none
x₁ x₂ l₁ l₂ : Int
w₁ : l₁ ≤ x₁
w₂ : l₂ ≤ x₂
⊢ l₁ + l₂ ≤ x₁ + x₂

case mk.some.none.mk.some.some
x₁ x₂ l₁ l₂ u₂ : Int
w₁ : l₁ ≤ x₁
w₂ : l₂ ≤ x₂ ∧ x₂ ≤ u₂
⊢ l₁ + l₂ ≤ x₁ + x₂

case mk.some.some.mk.none.some
x₁ x₂ l₁ u₁ u₂ : Int
w₁ : l₁ ≤ x₁ ∧ x₁ ≤ u₁
w₂ : x₂ ≤ u₂
⊢ x₁ + x₂ ≤ u₁ + u₂

case mk.some.some.mk.some.none
x₁ x₂ l₁ u₁ l₂ : Int
w₁ : l₁ ≤ x₁ ∧ x₁ ≤ u₁
w₂ : l₂ ≤ x₂
⊢ l₁ + l₂ ≤ x₁ + x₂

case mk.some.some.mk.some.some
x₁ x₂ l₁ u₁ l₂ u₂ : Int
w₁ : l₁ ≤ x₁ ∧ x₁ ≤ u₁
w₂ : l₂ ≤ x₂ ∧ x₂ ≤ u₂
⊢ l₁ + l₂ ≤ x₁ + x₂ ∧ x₁ + x₂ ≤ u₁ + u₂
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem IsHilbertSum.linearIsometryEquiv_symm_apply (hV : IsHilbertSum 𝕜 G V)
    (w : lp G 2) : hV.linearIsometryEquiv.symm w = ∑' i, V i (w i)

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : IsHilbertSum 𝕜 G V
w : ↥(lp G 2)
⊢ hV.linearIsometryEquiv.symm w = ∑' (i : ι), (V i) (↑w i)

Tactic:
simp [IsHilbertSum.linearIsometryEquiv, OrthogonalFamily.linearIsometry_apply]

Result:
no goals
-- Mathlib/Data/Matrix/PEquiv.lean
lemma vecMul_toMatrix_toPEquiv [DecidableEq n] [Fintype m]
    [NonAssocSemiring α] (σ : m ≃ n) (a : m → α) :
    a ᵥ* σ.toPEquiv.toMatrix = a ∘ σ.symm

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonAssocSemiring α
σ : m ≃ n
a : m → α
⊢ a ᵥ* σ.toPEquiv.toMatrix = a ∘ ⇑σ.symm

Tactic:
classical
ext j
simp [toMatrix, σ.apply_eq_iff_eq_symm_apply, vecMul, dotProduct]

Result:
no goals

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonAssocSemiring α
σ : m ≃ n
a : m → α
⊢ a ᵥ* σ.toPEquiv.toMatrix = a ∘ ⇑σ.symm

Tactic:
ext j

Result:
case h
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonAssocSemiring α
σ : m ≃ n
a : m → α
j : n
⊢ (a ᵥ* σ.toPEquiv.toMatrix) j = (a ∘ ⇑σ.symm) j

Proof state:
case h
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonAssocSemiring α
σ : m ≃ n
a : m → α
j : n
⊢ (a ᵥ* σ.toPEquiv.toMatrix) j = (a ∘ ⇑σ.symm) j

Tactic:
simp [toMatrix, σ.apply_eq_iff_eq_symm_apply, vecMul, dotProduct]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem neg_tdiv_neg (a b : Int) : (-a).tdiv (-b) = a.tdiv b

Proof state:
a b : Int
⊢ (-a).tdiv (-b) = a.tdiv b

Tactic:
simp [Int.tdiv_neg, Int.neg_tdiv, Int.neg_neg]

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem mem_roots_iff [IsDomain R] (h0 : P.toPoly ≠ 0) (x : R) :
    x ∈ P.roots ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0

Proof state:
R : Type u_1
P : Cubic R
inst✝¹ : CommRing R
inst✝ : IsDomain R
h0 : P.toPoly ≠ 0
x : R
⊢ x ∈ P.roots ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0

Tactic:
rw [roots, mem_roots h0, IsRoot, toPoly]

Result:
R : Type u_1
P : Cubic R
inst✝¹ : CommRing R
inst✝ : IsDomain R
h0 : P.toPoly ≠ 0
x : R
⊢ eval x (C P.a * X ^ 3 + C P.b * X ^ 2 + C P.c * X + C P.d) = 0 ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0

Proof state:
R : Type u_1
P : Cubic R
inst✝¹ : CommRing R
inst✝ : IsDomain R
h0 : P.toPoly ≠ 0
x : R
⊢ eval x (C P.a * X ^ 3 + C P.b * X ^ 2 + C P.c * X + C P.d) = 0 ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0

Tactic:
simp only [eval_C, eval_X, eval_add, eval_mul, eval_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_pos_iff {a : α} {l : Vector α n} : 0 < count a l ↔ a ∈ l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a : α
l : Vector α n
⊢ 0 < count a l ↔ a ∈ l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ 0 < count a { toArray := l, size_toArray := ⋯ } ↔ a ∈ { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ 0 < count a { toArray := l, size_toArray := ⋯ } ↔ a ∈ { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.count_pos_iff, beq_iff_eq, exists_eq_right]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
/-- Any morphism `Y ⟶ Z` is part of a distinguished triangle `X ⟶ Y ⟶ Z ⟶ X⟦1⟧` -/
lemma distinguished_cocone_triangle₁ {Y Z : C} (g : Y ⟶ Z) :
    ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ X⟦(1 : ℤ)⟧), Triangle.mk f g h ∈ distTriang C

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
Y Z : C
g : Y ⟶ Z
⊢ ∃ X f h, Triangle.mk f g h ∈ distinguishedTriangles

Tactic:
obtain ⟨X', f', g', mem⟩ := distinguished_cocone_triangle g

Result:
case intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
Y Z : C
g : Y ⟶ Z
X' : C
f' : Z ⟶ X'
g' : X' ⟶ (shiftFunctor C 1).obj Y
mem : Triangle.mk g f' g' ∈ distinguishedTriangles
⊢ ∃ X f h, Triangle.mk f g h ∈ distinguishedTriangles

Proof state:
case intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
Y Z : C
g : Y ⟶ Z
X' : C
f' : Z ⟶ X'
g' : X' ⟶ (shiftFunctor C 1).obj Y
mem : Triangle.mk g f' g' ∈ distinguishedTriangles
⊢ ∃ X f h, Triangle.mk f g h ∈ distinguishedTriangles

Tactic:
exact ⟨_, _, _, inv_rot_of_distTriang _ mem⟩

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem corec_id_id_eq_const (a : α) : corec id id a = const a

Proof state:
α : Type u
a : α
⊢ corec id id a = const a

Tactic:
rw [corec_def, map_id, iterate_id]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem rightDistributor_ext₂_left {J : Type} [Fintype J]
    {f : J → C} {X Y Z : C} {g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z}
    (w : ∀ j, ((biproduct.ι f j ▷ X) ▷ Y) ≫ g = ((biproduct.ι f j ▷ X) ▷ Y) ≫ h) :
    g = h

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z
w : ∀ (j : J), biproduct.ι f j ▷ X ▷ Y ≫ g = biproduct.ι f j ▷ X ▷ Y ≫ h
⊢ g = h

Tactic:
apply (cancel_epi (α_ _ _ _).inv).mp

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z
w : ∀ (j : J), biproduct.ι f j ▷ X ▷ Y ≫ g = biproduct.ι f j ▷ X ▷ Y ≫ h
⊢ (α_ (⨁ f) X Y).inv ≫ g = (α_ (⨁ f) X Y).inv ≫ h

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z
w : ∀ (j : J), biproduct.ι f j ▷ X ▷ Y ≫ g = biproduct.ι f j ▷ X ▷ Y ≫ h
⊢ (α_ (⨁ f) X Y).inv ≫ g = (α_ (⨁ f) X Y).inv ≫ h

Tactic:
ext

Result:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z
w : ∀ (j : J), biproduct.ι f j ▷ X ▷ Y ≫ g = biproduct.ι f j ▷ X ▷ Y ≫ h
j✝ : J
⊢ biproduct.ι f j✝ ▷ (X ⊗ Y) ≫ (α_ (⨁ f) X Y).inv ≫ g = biproduct.ι f j✝ ▷ (X ⊗ Y) ≫ (α_ (⨁ f) X Y).inv ≫ h

Proof state:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z
w : ∀ (j : J), biproduct.ι f j ▷ X ▷ Y ≫ g = biproduct.ι f j ▷ X ▷ Y ≫ h
j✝ : J
⊢ biproduct.ι f j✝ ▷ (X ⊗ Y) ≫ (α_ (⨁ f) X Y).inv ≫ g = biproduct.ι f j✝ ▷ (X ⊗ Y) ≫ (α_ (⨁ f) X Y).inv ≫ h

Tactic:
simp [w]

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
@[simp]
lemma _root_.NonUnitalStarAlgHom.map_adjoin_singleton (f : F) (x : A) :
    map f (adjoin R {x}) = adjoin R {f x}

Proof state:
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : NonUnitalSemiring A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module R A
inst✝¹² : NonUnitalSemiring B
inst✝¹¹ : StarRing B
inst✝¹⁰ : Module R B
inst✝⁹ : FunLike F A B
inst✝⁸ : NonUnitalAlgHomClass F R A B
inst✝⁷ : StarHomClass F A B
inst✝⁶ : StarRing R
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : StarModule R A
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : StarModule R B
f : F
x : A
⊢ map f (adjoin R {x}) = adjoin R {f x}

Tactic:
simp [NonUnitalStarAlgHom.map_adjoin]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem mem_map_of_involutive {f : α → α} (hf : Involutive f) {a : α} {l : List α} :
    a ∈ map f l ↔ f a ∈ l

Proof state:
α : Type u
f : α → α
hf : Involutive f
a : α
l : List α
⊢ a ∈ map f l ↔ f a ∈ l

Tactic:
rw [mem_map, hf.exists_mem_and_apply_eq_iff]

Result:
no goals