harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Ring/NonZeroDivisors.lean
lemma dvd_cancel_right_mem_nonZeroDivisors (hr : r ∈ R⁰) : x * r ∣ y * r ↔ x ∣ y :=
  ⟨fun ⟨z, _⟩ ↦ ⟨z, by rwa [← mul_cancel_right_mem_nonZeroDivisors hr, mul_assoc, mul_comm z r,
    ← mul_assoc]⟩, fun ⟨z, h⟩ ↦ ⟨z, by rw [h, mul_assoc, mul_comm z r, ← mul_assoc]⟩⟩

Proof state:
R : Type u_1
inst✝ : CommRing R
r x y : R
hr : r ∈ R⁰
x✝ : x * r ∣ y * r
z : R
h✝ : y * r = x * r * z
⊢ y = x * z

Tactic:
rwa [← mul_cancel_right_mem_nonZeroDivisors hr, mul_assoc, mul_comm z r,
← mul_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
r x y : R
hr : r ∈ R⁰
x✝ : x ∣ y
z : R
h : y = x * z
⊢ y * r = x * r * z

Tactic:
rw [h, mul_assoc, mul_comm z r, ← mul_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_filter (q) : ∀ l, filter p (filter q l) = filter (fun a => p a && q a) l
  | [] => rfl
  | a :: l => by by_cases hp : p a <;> by_cases hq : q a <;> simp [hp, hq, filter_filter _ l]

Proof state:
α✝ : Type u_1
p q : α✝ → Bool
a : α✝
l : List α✝
⊢ filter p (filter q (a :: l)) = filter (fun a => p a && q a) (a :: l)

Tactic:
by_cases hp : p a <;> by_cases hq : q a <;> simp [hp, hq, filter_filter _ l]

Result:
no goals
-- Mathlib/RingTheory/Etale/Basic.lean
lemma formallyEtale_algebraMap [Algebra R S] :
    (algebraMap R S).FormallyEtale ↔ Algebra.FormallyEtale R S

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).FormallyEtale ↔ Algebra.FormallyEtale R S

Tactic:
delta FormallyEtale

Result:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Algebra.FormallyEtale R S ↔ Algebra.FormallyEtale R S

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Algebra.FormallyEtale R S ↔ Algebra.FormallyEtale R S

Tactic:
congr!

Result:
case a.h.e'_5
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).toAlgebra = inst✝

Proof state:
case a.h.e'_5
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).toAlgebra = inst✝

Tactic:
exact Algebra.algebra_ext _ _ fun _ ↦ rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem aleph0_le_lift {c : Cardinal.{u}} : ℵ₀ ≤ lift.{v} c ↔ ℵ₀ ≤ c

Proof state:
c : Cardinal.{u}
⊢ ℵ₀ ≤ lift.{v, u} c ↔ ℵ₀ ≤ c

Tactic:
simpa using lift_le (a := ℵ₀)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.diag_comp {X Y : C} [HasBinaryCoproduct X X] (f : X ⟶ Y) :
    codiag X ≫ f = coprod.desc f f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryCoproduct X X
f : X ⟶ Y
⊢ codiag X ≫ f = desc f f

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem take_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) :
    (l₁ ++ l₂).take n = l₁.take n

Proof state:
α : Type u_1
l₁ l₂ : List α
n : Nat
h : n ≤ l₁.length
⊢ take n (l₁ ++ l₂) = take n l₁

Tactic:
simp [take_append_eq_append_take, Nat.sub_eq_zero_of_le h]

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem sub_singleton_eq (a : A) (r : R) : σ a - {r} = σ (a - ↑ₐ r)

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ σ a - {r} = σ (a - ↑ₐ r)

Tactic:
simpa only [neg_sub, neg_eq] using congr_arg Neg.neg (singleton_sub_eq a r)

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem le_himp_comm : a ≤ b ⇨ c ↔ b ≤ a ⇨ c

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ≤ b ⇨ c ↔ b ≤ a ⇨ c

