harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem foldRev_succ {α : Type u} (n : Nat) (f : (i : Nat) → i < n + 1 → α → α) (init : α) :
    foldRev (n + 1) f init = foldRev n (fun i h => f i (by omega)) (f n (by omega) init)

Proof state:
α : Type u
n : Nat
f : (i : Nat) → i < n + 1 → α → α
init : α
⊢ n < n + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
n : Nat
f : (i : Nat) → i < n + 1 → α → α
init : α
⊢ (n + 1).foldRev f init = n.foldRev (fun i h => f i ⋯) (f n ⋯ init)

Tactic:
simp [foldRev]

Result:
no goals

Proof state:
α : Type u
n : Nat
f : (i : Nat) → i < n + 1 → α → α
init : α
i : Nat
h : i < n
⊢ i < n + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Star/Subsemiring.lean
theorem toSubsemiring_injective :
    Function.Injective (toSubsemiring : StarSubsemiring R → Subsemiring R) := fun S T h =>
  ext fun x => by rw [← mem_toSubsemiring, ← mem_toSubsemiring, h]

Proof state:
R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
S T : StarSubsemiring R
h : S.toSubsemiring = T.toSubsemiring
x : R
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toSubsemiring, ← mem_toSubsemiring, h]

Result:
no goals
-- Mathlib/GroupTheory/GroupExtension/Defs.lean
theorem inl_conjAct_comm {e : E} {n : N} : S.inl (S.conjAct e n) = e * S.inl n * e⁻¹

Proof state:
N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
e : E
n : N
⊢ S.inl ((S.conjAct e) n) = e * S.inl n * e⁻¹

Tactic:
simp only [conjAct, MonoidHom.coe_mk, OneHom.coe_mk, MulEquiv.trans_apply,
  MonoidHom.apply_ofInjective_symm, MulAut.conjNormal_apply, MonoidHom.ofInjective_apply]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_eq_top :
    emultiplicity a b = ⊤ ↔ ¬FiniteMultiplicity a b

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

Tactic:
simp [emultiplicity]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem loopyOn_indep_iff : (loopyOn E).Indep I ↔ I = ∅

Proof state:
α : Type u_1
E I : Set α
⊢ I = ∅ → I ⊆ E

Tactic:
rintro rfl

Result:
α : Type u_1
E : Set α
⊢ ∅ ⊆ E

Proof state:
α : Type u_1
E : Set α
⊢ ∅ ⊆ E

Tactic:
apply empty_subset

Result:
no goals

Proof state:
α : Type u_1
E I : Set α
⊢ (loopyOn E).Indep I ↔ I = ∅

Tactic:
simp only [loopyOn, restrict_indep_iff, emptyOn_indep_iff, and_iff_left_iff_imp]

Result:
α : Type u_1
E I : Set α
⊢ I = ∅ → I ⊆ E
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem isBridge_iff_adj_and_forall_walk_mem_edges {v w : V} :
    G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ p : G.Walk v w, s(v, w) ∈ p.edges

