harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Valuation/Integers.lean
lemma isPrincipal_iff_exists_eq_setOf_valuation_le (hv : Integers v O) {I : Ideal O} :
    I.IsPrincipal ↔ ∃ x, (I : Set O) = {y | v (algebraMap O F y) ≤ v (algebraMap O F x)}

Proof state:
case mpr.intro.refine_1
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}
⊢ x ∈ ↑I

Tactic:
simp [hx]

Result:
no goals

Proof state:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : Γ₀
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x
⊢ ∃ a ∈ I, (⇑v ∘ ⇑(algebraMap O F)) a = x

Tactic:
simpa using hx.left

Result:
no goals

Proof state:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
⊢ (∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x) ↔ ∃ x, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}

Tactic:
constructor <;> rintro ⟨x, hx⟩

Result:
case mp.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : Γ₀
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x
⊢ ∃ x, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}

case mpr.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}
⊢ ∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x

Proof state:
case mpr.intro.refine_2
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}
⊢ v ((algebraMap O F) x) ∈ upperBounds (⇑v ∘ ⇑(algebraMap O F) '' ↑I)

Tactic:
simp [hx, mem_upperBounds]

Result:
no goals
-- Mathlib/Data/Setoid/Partition.lean
theorem classes_mkClasses (c : Set (Set α)) (hc : IsPartition c) :
    (mkClasses c hc.2).classes = c

Proof state:
case h
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ (mkClasses c ⋯).classes ↔ s ∈ c

Tactic:
constructor

Result:
case h.mp
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ (mkClasses c ⋯).classes → s ∈ c

case h.mpr
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ c → s ∈ (mkClasses c ⋯).classes

Proof state:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
⊢ (mkClasses c ⋯).classes = c

Tactic:
ext s

Result:
case h
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ (mkClasses c ⋯).classes ↔ s ∈ c

Proof state:
case h.mpr
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ c → s ∈ (mkClasses c ⋯).classes

Tactic:
exact exists_of_mem_partition hc

Result:
no goals

Proof state:
case h.mp
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ (mkClasses c ⋯).classes → s ∈ c

Tactic:
rintro ⟨y, rfl⟩

Result:
case h.mp.intro
α : Type u_1
c : Set (Set α)
hc : IsPartition c
y : α
⊢ {x | (mkClasses c ⋯) x y} ∈ c

Proof state:
case h.mp.intro
α : Type u_1
c : Set (Set α)
hc : IsPartition c
y : α
⊢ {x | (mkClasses c ⋯) x y} ∈ c

Tactic:
obtain ⟨b, ⟨hb, hy⟩, _⟩ := hc.2 y

Result:
case h.mp.intro.intro.intro.intro
α : Type u_1
c : Set (Set α)
hc : IsPartition c
y : α
b : Set α
right✝ : ∀ (y_1 : Set α), (fun b => b ∈ c ∧ y ∈ b) y_1 → y_1 = b
hb : b ∈ c
hy : y ∈ b
⊢ {x | (mkClasses c ⋯) x y} ∈ c

Proof state:
case h.mp.intro.intro.intro.intro
α : Type u_1
c : Set (Set α)
hc : IsPartition c
y : α
b : Set α
right✝ : ∀ (y_1 : Set α), (fun b => b ∈ c ∧ y ∈ b) y_1 → y_1 = b
hb : b ∈ c
hy : y ∈ b
⊢ {x | (mkClasses c ⋯) x y} ∈ c

Tactic:
rwa [← eq_eqv_class_of_mem _ hb hy]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_mul_C_le (f : R[X]) (a : R) : (f * C a).natDegree ≤ f.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
a : R
⊢ (f * C a).natDegree ≤ f.natDegree