Tactic:
rw [le_himp_iff, le_himp_iff']

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Continuity.lean
theorem tendsto_norm_div_self_nhdsGE (x : E) : Tendsto (fun a ↦ ‖a / x‖) (𝓝 x) (𝓝[≥] 0) :=
  tendsto_nhdsWithin_iff.mpr ⟨tendsto_norm_div_self x, by simp⟩

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x : E
⊢ ∀ᶠ (n : E) in 𝓝 x, ‖n / x‖ ∈ Set.Ici 0

Tactic:
simp

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem Set.Nonempty.csSup_mem (h : s.Nonempty) (hs : s.Finite) : sSup s ∈ s

Proof state:
case intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Finset α
h : (↑s).Nonempty
⊢ sSup ↑s ∈ ↑s

Tactic:
exact Finset.Nonempty.csSup_mem h

Result:
no goals

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
h : s.Nonempty
hs : s.Finite
⊢ sSup s ∈ s

Tactic:
lift s to Finset α using hs

Result:
case intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Finset α
h : (↑s).Nonempty
⊢ sSup ↑s ∈ ↑s
-- Mathlib/Data/Complex/Basic.lean
theorem normSq_add_mul_I (x y : ℝ) : normSq (x + y * I) = x ^ 2 + y ^ 2

Proof state:
x y : ℝ
⊢ normSq (↑x + ↑y * I) = x ^ 2 + y ^ 2

Tactic:
rw [← mk_eq_add_mul_I, normSq_mk, sq, sq]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiableWithinAt_inter (ht : t ∈ 𝓝 x) :
    MDifferentiableWithinAt I I' f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
ht : t ∈ 𝓝 x
⊢ MDifferentiableWithinAt I I' f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x

Tactic:
rw [MDifferentiableWithinAt, MDifferentiableWithinAt,
  differentiableWithinAt_localInvariantProp.liftPropWithinAt_inter ht]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
lemma div_def' (q r : ℚ) : q / r = (q.num * r.den) /. (q.den * r.num)

Proof state:
q r : ℚ
⊢ q / r = q.num * ↑r.den /. (↑q.den * r.num)

Tactic:
rw [← divInt_div_divInt, num_divInt_den, num_divInt_den]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
theorem algebraMap_leftInverse :
    Function.LeftInverse algebraMapInv (algebraMap R <| TensorAlgebra R M) := fun x => by
  simp [algebraMapInv]

Proof state:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
⊢ algebraMapInv ((algebraMap R (TensorAlgebra R M)) x) = x

Tactic:
simp [algebraMapInv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem sign_eq_zero_iff_zero {a : Int} : sign a = 0 ↔ a = 0 :=
  ⟨eq_zero_of_sign_eq_zero, fun h => by rw [h, sign_zero]⟩

Proof state:
a : Int
h : a = 0
⊢ a.sign = 0

Tactic:
rw [h, sign_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List ((a : α) × β a)} {k : α}
    (contains_eq_false : (l.map Sigma.fst).contains k = false) :
    (m.insertMany l).getKey? k = m.getKey? k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List ((a : α) × β a)
k : α
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ (m.insertMany l).getKey? k = m.getKey? k

Tactic:
simp_to_raw using Raw₀.getKey?_insertMany_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem inv_le_of_neg (ha : a < 0) (hb : b < 0) : a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
ha : a < 0
hb : b < 0
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Tactic:
rw [← inv_le_inv_of_neg hb (inv_lt_zero.2 ha), inv_inv]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem mem_filter {a : α} {s} : a ∈ filter p s ↔ a ∈ s ∧ p a :=
  Quot.inductionOn s fun _l => by simp

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
_l : List α
⊢ a ∈ filter p (Quot.mk (⇑(isSetoid α)) _l) ↔ a ∈ Quot.mk (⇑(isSetoid α)) _l ∧ p a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
lemma emb_ne_emb_of_ne {i j : Fin c.length} {a : Fin (c.partSize i)} {b : Fin (c.partSize j)}
    (h : i ≠ j) : c.emb i a ≠ c.emb j b :=
  c.emb_injective.ne (a₁ := ⟨i, a⟩) (a₂ := ⟨j, b⟩) (by simp [h])

Proof state:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
a : Fin (c.partSize i)
b : Fin (c.partSize j)
h : i ≠ j
⊢ ⟨i, a⟩ ≠ ⟨j, b⟩

Tactic:
simp [h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/FunctorToTypes.lean
@[simp]
lemma binaryProductIso_inv_comp_fst :
    (binaryProductIso F G).inv ≫ Limits.prod.fst = prod.fst

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ (binaryProductIso F G).inv ≫ Limits.prod.fst = prod.fst

Tactic:
simp [binaryProductIso, binaryProductLimitCone]

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem chain_split {a b : α} {l₁ l₂ : List α} :
    Chain R a (l₁ ++ b :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ Chain R b l₂

Proof state:
α : Type u
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ Chain R a (l₁ ++ b :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ Chain R b l₂

Tactic:
induction' l₁ with x l₁ IH generalizing a <;>
  simp only [*, nil_append, cons_append, Chain.nil, chain_cons, and_true, and_assoc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ResidueField.lean
lemma Hom.residueFieldMap_congr {f g : X ⟶ Y} (e : f = g) (x : X) :
    f.residueFieldMap x = (Y.residueFieldCongr (by subst e; rfl)).hom ≫ g.residueFieldMap x

Proof state:
X Y : Scheme
f g : X ⟶ Y
e : f = g
x : ↑↑X.toPresheafedSpace
⊢ residueFieldMap f x = (residueFieldCongr ⋯).hom ≫ residueFieldMap g x

Tactic:
subst e

Result:
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
⊢ residueFieldMap f x = (residueFieldCongr ⋯).hom ≫ residueFieldMap f x

Proof state:
X✝ : Scheme
U : X✝.Opens
X Y : Scheme
f✝ f g : X ⟶ Y
e : f = g
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) x

Tactic:
subst e

Result:
X✝ : Scheme
U : X✝.Opens
X Y : Scheme
f✝ f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom f.base) x

Proof state:
X✝ : Scheme
U : X✝.Opens
X Y : Scheme
f✝ f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom f.base) x

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
⊢ residueFieldMap f x = (residueFieldCongr ⋯).hom ≫ residueFieldMap f x

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem basicOpen_mul_le_right (f g : R) : basicOpen (f * g) ≤ basicOpen g

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R
⊢ basicOpen (f * g) ≤ basicOpen g

Tactic:
rw [basicOpen_mul f g]

Result:
R : Type u
inst✝ : CommSemiring R
f g : R
⊢ basicOpen f ⊓ basicOpen g ≤ basicOpen g

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R
⊢ basicOpen f ⊓ basicOpen g ≤ basicOpen g

Tactic:
exact inf_le_right

Result:
no goals
-- Mathlib/Order/Partition/Equipartition.lean
theorem IsEquipartition.card_large_parts_eq_mod (hP : P.IsEquipartition) :
    #{p ∈ P.parts | #p = #s / #P.parts + 1} = #s % #P.parts

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z :
  #(filter (fun x => #x = #s / #P.parts + 1) P.parts) * (#s / #P.parts + 1) +
      ∑ x ∈ filter (fun p => #p = #s / #P.parts) P.parts, #x =
    #s
⊢ ∀ x ∈ filter (fun p => #p = #s / #P.parts) P.parts, #x = #s / #P.parts

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ #(filter (fun p => #p = #s / #P.parts + 1) P.parts) = #s % #P.parts

Tactic:
have z := P.sum_card_parts

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : ∑ i ∈ P.parts, #i = #s
⊢ #(filter (fun p => #p = #s / #P.parts + 1) P.parts) = #s % #P.parts

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z :
  ∑ x ∈ filter (fun x => #x = #s / #P.parts + 1) P.parts, #x + ∑ x ∈ filter (fun p => #p = #s / #P.parts) P.parts, #x =
    #s
⊢ ∀ x ∈ filter (fun x => #x = #s / #P.parts + 1) P.parts, #x = #s / #P.parts + 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : ∑ i ∈ P.parts, #i = #s
⊢ #(filter (fun p => #p = #s / #P.parts + 1) P.parts) = #s % #P.parts

Tactic:
rw [← sum_filter_add_sum_filter_not (s := P.parts) (p := fun x ↦ #x = #s / #P.parts + 1),
  hP.filter_ne_average_add_one_eq_average, sum_const_nat (m := #s / #P.parts + 1) (by simp),
  sum_const_nat (m := #s / #P.parts) (by simp), ← hP.filter_ne_average_add_one_eq_average,
  mul_add, add_comm, ← add_assoc, ← add_mul, mul_one, add_comm #_,
  filter_card_add_filter_neg_card_eq_card, add_comm] at z

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : #(filter (fun x => #x = #s / #P.parts + 1) P.parts) + #P.parts * (#s / #P.parts) = #s
⊢ #(filter (fun p => #p = #s / #P.parts + 1) P.parts) = #s % #P.parts

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : #(filter (fun x => #x = #s / #P.parts + 1) P.parts) + #P.parts * (#s / #P.parts) = #s
⊢ #(filter (fun p => #p = #s / #P.parts + 1) P.parts) = #s % #P.parts

Tactic:
rw [← add_left_inj, Nat.mod_add_div, z]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem mul_two (n) : n * 2 = n + n

Proof state:
n : Nat
⊢ n * 2 = n + n

Tactic:
rw [Nat.mul_succ, Nat.mul_one]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem iSup_toSubfield {ι : Sort*} [Nonempty ι] (S : ι → IntermediateField F E) :
    (iSup S).toSubfield = ⨆ i, (S i).toSubfield

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Sort u_3
inst✝ : Nonempty ι
S : ι → IntermediateField F E
⊢ (iSup S).toSubfield = ⨆ i, (S i).toSubfield

Tactic:
simp only [iSup, Set.range_nonempty, sSup_toSubfield, ← Set.range_comp, Function.comp_def]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem quadraticChar_zero : quadraticChar F 0 = 0

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
⊢ (quadraticChar F) 0 = 0

Tactic:
simp only [quadraticChar_apply, quadraticCharFun_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem bind_throw [Monad m] [LawfulMonad m] (f : α → ExceptT ε m β) : (throw e >>= f) = throw e

Proof state:
m : Type u_1 → Type u_2
α ε β : Type u_1
e : ε
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → ExceptT ε m β
⊢ throw e >>= f = throw e

Tactic:
simp [throw, throwThe, MonadExceptOf.throw, bind, ExceptT.bind, ExceptT.bindCont, ExceptT.mk]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem sum_const [AddCommMonoid α] (n : ℕ) (x : α) : ∑ _i : Fin n, x = n • x

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
n : ℕ
x : α
⊢ ∑ _i : Fin n, x = n • x

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem chain_dartAdj_darts {d : G.Dart} {v w : V} (h : d.snd = v) (p : G.Walk v w) :
    List.Chain G.DartAdj d p.darts

Proof state:
V : Type u
G : SimpleGraph V
d : G.Dart
v w : V
h : d.toProd.2 = v
p : G.Walk v w
⊢ List.Chain G.DartAdj d p.darts

Tactic:
induction p generalizing d with
| nil => exact List.Chain.nil
| cons h' p ih => exact List.Chain.cons h (ih rfl)

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : ∀ {d : G.Dart}, d.toProd.2 = v✝ → List.Chain G.DartAdj d p.darts
d : G.Dart
h : d.toProd.2 = u✝
⊢ List.Chain G.DartAdj d (cons h' p).darts

Tactic:
exact List.Chain.cons h (ih rfl)

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
v w u✝ : V
d : G.Dart
h : d.toProd.2 = u✝
⊢ List.Chain G.DartAdj d nil.darts

Tactic:
exact List.Chain.nil

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem affineIndependent_iff_not_collinear {p : Fin 3 → P} :
    AffineIndependent k p ↔ ¬Collinear k (Set.range p)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
⊢ AffineIndependent k p ↔ ¬Collinear k (Set.range p)

Tactic:
rw [collinear_iff_finrank_le_one,
  affineIndependent_iff_not_finrank_vectorSpan_le k p (Fintype.card_fin 3)]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem isBounded_principal (s : Set α) : IsBounded r (𝓟 s) ↔ ∃ t, ∀ x ∈ s, r x t

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
⊢ IsBounded r (𝓟 s) ↔ ∃ t, ∀ x ∈ s, r x t

Tactic:
simp [IsBounded, subset_def]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem Red.step_invRev_iff :
    Red.Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂) ↔ Red.Step L₁ L₂ :=
  ⟨fun h => by simpa only [invRev_invRev] using h.invRev, fun h => h.invRev⟩

Proof state:
α : Type u
L₁ L₂ : List (α × Bool)
h : Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)
⊢ Step L₁ L₂

Tactic:
simpa only [invRev_invRev] using h.invRev

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Images.lean
theorem factorThruImage_comp_hom {X Y : A} (f : X ⟶ Y) :
    factorThruImage (L.map f) ≫ (iso L f).hom = L.map (factorThruImage f)

Proof state:
A : Type u₁
B : Type u₂
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Category.{v₂, u₂} B
inst✝⁵ : HasEqualizers A
inst✝⁴ : HasImages A
inst✝³ : StrongEpiCategory B
inst✝² : HasImages B
L : A ⥤ B
inst✝¹ : ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) L
inst✝ : ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
⊢ factorThruImage (L.map f) ≫ (iso L f).hom = L.map (factorThruImage f)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_subset_Ioo_iff (h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂

Proof state:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂

Tactic:
rw [← coe_subset, coe_Icc, coe_Ioo, Set.Icc_subset_Ioo_iff h₁]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem preimage_metric_ball {r : ℝ} : p ⁻¹' Metric.ball 0 r = { x | p x < r }

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ ⇑p ⁻¹' Metric.ball 0 r = {x | p x < r}

Tactic:
ext x

Result:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ x ∈ ⇑p ⁻¹' Metric.ball 0 r ↔ x ∈ {x | p x < r}

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ x ∈ ⇑p ⁻¹' Metric.ball 0 r ↔ x ∈ {x | p x < r}

Tactic:
simp only [mem_setOf, mem_preimage, mem_ball_zero_iff, Real.norm_of_nonneg (apply_nonneg p _)]

Result:
no goals
-- Mathlib/Data/Finset/Functor.lean
theorem map_traverse (g : α → G β) (h : β → γ) (s : Finset α) :
    Functor.map h <$> traverse g s = traverse (Functor.map h ∘ g) s

Proof state:
α β γ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ Functor.map h <$> Multiset.toFinset <$> Multiset.traverse g s.val =
    Multiset.toFinset <$> Multiset.traverse (Functor.map h ∘ g) s.val

Tactic:
simp only [Functor.map_map, fmap_def, map_comp_coe_apply, Multiset.fmap_def, ←
  Multiset.map_traverse]

Result:
no goals

Proof state:
α β γ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ Functor.map h <$> traverse g s = traverse (Functor.map h ∘ g) s

Tactic:
unfold traverse

Result:
α β γ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ Functor.map h <$> Multiset.toFinset <$> Multiset.traverse g s.val =
    Multiset.toFinset <$> Multiset.traverse (Functor.map h ∘ g) s.val
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k a : α} :
    (m.erase k).getKey! a = if k == a then default else m.getKey! a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
k a : α
⊢ (m.erase k).getKey! a = if (k == a) = true then default else m.getKey! a

Tactic:
simp_to_raw using Raw₀.getKey!_erase

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Extend.lean
theorem hasDerivAt_of_hasDerivAt_of_ne' {f g : ℝ → E} {x : ℝ}
    (f_diff : ∀ y ≠ x, HasDerivAt f (g y) y) (hf : ContinuousAt f x)
    (hg : ContinuousAt g x) (y : ℝ) : HasDerivAt f (g y) y

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
y : ℝ
⊢ HasDerivAt f (g y) y

Tactic:
rcases eq_or_ne y x with (rfl | hne)

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
y : ℝ
f_diff : ∀ (y_1 : ℝ), y_1 ≠ y → HasDerivAt f (g y_1) y_1
hf : ContinuousAt f y
hg : ContinuousAt g y
⊢ HasDerivAt f (g y) y

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
y : ℝ
hne : y ≠ x
⊢ HasDerivAt f (g y) y

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
y : ℝ
f_diff : ∀ (y_1 : ℝ), y_1 ≠ y → HasDerivAt f (g y_1) y_1
hf : ContinuousAt f y
hg : ContinuousAt g y
⊢ HasDerivAt f (g y) y

Tactic:
exact hasDerivAt_of_hasDerivAt_of_ne f_diff hf hg

Result:
no goals

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
y : ℝ
hne : y ≠ x
⊢ HasDerivAt f (g y) y

Tactic:
exact f_diff y hne

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem differentiableWithinAt_univ :
    DifferentiableWithinAt 𝕜 f univ x ↔ DifferentiableAt 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ DifferentiableWithinAt 𝕜 f univ x ↔ DifferentiableAt 𝕜 f x

Tactic:
simp only [DifferentiableWithinAt, hasFDerivWithinAt_univ, DifferentiableAt]

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive (attr := simp)] lemma leOnePart_inv (a : α) : a⁻¹⁻ᵐ = a⁺ᵐ

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ a⁻¹⁻ᵐ = a⁺ᵐ

Tactic:
simp [oneLePart, leOnePart]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem zipIdx_eq_zip_range' (l : Vector α n) : l.zipIdx m = l.zip (range' m n)

Proof state:
α : Type u_1
n m : Nat
l : Vector α n
⊢ l.zipIdx m = l.zip (range' m n)

Tactic:
simp [zip_of_prod (zipIdx_map_fst _ _) (zipIdx_map_snd _ _)]

Result:
no goals