harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matroid/Closure.lean
lemma mem_closure_iff_forall_mem_isFlat (X : Set α) (hX : X ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
e : α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ e ∈ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F

Tactic:
simp_rw [M.closure_def' X, mem_sInter, mem_setOf, and_imp]

Result:
no goals
-- Mathlib/Analysis/Calculus/DSlope.lean
theorem dslope_sub_smul_of_ne (f : 𝕜 → E) (h : b ≠ a) :
    dslope (fun x => (x - a) • f x) a b = f b

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : 𝕜
f : 𝕜 → E
h : b ≠ a
⊢ dslope (fun x => (x - a) • f x) a b = f b

Tactic:
rw [dslope_of_ne _ h, slope_sub_smul _ h.symm]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_comp_mul_deriv''' {a b : ℝ} {f f' : ℝ → ℝ} {g : ℝ → ℝ}
    (hf : ContinuousOn f [[a, b]])
    (hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x)
    (hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))) (hg1 : IntegrableOn g (f '' [[a, b]]))
    (hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) [[a, b]]) :
    (∫ x in a..b, (g ∘ f) x * f' x) = ∫ u in f a..f b, g u

Proof state:
a b : ℝ
f f' g : ℝ → ℝ
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (a ⊓ b) (a ⊔ b))
hg1 : IntegrableOn g (f '' [[a, b]]) volume
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) [[a, b]] volume
⊢ ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u

Tactic:
have hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] := by simpa [mul_comm] using hg2

Result:
a b : ℝ
f f' g : ℝ → ℝ
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (a ⊓ b) (a ⊔ b))
hg1 : IntegrableOn g (f '' [[a, b]]) volume
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) [[a, b]] volume
hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume
⊢ ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u

Proof state:
a b : ℝ
f f' g : ℝ → ℝ
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (a ⊓ b) (a ⊔ b))
hg1 : IntegrableOn g (f '' [[a, b]]) volume
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) [[a, b]] volume
⊢ IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume

Tactic:
simpa [mul_comm] using hg2

Result:
no goals

Proof state:
a b : ℝ
f f' g : ℝ → ℝ
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (a ⊓ b) (a ⊔ b))
hg1 : IntegrableOn g (f '' [[a, b]]) volume
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) [[a, b]] volume
hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume
⊢ ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u

Tactic:
simpa [mul_comm] using integral_comp_smul_deriv''' hf hff' hg_cont hg1 hg2'

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/HomEquiv.lean
lemma liftExtend_f :
    (e.liftExtend φ hφ).f i' = (K.restrictionXIso e hi).inv ≫ φ.f i ≫
      (L.extendXIso e hi).inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
i : ι
hi : e.f i = i'
⊢ (e.liftExtend φ hφ).f i' = (K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv

Tactic:
apply liftExtend.f_eq

Result:
no goals
-- Mathlib/NumberTheory/SumTwoSquares.lean
theorem ZMod.isSquare_neg_one_of_dvd {m n : ℕ} (hd : m ∣ n) (hs : IsSquare (-1 : ZMod n)) :
    IsSquare (-1 : ZMod m)

Proof state:
m n : ℕ
hd : m ∣ n
hs : IsSquare (-1)
f : ZMod n →+* ZMod m := castHom hd (ZMod m)
⊢ IsSquare (f (-1))

Tactic:
exact hs.map f

Result:
no goals

Proof state:
m n : ℕ
hd : m ∣ n
hs : IsSquare (-1)
⊢ IsSquare (-1)

Tactic:
let f : ZMod n →+* ZMod m := ZMod.castHom hd _

Result:
m n : ℕ
hd : m ∣ n
hs : IsSquare (-1)
f : ZMod n →+* ZMod m := castHom hd (ZMod m)
⊢ IsSquare (-1)

Proof state:
m n : ℕ
hd : m ∣ n
hs : IsSquare (-1)
f : ZMod n →+* ZMod m := castHom hd (ZMod m)
⊢ IsSquare (-1)

Tactic:
rw [← RingHom.map_one f, ← RingHom.map_neg]

Result:
m n : ℕ
hd : m ∣ n
hs : IsSquare (-1)
f : ZMod n →+* ZMod m := castHom hd (ZMod m)
⊢ IsSquare (f (-1))
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem reindexFinsetRange_repr_self (i : ι) :
    b.reindexFinsetRange.repr (b i) =
      Finsupp.single ⟨b i, Finset.mem_image_of_mem b (Finset.mem_univ i)⟩ 1

Proof state:
case h.mk
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ (b.reindexFinsetRange.repr (b i)) ⟨bi, hbi⟩ = (single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩

Tactic:
rw [reindexFinsetRange, repr_reindex, Finsupp.mapDomain_equiv_apply, reindexRange_repr_self]

Result:
case h.mk
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ (single ⟨b i, ⋯⟩ 1) (((Equiv.refl M).subtypeEquiv ⋯).symm ⟨bi, hbi⟩) = (single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
⊢ b.reindexFinsetRange.repr (b i) = single ⟨b i, ⋯⟩ 1

Tactic:
ext ⟨bi, hbi⟩

Result:
case h.mk
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ (b.reindexFinsetRange.repr (b i)) ⟨bi, hbi⟩ = (single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩

Proof state:
case h.mk
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ (single ⟨b i, ⋯⟩ 1) (((Equiv.refl M).subtypeEquiv ⋯).symm ⟨bi, hbi⟩) = (single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩

Tactic:
simp [Finsupp.single_apply]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ValuativeCriterion.lean
/-- The **valuative criterion** for proper morphisms. -/
@[stacks 0BX5]
lemma IsProper.eq_valuativeCriterion :
    @IsProper = ValuativeCriterion ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType

Proof state:
⊢ ValuativeCriterion.Uniqueness ⊓
      (@QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ (@QuasiCompact ⊓ @LocallyOfFiniteType))) =
    ValuativeCriterion.Existence ⊓
      (ValuativeCriterion.Uniqueness ⊓ (@QuasiCompact ⊓ (@QuasiSeparated ⊓ @LocallyOfFiniteType)))

Tactic:
ext X Y f

Result:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ (ValuativeCriterion.Uniqueness ⊓
        (@QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ (@QuasiCompact ⊓ @LocallyOfFiniteType))))
      f ↔
    (ValuativeCriterion.Existence ⊓
        (ValuativeCriterion.Uniqueness ⊓ (@QuasiCompact ⊓ (@QuasiSeparated ⊓ @LocallyOfFiniteType))))
      f

Proof state:
⊢ ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ @QuasiCompact) ⊓
      @LocallyOfFiniteType =
    ValuativeCriterion.Existence ⊓ ValuativeCriterion.Uniqueness ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓
      @LocallyOfFiniteType

Tactic:
simp_rw [inf_assoc]

Result:
⊢ ValuativeCriterion.Uniqueness ⊓
      (@QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ (@QuasiCompact ⊓ @LocallyOfFiniteType))) =
    ValuativeCriterion.Existence ⊓
      (ValuativeCriterion.Uniqueness ⊓ (@QuasiCompact ⊓ (@QuasiSeparated ⊓ @LocallyOfFiniteType)))

Proof state:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ (ValuativeCriterion.Uniqueness ⊓
        (@QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ (@QuasiCompact ⊓ @LocallyOfFiniteType))))
      f ↔
    (ValuativeCriterion.Existence ⊓
        (ValuativeCriterion.Uniqueness ⊓ (@QuasiCompact ⊓ (@QuasiSeparated ⊓ @LocallyOfFiniteType))))
      f

Tactic:
show _ ∧ _ ∧ _ ∧ _ ∧ _ ↔ _ ∧ _ ∧ _ ∧ _ ∧ _

Result:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f ↔
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f

Proof state:
⊢ @IsProper = ValuativeCriterion ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType

Tactic:
rw [isProper_eq, IsSeparated.eq_valuativeCriterion, ValuativeCriterion.eq,
  UniversallyClosed.eq_valuativeCriterion]

Result:
⊢ ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ @QuasiCompact) ⊓
      @LocallyOfFiniteType =
    ValuativeCriterion.Existence ⊓ ValuativeCriterion.Uniqueness ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓
      @LocallyOfFiniteType