Tactic:
simpa using natDegree_mul_le (q := C a)

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem prelimitRecOn_of_isSuccPrelimit (hb : IsSuccPrelimit b) :
    prelimitRecOn b hs hl = hl b hb fun x _ ↦ SuccOrder.prelimitRecOn x hs hl

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → C b) → C a
hb : IsSuccPrelimit b
⊢ (hl b hb fun y x =>
      ⋯.fix
        (fun a IH =>
          if h : IsSuccPrelimit a then hl a h IH else cast ⋯ (hs (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
        y) =
    hl b hb fun x x_1 => prelimitRecOn x hs hl

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → C b) → C a
hb : IsSuccPrelimit b
⊢ prelimitRecOn b hs hl = hl b hb fun x x_1 => prelimitRecOn x hs hl

Tactic:
rw [prelimitRecOn, WellFounded.fix_eq, dif_pos hb]

Result:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → C b) → C a
hb : IsSuccPrelimit b
⊢ (hl b hb fun y x =>
      ⋯.fix
        (fun a IH =>
          if h : IsSuccPrelimit a then hl a h IH else cast ⋯ (hs (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
        y) =
    hl b hb fun x x_1 => prelimitRecOn x hs hl
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma mem_supp_congr_adj {v w : V} (c : G.ConnectedComponent) (hadj : G.Adj v w) :
    v ∈ c.supp ↔ w ∈ c.supp

Proof state:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
⊢ G.connectedComponentMk v = c ↔ G.connectedComponentMk w = c

Tactic:
constructor <;> intro h <;> simp only [← h] <;> apply connectedComponentMk_eq_of_adj

Result:
case mp.a
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk v = c
⊢ G.Adj w v

case mpr.a
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
⊢ G.Adj v w

Proof state:
case mpr.a
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
⊢ G.Adj v w

Tactic:
exact hadj

Result:
no goals

Proof state:
case mp.a
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk v = c
⊢ G.Adj w v

Tactic:
exact hadj.symm

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
⊢ v ∈ c.supp ↔ w ∈ c.supp

Tactic:
simp only [ConnectedComponent.mem_supp_iff] at *

Result:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
⊢ G.connectedComponentMk v = c ↔ G.connectedComponentMk w = c
-- Mathlib/Combinatorics/Additive/Corner/Roth.lean
@[simp]
private lemma mk_mem_triangleIndices : (a, b, c) ∈ triangleIndices A ↔ (a, b) ∈ A ∧ c = a + b

Proof state:
case intro.intro.intro.intro.intro
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
h₁ : (a, b) ∈ A
h₂ : c = a + b
⊢ (a, b) ∈ A ∧ c = a + b

Tactic:
exact ⟨h₁, h₂⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
⊢ (∃ a_1 b_1, (a_1, b_1) ∈ A ∧ a = a_1 ∧ b = b_1 ∧ c = a_1 + b_1) → (a, b) ∈ A ∧ c = a + b

Tactic:
rintro ⟨_, _, h₁, rfl, rfl, h₂⟩

Result:
case intro.intro.intro.intro.intro
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
h₁ : (a, b) ∈ A
h₂ : c = a + b
⊢ (a, b) ∈ A ∧ c = a + b

Proof state:
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
⊢ (a, b, c) ∈ Corners.triangleIndices A ↔ (a, b) ∈ A ∧ c = a + b

Tactic:
simp only [triangleIndices, Prod.ext_iff, mem_map, Embedding.coeFn_mk, exists_prop, Prod.exists,
  eq_comm]

Result:
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
⊢ (∃ a_1 b_1, (a_1, b_1) ∈ A ∧ a = a_1 ∧ b = b_1 ∧ c = a_1 + b_1) ↔ (a, b) ∈ A ∧ c = a + b

Proof state:
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
⊢ (∃ a_1 b_1, (a_1, b_1) ∈ A ∧ a = a_1 ∧ b = b_1 ∧ c = a_1 + b_1) ↔ (a, b) ∈ A ∧ c = a + b

Tactic:
refine ⟨?_, fun h ↦ ⟨_, _, h.1, rfl, rfl, h.2⟩⟩

Result:
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
⊢ (∃ a_1 b_1, (a_1, b_1) ∈ A ∧ a = a_1 ∧ b = b_1 ∧ c = a_1 + b_1) → (a, b) ∈ A ∧ c = a + b
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubOfPoint_eq_of_sum_eq_zero (w : ι → k) (p : ι → P) (h : ∑ i ∈ s, w i = 0)
    (b₁ b₂ : P) : s.weightedVSubOfPoint p b₁ w = s.weightedVSubOfPoint p b₂ w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : ∑ i ∈ s, w i = 0
b₁ b₂ : P
⊢ (s.weightedVSubOfPoint p b₁) w = (s.weightedVSubOfPoint p b₂) w

Tactic:
apply eq_of_sub_eq_zero

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : ∑ i ∈ s, w i = 0
b₁ b₂ : P
⊢ (s.weightedVSubOfPoint p b₁) w - (s.weightedVSubOfPoint p b₂) w = 0

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : ∑ i ∈ s, w i = 0
b₁ b₂ : P
⊢ (s.weightedVSubOfPoint p b₁) w - (s.weightedVSubOfPoint p b₂) w = 0

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_sub_distrib]

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : ∑ i ∈ s, w i = 0
b₁ b₂ : P
⊢ ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)) = 0

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : ∑ i ∈ s, w i = 0
b₁ b₂ : P
⊢ ∑ x ∈ s, w x • (b₂ -ᵥ b₁) = 0

Tactic:
rw [← sum_smul, h, zero_smul]

Result:
no goals
-- Mathlib/Topology/GDelta/Basic.lean
theorem IsGδ.biUnion {s : Set ι} (hs : s.Finite) {f : ι → Set X} (h : ∀ i ∈ s, IsGδ (f i)) :
    IsGδ (⋃ i ∈ s, f i)

Proof state:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Finite
f : ι → Set X
h : ∀ i ∈ s, IsGδ (f i)
⊢ IsGδ (⋃ i ∈ s, f i)

Tactic:
rw [← sUnion_image]

Result:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Finite
f : ι → Set X
h : ∀ i ∈ s, IsGδ (f i)
⊢ IsGδ (⋃₀ (f '' s))

Proof state:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Finite
f : ι → Set X
h : ∀ i ∈ s, IsGδ (f i)
⊢ IsGδ (⋃₀ (f '' s))

Tactic:
exact .sUnion (hs.image _) (forall_mem_image.2 h)

Result:
no goals
-- Mathlib/Algebra/Homology/CommSq.lean
lemma IsPullback.mono_shortComplex'_f (h : IsPullback fst snd f g) :
    Mono h.shortComplex'.f

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
P✝ : C
b : P✝ ⟶ ⋯.shortComplex'.X₁
hb : b ≫ ⋯.shortComplex'.f = 0
⊢ b = 0

Tactic:
exact Fork.IsLimit.hom_ext h.isLimitKernelFork (by simpa using hb)

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
⊢ Mono ⋯.shortComplex'.f

Tactic:
rw [Preadditive.mono_iff_cancel_zero]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
⊢ ∀ (P : C) (g_1 : P ⟶ ⋯.shortComplex'.X₁), g_1 ≫ ⋯.shortComplex'.f = 0 → g_1 = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
⊢ ∀ (P : C) (g_1 : P ⟶ ⋯.shortComplex'.X₁), g_1 ≫ ⋯.shortComplex'.f = 0 → g_1 = 0

Tactic:
intro _ b hb

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
P✝ : C
b : P✝ ⟶ ⋯.shortComplex'.X₁
hb : b ≫ ⋯.shortComplex'.f = 0
⊢ b = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
P✝ : C
b : P✝ ⟶ ⋯.shortComplex'.X₁
hb : b ≫ ⋯.shortComplex'.f = 0
⊢ b ≫ Fork.ι ⋯.kernelFork = 0 ≫ Fork.ι ⋯.kernelFork

Tactic:
simpa using hb

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma algebraMap_le_of_le_spectrum {r : R} {a : A} (h : ∀ x ∈ spectrum R a, r ≤ x)
    (ha : p a

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.711710) [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
r : R
a : A
h : ∀ x ∈ spectrum R a, r ≤ x
ha : autoParam (p a) _auto✝
⊢ (algebraMap R A) r ≤ cfc id a

Tactic:
exact algebraMap_le_cfc id r a h

Result:
no goals

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.711710) [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
r : R
a : A
h : ∀ x ∈ spectrum R a, r ≤ x
ha : autoParam (p a) _auto✝
⊢ (algebraMap R A) r ≤ a

Tactic:
rw [← cfc_id R a]

Result:
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.711710) [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
r : R
a : A
h : ∀ x ∈ spectrum R a, r ≤ x
ha : autoParam (p a) _auto✝
⊢ (algebraMap R A) r ≤ cfc id a
-- Mathlib/Data/Nat/PartENat.lean
theorem le_coe_iff (x : PartENat) (n : ℕ) : x ≤ n ↔ ∃ h : x.Dom, x.get h ≤ n

Proof state:
x : PartENat
n : ℕ
⊢ x ≤ ↑n ↔ ∃ (h : x.Dom), x.get h ≤ n

Tactic:
show (∃ h : True → x.Dom, _) ↔ ∃ h : x.Dom, x.get h ≤ n

Result:
x : PartENat
n : ℕ
⊢ (∃ (h : True → x.Dom), ∀ (hy : (↑n).Dom), x.get ⋯ ≤ (↑n).get hy) ↔ ∃ (h : x.Dom), x.get h ≤ n

Proof state:
x : PartENat
n : ℕ
⊢ (∃ (h : True → x.Dom), ∀ (hy : (↑n).Dom), x.get ⋯ ≤ (↑n).get hy) ↔ ∃ (h : x.Dom), x.get h ≤ n

Tactic:
simp only [forall_prop_of_true, dom_natCast, get_natCast']

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
theorem disjoint_map_map {f : α → γ} {g : β → γ} {s : Multiset α} {t : Multiset β} :
    Disjoint (s.map f) (t.map g) ↔ ∀ a ∈ s, ∀ b ∈ t, f a ≠ g b

Proof state:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
⊢ _root_.Disjoint (map f s) (map g t) ↔ ∀ a ∈ s, ∀ b ∈ t, f a ≠ g b

Tactic:
simp [disjoint_iff_ne]

Result:
no goals
-- Mathlib/Topology/LocalAtTarget.lean
theorem Set.restrictPreimage_isInducing (s : Set β) (h : IsInducing f) :
    IsInducing (s.restrictPreimage f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
h : IsInducing f
⊢ IsInducing (s.restrictPreimage f)

Tactic:
simp_rw [← IsInducing.subtypeVal.of_comp_iff, isInducing_iff_nhds, restrictPreimage,
  MapsTo.coe_restrict, restrict_eq, ← @Filter.comap_comap _ _ _ _ _ f, Function.comp_apply] at h ⊢

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))
⊢ ∀ (x : ↑(f ⁻¹' s)), 𝓝 x = comap Subtype.val (comap f (𝓝 (f ↑x)))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))
a : ↑(f ⁻¹' s)
⊢ 𝓝 a = comap Subtype.val (comap f (𝓝 (f ↑a)))

Tactic:
rw [← h, ← IsInducing.subtypeVal.nhds_eq_comap]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))
⊢ ∀ (x : ↑(f ⁻¹' s)), 𝓝 x = comap Subtype.val (comap f (𝓝 (f ↑x)))

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))
a : ↑(f ⁻¹' s)
⊢ 𝓝 a = comap Subtype.val (comap f (𝓝 (f ↑a)))
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bsup_eq_bsup {ι : Type u} (r r' : ι → ι → Prop) [IsWellOrder ι r] [IsWellOrder ι r']
    (f : ι → Ordinal.{max u v}) :
    bsup.{_, v} _ (bfamilyOfFamily' r f) = bsup.{_, v} _ (bfamilyOfFamily' r' f)

Proof state:
ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ (type r).bsup (bfamilyOfFamily' r f) = (type r').bsup (bfamilyOfFamily' r' f)

Tactic:
rw [bsup_eq_sup', bsup_eq_sup']

Result:
no goals
-- Mathlib/Algebra/DualNumber.lean
theorem lift_smul (fe : {fe : (A →ₐ[R] B) × B // _}) (a : A) (ad : A[ε]) :
    lift fe (a • ad) = fe.val.1 a * lift fe ad

Proof state:
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
a : A
ad : A[ε]
⊢ (lift fe) (a • ad) = (↑fe).1 a * (lift fe) ad

Tactic:
rw [← inl_mul_eq_smul, map_mul, lift_apply_inl]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem pred_le_iff {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : pred i hi ≤ j ↔ i ≤ succ j

Proof state:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ i.pred hi ≤ j ↔ i ≤ j.succ

Tactic:
rw [← succ_le_succ_iff, succ_pred]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldrM_reverse' [Monad m] (l : Array α) (f : α → β → m β) (b)
    (w : start = l.size) :
    l.reverse.foldrM f b start 0 = l.foldlM (fun x y => f y x) b

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
b : β
l : List α
⊢ foldrM f b { toList := l }.reverse { toList := l }.size = foldlM (fun x y => f y x) b { toList := l }

Tactic:
simp [List.foldrM_reverse]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : Array α
f : α → β → m β
b : β
⊢ foldrM f b l.reverse l.size = foldlM (fun x y => f y x) b l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
b : β
l : List α
⊢ foldrM f b { toList := l }.reverse { toList := l }.size = foldlM (fun x y => f y x) b { toList := l }

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
start : Nat
inst✝ : Monad m
l : Array α
f : α → β → m β
b : β
w : start = l.size
⊢ foldrM f b l.reverse start = foldlM (fun x y => f y x) b l

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : Array α
f : α → β → m β
b : β
⊢ foldrM f b l.reverse l.size = foldlM (fun x y => f y x) b l
-- Mathlib/CategoryTheory/Galois/Basic.lean
@[simp]
lemma fiberBinaryProductEquiv_symm_fst_apply {X Y : C} (x : F.obj X) (y : F.obj Y) :
    F.map prod.fst ((fiberBinaryProductEquiv F X Y).symm (x, y)) = x

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).carrier
y : (F.obj Y).carrier
⊢ ((Types.binaryProductIso (F.obj X).carrier (F.obj Y).carrier).inv ≫
        (PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y).inv ≫ (F ⋙ FintypeCat.incl).map prod.fst)
      (x, y) =
    x

Tactic:
erw [PreservesLimitPair.iso_inv_fst, Types.binaryProductIso_inv_comp_fst]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).carrier
y : (F.obj Y).carrier
⊢ F.map prod.fst ((fiberBinaryProductEquiv F X Y).symm (x, y)) = x

Tactic:
simp only [fiberBinaryProductEquiv, comp_obj, FintypeCat.incl_obj, Iso.toEquiv_comp,
  Equiv.symm_trans_apply, Iso.toEquiv_symm_fun]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).carrier
y : (F.obj Y).carrier
⊢ F.map prod.fst
      ((PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y).inv
        ((Types.binaryProductIso (F.obj X).carrier (F.obj Y).carrier).inv (x, y))) =
    x

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).carrier
y : (F.obj Y).carrier
⊢ F.map prod.fst
      ((PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y).inv
        ((Types.binaryProductIso (F.obj X).carrier (F.obj Y).carrier).inv (x, y))) =
    x

Tactic:
change ((Types.binaryProductIso _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map prod.fst) _ = _

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).carrier
y : (F.obj Y).carrier
⊢ ((Types.binaryProductIso (F.obj X).carrier (F.obj Y).carrier).inv ≫
        (PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y).inv ≫ (F ⋙ FintypeCat.incl).map prod.fst)
      (x, y) =
    x
-- Mathlib/Data/Matrix/Mul.lean
theorem one_mulVec (v : m → α) : 1 *ᵥ v = v

Proof state:
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
⊢ 1 *ᵥ v = v

Tactic:
ext

Result:
case h
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
x✝ : m
⊢ (1 *ᵥ v) x✝ = v x✝

Proof state:
case h
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
x✝ : m
⊢ (1 *ᵥ v) x✝ = v x✝

Tactic:
rw [← diagonal_one, mulVec_diagonal, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem sub_bmod_bmod : Int.bmod (x - Int.bmod y n) n = Int.bmod (x - y) n

Proof state:
x y : Int
n : Nat
⊢ (x - y.bmod n + y.bmod n).bmod n = (x - y + y.bmod n).bmod n

Tactic:
rw [Int.sub_add_cancel, add_bmod_bmod, Int.sub_add_cancel]

Result:
no goals

Proof state:
x y : Int
n : Nat
⊢ (x - y.bmod n).bmod n = (x - y).bmod n

Tactic:
apply (bmod_add_cancel_right (bmod y n)).mp

Result:
x y : Int
n : Nat
⊢ (x - y.bmod n + y.bmod n).bmod n = (x - y + y.bmod n).bmod n
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_zsmul_add' (a b : α) (m : ℤ) :
    toIcoMod hp (m • p + a) b = m • p + toIcoMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp (m • p + a) b = m • p + toIcoMod hp a b

Tactic:
rw [add_comm, toIcoMod_add_zsmul', add_comm]

Result:
no goals