harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem cycleRange_apply {n : ℕ} [NeZero n] (i j : Fin n) :
    cycleRange i j = if j < i then j + 1 else if j = i then 0 else j

Proof state:
case pos
n : ℕ
inst✝ : NeZero n
i j : Fin n
h₁ : ¬j < i
h₂ : j = i
⊢ i.cycleRange j = 0

Tactic:
exact cycleRange_of_eq h₂

Result:
no goals

Proof state:
case pos
n : ℕ
inst✝ : NeZero n
i j : Fin n
h₁ : j < i
⊢ i.cycleRange j = j + 1

Tactic:
exact cycleRange_of_lt h₁

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
i j : Fin n
⊢ i.cycleRange j = if j < i then j + 1 else if j = i then 0 else j

Tactic:
split_ifs with h₁ h₂

Result:
case pos
n : ℕ
inst✝ : NeZero n
i j : Fin n
h₁ : j < i
⊢ i.cycleRange j = j + 1

case pos
n : ℕ
inst✝ : NeZero n
i j : Fin n
h₁ : ¬j < i
h₂ : j = i
⊢ i.cycleRange j = 0

case neg
n : ℕ
inst✝ : NeZero n
i j : Fin n
h₁ : ¬j < i
h₂ : ¬j = i
⊢ i.cycleRange j = j

Proof state:
case neg
n : ℕ
inst✝ : NeZero n
i j : Fin n
h₁ : ¬j < i
h₂ : ¬j = i
⊢ i.cycleRange j = j

Tactic:
exact cycleRange_of_gt (lt_of_le_of_ne (le_of_not_gt h₁) (Ne.symm h₂))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem dropWhile_map (f : α → β) (p : β → Bool) (l : List α) :
    (l.map f).dropWhile p = (l.dropWhile (p ∘ f)).map f

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
p : β → Bool
⊢ dropWhile p (map f []) = map f (dropWhile (p ∘ f) [])

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
p : β → Bool
x : α
xs : List α
ih : dropWhile p (map f xs) = map f (dropWhile (p ∘ f) xs)
⊢ dropWhile p (map f (x :: xs)) = map f (dropWhile (p ∘ f) (x :: xs))

Tactic:
simp only [map_cons, dropWhile_cons]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → β
p : β → Bool
x : α
xs : List α
ih : dropWhile p (map f xs) = map f (dropWhile (p ∘ f) xs)
⊢ (if p (f x) = true then dropWhile p (map f xs) else f x :: map f xs) =
    map f (if (p ∘ f) x = true then dropWhile (p ∘ f) xs else x :: xs)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : β → Bool
l : List α
⊢ dropWhile p (map f l) = map f (dropWhile (p ∘ f) l)

