harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem orthonormal (b : HilbertBasis ι 𝕜 E) : Orthonormal 𝕜 b

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ inner (b i) (b j) = if i = j then 1 else 0

Tactic:
rw [← b.repr.inner_map_map (b i) (b j), b.repr_self, b.repr_self, lp.inner_single_left,
  lp.single_apply, Pi.single_apply]

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ inner 1 (if i = j then 1 else 0) = if i = j then 1 else 0

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
⊢ Orthonormal 𝕜 ⇑b

Tactic:
classical
rw [orthonormal_iff_ite]
intro i j
rw [← b.repr.inner_map_map (b i) (b j), b.repr_self, b.repr_self, lp.inner_single_left,
  lp.single_apply, Pi.single_apply]
simp

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
⊢ Orthonormal 𝕜 ⇑b

Tactic:
rw [orthonormal_iff_ite]

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
⊢ ∀ (i j : ι), inner (b i) (b j) = if i = j then 1 else 0

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
⊢ ∀ (i j : ι), inner (b i) (b j) = if i = j then 1 else 0

Tactic:
intro i j

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ inner (b i) (b j) = if i = j then 1 else 0

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ inner 1 (if i = j then 1 else 0) = if i = j then 1 else 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem lift_root (h : IsAdjoinRoot S f) : h.lift i x hx h.root = x

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
h : IsAdjoinRoot S f
⊢ (lift i x h hx) h.root = x

Tactic:
rw [← h.map_X, lift_map, eval₂_X]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/List.lean
lemma sum_le_foldr_max [AddMonoid M] [AddMonoid N] [LinearOrder N] (f : M → N) (h0 : f 0 ≤ 0)
    (hadd : ∀ x y, f (x + y) ≤ max (f x) (f y)) (l : List M) : f l.sum ≤ (l.map f).foldr max 0

Proof state:
case nil
M : Type u_3
N : Type u_4
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ f x ⊔ f y
⊢ f [].sum ≤ foldr max 0 (map f [])

Tactic:
simpa using h0

Result:
no goals

Proof state:
M : Type u_3
N : Type u_4
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ f x ⊔ f y
l : List M
⊢ f l.sum ≤ foldr max 0 (map f l)

Tactic:
induction' l with hd tl IH

Result:
case nil
M : Type u_3
N : Type u_4
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ f x ⊔ f y
⊢ f [].sum ≤ foldr max 0 (map f [])

case cons
M : Type u_3
N : Type u_4
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ f x ⊔ f y
hd : M
tl : List M
IH : f tl.sum ≤ foldr max 0 (map f tl)
⊢ f (hd :: tl).sum ≤ foldr max 0 (map f (hd :: tl))

Proof state:
case cons
M : Type u_3
N : Type u_4
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ f x ⊔ f y
hd : M
tl : List M
IH : f tl.sum ≤ foldr (fun x y => f x ⊔ y) 0 tl
⊢ f (hd + tl.sum) ≤ f hd ⊔ foldr (fun x y => f x ⊔ y) 0 tl

Tactic:
exact (hadd _ _).trans (max_le_max le_rfl IH)

Result:
no goals

Proof state:
case cons
M : Type u_3
N : Type u_4
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ f x ⊔ f y
hd : M
tl : List M
IH : f tl.sum ≤ foldr max 0 (map f tl)
⊢ f (hd :: tl).sum ≤ foldr max 0 (map f (hd :: tl))

Tactic:
simp only [List.sum_cons, List.foldr_map, List.foldr] at IH ⊢

Result:
case cons
M : Type u_3
N : Type u_4
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ f x ⊔ f y
hd : M
tl : List M
IH : f tl.sum ≤ foldr (fun x y => f x ⊔ y) 0 tl
⊢ f (hd + tl.sum) ≤ f hd ⊔ foldr (fun x y => f x ⊔ y) 0 tl
-- Mathlib/Order/Cover.lean
theorem WCovBy.le_and_le_iff (h : a ⩿ b) : a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ c = a ∨ c = b → a ≤ c ∧ c ≤ b