Proof state:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f ↔
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f

Tactic:
tauto

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem toDual_apply_left (m : M) (i : ι) : b.toDual m (b i) = b.repr m i

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
i : ι
⊢ (b.toDual m) (b i) = (b.repr m) i

Tactic:
rw [← b.toDual_linearCombination_left, b.linearCombination_repr]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem mul_equiv_mul {f1 f2 g1 g2 : CauSeq β abv} (hf : f1 ≈ f2) (hg : g1 ≈ g2) :
    f1 * g1 ≈ f2 * g2

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 g1 g2 : CauSeq β abv
hf : f1 ≈ f2
hg : g1 ≈ g2
⊢ f1 * g1 ≈ f2 * g2

Tactic:
simpa only [mul_sub, sub_mul, sub_add_sub_cancel]
  using add_limZero (mul_limZero_left g1 hf) (mul_limZero_right f2 hg)

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem lift_rank_le_of_injective_injectiveₛ (i : R' → R) (j : M →+ M')
    (hi : Injective i) (hj : Injective j)
    (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) :
    lift.{v'} (Module.rank R M) ≤ lift.{v} (Module.rank R' M')

Proof state:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')

Tactic:
simp_rw [Module.rank, lift_iSup (bddAbove_range _)]

Result:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ ⨆ i, lift.{v', v} #↑↑i ≤ ⨆ i, lift.{v, v'} #↑↑i

Proof state:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ ⨆ i, lift.{v', v} #↑↑i ≤ ⨆ i, lift.{v, v'} #↑↑i

Tactic:
exact ciSup_mono' (bddAbove_range _) fun ⟨s, h⟩ ↦ ⟨⟨j '' s,
  LinearIndepOn.id_image (h.linearIndependent.map_of_injective_injectiveₛ i j hi hj hc)⟩,
  lift_mk_le'.mpr ⟨(Equiv.Set.image j s hj).toEmbedding⟩⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem Filter.EventuallyEq.gradient_eq (hL : f₁ =ᶠ[𝓝 x] f) : ∇ f₁ x = ∇ f x

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
x : F
f₁ : F → 𝕜
hL : f₁ =ᶠ[𝓝 x] f
⊢ (toDual 𝕜 F).symm (fderiv 𝕜 f₁ x) = (toDual 𝕜 F).symm (fderiv 𝕜 f x)

Tactic:
rwa [Filter.EventuallyEq.fderiv_eq]

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
x : F
f₁ : F → 𝕜
hL : f₁ =ᶠ[𝓝 x] f
⊢ ∇ f₁ x = ∇ f x

Tactic:
unfold gradient

Result:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
x : F
f₁ : F → 𝕜
hL : f₁ =ᶠ[𝓝 x] f
⊢ (toDual 𝕜 F).symm (fderiv 𝕜 f₁ x) = (toDual 𝕜 F).symm (fderiv 𝕜 f x)
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem sup_apply (m₁ m₂ : OuterMeasure α) (s : Set α) : (m₁ ⊔ m₂) s = m₁ s ⊔ m₂ s

Proof state:
α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
this : (⨆ i, bif i then m₁ else m₂) s = ⨆ i, (bif i then m₁ else m₂) s
⊢ (m₁ ⊔ m₂) s = m₁ s ⊔ m₂ s

Tactic:
rwa [iSup_bool_eq, iSup_bool_eq] at this

Result:
no goals

Proof state:
α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
⊢ (m₁ ⊔ m₂) s = m₁ s ⊔ m₂ s

Tactic:
have := iSup_apply (fun b => cond b m₁ m₂) s

Result:
α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
this : (⨆ i, bif i then m₁ else m₂) s = ⨆ i, (bif i then m₁ else m₂) s
⊢ (m₁ ⊔ m₂) s = m₁ s ⊔ m₂ s
-- Mathlib/Order/SuccPred/Archimedean.lean
lemma lt_or_le_of_directed [PredOrder α] [IsPredArchimedean α] {r v₁ v₂ : α} (h₁ : v₁ ≤ r)
    (h₂ : v₂ ≤ r) : v₁ < v₂ ∨ v₂ ≤ v₁

Proof state:
case inl
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
r v₁ v₂ : α
h₁ : v₁ ≤ r
h₂ : v₂ ≤ r
nh : ¬v₂ ≤ v₁
h : v₁ ≤ v₂
⊢ v₁ < v₂

Tactic:
apply lt_of_le_of_ne h (ne_of_not_le nh).symm

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
r v₁ v₂ : α
h₁ : v₁ ≤ r
h₂ : v₂ ≤ r
nh : ¬v₂ ≤ v₁
h : v₂ ≤ v₁
⊢ v₁ < v₂

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
r v₁ v₂ : α
h₁ : v₁ ≤ r
h₂ : v₂ ≤ r
⊢ v₁ < v₂ ∨ v₂ ≤ v₁

Tactic:
rw [Classical.or_iff_not_imp_right]

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
r v₁ v₂ : α
h₁ : v₁ ≤ r
h₂ : v₂ ≤ r
⊢ ¬v₂ ≤ v₁ → v₁ < v₂

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
r v₁ v₂ : α
h₁ : v₁ ≤ r
h₂ : v₂ ≤ r
⊢ ¬v₂ ≤ v₁ → v₁ < v₂

Tactic:
intro nh

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
r v₁ v₂ : α
h₁ : v₁ ≤ r
h₂ : v₂ ≤ r
nh : ¬v₂ ≤ v₁
⊢ v₁ < v₂

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
r v₁ v₂ : α
h₁ : v₁ ≤ r
h₂ : v₂ ≤ r
nh : ¬v₂ ≤ v₁
⊢ v₁ < v₂

Tactic:
rcases le_total_of_directed h₁ h₂ with h | h

Result:
case inl
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
r v₁ v₂ : α
h₁ : v₁ ≤ r
h₂ : v₂ ≤ r
nh : ¬v₂ ≤ v₁
h : v₁ ≤ v₂
⊢ v₁ < v₂

case inr
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
r v₁ v₂ : α
h₁ : v₁ ≤ r
h₂ : v₂ ≤ r
nh : ¬v₂ ≤ v₁
h : v₂ ≤ v₁
⊢ v₁ < v₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem unzip_zip_left {l₁ : Array α} {l₂ : Array β} (h : l₁.size ≤ l₂.size) :
    (unzip (zip l₁ l₂)).1 = l₁

Proof state:
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₁.size ≤ l₂.size
⊢ (l₁.zip l₂).unzip.fst = l₁

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
h : { toList := toList✝ }.size ≤ l₂.size
⊢ ({ toList := toList✝ }.zip l₂).unzip.fst = { toList := toList✝ }

Proof state:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
h : { toList := toList✝ }.size ≤ l₂.size
⊢ ({ toList := toList✝ }.zip l₂).unzip.fst = { toList := toList✝ }

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
h : { toList := toList✝¹ }.size ≤ { toList := toList✝ }.size
⊢ ({ toList := toList✝¹ }.zip { toList := toList✝ }).unzip.fst = { toList := toList✝¹ }

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
h : { toList := toList✝¹ }.size ≤ { toList := toList✝ }.size
⊢ ({ toList := toList✝¹ }.zip { toList := toList✝ }).unzip.fst = { toList := toList✝¹ }

Tactic:
simp_all only [size_toArray, List.zip_toArray, List.unzip_toArray, Prod.map_fst,
  List.unzip_zip_left]

Result:
no goals
-- Mathlib/Algebra/Field/Periodic.lean
theorem Periodic.const_inv_smul₀ [AddCommMonoid α] [DivisionSemiring γ] [Module γ α]
    (h : Periodic f c) (a : γ) : Periodic (fun x => f (a⁻¹ • x)) (a • c)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
⊢ Periodic (fun x => f (a⁻¹ • x)) (a • c)

Tactic:
simpa only [inv_inv] using h.const_smul₀ a⁻¹

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem mem_comap' : s ∈ comap f l ↔ { y | ∀ ⦃x⦄, f x = y → x ∈ s } ∈ l :=
  ⟨fun ⟨t, ht, hts⟩ => mem_of_superset ht fun y hy x hx => hts <| mem_preimage.2 <| by rwa [hx],
    fun h => ⟨_, h, fun _ hx => hx rfl⟩⟩

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
x✝ : s ∈ comap f l
t : Set β
ht : t ∈ l
hts : f ⁻¹' t ⊆ s
y : β
hy : y ∈ t
x : α
hx : f x = y
⊢ f x ∈ t

Tactic:
rwa [hx]

Result:
no goals
-- Mathlib/Algebra/Field/Subfield/Basic.lean
theorem mem_map {f : K →+* L} {s : Subfield K} {y : L} : y ∈ s.map f ↔ ∃ x ∈ s, f x = y

Proof state:
K : Type u
L : Type v
inst✝¹ : DivisionRing K
inst✝ : DivisionRing L
f : K →+* L
s : Subfield K
y : L
⊢ y ∈ map f s ↔ ∃ x ∈ s, f x = y

Tactic:
unfold map

Result:
K : Type u
L : Type v
inst✝¹ : DivisionRing K
inst✝ : DivisionRing L
f : K →+* L
s : Subfield K
y : L
⊢ (y ∈
      let __src := Subring.map f s.toSubring;
      { toSubring := __src, inv_mem' := ⋯ }) ↔
    ∃ x ∈ s, f x = y

Proof state:
K : Type u
L : Type v
inst✝¹ : DivisionRing K
inst✝ : DivisionRing L
f : K →+* L
s : Subfield K
y : L
⊢ (y ∈
      let __src := Subring.map f s.toSubring;
      { toSubring := __src, inv_mem' := ⋯ }) ↔
    ∃ x ∈ s, f x = y

Tactic:
simp only [mem_mk, Subring.mem_mk, Subring.mem_toSubsemiring, Subring.mem_map, mem_toSubring]

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
theorem subtype_equivRange (f : M ↪[L] N) : (subtype _).comp f.equivRange.toEmbedding = f

Proof state:
case h
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
x✝ : M
⊢ (f.toHom.range.subtype.comp f.equivRange.toEmbedding) x✝ = f x✝

Tactic:
rfl

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
⊢ f.toHom.range.subtype.comp f.equivRange.toEmbedding = f

Tactic:
ext

Result:
case h
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
x✝ : M
⊢ (f.toHom.range.subtype.comp f.equivRange.toEmbedding) x✝ = f x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_insert_zero (l : List α) (a : α) :
    (l.insert a)[0]? = if a ∈ l then l[0]? else some a

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ (if a ∈ l then l else a :: l)[0]? = if a ∈ l then l[0]? else some a

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ (List.insert a l)[0]? = if a ∈ l then l[0]? else some a

Tactic:
simp only [insert_eq]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ (if a ∈ l then l else a :: l)[0]? = if a ∈ l then l[0]? else some a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/OfFn.lean
theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
    (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
h : i < n
⊢ (ofFn f)[i] = f ⟨i, h⟩

Tactic:
simp [ofFn]

Result:
no goals

Proof state:
α : Type ?u.31
n : Nat
f : Fin n → α
i : Nat
h : i < n
⊢ i < n

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem eq_iff_forall_dual_eq {x y : E} : x = y ↔ ∀ g : Dual 𝕜 E, g x = g y

Proof state:
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ x = y ↔ ∀ (g : Dual 𝕜 E), g x = g y

Tactic:
rw [← sub_eq_zero, eq_zero_iff_forall_dual_eq_zero 𝕜 (x - y)]

Result:
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ (∀ (g : Dual 𝕜 E), g (x - y) = 0) ↔ ∀ (g : Dual 𝕜 E), g x = g y

Proof state:
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ (∀ (g : Dual 𝕜 E), g (x - y) = 0) ↔ ∀ (g : Dual 𝕜 E), g x = g y

Tactic:
simp [sub_eq_zero]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem infEdist_cthickening (δ : ℝ) (s : Set E) (x : E) :
    infEdist x (cthickening δ s) = infEdist x s - ENNReal.ofReal δ

Proof state:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : 0 < δ
⊢ infEdist x (cthickening δ s) = infEdist x s - ENNReal.ofReal δ

Tactic:
rw [← closure_thickening hδ, infEdist_closure, infEdist_thickening hδ]

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
⊢ infEdist x (cthickening δ s) = infEdist x s - ENNReal.ofReal δ

Tactic:
obtain hδ | hδ := le_or_lt δ 0

Result:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : δ ≤ 0
⊢ infEdist x (cthickening δ s) = infEdist x s - ENNReal.ofReal δ

case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : 0 < δ
⊢ infEdist x (cthickening δ s) = infEdist x s - ENNReal.ofReal δ

Proof state:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : δ ≤ 0
⊢ infEdist x (cthickening δ s) = infEdist x s - ENNReal.ofReal δ

Tactic:
rw [cthickening_of_nonpos hδ, infEdist_closure, ofReal_of_nonpos hδ, tsub_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/DecidableEq.lean
theorem isEqv_iff_rel {a b : Array α} {r} :
    Array.isEqv a b r ↔ ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) :=
  ⟨rel_of_isEqv, fun ⟨h, w⟩ => by
    simp only [isEqv, ← h, ↓reduceDIte]
    exact isEqvAux_of_rel h (by simp [h]) w⟩

Proof state:
α : Type u_1
a b : Array α
r : α → α → Bool
x✝ : ∃ h, ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true
h : a.size = b.size
w : ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true
⊢ a.isEqv b r = true

Tactic:
simp only [isEqv, ← h, ↓reduceDIte]

Result:
α : Type u_1
a b : Array α
r : α → α → Bool
x✝ : ∃ h, ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true
h : a.size = b.size
w : ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true
⊢ a.isEqvAux b ⋯ r a.size ⋯ = true

Proof state:
α : Type u_1
a b : Array α
r : α → α → Bool
x✝ : ∃ h, ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true
h : a.size = b.size
w : ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true
⊢ a.size ≤ a.size

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
a b : Array α
r : α → α → Bool
x✝ : ∃ h, ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true
h : a.size = b.size
w : ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true
⊢ a.isEqvAux b ⋯ r a.size ⋯ = true

Tactic:
exact isEqvAux_of_rel h (by simp [h]) w

Result:
no goals