Proof state:
V : Type u
G : SimpleGraph V
v w : V
⊢ ¬(G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges

Tactic:
rw [reachable_delete_edges_iff_exists_walk, not_exists_not]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges

Tactic:
rw [isBridge_iff, and_congr_right']

Result:
V : Type u
G : SimpleGraph V
v w : V
⊢ ¬(G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
-- Mathlib/Data/Set/Image.lean
theorem forall_subtype_range_iff {p : range f → Prop} :
    (∀ a : range f, p a) ↔ ∀ i, p ⟨f i, mem_range_self _⟩ :=
  ⟨fun H _ => H _, fun H ⟨y, i, hi⟩ => by
    subst hi
    apply H⟩

Proof state:
α : Type u_1
ι : Sort u_4
f : ι → α
p : ↑(range f) → Prop
H : ∀ (i : ι), p ⟨f i, ⋯⟩
x✝ : ↑(range f)
y : α
i : ι
hi : f i = y
⊢ p ⟨y, ⋯⟩

Tactic:
subst hi

Result:
α : Type u_1
ι : Sort u_4
f : ι → α
p : ↑(range f) → Prop
H : ∀ (i : ι), p ⟨f i, ⋯⟩
x✝ : ↑(range f)
i : ι
⊢ p ⟨f i, ⋯⟩

Proof state:
α : Type u_1
ι : Sort u_4
f : ι → α
p : ↑(range f) → Prop
H : ∀ (i : ι), p ⟨f i, ⋯⟩
x✝ : ↑(range f)
i : ι
⊢ p ⟨f i, ⋯⟩

Tactic:
apply H

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
theorem inr_coprodZeroIso_hom (X : C) : coprod.inl ≫ (coprodZeroIso X).hom = 𝟙 X

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inl ≫ (coprodZeroIso X).hom = 𝟙 X

Tactic:
dsimp [coprodZeroIso, binaryCofanZeroRight]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inl ≫
      (colimit.isoColimitCocone
          { cocone := BinaryCofan.mk (𝟙 X) 0, isColimit := binaryCofanZeroRightIsColimit X }).hom =
    𝟙 X

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inl ≫
      (colimit.isoColimitCocone
          { cocone := BinaryCofan.mk (𝟙 X) 0, isColimit := binaryCofanZeroRightIsColimit X }).hom =
    𝟙 X

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem indicatorConstLp_eq_toSpanSingleton_compLp {s : Set α} [NormedSpace ℝ F]
    (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : F) :
    indicatorConstLp 2 hs hμs x =
      (ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs (1 : ℝ))

Proof state:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
h_compLp :
  ∀ᵐ (a : α) ∂μ,
    ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) a =
      (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
⊢ (s.indicator fun x_1 => x) =ᶠ[ae μ] ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))

Tactic:
rw [← EventuallyEq] at h_compLp

Result:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a =>
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
⊢ (s.indicator fun x_1 => x) =ᶠ[ae μ] ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))

Proof state:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a =>
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = s.indicator (fun x => 1) y
⊢ s.indicator (fun x_1 => x) y = (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) y)

Tactic:
rw [hy]

Result:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a =>
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = s.indicator (fun x => 1) y
⊢ s.indicator (fun x_1 => x) y = (ContinuousLinearMap.toSpanSingleton ℝ x) (s.indicator (fun x => 1) y)
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_nonpos (f : R → R) (a : A) (h : ∀ x ∈ spectrum R a, f x ≤ 0) :
    cfc f a ≤ 0

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.691365) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 0
⊢ cfc f a ≤ 0

Tactic:
by_cases hf : ContinuousOn f (spectrum R a)

Result:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.691365) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 0
hf : ContinuousOn f (spectrum R a)
⊢ cfc f a ≤ 0

case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.691365) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 0
hf : ¬ContinuousOn f (spectrum R a)
⊢ cfc f a ≤ 0

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.691365) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 0
hf : ContinuousOn f (spectrum R a)
⊢ cfc f a ≤ 0

Tactic:
simpa using cfc_mono h

Result:
no goals

Proof state:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 0
hf : ¬ContinuousOn f (spectrum R a)
⊢ cfc f a ≤ 0

Tactic:
simp only [cfc_apply_of_not_continuousOn _ hf, le_rfl]

Result:
no goals
-- Mathlib/Order/OrdContinuous.lean
theorem id : LeftOrdContinuous (id : α → α) := fun s x h => by
  simpa only [image_id] using h

Proof state:
α : Type u
inst✝ : Preorder α
s : Set α
x : α
h : IsLUB s x
⊢ IsLUB (id '' s) (id x)