Tactic:
rintro (rfl | rfl)

Result:
case inl
α : Type u_1
inst✝ : PartialOrder α
b c : α
h : c ⩿ b
⊢ c ≤ c ∧ c ≤ b

case inr
α : Type u_1
inst✝ : PartialOrder α
a c : α
h : a ⩿ c
⊢ a ≤ c ∧ c ≤ c

Proof state:
case inl
α : Type u_1
inst✝ : PartialOrder α
b c : α
h : c ⩿ b
⊢ c ≤ c ∧ c ≤ b

case inr
α : Type u_1
inst✝ : PartialOrder α
a c : α
h : a ⩿ c
⊢ a ≤ c ∧ c ≤ c

Tactic:
exacts [⟨le_rfl, h.le⟩, ⟨h.le, le_rfl⟩]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b

Tactic:
refine ⟨fun h2 => h.eq_or_eq h2.1 h2.2, ?_⟩

Result:
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ c = a ∨ c = b → a ≤ c ∧ c ≤ b
-- Mathlib/Data/Multiset/Range.lean
theorem range_disjoint_map_add (a : ℕ) (m : Multiset ℕ) :
    Disjoint (range a) (m.map (a + ·))

Proof state:
case intro.intro
a : ℕ
m : Multiset ℕ
c : ℕ
left✝ : c ∈ m
hxa : a + c < a
hxb : a + c ∈ map (fun x => a + x) m
⊢ False

Tactic:
exact (Nat.le_add_right _ _).not_lt hxa

Result:
no goals

Proof state:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x < a
hxb : x ∈ map (fun x => a + x) m
⊢ False

Tactic:
obtain ⟨c, _, rfl⟩ := mem_map.1 hxb

Result:
case intro.intro
a : ℕ
m : Multiset ℕ
c : ℕ
left✝ : c ∈ m
hxa : a + c < a
hxb : a + c ∈ map (fun x => a + x) m
⊢ False

Proof state:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x ∈ range a
hxb : x ∈ map (fun x => a + x) m
⊢ False

Tactic:
rw [range, mem_coe, List.mem_range] at hxa

Result:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x < a
hxb : x ∈ map (fun x => a + x) m
⊢ False

Proof state:
a : ℕ
m : Multiset ℕ
⊢ ∀ {a_1 : ℕ}, a_1 ∈ range a → a_1 ∉ map (fun x => a + x) m

Tactic:
intro x hxa hxb

Result:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x ∈ range a
hxb : x ∈ map (fun x => a + x) m
⊢ False

Proof state:
a : ℕ
m : Multiset ℕ
⊢ _root_.Disjoint (range a) (map (fun x => a + x) m)

Tactic:
rw [disjoint_left]

Result:
a : ℕ
m : Multiset ℕ
⊢ ∀ {a_1 : ℕ}, a_1 ∈ range a → a_1 ∉ map (fun x => a + x) m
-- Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean
@[simp]
lemma d_add (b b' : B) : D.d (b + b') = D.d b + D.d b'

