harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem idxOf_append [BEq α] [LawfulBEq α] {l₁ l₂ : Array α} {a : α} :
    (l₁ ++ l₂).idxOf a = if a ∈ l₁ then l₁.idxOf a else l₂.idxOf a + l₁.size

Proof state:
case isTrue
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : Array α
a : α
h : findIdx (fun x => x == a) l₁ < l₁.size
⊢ findIdx (fun x => x == a) l₁ = if a ∈ l₁ then findIdx (fun x => x == a) l₁ else findIdx (fun x => x == a) l₂ + l₁.size

Tactic:
rw [if_pos]

Result:
case isTrue.hc
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : Array α
a : α
h : findIdx (fun x => x == a) l₁ < l₁.size
⊢ a ∈ l₁

Proof state:
case isFalse.hnc
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : Array α
a : α
h : ¬findIdx (fun x => x == a) l₁ < l₁.size
⊢ ¬a ∈ l₁

Tactic:
simpa using h

Result:
no goals

Proof state:
case isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : Array α
a : α
h : ¬findIdx (fun x => x == a) l₁ < l₁.size
⊢ findIdx (fun x => x == a) l₂ + l₁.size =
    if a ∈ l₁ then findIdx (fun x => x == a) l₁ else findIdx (fun x => x == a) l₂ + l₁.size

Tactic:
rw [if_neg]

Result:
case isFalse.hnc
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : Array α
a : α
h : ¬findIdx (fun x => x == a) l₁ < l₁.size
⊢ ¬a ∈ l₁

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : Array α
a : α
⊢ idxOf a (l₁ ++ l₂) = if a ∈ l₁ then idxOf a l₁ else idxOf a l₂ + l₁.size

Tactic:
rw [idxOf, findIdx_append]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : Array α
a : α
⊢ (if findIdx (fun x => x == a) l₁ < l₁.size then findIdx (fun x => x == a) l₁
    else findIdx (fun x => x == a) l₂ + l₁.size) =
    if a ∈ l₁ then findIdx (fun x => x == a) l₁ else findIdx (fun x => x == a) l₂ + l₁.size

Proof state:
case isTrue.hc
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : Array α
a : α
h : findIdx (fun x => x == a) l₁ < l₁.size
⊢ a ∈ l₁

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : Array α
a : α
⊢ (if findIdx (fun x => x == a) l₁ < l₁.size then findIdx (fun x => x == a) l₁
    else findIdx (fun x => x == a) l₂ + l₁.size) =
    if a ∈ l₁ then findIdx (fun x => x == a) l₁ else findIdx (fun x => x == a) l₂ + l₁.size

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : Array α
a : α
h : findIdx (fun x => x == a) l₁ < l₁.size
⊢ findIdx (fun x => x == a) l₁ = if a ∈ l₁ then findIdx (fun x => x == a) l₁ else findIdx (fun x => x == a) l₂ + l₁.size

case isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : Array α
a : α
h : ¬findIdx (fun x => x == a) l₁ < l₁.size
⊢ findIdx (fun x => x == a) l₂ + l₁.size =
    if a ∈ l₁ then findIdx (fun x => x == a) l₁ else findIdx (fun x => x == a) l₂ + l₁.size
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma rpow_rpow [IsTopologicalRing A] [T2Space A]
    (a : A) (x y : ℝ) (ha₁ : 0 ∉ spectrum ℝ≥0 a) (hx : x ≠ 0) (ha₂ : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
ha₁ : 0 ∉ spectrum ℝ≥0 a
hx : x ≠ 0
ha₂ : autoParam (0 ≤ a) _auto✝
x✝¹ : ℝ≥0
x✝ : x✝¹ ∈ spectrum ℝ≥0 a
⊢ ((fun x => x ^ y) ∘ fun x_1 => x_1 ^ x) x✝¹ = x✝¹ ^ (x * y)

Tactic:
simp [NNReal.rpow_mul]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
ha₁ : 0 ∉ spectrum ℝ≥0 a
hx : x ≠ 0
ha₂ : autoParam (0 ≤ a) _auto✝
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
simp only [rpow_def]

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
ha₁ : 0 ∉ spectrum ℝ≥0 a
hx : x ≠ 0
ha₂ : autoParam (0 ≤ a) _auto✝
⊢ cfc (fun x => x ^ y) (cfc (fun x_1 => x_1 ^ x) a) = cfc (fun x_1 => x_1 ^ (x * y)) a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
ha₁ : 0 ∉ spectrum ℝ≥0 a
hx : x ≠ 0
ha₂ : autoParam (0 ≤ a) _auto✝
⊢ cfc ((fun x => x ^ y) ∘ fun x_1 => x_1 ^ x) a = cfc (fun x_1 => x_1 ^ (x * y)) a

Tactic:
refine cfc_congr fun _ _ => ?_

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
ha₁ : 0 ∉ spectrum ℝ≥0 a
hx : x ≠ 0
ha₂ : autoParam (0 ≤ a) _auto✝
x✝¹ : ℝ≥0
x✝ : x✝¹ ∈ spectrum ℝ≥0 a
⊢ ((fun x => x ^ y) ∘ fun x_1 => x_1 ^ x) x✝¹ = x✝¹ ^ (x * y)

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
ha₁ : 0 ∉ spectrum ℝ≥0 a
hx : x ≠ 0
ha₂ : autoParam (0 ≤ a) _auto✝
⊢ cfc (fun x => x ^ y) (cfc (fun x_1 => x_1 ^ x) a) = cfc (fun x_1 => x_1 ^ (x * y)) a

Tactic:
rw [← cfc_comp _ _ a ha₂]

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
ha₁ : 0 ∉ spectrum ℝ≥0 a
hx : x ≠ 0
ha₂ : autoParam (0 ≤ a) _auto✝
⊢ cfc ((fun x => x ^ y) ∘ fun x_1 => x_1 ^ x) a = cfc (fun x_1 => x_1 ^ (x * y)) a
-- Mathlib/Data/NNReal/Defs.lean
@[simp] lemma toNNReal_abs (x : ℝ) : |x|.toNNReal = nnabs x := NNReal.coe_injective <| by simp

Proof state:
x : ℝ
⊢ ↑|x|.toNNReal = ↑(nnabs x)

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/TMConfig.lean
theorem stepNormal.is_ret (c k v) : ∃ k' v', stepNormal c k v = Cfg.ret k' v'

Proof state:
c : Code
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal c k v = Cfg.ret k' v'

Tactic:
induction c generalizing k v with
| cons _f fs IHf _IHfs => apply IHf
| comp f _g _IHf IHg => apply IHg
| case f g IHf IHg =>
  rw [stepNormal]
  simp only []
  cases v.headI <;> [apply IHf; apply IHg]
| fix f IHf => apply IHf
| _ => exact ⟨_, _, rfl⟩

Result:
no goals

Proof state:
case fix
f : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal f.fix k v = Cfg.ret k' v'

Tactic:
apply IHf

Result:
no goals

Proof state:
case case
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v',
    (fun k v => Nat.rec (stepNormal f k v.tail) (fun y x => stepNormal g k (y :: v.tail)) v.headI) k v = Cfg.ret k' v'

Tactic:
simp only []

Result:
case case
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', Nat.rec (stepNormal f k v.tail) (fun y x => stepNormal g k (y :: v.tail)) v.headI = Cfg.ret k' v'

Proof state:
case case
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (f.case g) k v = Cfg.ret k' v'

Tactic:
rw [stepNormal]

Result:
case case
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v',
    (fun k v => Nat.rec (stepNormal f k v.tail) (fun y x => stepNormal g k (y :: v.tail)) v.headI) k v = Cfg.ret k' v'

Proof state:
case case
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', Nat.rec (stepNormal f k v.tail) (fun y x => stepNormal g k (y :: v.tail)) v.headI = Cfg.ret k' v'

Tactic:
cases v.headI <;> [apply IHf; apply IHg]

Result:
no goals

Proof state:
case cons
_f fs : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal _f k v = Cfg.ret k' v'
_IHfs : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal fs k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (_f.cons fs) k v = Cfg.ret k' v'

Tactic:
apply IHf

Result:
no goals

Proof state:
case tail
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal Code.tail k v = Cfg.ret k' v'

Tactic:
exact ⟨_, _, rfl⟩

Result:
no goals

Proof state:
case comp
f _g : Code
_IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal _g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (f.comp _g) k v = Cfg.ret k' v'

Tactic:
apply IHg

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem _root_.minpoly.degree_dvd {x : L} (hx : IsIntegral K x) :
    (minpoly K x).natDegree ∣ finrank K L

Proof state:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ ∃ c, finrank K L = c * finrank K ↥K⟮x⟯

Tactic:
use finrank K⟮x⟯ L

Result:
case h
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ finrank K L = finrank (↥K⟮x⟯) L * finrank K ↥K⟮x⟯

Proof state:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ (minpoly K x).natDegree ∣ finrank K L

Tactic:
rw [dvd_iff_exists_eq_mul_left, ← IntermediateField.adjoin.finrank hx]

Result:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ ∃ c, finrank K L = c * finrank K ↥K⟮x⟯

Proof state:
case h
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ finrank K L = finrank (↥K⟮x⟯) L * finrank K ↥K⟮x⟯

Tactic:
rw [mul_comm, finrank_mul_finrank]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem mul_smul (b b' : B) (x : X') : (b * b') • x = b • b' • x :=
  match x with
  | fromCoset y => by
    change fromCoset _ = fromCoset _
    simp only [leftCoset_assoc]
  | ∞ => rfl

Proof state:
A B : Grp
f : A ⟶ B
b b' : ↑B
x : X'
y : ↑X
⊢ (b * b') • fromCoset y = b • b' • fromCoset y

Tactic:
change fromCoset _ = fromCoset _

Result:
A B : Grp
f : A ⟶ B
b b' : ↑B
x : X'
y : ↑X
⊢ fromCoset ⟨(b * b') • ↑y, ⋯⟩ = fromCoset ⟨b • ↑⟨b' • ↑y, ⋯⟩, ⋯⟩

Proof state:
A B : Grp
f : A ⟶ B
b b' : ↑B
x : X'
y : ↑X
⊢ fromCoset ⟨(b * b') • ↑y, ⋯⟩ = fromCoset ⟨b • ↑⟨b' • ↑y, ⋯⟩, ⋯⟩

Tactic:
simp only [leftCoset_assoc]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem range_eq_top : f.range = ⊤ ↔ Function.Surjective f

Proof state:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ f.range = ⊤ ↔ Function.Surjective ⇑f

Tactic:
rw [SetLike.ext'_iff, coe_range, LieSubmodule.top_coe, Set.range_eq_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get_insertMany_list_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l)
    {h} :
    (m.insertMany l).get k' h = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v :=
  Raw₀.get_insertMany_list_of_mem ⟨m.1, _⟩ m.2 k_beq distinct mem

Proof state:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h : k' ∈ m.insertMany l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h : k' ∈ m.insertMany l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h : k' ∈ m.insertMany l
⊢ k = k'
-- Mathlib/Data/Num/Lemmas.lean
theorem cmp_eq (m n) : cmp m n = Ordering.eq ↔ m = n

Proof state:
m n : Num
this : Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ m.cmp n = Ordering.eq ↔ m = n

Tactic:
revert this

Result:
m n : Num
⊢ Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m) → (m.cmp n = Ordering.eq ↔ m = n)

Proof state:
m n : Num
⊢ Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m) → (m.cmp n = Ordering.eq ↔ m = n)

Tactic:
cases cmp m n <;> intro this <;> simp at this ⊢ <;> try { exact this } <;>
simp [show m ≠ n from fun e => by rw [e] at this; exact lt_irrefl _ this]

Result:
no goals

Proof state:
case eq
m n : Num
this : m = n
⊢ m = n

Tactic:
exact this

Result:
no goals

Proof state:
m n : Num
this : ↑n < ↑m
e : m = n
⊢ False

Tactic:
rw [e] at this

Result:
m n : Num
this : ↑n < ↑n
e : m = n
⊢ False

Proof state:
m n : Num
⊢ m.cmp n = Ordering.eq ↔ m = n

Tactic:
have := cmp_to_nat m n

Result:
m n : Num
this : Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ m.cmp n = Ordering.eq ↔ m = n

Proof state:
m n : Num
this : ↑n < ↑n
e : m = n
⊢ False

Tactic:
exact lt_irrefl _ this

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem WCovBy.Ico_subset (h : a ⩿ b) : Ico a b ⊆ {a}

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ Ico a b ⊆ {a}

Tactic:
rw [← Icc_diff_right, h.Icc_eq, diff_singleton_subset_iff, pair_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Injective/Basic.lean
theorem injective_iff_preservesEpimorphisms_yoneda_obj (J : C) :
    Injective J ↔ (yoneda.obj J).PreservesEpimorphisms

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : C
⊢ Injective J ↔ (yoneda.obj J).PreservesEpimorphisms

Tactic:
rw [injective_iff_projective_op, Projective.projective_iff_preservesEpimorphisms_coyoneda_obj]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : C
⊢ (coyoneda.obj (op (op J))).PreservesEpimorphisms ↔ (yoneda.obj J).PreservesEpimorphisms

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : C
⊢ (coyoneda.obj (op (op J))).PreservesEpimorphisms ↔ (yoneda.obj J).PreservesEpimorphisms

Tactic:
exact Functor.preservesEpimorphisms.iso_iff (Coyoneda.objOpOp _)

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem le_of_mem_primeFactorsList {n p : ℕ} (h : p ∈ n.primeFactorsList) : p ≤ n

Proof state:
n p : ℕ
h : p ∈ n.primeFactorsList
⊢ p ≤ n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Result:
case inl
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ≤ 0

case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ≤ n

Proof state:
case inl
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ≤ 0

Tactic:
rw [primeFactorsList_zero] at h

Result:
case inl
p : ℕ
h : p ∈ []
⊢ p ≤ 0

Proof state:
case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ≤ n

Tactic:
exact le_of_dvd hn (dvd_of_mem_primeFactorsList h)

Result:
no goals

Proof state:
case inl
p : ℕ
h : p ∈ []
⊢ p ≤ 0

Tactic:
cases h

Result:
no goals
-- Mathlib/Algebra/Category/Semigrp/Basic.lean
@[to_additive]
lemma comp_apply {X Y T : Semigrp} (f : X ⟶ Y) (g : Y ⟶ T) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y T : Semigrp
f : X ⟶ Y
g : Y ⟶ T
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
theorem integral_comp_inv_mul_right (g : ℝ → F) (a : ℝ) :
    (∫ x : ℝ, g (x * a⁻¹)) = |a| • ∫ y : ℝ, g y

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
g : ℝ → F
a : ℝ
⊢ ∫ (x : ℝ), g (x * a⁻¹) = |a| • ∫ (y : ℝ), g y

Tactic:
simpa only [mul_comm] using integral_comp_inv_mul_left g a

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem compRel_assoc {r s t : Set (α × α)} : r ○ s ○ t = r ○ (s ○ t)

Proof state:
α : Type ua
r s t : Set (α × α)
⊢ r ○ s ○ t = r ○ (s ○ t)

Tactic:
ext ⟨a, b⟩

Result:
case h.mk
α : Type ua
r s t : Set (α × α)
a b : α
⊢ (a, b) ∈ r ○ s ○ t ↔ (a, b) ∈ r ○ (s ○ t)

Proof state:
case h.mk
α : Type ua
r s t : Set (α × α)
a b : α
⊢ (∃ z, (∃ z_1, (a, z_1) ∈ r ∧ (z_1, z) ∈ s) ∧ (z, b) ∈ t) ↔ ∃ z, (a, z) ∈ r ∧ ∃ z_1, (z, z_1) ∈ s ∧ (z_1, b) ∈ t

Tactic:
tauto

Result:
no goals

Proof state:
case h.mk
α : Type ua
r s t : Set (α × α)
a b : α
⊢ (a, b) ∈ r ○ s ○ t ↔ (a, b) ∈ r ○ (s ○ t)

Tactic:
simp only [mem_compRel]

Result:
case h.mk
α : Type ua
r s t : Set (α × α)
a b : α
⊢ (∃ z, (∃ z_1, (a, z_1) ∈ r ∧ (z_1, z) ∈ s) ∧ (z, b) ∈ t) ↔ ∃ z, (a, z) ∈ r ∧ ∃ z_1, (z, z_1) ∈ s ∧ (z_1, b) ∈ t
-- Mathlib/Computability/Tape.lean
theorem BlankExtends.below_of_le {Γ} [Inhabited Γ] {l l₁ l₂ : List Γ} :
    BlankExtends l l₁ → BlankExtends l l₂ → l₁.length ≤ l₂.length → BlankExtends l₁ l₂

Proof state:
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
i j : ℕ
h : (l ++ List.replicate i default).length ≤ (l ++ List.replicate j default).length
⊢ BlankExtends (l ++ List.replicate i default) (l ++ List.replicate j default)

Tactic:
use j - i

Result:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
i j : ℕ
h : (l ++ List.replicate i default).length ≤ (l ++ List.replicate j default).length
⊢ l ++ List.replicate j default = l ++ List.replicate i default ++ List.replicate (j - i) default

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
l l₁ l₂ : List Γ
⊢ BlankExtends l l₁ → BlankExtends l l₂ → l₁.length ≤ l₂.length → BlankExtends l₁ l₂

Tactic:
rintro ⟨i, rfl⟩ ⟨j, rfl⟩ h

Result:
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
i j : ℕ
h : (l ++ List.replicate i default).length ≤ (l ++ List.replicate j default).length
⊢ BlankExtends (l ++ List.replicate i default) (l ++ List.replicate j default)

Proof state:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
i j : ℕ
h : i ≤ j
⊢ l ++ List.replicate j default = l ++ List.replicate i default ++ List.replicate (j - i) default

Tactic:
simp only [← List.replicate_add, Nat.add_sub_cancel' h, List.append_assoc]

Result:
no goals

Proof state:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
i j : ℕ
h : (l ++ List.replicate i default).length ≤ (l ++ List.replicate j default).length
⊢ l ++ List.replicate j default = l ++ List.replicate i default ++ List.replicate (j - i) default

Tactic:
simp only [List.length_append, Nat.add_le_add_iff_left, List.length_replicate] at h

Result:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
i j : ℕ
h : i ≤ j
⊢ l ++ List.replicate j default = l ++ List.replicate i default ++ List.replicate (j - i) default
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_eq_some_get [LawfulBEq α] (h : m.1.WF) {a : α} {h'} : m.get? a = some (m.get a h')

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
a : α
h' : m.contains a = true
⊢ m.get? a = some (m.get a h')

Tactic:
simp_to_model using List.getValueCast?_eq_some_getValueCast

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem sup_inf {x' y'} (h : IsCompl x y) (h' : IsCompl x' y') : IsCompl (x ⊔ x') (y ⊓ y') :=
  of_eq
    (by rw [inf_sup_right, ← inf_assoc, h.inf_eq_bot, bot_inf_eq, bot_sup_eq, inf_left_comm,
      h'.inf_eq_bot, inf_bot_eq])
    (by rw [sup_inf_left, sup_comm x, sup_assoc, h.sup_eq_top, sup_top_eq, top_inf_eq,
      sup_assoc, sup_left_comm, h'.sup_eq_top, sup_top_eq])

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ (x ⊔ x') ⊓ (y ⊓ y') = ⊥

Tactic:
rw [inf_sup_right, ← inf_assoc, h.inf_eq_bot, bot_inf_eq, bot_sup_eq, inf_left_comm,
h'.inf_eq_bot, inf_bot_eq]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤

Tactic:
rw [sup_inf_left, sup_comm x, sup_assoc, h.sup_eq_top, sup_top_eq, top_inf_eq,
sup_assoc, sup_left_comm, h'.sup_eq_top, sup_top_eq]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem exists_set_subtype {t : Set α} (p : Set α → Prop) :
    (∃ s : Set t, p (((↑) : t → α) '' s)) ↔ ∃ s : Set α, s ⊆ t ∧ p s

Proof state:
α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∃ s, p (val '' s)) ↔ ∃ s ⊆ t, p s

Tactic:
rw [← exists_subset_range_and_iff, range_coe]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Preserves.lean
/--
If `F` is a presheaf which `IsSheafFor` a presieve of arrows and the empty presieve, then it
preserves the product corresponding to the presieve of arrows.
-/
lemma preservesProduct_of_isSheafFor
    (hF' : (ofArrows X c.inj).IsSheafFor F) :
    PreservesLimit (Discrete.functor (fun x ↦ op (X x))) F

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct X
⊢ IsIso
    (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
      Equalizer.Presieve.Arrows.forkMap F X c.inj)

Tactic:
refine IsIso.comp_isIso' inferInstance ?_

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct X
⊢ IsIso (Equalizer.Presieve.Arrows.forkMap F X c.inj)
-- Mathlib/Topology/Algebra/InfiniteSum/Real.lean
theorem summable_iff_not_tendsto_nat_atTop_of_nonneg {f : ℕ → ℝ} (hf : ∀ n, 0 ≤ f n) :
    Summable f ↔ ¬Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop atTop

Proof state:
f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ Summable f ↔ ¬Tendsto (fun n => ∑ i ∈ range n, f i) atTop atTop

Tactic:
rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop_of_nonneg hf]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
theorem isHermitian_mul_mul_conjTranspose [Fintype m] {A : Matrix m m α} (B : Matrix n m α)
    (hA : A.IsHermitian) : (B * A * Bᴴ).IsHermitian

Proof state:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝² : NonUnitalSemiring α
inst✝¹ : StarRing α
inst✝ : Fintype m
A : Matrix m m α
B : Matrix n m α
hA : A.IsHermitian
⊢ (B * A * Bᴴ).IsHermitian

Tactic:
simp only [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose, hA.eq, Matrix.mul_assoc]

Result:
no goals