Tactic:
induction l with
| nil => rfl
| cons x xs ih =>
  simp only [map_cons, dropWhile_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
p : β → Bool
x : α
xs : List α
ih : dropWhile p (map f xs) = map f (dropWhile (p ∘ f) xs)
⊢ (if p (f x) = true then dropWhile p (map f xs) else f x :: map f xs) =
    map f (if (p ∘ f) x = true then dropWhile (p ∘ f) xs else x :: xs)

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem sModNat_aux_eq (q k : ℕ) : sModNat_aux (4 % q) q k = sModNat q k

Proof state:
q k : ℕ
⊢ sModNat_aux (4 % q) q k = sModNat q k

Tactic:
induction k with
| zero => rfl
| succ k ih => rw [sModNat_aux, ih, sModNat, ← ih]

Result:
no goals

Proof state:
case succ
q k : ℕ
ih : sModNat_aux (4 % q) q k = sModNat q k
⊢ sModNat_aux (4 % q) q (k + 1) = sModNat q (k + 1)

Tactic:
rw [sModNat_aux, ih, sModNat, ← ih]

Result:
no goals

Proof state:
case zero
q : ℕ
⊢ sModNat_aux (4 % q) q 0 = sModNat q 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ExactSequence.lean
lemma Exact.δlast {S : ComposableArrows C (n + 2)} (hS : S.Exact) :
    S.δlast.Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
hS : S.Exact
⊢ S.δlast.Exact

Tactic:
rw [exact_iff_δlast] at hS

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
hS : S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ S.δlast.Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
hS : S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ S.δlast.Exact

Tactic:
exact hS.1

Result:
no goals
-- Mathlib/RingTheory/DualNumber.lean
lemma isUnit_or_isNilpotent [DivisionSemiring R] [AddCommGroup M]
    [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]
    (a : TrivSqZeroExt R M) :
    IsUnit a ∨ IsNilpotent a

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a : TrivSqZeroExt R M
⊢ IsUnit a ∨ IsNilpotent a

Tactic:
simp [isUnit_iff_isUnit_fst, isNilpotent_iff_isNilpotent_fst, em']

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_pi_eq {I : Set ι} (hI : I.Finite) (s : ∀ i, Set (π i)) (x : ∀ i, π i) :
    𝓝[pi I s] x =
      (⨅ i ∈ I, comap (fun x => x i) (𝓝[s i] x i)) ⊓
        ⨅ (i) (_ : i ∉ I), comap (fun x => x i) (𝓝 (x i))

Proof state:
ι : Type u_5
π : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (π i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (π i)
x : (i : ι) → π i
⊢ 𝓝[I.pi s] x = (⨅ i ∈ I, comap (fun x => x i) (𝓝[s i] x i)) ⊓ ⨅ i, ⨅ (_ : i ∉ I), comap (fun x => x i) (𝓝 (x i))

Tactic:
simp only [nhdsWithin, nhds_pi, Filter.pi, pi_def, ← iInf_principal_finite hI, comap_inf,
  comap_principal, eval]

Result:
ι : Type u_5
π : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (π i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (π i)
x : (i : ι) → π i
⊢ (⨅ i, comap (eval i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval i ⁻¹' s i) =
    (⨅ i ∈ I, comap (fun x => x i) (𝓝 (x i)) ⊓ 𝓟 ((fun x => x i) ⁻¹' s i)) ⊓
      ⨅ i, ⨅ (_ : i ∉ I), comap (fun x => x i) (𝓝 (x i))

Proof state:
ι : Type u_5
π : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (π i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (π i)
x : (i : ι) → π i
⊢ ((⨅ i ∈ I, comap (eval i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval i ⁻¹' s i)) ⊓ ⨅ i, ⨅ (_ : i ∉ I), comap (eval i) (𝓝 (x i)) =
    (⨅ i ∈ I, comap (fun x => x i) (𝓝 (x i)) ⊓ 𝓟 ((fun x => x i) ⁻¹' s i)) ⊓
      ⨅ i, ⨅ (_ : i ∉ I), comap (fun x => x i) (𝓝 (x i))

Tactic:
simp only [iInf_inf_eq]

Result:
no goals

Proof state:
ι : Type u_5
π : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (π i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (π i)
x : (i : ι) → π i
⊢ (⨅ i, comap (eval i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval i ⁻¹' s i) =
    (⨅ i ∈ I, comap (fun x => x i) (𝓝 (x i)) ⊓ 𝓟 ((fun x => x i) ⁻¹' s i)) ⊓
      ⨅ i, ⨅ (_ : i ∉ I), comap (fun x => x i) (𝓝 (x i))

Tactic:
rw [iInf_split _ fun i => i ∈ I, inf_right_comm]

Result:
ι : Type u_5
π : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (π i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (π i)
x : (i : ι) → π i
⊢ ((⨅ i ∈ I, comap (eval i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval i ⁻¹' s i)) ⊓ ⨅ i, ⨅ (_ : i ∉ I), comap (eval i) (𝓝 (x i)) =
    (⨅ i ∈ I, comap (fun x => x i) (𝓝 (x i)) ⊓ 𝓟 ((fun x => x i) ⁻¹' s i)) ⊓
      ⨅ i, ⨅ (_ : i ∉ I), comap (fun x => x i) (𝓝 (x i))
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_comap_comap_eq_relfinrank_of_le (f : L →+* E) (h : B ≤ f.fieldRange) :
    relfinrank (A.comap f) (B.comap f) = relfinrank A B

Proof state:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
h : B ≤ f.fieldRange
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank B

Tactic:
simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_of_le A B f h))

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Defs.lean
theorem prod_map_one {l : List ι} :
    (l.map fun _ => (1 : M)).prod = 1

Proof state:
case nil
ι : Type u_1
M : Type u_4
inst✝ : MulOneClass M
⊢ (map (fun x => 1) []).prod = 1

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : MulOneClass M
l : List ι
⊢ (map (fun x => 1) l).prod = 1

Tactic:
induction l with
| nil => rfl
| cons hd tl ih => rw [map_cons, prod_one_cons, ih]

Result:
no goals

Proof state:
case cons
ι : Type u_1
M : Type u_4
inst✝ : MulOneClass M
hd : ι
tl : List ι
ih : (map (fun x => 1) tl).prod = 1
⊢ (map (fun x => 1) (hd :: tl)).prod = 1

Tactic:
rw [map_cons, prod_one_cons, ih]

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
theorem IsIntegral.map {B C F : Type*} [Ring B] [Ring C] [Algebra R B] [Algebra A B] [Algebra R C]
    [IsScalarTower R A B] [Algebra A C] [IsScalarTower R A C] {b : B}
    [FunLike F B C] [AlgHomClass F A B C] (f : F)
    (hb : IsIntegral R b) : IsIntegral R (f b)

Proof state:
R : Type u_1
A : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
B : Type u_5
C : Type u_6
F : Type u_7
inst✝⁹ : Ring B
inst✝⁸ : Ring C
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra A B
inst✝⁵ : Algebra R C
inst✝⁴ : IsScalarTower R A B
inst✝³ : Algebra A C
inst✝² : IsScalarTower R A C
b : B
inst✝¹ : FunLike F B C
inst✝ : AlgHomClass F A B C
f : F
hb : IsIntegral R b
⊢ IsIntegral R (f b)

Tactic:
obtain ⟨P, hP⟩ := hb

Result:
case intro
R : Type u_1
A : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
B : Type u_5
C : Type u_6
F : Type u_7
inst✝⁹ : Ring B
inst✝⁸ : Ring C
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra A B
inst✝⁵ : Algebra R C
inst✝⁴ : IsScalarTower R A B
inst✝³ : Algebra A C
inst✝² : IsScalarTower R A C
b : B
inst✝¹ : FunLike F B C
inst✝ : AlgHomClass F A B C
f : F
P : R[X]
hP : P.Monic ∧ eval₂ (algebraMap R B) b P = 0
⊢ IsIntegral R (f b)

Proof state:
case intro
R : Type u_1
A : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
B : Type u_5
C : Type u_6
F : Type u_7
inst✝⁹ : Ring B
inst✝⁸ : Ring C
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra A B
inst✝⁵ : Algebra R C
inst✝⁴ : IsScalarTower R A B
inst✝³ : Algebra A C
inst✝² : IsScalarTower R A C
b : B
inst✝¹ : FunLike F B C
inst✝ : AlgHomClass F A B C
f : F
P : R[X]
hP : P.Monic ∧ eval₂ (algebraMap R B) b P = 0
⊢ IsIntegral R (f b)

Tactic:
refine ⟨P, hP.1, ?_⟩

Result:
case intro
R : Type u_1
A : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
B : Type u_5
C : Type u_6
F : Type u_7
inst✝⁹ : Ring B
inst✝⁸ : Ring C
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra A B
inst✝⁵ : Algebra R C
inst✝⁴ : IsScalarTower R A B
inst✝³ : Algebra A C
inst✝² : IsScalarTower R A C
b : B
inst✝¹ : FunLike F B C
inst✝ : AlgHomClass F A B C
f : F
P : R[X]
hP : P.Monic ∧ eval₂ (algebraMap R B) b P = 0
⊢ eval₂ (algebraMap R C) (f b) P = 0

Proof state:
case intro
R : Type u_1
A : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
B : Type u_5
C : Type u_6
F : Type u_7
inst✝⁹ : Ring B
inst✝⁸ : Ring C
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra A B
inst✝⁵ : Algebra R C
inst✝⁴ : IsScalarTower R A B
inst✝³ : Algebra A C
inst✝² : IsScalarTower R A C
b : B
inst✝¹ : FunLike F B C
inst✝ : AlgHomClass F A B C
f : F
P : R[X]
hP : P.Monic ∧ eval₂ (algebraMap R B) b P = 0
⊢ eval₂ (algebraMap R C) (f b) P = 0

Tactic:
rw [← aeval_def, ← aeval_map_algebraMap A,
  aeval_algHom_apply, aeval_map_algebraMap, aeval_def, hP.2, _root_.map_zero]

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem mem_adjoin_support (f : MonoidAlgebra R M) : f ∈ adjoin R (of R M '' f.support)

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
⊢ f ∈ adjoin R (⇑(of R M) '' ↑f.support)

Tactic:
suffices span R (of R M '' f.support) ≤ Subalgebra.toSubmodule (adjoin R (of R M '' f.support)) by
  exact this (mem_span_support f)

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
⊢ span R (⇑(of R M) '' ↑f.support) ≤ Subalgebra.toSubmodule (adjoin R (⇑(of R M) '' ↑f.support))

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
⊢ ⇑(of R M) '' ↑f.support ⊆ ↑(Subalgebra.toSubmodule (adjoin R (⇑(of R M) '' ↑f.support)))

Tactic:
exact subset_adjoin

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
⊢ span R (⇑(of R M) '' ↑f.support) ≤ Subalgebra.toSubmodule (adjoin R (⇑(of R M) '' ↑f.support))

Tactic:
rw [Submodule.span_le]

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
⊢ ⇑(of R M) '' ↑f.support ⊆ ↑(Subalgebra.toSubmodule (adjoin R (⇑(of R M) '' ↑f.support)))

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
this : span R (⇑(of R M) '' ↑f.support) ≤ Subalgebra.toSubmodule (adjoin R (⇑(of R M) '' ↑f.support))
⊢ f ∈ adjoin R (⇑(of R M) '' ↑f.support)

Tactic:
exact this (mem_span_support f)

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Linear.lean
theorem IsBoundedLinearMap.fderivWithin (h : IsBoundedLinearMap 𝕜 f)
    (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 f s x = h.toContinuousLinearMap

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
h : IsBoundedLinearMap 𝕜 f
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ _root_.fderiv 𝕜 f x = h.toContinuousLinearMap

Tactic:
exact h.fderiv

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
h : IsBoundedLinearMap 𝕜 f
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ _root_.fderivWithin 𝕜 f s x = h.toContinuousLinearMap

Tactic:
rw [DifferentiableAt.fderivWithin h.differentiableAt hxs]

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
h : IsBoundedLinearMap 𝕜 f
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ _root_.fderiv 𝕜 f x = h.toContinuousLinearMap
-- Mathlib/Data/Real/GoldenRatio.lean
theorem goldConj_neg : ψ < 0

Proof state:
⊢ ψ < 0

Tactic:
linarith [one_sub_goldConj, one_lt_gold]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem preimage_map_fst_pullbackDiagonal {f : X → Y} {g : Z → Y} :
    @map_fst X Y Z f g ⁻¹' pullbackDiagonal f = pullbackDiagonal (@snd X Y Z f g)

Proof state:
case h.mk.mk
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' {p | p.fst = p.snd} ↔
    (↑(fst ⟨(p₁, p₂), he⟩)).1 = (↑(snd ⟨(p₁, p₂), he⟩)).1 ∧ (↑(fst ⟨(p₁, p₂), he⟩)).2 = (↑(snd ⟨(p₁, p₂), he⟩)).2

Tactic:
exact (and_iff_left he).symm

Result:
no goals

Proof state:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
⊢ map_fst ⁻¹' pullbackDiagonal f = pullbackDiagonal snd

Tactic:
ext ⟨⟨p₁, p₂⟩, he⟩

Result:
case h.mk.mk
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' pullbackDiagonal f ↔ ⟨(p₁, p₂), he⟩ ∈ pullbackDiagonal snd

Proof state:
case h.mk.mk
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' pullbackDiagonal f ↔ ⟨(p₁, p₂), he⟩ ∈ pullbackDiagonal snd

Tactic:
simp_rw [pullbackDiagonal, mem_setOf, Subtype.ext_iff, Prod.ext_iff]

Result:
case h.mk.mk
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' {p | p.fst = p.snd} ↔
    (↑(fst ⟨(p₁, p₂), he⟩)).1 = (↑(snd ⟨(p₁, p₂), he⟩)).1 ∧ (↑(fst ⟨(p₁, p₂), he⟩)).2 = (↑(snd ⟨(p₁, p₂), he⟩)).2
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tan_neg_of_neg_of_pi_div_two_lt {x : ℝ} (hx0 : x < 0) (hpx : -(π / 2) < x) : tan x < 0 :=
  neg_pos.1 (tan_neg x ▸ tan_pos_of_pos_of_lt_pi_div_two (by linarith) (by linarith [pi_pos]))

Proof state:
x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
⊢ -x < π / 2

Tactic:
linarith [pi_pos]

Result:
no goals

Proof state:
x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
⊢ 0 < -x

Tactic:
linarith

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem pow_of_dvd (h : IsPrimitiveRoot ζ k) {p : ℕ} (hp : p ≠ 0) (hdiv : p ∣ k) :
    IsPrimitiveRoot (ζ ^ p) (k / p)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ orderOf ζ
⊢ IsPrimitiveRoot (ζ ^ p) (orderOf (ζ ^ p))

Tactic:
exact IsPrimitiveRoot.orderOf _

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ k
⊢ IsPrimitiveRoot (ζ ^ p) (k / p)

Tactic:
rw [h.eq_orderOf] at hdiv ⊢

Result:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ orderOf ζ
⊢ IsPrimitiveRoot (ζ ^ p) (orderOf ζ / p)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ orderOf ζ
⊢ IsPrimitiveRoot (ζ ^ p) (orderOf ζ / p)

Tactic:
rw [← orderOf_pow_of_dvd hp hdiv]

Result:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ orderOf ζ
⊢ IsPrimitiveRoot (ζ ^ p) (orderOf (ζ ^ p))
-- Mathlib/Computability/Primrec.lean
theorem list_flatten : Primrec (@List.flatten α) :=
  (list_foldr .id (const []) <| to₂ <| comp (@list_append α _) snd).of_eq fun l => by
    dsimp; induction l <;> simp [*]

Proof state:
α : Type u_1
inst✝ : Primcodable α
l : List (List α)
⊢ List.foldr (fun b s => b ++ s) [] l = l.flatten

Tactic:
induction l <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Primcodable α
l : List (List α)
⊢ List.foldr (fun b s => (fun x1 x2 => x1 ++ x2) (l, b, s).2.1 (l, b, s).2.2) [] (id l) = l.flatten

Tactic:
dsimp

Result:
α : Type u_1
inst✝ : Primcodable α
l : List (List α)
⊢ List.foldr (fun b s => b ++ s) [] l = l.flatten
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioc_subset_Ioc (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Ioc a₁ b₁ ⊆ Ioc a₂ b₂

Proof state:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ioc a₁ b₁ ⊆ Ioc a₂ b₂

Tactic:
simpa [← coe_subset] using Set.Ioc_subset_Ioc ha hb

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma inv_sSup (s : Set ℝ≥0∞) : (sSup s)⁻¹ = ⨅ a ∈ s, a⁻¹

Proof state:
s : Set ℝ≥0∞
⊢ (sSup s)⁻¹ = ⨅ a ∈ s, a⁻¹

Tactic:
simp [sSup_eq_iSup, inv_iSup]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Symmetric.lean
theorem IsSymm.fromBlocks {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α}
    {D : Matrix n n α} (hA : A.IsSymm) (hBC : Bᵀ = C) (hD : D.IsSymm) :
    (A.fromBlocks B C D).IsSymm

Proof state:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
⊢ Cᵀ = B

Tactic:
rw [← hBC]

Result:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
⊢ Bᵀᵀ = B

Proof state:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
⊢ Bᵀᵀ = B

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
⊢ (Matrix.fromBlocks A B C D).IsSymm

Tactic:
unfold Matrix.IsSymm

Result:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
⊢ (Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D

Proof state:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
⊢ (Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D

Tactic:
rw [fromBlocks_transpose, hA, hCB, hBC, hD]

Result:
no goals

Proof state:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
⊢ (Matrix.fromBlocks A B C D).IsSymm

Tactic:
have hCB : Cᵀ = B := by
  rw [← hBC]
  simp

Result:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
⊢ (Matrix.fromBlocks A B C D).IsSymm
-- Mathlib/Data/List/Sym.lean
theorem length_sym2 {xs : List α} : xs.sym2.length = Nat.choose (xs.length + 1) 2

Proof state:
case cons
α : Type u_1
x : α
xs : List α
ih : xs.sym2.length = (xs.length + 1).choose 2
⊢ (x :: xs).sym2.length = ((x :: xs).length + 1).choose 2

Tactic:
rw [List.sym2, length_append, length_map, length_cons,
    Nat.choose_succ_succ, ← ih, Nat.choose_one_right]

Result:
no goals

Proof state:
α : Type u_1
xs : List α
⊢ xs.sym2.length = (xs.length + 1).choose 2

Tactic:
induction xs with
| nil => rfl
| cons x xs ih =>
  rw [List.sym2, length_append, length_map, length_cons,
      Nat.choose_succ_succ, ← ih, Nat.choose_one_right]

Result:
no goals

Proof state:
case nil
α : Type u_1
⊢ [].sym2.length = ([].length + 1).choose 2

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
@[to_additive (attr := simp)]
lemma inv_Ioo (a b : α) : (Ioo a b)⁻¹ = Ioo b⁻¹ a⁻¹

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ (Ioo a b)⁻¹ = Ioo b⁻¹ a⁻¹

Tactic:
simp [← Ioi_inter_Iio, inter_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem any_eq_false {l : List α} : l.any p = false ↔ ∀ x, x ∈ l → ¬p x

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ l.any p = false ↔ ∀ (x : α), x ∈ l → ¬p x = true

Tactic:
simp [any_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
lemma LinearIndependent.eq_zero_of_pair {x y : M} (h : LinearIndependent R ![x, y])
    {s t : R} (h' : s • x + t • y = 0) : s = 0 ∧ t = 0

Proof state:
case refine_1
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x + t • y = 0
⊢ (Finsupp.linearCombination R ![x, y]) (Finsupp.single 0 s + Finsupp.single 1 t) =
    (Finsupp.linearCombination R ![x, y]) 0

Tactic:
simpa

Result:
no goals

Proof state:
case refine_2
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : Finsupp.single 0 s + Finsupp.single 1 t = 0
⊢ s = 0 ∧ t = 0

Tactic:
exact ⟨by simpa using congr($h 0), by simpa using congr($h 1)⟩

Result:
no goals

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x + t • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
replace h := @h (.single 0 s + .single 1 t) 0 ?_

Result:
case refine_2
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : Finsupp.single 0 s + Finsupp.single 1 t = 0
⊢ s = 0 ∧ t = 0

case refine_1
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x + t • y = 0
⊢ (Finsupp.linearCombination R ![x, y]) (Finsupp.single 0 s + Finsupp.single 1 t) =
    (Finsupp.linearCombination R ![x, y]) 0

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : Finsupp.single 0 s + Finsupp.single 1 t = 0
⊢ t = 0

Tactic:
simpa using congr($h 1)

Result:
no goals

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : Finsupp.single 0 s + Finsupp.single 1 t = 0
⊢ s = 0

Tactic:
simpa using congr($h 0)

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_neg_left (x y : E) : ⟪-x, y⟫ = -⟪x, y⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ (starRingEnd 𝕜) (-1) * ⟪x, y⟫_𝕜 = -⟪x, y⟫_𝕜

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪-x, y⟫_𝕜 = -⟪x, y⟫_𝕜

Tactic:
rw [← neg_one_smul 𝕜 x, inner_smul_left]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ (starRingEnd 𝕜) (-1) * ⟪x, y⟫_𝕜 = -⟪x, y⟫_𝕜