Proof state:
A B : CommRingCat
M : ModuleCat ↑B
f : A ⟶ B
D : M.Derivation f
b b' : ↑B
⊢ D.d (b + b') = D.d b + D.d b'

Tactic:
simp [d]

Result:
no goals
-- Mathlib/Order/WithBot.lean
@[simp, norm_cast] lemma coe_lt_coe : (a : WithBot α) < b ↔ a < b

Proof state:
α : Type u_1
a b : α
inst✝ : LT α
⊢ ↑a < ↑b ↔ a < b

Tactic:
simp [lt_def]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem norm_eq' (hp : 0 < p) {x : ℝ} : ‖(x : AddCircle p)‖ = p * |p⁻¹ * x - round (p⁻¹ * x)|

Proof state:
p : ℝ
hp : 0 < p
x : ℝ
⊢ ‖↑x‖ = |p| * |p⁻¹ * x - ↑(round (p⁻¹ * x))|

Tactic:
rw [← abs_mul, mul_sub, mul_inv_cancel_left₀ hp.ne.symm, norm_eq, mul_comm p]

Result:
no goals

Proof state:
p : ℝ
hp : 0 < p
x : ℝ
⊢ ‖↑x‖ = p * |p⁻¹ * x - ↑(round (p⁻¹ * x))|

Tactic:
conv_rhs =>
  congr
  rw [← abs_eq_self.mpr hp.le]

Result:
p : ℝ
hp : 0 < p
x : ℝ
⊢ ‖↑x‖ = |p| * |p⁻¹ * x - ↑(round (p⁻¹ * x))|
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem biUnion_congr (h : π₁ = π₂) (hi : ∀ J ∈ π₁, πi₁ J = πi₂ J) :
    π₁.biUnion πi₁ = π₂.biUnion πi₂

Proof state:
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
⊢ π₁.biUnion πi₁ = π₁.biUnion πi₂

Tactic:
ext J

Result:
case h
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ J ∈ π₁.biUnion πi₁ ↔ J ∈ π₁.biUnion πi₂

Proof state:
case h
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J' ∈ π₁, J ∈ πi₁ J') ↔ ∃ J' ∈ π₁, J ∈ πi₂ J'

Tactic:
constructor <;> exact fun ⟨J', h₁, h₂⟩ => ⟨J', h₁, hi J' h₁ ▸ h₂⟩

Result:
no goals

Proof state:
case h
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ J ∈ π₁.biUnion πi₁ ↔ J ∈ π₁.biUnion πi₂

Tactic:
simp only [mem_biUnion]

Result:
case h
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J' ∈ π₁, J ∈ πi₁ J') ↔ ∃ J' ∈ π₁, J ∈ πi₂ J'

Proof state:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
h : π₁ = π₂
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
⊢ π₁.biUnion πi₁ = π₂.biUnion πi₂

Tactic:
subst π₂

Result:
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
⊢ π₁.biUnion πi₁ = π₁.biUnion πi₂
-- Mathlib/Combinatorics/SetFamily/Compression/UV.lean
theorem compression_idem (u v : α) (s : Finset α) : 𝓒 u v (𝓒 u v s) = 𝓒 u v s

Proof state:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u v : α
s : Finset α
⊢ 𝓒 u v (𝓒 u v s) = 𝓒 u v s