Tactic:
simpa only [image_id] using h

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean
theorem exists_mem_adjoin_mul_eq_pow_natDegree {x : S} (hx : aeval x f = 0) (hmo : f.Monic)
    (hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})) : ∃ y ∈ adjoin R ({x} : Set S),
    (algebraMap R S) p * y = x ^ (f.map (algebraMap R S)).natDegree

Proof state:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree

Tactic:
have : ∀ n < f.natDegree, p ∣ f.coeff n := by
  intro n hn
  exact mem_span_singleton.1 (by simpa using hf.mem hn)

Result:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
this : ∀ n < f.natDegree, p ∣ f.coeff n
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree

Proof state:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
⊢ ∀ n < f.natDegree, p ∣ f.coeff n

Tactic:
intro n hn

Result:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
n : ℕ
hn : n < f.natDegree
⊢ p ∣ f.coeff n
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem comp_ofDual (f : α → E) (s : Set α) :
    eVariationOn (f ∘ ofDual) (ofDual ⁻¹' s) = eVariationOn f s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s) = eVariationOn f s

Tactic:
convert comp_eq_of_antitoneOn f ofDual fun _ _ _ _ => id

Result:
case h.e'_3.h.e'_6
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ s = ⇑ofDual '' (⇑ofDual ⁻¹' s)

Proof state:
case h.e'_3.h.e'_6
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ s = ⇑ofDual '' (⇑ofDual ⁻¹' s)

Tactic:
simp only [Equiv.image_preimage]

Result:
no goals
-- Mathlib/Data/Fin/Rev.lean
/-- `rev` commutes with `predAbove`. -/
lemma rev_predAbove {n : ℕ} (p : Fin n) (i : Fin (n + 1)) :
    (predAbove p i).rev = predAbove p.rev i.rev

Proof state:
n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ (p.predAbove i).rev = p.rev.predAbove i.rev

Tactic:
rw [predAbove_rev_left, rev_rev]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem differentiableWithinAt_of_isInvertible_fderivWithin
    (hf : (fderivWithin 𝕜 f s x).IsInvertible) : DifferentiableWithinAt 𝕜 f s 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
s : Set E
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬IsInvertible 0

Tactic:
contrapose! hf

Result:
𝕜 : 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
s : Set E
hf : IsInvertible 0
⊢ DifferentiableWithinAt 𝕜 f s 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
s : Set E
hf : (fderivWithin 𝕜 f s x).IsInvertible
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
contrapose hf

Result:
𝕜 : 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
s : Set E
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬(fderivWithin 𝕜 f s x).IsInvertible

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
s : Set E
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬(fderivWithin 𝕜 f s x).IsInvertible

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]

Result:
𝕜 : 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
s : Set E
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬IsInvertible 0

Proof state:
case intro
𝕜 : 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
s : Set E
hf : IsInvertible 0
hE : Subsingleton E
hF : Subsingleton F
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
exact (hasFDerivAt_of_subsingleton _ _).differentiableAt.differentiableWithinAt

Result:
no goals

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
s : Set E
hf : IsInvertible 0
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
rcases isInvertible_zero_iff.1 hf with ⟨hE, hF⟩

Result:
case intro
𝕜 : 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
s : Set E
hf : IsInvertible 0
hE : Subsingleton E
hF : Subsingleton F
⊢ DifferentiableWithinAt 𝕜 f s x
-- Mathlib/Data/Nat/Init.lean
lemma dvd_mul_of_div_dvd (h : b ∣ a) (hdiv : a / b ∣ c) : a ∣ b * c

Proof state:
a b c : ℕ
h : b ∣ a
hdiv : a / b ∣ c
⊢ a ∣ b * c

Tactic:
obtain ⟨e, rfl⟩ := hdiv

Result:
case intro
a b : ℕ
h : b ∣ a
e : ℕ
⊢ a ∣ b * (a / b * e)

Proof state:
case intro
a b : ℕ
h : b ∣ a
e : ℕ
⊢ a ∣ b * (a / b * e)

Tactic:
rw [← Nat.mul_assoc, Nat.mul_comm _ (a / b), Nat.div_mul_cancel h]

Result:
case intro
a b : ℕ
h : b ∣ a
e : ℕ
⊢ a ∣ a * e

Proof state:
case intro
a b : ℕ
h : b ∣ a
e : ℕ
⊢ a ∣ a * e

Tactic:
exact Nat.dvd_mul_right a e

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem erase_inter_comm (s t : Finset α) (a : α) : s.erase a ∩ t = s ∩ t.erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s.erase a ∩ t = s ∩ t.erase a

Tactic:
rw [erase_inter, inter_erase]

Result:
no goals
-- Mathlib/Algebra/Polynomial/RingDivision.lean
lemma aeval_ne_zero_of_isCoprime {R} [CommSemiring R] [Nontrivial S] [Semiring S] [Algebra R S]
    {p q : R[X]} (h : IsCoprime p q) (s : S) : aeval s p ≠ 0 ∨ aeval s q ≠ 0

Proof state:
case intro.intro
S : Type v
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : Nontrivial S
inst✝¹ : Semiring S
inst✝ : Algebra R S
p q : R[X]
s : S
hpq : (aeval s) p = 0 ∧ (aeval s) q = 0
w✝¹ w✝ : R[X]
h : (aeval s) (w✝¹ * p + w✝ * q) = (aeval s) 1
⊢ False

Tactic:
simp only [map_add, map_mul, map_one, hpq.left, hpq.right, mul_zero, add_zero, zero_ne_one] at h

Result:
no goals

Proof state:
S : Type v
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : Nontrivial S
inst✝¹ : Semiring S
inst✝ : Algebra R S
p q : R[X]
h : IsCoprime p q
s : S
hpq : (aeval s) p = 0 ∧ (aeval s) q = 0
⊢ False

Tactic:
rcases h with ⟨_, _, h⟩

Result:
case intro.intro
S : Type v
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : Nontrivial S
inst✝¹ : Semiring S
inst✝ : Algebra R S
p q : R[X]
s : S
hpq : (aeval s) p = 0 ∧ (aeval s) q = 0
w✝¹ w✝ : R[X]
h : w✝¹ * p + w✝ * q = 1
⊢ False

Proof state:
case intro.intro
S : Type v
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : Nontrivial S
inst✝¹ : Semiring S
inst✝ : Algebra R S
p q : R[X]
s : S
hpq : (aeval s) p = 0 ∧ (aeval s) q = 0
w✝¹ w✝ : R[X]
h : w✝¹ * p + w✝ * q = 1
⊢ False

Tactic:
apply_fun aeval s at h

Result:
case intro.intro
S : Type v
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : Nontrivial S
inst✝¹ : Semiring S
inst✝ : Algebra R S
p q : R[X]
s : S
hpq : (aeval s) p = 0 ∧ (aeval s) q = 0
w✝¹ w✝ : R[X]
h : (aeval s) (w✝¹ * p + w✝ * q) = (aeval s) 1
⊢ False

Proof state:
S : Type v
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : Nontrivial S
inst✝¹ : Semiring S
inst✝ : Algebra R S
p q : R[X]
h : IsCoprime p q
s : S
⊢ (aeval s) p ≠ 0 ∨ (aeval s) q ≠ 0

Tactic:
by_contra! hpq

Result:
S : Type v
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : Nontrivial S
inst✝¹ : Semiring S
inst✝ : Algebra R S
p q : R[X]
h : IsCoprime p q
s : S
hpq : (aeval s) p = 0 ∧ (aeval s) q = 0
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_right_cancel {n m k : Nat} (mp : 0 < m) (h : n * m = k * m) : n = k

Proof state:
n m k : Nat
mp : 0 < m
h : n * m = k * m
⊢ n = k

Tactic:
simp [Nat.mul_comm _ m] at h

Result:
n m k : Nat
mp : 0 < m
h : m * n = m * k
⊢ n = k

Proof state:
n m k : Nat
mp : 0 < m
h : m * n = m * k
⊢ n = k

Tactic:
apply Nat.mul_left_cancel mp h

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
/-- A common factor that's coprime with the modulus can be cancelled from a `ModEq` -/
lemma cancel_left_of_coprime (hmc : gcd m c = 1) (h : c * a ≡ c * b [MOD m]) : a ≡ b [MOD m]

Proof state:
case inl
a c : ℕ
hmc : c = 1
⊢ a ≡ a [MOD 0]

Tactic:
rfl

Result:
no goals

Proof state:
case inr
m a b c : ℕ
hmc : m.gcd c = 1
h : c * a ≡ c * b [MOD m]
hm : m > 0
⊢ a ≡ b [MOD m]

Tactic:
simpa [hmc] using h.cancel_left_div_gcd hm

Result:
no goals

Proof state:
m a b c : ℕ
hmc : m.gcd c = 1
h : c * a ≡ c * b [MOD m]
⊢ a ≡ b [MOD m]

Tactic:
rcases m.eq_zero_or_pos with (rfl | hm)

Result:
case inl
a b c : ℕ
hmc : gcd 0 c = 1
h : c * a ≡ c * b [MOD 0]
⊢ a ≡ b [MOD 0]

case inr
m a b c : ℕ
hmc : m.gcd c = 1
h : c * a ≡ c * b [MOD m]
hm : m > 0
⊢ a ≡ b [MOD m]

Proof state:
case inl
a b c : ℕ
hmc : gcd 0 c = 1
h : c * a ≡ c * b [MOD 0]
⊢ a ≡ b [MOD 0]

Tactic:
simp only [gcd_zero_left] at hmc

Result:
case inl
a b c : ℕ
h : c * a ≡ c * b [MOD 0]
hmc : c = 1
⊢ a ≡ b [MOD 0]

Proof state:
case inl
a b c : ℕ
hmc : c = 1
h : a = b
⊢ a ≡ b [MOD 0]

Tactic:
subst h

Result:
case inl
a c : ℕ
hmc : c = 1
⊢ a ≡ a [MOD 0]

Proof state:
case inl
a b c : ℕ
h : c * a ≡ c * b [MOD 0]
hmc : c = 1
⊢ a ≡ b [MOD 0]

Tactic:
simp only [gcd_zero_left, hmc, one_mul, modEq_zero_iff] at h

Result:
case inl
a b c : ℕ
hmc : c = 1
h : a = b
⊢ a ≡ b [MOD 0]
-- Mathlib/ModelTheory/Basic.lean
theorem ofInjective_toHom [L.IsAlgebraic] {f : M →[L] N} (hf : Function.Injective f) :
    (ofInjective hf).toHom = f

Proof state:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.IsAlgebraic
f : M →[L] N
hf : Function.Injective ⇑f
⊢ (ofInjective hf).toHom = f

Tactic:
ext

Result:
case h
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.IsAlgebraic
f : M →[L] N
hf : Function.Injective ⇑f
x✝ : M
⊢ (ofInjective hf).toHom x✝ = f x✝

Proof state:
case h
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.IsAlgebraic
f : M →[L] N
hf : Function.Injective ⇑f
x✝ : M
⊢ (ofInjective hf).toHom x✝ = f x✝

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem sum_apply {α : Type*} (f : α → MultilinearMap R M₁ M₂) (m : ∀ i, M₁ i) {s : Finset α} :
    (∑ a ∈ s, f a) m = ∑ a ∈ s, f a m

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M₁ i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : ι) → Module R (M₁ i)
inst✝ : Module R M₂
α : Type u_1
f : α → MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
s : Finset α
⊢ (∑ a ∈ s, f a) m = ∑ a ∈ s, (f a) m

Tactic:
simp

Result:
no goals