Tactic:
have h : {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = ∅ :=
  filter_false_of_mem fun a ha h ↦ h <| compress_mem_compression_of_mem_compression ha

Result:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u v : α
s : Finset α
h : filter (fun a => compress u v a ∉ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ 𝓒 u v (𝓒 u v s) = 𝓒 u v s

Proof state:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u v : α
s : Finset α
h : filter (fun a => compress u v a ∉ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ filter (fun a => compress u v a ∈ 𝓒 u v s) (𝓒 u v s) ∪ filter (fun a => compress u v a ∉ 𝓒 u v s) (𝓒 u v s) = 𝓒 u v s

Tactic:
exact filter_union_filter_neg_eq _ (compression u v s)

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u v : α
s : Finset α
h : filter (fun a => compress u v a ∉ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ 𝓒 u v (𝓒 u v s) = 𝓒 u v s

Tactic:
rw [compression, filter_image, h, image_empty, ← h]

Result:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u v : α
s : Finset α
h : filter (fun a => compress u v a ∉ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ filter (fun a => compress u v a ∈ 𝓒 u v s) (𝓒 u v s) ∪ filter (fun a => compress u v a ∉ 𝓒 u v s) (𝓒 u v s) = 𝓒 u v s
-- Mathlib/Analysis/RCLike/Basic.lean
@[simp, norm_cast]
lemma ofReal_lt_zero {x : ℝ} : (x : K) < 0 ↔ x < 0

Proof state:
K : Type u_1
inst✝ : RCLike K
x : ℝ
⊢ ↑x < 0 ↔ x < 0

Tactic:
rw [← ofReal_zero, ofReal_lt_ofReal]

Result:
no goals
-- Mathlib/Data/Nat/Fib/Zeckendorf.lean
lemma greatestFib_sub_fib_greatestFib_le_greatestFib (hn : n ≠ 0) :
    greatestFib (n - fib (greatestFib n)) ≤ greatestFib n - 2

Proof state:
n : ℕ
hn : n ≠ 0
⊢ (n - fib n.greatestFib).greatestFib ≤ n.greatestFib - 2

Tactic:
rw [← Nat.lt_succ_iff, greatestFib_lt, tsub_lt_iff_right n.fib_greatestFib_le, Nat.sub_succ,
  succ_pred, ← fib_add_one]

Result:
n : ℕ
hn : n ≠ 0
⊢ n < fib (n.greatestFib + 1)

n : ℕ
hn : n ≠ 0
⊢ n.greatestFib ≠ 0

n : ℕ
hn : n ≠ 0
⊢ n.greatestFib - 1 ≠ 0

Proof state:
n : ℕ
hn : n ≠ 0
⊢ n < fib (n.greatestFib + 1)

Tactic:
exact n.lt_fib_greatestFib_add_one

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
⊢ n.greatestFib - 1 ≠ 0

Tactic:
simpa [← succ_le_iff, tsub_eq_zero_iff_le] using hn.bot_lt

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
⊢ n.greatestFib ≠ 0

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_eq_iff {l : List α} : mapIdx f l = l' ↔ ∀ i : Nat, l'[i]? = l[i]?.map (f i)

Proof state:
case mp
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l' : List α✝
l : List α
w : mapIdx f l = l'
i : Nat
⊢ l'[i]? = Option.map (f i) l[i]?

Tactic:
simpa using congrArg (fun l => l[i]?) w.symm

Result:
no goals

Proof state:
case mpr
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l' : List α✝
l : List α
w : ∀ (i : Nat), l'[i]? = Option.map (f i) l[i]?
⊢ mapIdx f l = l'

Tactic:
ext1 i

Result:
case mpr.h
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l' : List α✝
l : List α
w : ∀ (i : Nat), l'[i]? = Option.map (f i) l[i]?
i : Nat
⊢ (mapIdx f l)[i]? = l'[i]?

Proof state:
case mp
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l' : List α✝
l : List α
⊢ mapIdx f l = l' → ∀ (i : Nat), l'[i]? = Option.map (f i) l[i]?

Tactic:
intro w i

Result:
case mp
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l' : List α✝
l : List α
w : mapIdx f l = l'
i : Nat
⊢ l'[i]? = Option.map (f i) l[i]?

Proof state:
case mpr
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l' : List α✝
l : List α
⊢ (∀ (i : Nat), l'[i]? = Option.map (f i) l[i]?) → mapIdx f l = l'

Tactic:
intro w

Result:
case mpr
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l' : List α✝
l : List α
w : ∀ (i : Nat), l'[i]? = Option.map (f i) l[i]?
⊢ mapIdx f l = l'

Proof state:
case mpr.h
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l' : List α✝
l : List α
w : ∀ (i : Nat), l'[i]? = Option.map (f i) l[i]?
i : Nat
⊢ (mapIdx f l)[i]? = l'[i]?

Tactic:
simp [w]

Result:
no goals

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l' : List α✝
l : List α
⊢ mapIdx f l = l' ↔ ∀ (i : Nat), l'[i]? = Option.map (f i) l[i]?

Tactic:
constructor

Result:
case mp
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l' : List α✝
l : List α
⊢ mapIdx f l = l' → ∀ (i : Nat), l'[i]? = Option.map (f i) l[i]?

case mpr
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l' : List α✝
l : List α
⊢ (∀ (i : Nat), l'[i]? = Option.map (f i) l[i]?) → mapIdx f l = l'
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem SameCycle.cycleOf_eq [DecidableRel f.SameCycle] (h : SameCycle f x y) :
    cycleOf f x = cycleOf f y

Proof state:
case neg
α : Type u_2
f : Perm α
x y : α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
hz : ¬f.SameCycle x z
⊢ z = (f.cycleOf y) z

Tactic:
exact (cycleOf_apply_of_not_sameCycle (mt h.trans hz)).symm

Result:
no goals

Proof state:
case pos
α : Type u_2
f : Perm α
x y : α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
hz : f.SameCycle x z
⊢ f z = (f.cycleOf y) z

Tactic:
exact (h.symm.trans hz).cycleOf_apply.symm

Result:
no goals

Proof state:
case H
α : Type u_2
f : Perm α
x y : α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
⊢ (f.cycleOf x) z = (f.cycleOf y) z

Tactic:
rw [Equiv.Perm.cycleOf_apply]

Result:
case H
α : Type u_2
f : Perm α
x y : α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
⊢ (if f.SameCycle x z then f z else z) = (f.cycleOf y) z

Proof state:
case H
α : Type u_2
f : Perm α
x y : α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
⊢ (if f.SameCycle x z then f z else z) = (f.cycleOf y) z

Tactic:
split_ifs with hz

Result:
case pos
α : Type u_2
f : Perm α
x y : α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
hz : f.SameCycle x z
⊢ f z = (f.cycleOf y) z

case neg
α : Type u_2
f : Perm α
x y : α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
hz : ¬f.SameCycle x z
⊢ z = (f.cycleOf y) z

Proof state:
α : Type u_2
f : Perm α
x y : α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
⊢ f.cycleOf x = f.cycleOf y

Tactic:
ext z

Result:
case H
α : Type u_2
f : Perm α
x y : α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
⊢ (f.cycleOf x) z = (f.cycleOf y) z
-- Mathlib/Data/TypeVec.lean
theorem splitFun_inj {α α' : TypeVec (n + 1)} {f f' : drop α ⟹ drop α'} {g g' : last α → last α'}
    (H : splitFun f g = splitFun f' g') : f = f' ∧ g = g'

Proof state:
n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f f' : α.drop ⟹ α'.drop
g g' : α.last → α'.last
H : splitFun f g = splitFun f' g'
⊢ f = f' ∧ g = g'

Tactic:
rw [← dropFun_splitFun f g, H, ← lastFun_splitFun f g, H]

Result:
n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f f' : α.drop ⟹ α'.drop
g g' : α.last → α'.last
H : splitFun f g = splitFun f' g'
⊢ dropFun (splitFun f' g') = f' ∧ lastFun (splitFun f' g') = g'

Proof state:
n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f f' : α.drop ⟹ α'.drop
g g' : α.last → α'.last
H : splitFun f g = splitFun f' g'
⊢ dropFun (splitFun f' g') = f' ∧ lastFun (splitFun f' g') = g'

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem length_replace [BEq α] {a : α} : (replace a b l).length = l.length

Proof state:
α : Type u_1
β✝ : Type u_2
b : β✝
l : AssocList α β✝
inst✝ : BEq α
a : α
⊢ (replace a b l).length = l.length

Tactic:
induction l

Result:
case nil
α : Type u_1
β✝ : Type u_2
b : β✝
inst✝ : BEq α
a : α
⊢ (replace a b nil).length = nil.length

case cons
α : Type u_1
β✝ : Type u_2
b : β✝
inst✝ : BEq α
a key✝ : α
value✝ : β✝
tail✝ : AssocList α β✝
tail_ih✝ : (replace a b tail✝).length = tail✝.length
⊢ (replace a b (cons key✝ value✝ tail✝)).length = (cons key✝ value✝ tail✝).length

Proof state:
case cons
α : Type u_1
β✝ : Type u_2
b : β✝
inst✝ : BEq α
a key✝ : α
value✝ : β✝
tail✝ : AssocList α β✝
tail_ih✝ : (replace a b tail✝).length = tail✝.length
⊢ (match key✝ == a with
      | true => cons a b tail✝
      | false => cons key✝ value✝ (replace a b tail✝)).length =
    tail✝.length + 1

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
β✝ : Type u_2
b : β✝
inst✝ : BEq α
a : α
⊢ (replace a b nil).length = nil.length

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β✝ : Type u_2
b : β✝
inst✝ : BEq α
a key✝ : α
value✝ : β✝
tail✝ : AssocList α β✝
tail_ih✝ : (replace a b tail✝).length = tail✝.length
⊢ (replace a b (cons key✝ value✝ tail✝)).length = (cons key✝ value✝ tail✝).length

Tactic:
simp only [replace, length_cons]

Result:
case cons
α : Type u_1
β✝ : Type u_2
b : β✝
inst✝ : BEq α
a key✝ : α
value✝ : β✝
tail✝ : AssocList α β✝
tail_ih✝ : (replace a b tail✝).length = tail✝.length
⊢ (match key✝ == a with
      | true => cons a b tail✝
      | false => cons key✝ value✝ (replace a b tail✝)).length =
    tail✝.length + 1
-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma CotangentSpace.map_toComp_injective :
    Function.Injective
      ((Extension.CotangentSpace.map (Q.toComp P).toExtensionHom).liftBaseChange T)

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ Function.Injective
    ⇑(↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))

Tactic:
apply (compEquiv Q P).symm.injective.comp

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ Function.Injective ⇑(LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ Function.Injective ⇑(LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))

Tactic:
rw [← compEquiv_symm_inr]

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ Function.Injective
    ⇑(↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ Function.Injective ⇑(LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))

Tactic:
exact Prod.mk.inj_left _

Result:
no goals
-- Mathlib/Analysis/NormedSpace/HomeomorphBall.lean
theorem univBall_apply_zero (c : P) (r : ℝ) : univBall c r 0 = c

Proof state:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) ⋯
        else (IsometryEquiv.vaddConst c).toHomeomorph.toPartialHomeomorph)
      0 =
    c

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(univBall c r) 0 = c

Tactic:
unfold univBall

Result:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) ⋯
        else (IsometryEquiv.vaddConst c).toHomeomorph.toPartialHomeomorph)
      0 =
    c
-- Mathlib/Order/Filter/Pi.lean
theorem pi_neBot : NeBot (pi f) ↔ ∀ i, NeBot (f i)

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
⊢ (pi f).NeBot ↔ ∀ (i : ι), (f i).NeBot

Tactic:
simp [neBot_iff]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four (x y : E) :
    im ⟪x, y⟫ = (‖x - IK • y‖ * ‖x - IK • y‖ - ‖x + IK • y‖ * ‖x + IK • y‖) / 4

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ im ⟪x, y⟫_𝕜 =
    (‖x‖ * ‖x‖ - 2 * -im ⟪x, y⟫_𝕜 + ‖I • y‖ * ‖I • y‖ - (‖x‖ * ‖x‖ + 2 * -im ⟪x, y⟫_𝕜 + ‖I • y‖ * ‖I • y‖)) / 4

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ im ⟪x, y⟫_𝕜 = (‖x - I • y‖ * ‖x - I • y‖ - ‖x + I • y‖ * ‖x + I • y‖) / 4

Tactic:
simp only [@norm_add_mul_self 𝕜, @norm_sub_mul_self 𝕜, inner_smul_right, I_mul_re]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ im ⟪x, y⟫_𝕜 =
    (‖x‖ * ‖x‖ - 2 * -im ⟪x, y⟫_𝕜 + ‖I • y‖ * ‖I • y‖ - (‖x‖ * ‖x‖ + 2 * -im ⟪x, y⟫_𝕜 + ‖I • y‖ * ‖I • y‖)) / 4
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem inv_unique {f : M →* N} (h : ∀ y : S, IsUnit (f y)) {y : S} {z : N} (H : f y * z = 1) :
    (IsUnit.liftRight (f.restrict S) h y)⁻¹ = z

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
z : N
H : f ↑y * z = 1
⊢ ↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ = z

Tactic:
rw [← one_mul _⁻¹, Units.val_mul, mul_inv_left]

Result:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
z : N
H : f ↑y * z = 1
⊢ ↑1 = f ↑y * z

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
z : N
H : f ↑y * z = 1
⊢ ↑1 = f ↑y * z

Tactic:
exact H.symm

Result:
no goals