harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_append {p : α → Bool} :
    ∀ (l₁ l₂ : List α), filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂
  | [], _ => rfl
  | a :: l₁, l₂ => by simp only [cons_append, filter]; split <;> simp [filter_append l₁]

Proof state:
α : Type u_1
p : α → Bool
a : α
l₁ l₂ : List α
⊢ filter p (a :: l₁ ++ l₂) = filter p (a :: l₁) ++ filter p l₂

Tactic:
simp only [cons_append, filter]

Result:
α : Type u_1
p : α → Bool
a : α
l₁ l₂ : List α
⊢ (match p a with
    | true => a :: filter p (l₁ ++ l₂)
    | false => filter p (l₁ ++ l₂)) =
    (match p a with
      | true => a :: filter p l₁
      | false => filter p l₁) ++
      filter p l₂

Proof state:
α : Type u_1
p : α → Bool
a : α
l₁ l₂ : List α
⊢ (match p a with
    | true => a :: filter p (l₁ ++ l₂)
    | false => filter p (l₁ ++ l₂)) =
    (match p a with
      | true => a :: filter p l₁
      | false => filter p l₁) ++
      filter p l₂

Tactic:
split <;> simp [filter_append l₁]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem filter_attach {o : Option α} {p : {x // x ∈ o} → Bool} :
    o.attach.filter p = o.pbind fun a h => if p ⟨a, h⟩ then some ⟨a, h⟩ else none

Proof state:
α : Type u_1
o : Option α
p : { x // x ∈ o } → Bool
⊢ Option.filter p o.attach = o.pbind fun a h => if p ⟨a, h⟩ = true then some ⟨a, h⟩ else none

Tactic:
cases o <;> simp [filter_some]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c))

Proof state:
a b c : Bool
⊢ (a || b || c) = (a || (b || c))

Tactic:
cases a <;> cases b <;> cases c <;> decide

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem fst_prod_mk {α α' β β' : TypeVec n} (f : α ⟹ β) (g : α' ⟹ β') :
    TypeVec.prod.fst ⊚ (f ⊗' g) = f ⊚ TypeVec.prod.fst

Proof state:
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
⊢ prod.fst ⊚ (f ⊗' g) = f ⊚ prod.fst

Tactic:
funext i

Result:
case h
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
⊢ (prod.fst ⊚ (f ⊗' g)) i = (f ⊚ prod.fst) i

Proof state:
case h
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
⊢ (prod.fst ⊚ (f ⊗' g)) i = (f ⊚ prod.fst) i

Tactic:
induction i with
| fz => rfl
| fs _ i_ih => apply i_ih

Result:
no goals

Proof state:
case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α α' β β' : TypeVec.{u_1} n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.fst ⊚ (f ⊗' g)) a✝ = (f ⊚ prod.fst) a✝
α α' β β' : TypeVec.{u_1} (n✝ + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.fst ⊚ (f ⊗' g)) a✝.fs = (f ⊚ prod.fst) a✝.fs

Tactic:
apply i_ih

Result:
no goals

Proof state:
case h.fz
n n✝ : ℕ
α α' β β' : TypeVec.{u_1} (n✝ + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.fst ⊚ (f ⊗' g)) Fin2.fz = (f ⊚ prod.fst) Fin2.fz

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem upper_two_blockTriangular [Zero R] [Preorder α] (A : Matrix m m R) (B : Matrix m n R)
    (D : Matrix n n R) {a b : α} (hab : a < b) :
    BlockTriangular (fromBlocks A B 0 D) (Sum.elim (fun _ => a) fun _ => b)

Proof state:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst✝¹ : Zero R
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
⊢ (fromBlocks A B 0 D).BlockTriangular (Sum.elim (fun x => a) fun x => b)

Tactic:
rintro (c | c) (d | d) hcd <;> first | simp [hab.not_lt] at hcd ⊢

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst✝¹ : Zero R
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c d : n
hcd : Sum.elim (fun x => a) (fun x => b) (Sum.inr d) < Sum.elim (fun x => a) (fun x => b) (Sum.inr c)
⊢ fromBlocks A B 0 D (Sum.inr c) (Sum.inr d) = 0

Tactic:
simp [hab.not_lt] at hcd ⊢

Result:
no goals
-- Mathlib/RingTheory/DividedPowers/Basic.lean
theorem nilpotent_of_mem_dpIdeal {n : ℕ} (hn : n ≠ 0) (hnI : ∀ {y} (_ : y ∈ I), n • y = 0)
    (hI : DividedPowers I) (ha : a ∈ I) : a ^ n = 0

Proof state:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
⊢ a ^ n = 0

Tactic:
have h_fac : (n ! : A) * hI.dpow n a =
  n • ((n - 1)! : A) * hI.dpow n a := by
  rw [nsmul_eq_mul, ← cast_mul, mul_factorial_pred (Nat.pos_of_ne_zero hn)]

Result:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
h_fac : ↑n ! * hI.dpow n a = n • ↑(n - 1)! * hI.dpow n a
⊢ a ^ n = 0

Proof state:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
h_fac : ↑n ! * hI.dpow n a = n • ↑(n - 1)! * hI.dpow n a
⊢ a ^ n = 0

Tactic:
rw [← hI.factorial_mul_dpow_eq_pow ha, h_fac, smul_mul_assoc]

Result:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
h_fac : ↑n ! * hI.dpow n a = n • ↑(n - 1)! * hI.dpow n a
⊢ n • (↑(n - 1)! * hI.dpow n a) = 0

Proof state:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
⊢ ↑n ! * hI.dpow n a = n • ↑(n - 1)! * hI.dpow n a

Tactic:
rw [nsmul_eq_mul, ← cast_mul, mul_factorial_pred (Nat.pos_of_ne_zero hn)]

Result:
no goals

Proof state:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
h_fac : ↑n ! * hI.dpow n a = n • ↑(n - 1)! * hI.dpow n a
⊢ n • (↑(n - 1)! * hI.dpow n a) = 0

Tactic:
exact hnI (I.mul_mem_left ((n - 1)! : A) (hI.dpow_mem hn ha))

Result:
no goals
-- Mathlib/Algebra/Category/MonCat/Basic.lean
@[to_additive]
lemma inv_hom_apply {M N : CommMonCat} (e : M ≅ N) (x : M) : e.inv (e.hom x) = x

Proof state:
M N : CommMonCat
e : M ≅ N
x : ↑M
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem length_darts {u v : V} (p : G.Walk u v) : p.darts.length = p.length

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.darts.length = p.length

Tactic:
induction p <;> simp [*]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem IsClique.card_le_of_colorable {s : Finset V} (h : G.IsClique s) {n : ℕ}
    (hc : G.Colorable n) : s.card ≤ n

Proof state:
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
n : ℕ
hc : G.Colorable n
⊢ s.card ≤ n

Tactic:
convert h.card_le_of_coloring hc.some

Result:
case h.e'_4
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
n : ℕ
hc : G.Colorable n
⊢ n = card (Fin n)

Proof state:
case h.e'_4
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
n : ℕ
hc : G.Colorable n
⊢ n = card (Fin n)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Classes/Order.lean
theorem cmp_eq_gt [OrientedCmp cmp] : cmp x y = .gt ↔ cmp y x = .lt

Proof state:
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
x y : α✝
inst✝ : OrientedCmp cmp
⊢ cmp y x = Ordering.gt.swap ↔ cmp y x = Ordering.lt

Tactic:
exact .rfl

Result:
no goals

Proof state:
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
x y : α✝
inst✝ : OrientedCmp cmp
⊢ cmp x y = Ordering.gt ↔ cmp y x = Ordering.lt

Tactic:
rw [← Ordering.swap_inj, symm]

Result:
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
x y : α✝
inst✝ : OrientedCmp cmp
⊢ cmp y x = Ordering.gt.swap ↔ cmp y x = Ordering.lt
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem guard_pos [DecidablePred p] (h : p a) : Option.guard p a = some a

Proof state:
α✝ : Type u_1
p : α✝ → Prop
a : α✝
inst✝ : DecidablePred p
h : p a
⊢ guard p a = some a

Tactic:
simp [Option.guard, h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_preimage (e : X ≃ᵢ Y) (d : ℝ) (s : Set Y) : μH[d] (e ⁻¹' s) = μH[d] s

Proof state:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
e : X ≃ᵢ Y
d : ℝ
s : Set Y
⊢ μH[d] (⇑e ⁻¹' s) = μH[d] s

Tactic:
rw [← e.image_symm, e.symm.hausdorffMeasure_image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem take_succ {l : List α} {n : Nat} : l.take (n + 1) = l.take n ++ l[n]?.toList

Proof state:
case cons.succ
α : Type u_1
hd : α
tl : List α
hl : ∀ {n : Nat}, take (n + 1) tl = take n tl ++ tl[n]?.toList
n✝ : Nat
⊢ take (n✝ + 1 + 1) (hd :: tl) = take (n✝ + 1) (hd :: tl) ++ (hd :: tl)[n✝ + 1]?.toList

Tactic:
simp only [take, hl, getElem?_cons_succ, cons_append]

Result:
no goals

Proof state:
case nil
α : Type u_1
n : Nat
⊢ take (n + 1) [] = take n [] ++ [][n]?.toList

Tactic:
simp only [take_nil, Option.toList, getElem?_nil, append_nil]

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
hd : α
tl : List α
hl : ∀ {n : Nat}, take (n + 1) tl = take n tl ++ tl[n]?.toList
⊢ take (0 + 1) (hd :: tl) = take 0 (hd :: tl) ++ (hd :: tl)[0]?.toList

Tactic:
simp only [take, Option.toList, getElem?_cons_zero, nil_append]

Result:
no goals

Proof state:
case cons
α : Type u_1
hd : α
tl : List α
hl : ∀ {n : Nat}, take (n + 1) tl = take n tl ++ tl[n]?.toList
n : Nat
⊢ take (n + 1) (hd :: tl) = take n (hd :: tl) ++ (hd :: tl)[n]?.toList

Tactic:
cases n

Result:
case cons.zero
α : Type u_1
hd : α
tl : List α
hl : ∀ {n : Nat}, take (n + 1) tl = take n tl ++ tl[n]?.toList
⊢ take (0 + 1) (hd :: tl) = take 0 (hd :: tl) ++ (hd :: tl)[0]?.toList

case cons.succ
α : Type u_1
hd : α
tl : List α
hl : ∀ {n : Nat}, take (n + 1) tl = take n tl ++ tl[n]?.toList
n✝ : Nat
⊢ take (n✝ + 1 + 1) (hd :: tl) = take (n✝ + 1) (hd :: tl) ++ (hd :: tl)[n✝ + 1]?.toList
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem toList_mapIdxM [Monad m] [LawfulMonad m] (l : Array α)
    (f : Nat → α → m β) :
    toList <$> l.mapIdxM f = l.toList.mapIdxM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
f : Nat → α → m β
⊢ toList <$> mapIdxM f l = List.mapIdxM f l.toList

Tactic:
rw [List.mapIdxM_toArray]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
f : Nat → α → m β
⊢ toList <$> List.toArray <$> List.mapIdxM f l.toList = List.mapIdxM f l.toList

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
f : Nat → α → m β
⊢ toList <$> List.toArray <$> List.mapIdxM f l.toList = List.mapIdxM f l.toList

Tactic:
simp only [Functor.map_map, id_map']

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
lemma getElem_rightInvSeq (ω : List B) (j : ℕ) (h : j < ω.length) :
    (ris ω)[j]'(by simp[h]) =
    (π (ω.drop (j + 1)))⁻¹
      * (Option.map (cs.simple) ω[j]?).getD 1
      * π (ω.drop (j + 1))

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
h : j < ω.length
⊢ j < (cs.rightInvSeq ω).length

Tactic:
simp[h]

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
h : j < ω.length
⊢ (cs.rightInvSeq ω)[j] =
    (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)

Tactic:
rw [← List.getD_eq_getElem (ris ω) 1, getD_rightInvSeq]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem nhds_comap_dist (a : α) : ((𝓝 (0 : ℝ)).comap (dist · a)) = 𝓝 a

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
a : α
⊢ comap (fun x => dist x a) (𝓝 0) = 𝓝 a

Tactic:
simp only [@nhds_eq_comap_uniformity α, Metric.uniformity_eq_comap_nhds_zero, comap_comap,
  Function.comp_def, dist_comm]

Result:
no goals
-- Mathlib/NumberTheory/ZetaValues.lean
theorem bernoulliFourierCoeff_zero {k : ℕ} (hk : k ≠ 0) : bernoulliFourierCoeff k 0 = 0

Proof state:
k : ℕ
hk : k ≠ 0
⊢ bernoulliFourierCoeff k 0 = 0

Tactic:
simp_rw [bernoulliFourierCoeff, fourierCoeffOn_eq_integral, neg_zero, fourier_zero, sub_zero,
  div_one, one_smul, intervalIntegral.integral_ofReal, integral_bernoulliFun_eq_zero hk,
  ofReal_zero]

Result:
no goals
-- Mathlib/Algebra/Ring/Commute.lean
@[simp] lemma mul_neg_one_pow_eq_zero_iff : a * (-1) ^ n = 0 ↔ a = 0

Proof state:
R : Type u
inst✝ : Ring R
a : R
n : ℕ
⊢ a * (-1) ^ n = 0 ↔ a = 0

Tactic:
obtain h | h := neg_one_pow_eq_or R n <;> simp [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem arctan_one : arctan 1 = π / 4 :=
  arctan_eq_of_tan_eq tan_pi_div_four <| by constructor <;> linarith [pi_pos]

Proof state:
⊢ π / 4 ∈ Ioo (-(π / 2)) (π / 2)

Tactic:
constructor <;> linarith [pi_pos]

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean
/-- Given a diagram
```
a --φ--> b        b'
|        |        |
v        v        v
R --f--> S --g--> S'
```
such that `φ` is strongly cocartesian, and morphisms `ψ ψ' : b ⟶ b'` such that
`g ≫ ψ = φ' = g ≫ ψ'`. Then we have that `ψ = ψ'`. -/
protected lemma ext (φ : a ⟶ b) [IsStronglyCocartesian p f φ] {S' : 𝒮} {b' : 𝒳} (g : S ⟶ S')
    {ψ ψ' : b ⟶ b'} [IsHomLift p g ψ] [IsHomLift p g ψ'] (h : φ ≫ ψ = φ ≫ ψ') : ψ = ψ'

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCocartesian f φ
S' : 𝒮
b' : 𝒳
g : S ⟶ S'
ψ ψ' : b ⟶ b'
inst✝¹ : p.IsHomLift g ψ
inst✝ : p.IsHomLift g ψ'
h : φ ≫ ψ = φ ≫ ψ'
⊢ ψ = ψ'

Tactic:
rw [map_uniq p f φ (g := g) rfl (φ ≫ ψ) ψ rfl, map_uniq p f φ (g := g) rfl (φ ≫ ψ) ψ' h.symm]

Result:
no goals
-- Mathlib/Data/Nat/Sqrt.lean
lemma eq_sqrt' : a = sqrt n ↔ a ^ 2 ≤ n ∧ n < (a + 1) ^ 2

Proof state:
n a : ℕ
⊢ a = n.sqrt ↔ a ^ 2 ≤ n ∧ n < (a + 1) ^ 2

Tactic:
simpa only [Nat.pow_two] using eq_sqrt

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
    a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
⊢ a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m

Tactic:
simp [mem_iff_contains, contains_erase]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
/-- The iterated derivative commutes with subtracting a constant. -/
lemma iteratedFDeriv_comp_sub (n : ℕ) (a : E) (x : E) :
    iteratedFDeriv 𝕜 n (fun z ↦ f (z - a)) x = iteratedFDeriv 𝕜 n f (x - a)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
a x : E
⊢ iteratedFDeriv 𝕜 n (fun z => f (z - a)) x = iteratedFDeriv 𝕜 n f (x - a)

Tactic:
simp [iteratedFDeriv_comp_sub']

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
lemma opcyclesMap_comm [S₁.HasRightHomology] [S₂.HasRightHomology] :
    opcyclesMap φ ≫ h₂.opcyclesIso.hom = h₁.opcyclesIso.hom ≫ γ.φQ

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ opcyclesMap φ ≫ h₂.opcyclesIso.hom = h₁.opcyclesIso.hom ≫ γ.φQ

Tactic:
simp only [γ.opcyclesMap_eq, assoc, Iso.inv_hom_id, comp_id]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cmp_swap (m) : ∀ n, (cmp m n).swap = cmp n m

Proof state:
case bit0.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ Ordering.gt.swap = Ordering.lt

Tactic:
rfl

Result:
no goals

Proof state:
m : PosNum
⊢ ∀ (n : PosNum), (m.cmp n).swap = n.cmp m

Tactic:
induction' m with m IH m IH <;> intro n <;> obtain - | n | n := n <;> unfold cmp <;>
  try { rfl } <;> rw [← IH] <;> cases cmp m n <;> rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.lean
theorem lintegral_enorm_le_of_forall_fin_meas_integral_eq (hm : m ≤ m0) {f g : α → ℝ}
    (hf : StronglyMeasurable f) (hfi : IntegrableOn f s μ) (hg : StronglyMeasurable[m] g)
    (hgi : IntegrableOn g s μ)
    (hgf : ∀ t, MeasurableSet[m] t → μ t < ∞ → ∫ x in t, g x ∂μ = ∫ x in t, f x ∂μ)
    (hs : MeasurableSet[m] s) (hμs : μ s ≠ ∞) : (∫⁻ x in s, ‖g x‖ₑ ∂μ) ≤ ∫⁻ x in s, ‖f x‖ₑ ∂μ

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∫ (x : α) in s, ‖g x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ

Tactic:
exact integral_norm_le_of_forall_fin_meas_integral_eq hm hf hfi hg hgi hgf hs hμs

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∫⁻ (x : α) in s, ‖g x‖ₑ ∂μ ≤ ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ

Tactic:
rw [← ofReal_integral_norm_eq_lintegral_enorm hfi, ←
  ofReal_integral_norm_eq_lintegral_enorm hgi, ENNReal.ofReal_le_ofReal_iff]

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∫ (x : α) in s, ‖g x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ

α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ 0 ≤ ∫ (x : α) in s, ‖f x‖ ∂μ

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ 0 ≤ ∫ (x : α) in s, ‖f x‖ ∂μ

Tactic:
positivity

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem interedges_empty_left (t : Finset β) : interedges r ∅ t = ∅

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
t : Finset β
⊢ interedges r ∅ t = ∅

Tactic:
rw [interedges, Finset.empty_product, filter_empty]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem composition_card (n : ℕ) : Fintype.card (Composition n) = 2 ^ (n - 1)

Proof state:
n : ℕ
⊢ Fintype.card (Composition n) = 2 ^ (n - 1)

Tactic:
rw [← compositionAsSet_card n]

Result:
n : ℕ
⊢ Fintype.card (Composition n) = Fintype.card (CompositionAsSet n)

Proof state:
n : ℕ
⊢ Fintype.card (Composition n) = Fintype.card (CompositionAsSet n)

Tactic:
exact Fintype.card_congr (compositionEquiv n)

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_mul_const_atTop_iff_neg [NeBot l] (h : Tendsto f l atBot) :
    Tendsto (fun x => f x * r) l atTop ↔ r < 0

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atBot
⊢ Tendsto (fun x => f x * r) l atTop ↔ r < 0

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atTop_iff_neg h]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem tail_append_singleton_of_ne_nil {a : α} {l : List α} (h : l ≠ nil) :
    tail (l ++ [a]) = tail l ++ [a]

Proof state:
case cons
α : Type u
a head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → (tail✝ ++ [a]).tail = tail✝.tail ++ [a]
h : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝ ++ [a]).tail = (head✝ :: tail✝).tail ++ [a]

Tactic:
rw [tail, cons_append, tail]

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
h : l ≠ []
⊢ (l ++ [a]).tail = l.tail ++ [a]

Tactic:
induction l

Result:
case nil
α : Type u
a : α
h : [] ≠ []
⊢ ([] ++ [a]).tail = [].tail ++ [a]

case cons
α : Type u
a head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → (tail✝ ++ [a]).tail = tail✝.tail ++ [a]
h : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝ ++ [a]).tail = (head✝ :: tail✝).tail ++ [a]

Proof state:
case nil
α : Type u
a : α
h : [] ≠ []
⊢ ([] ++ [a]).tail = [].tail ++ [a]

Tactic:
contradiction

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_mul_X_of_ne {i j : σ} (f : MvPolynomial σ R) (h : i ≠ j) :
    degreeOf i (f * X j) = degreeOf i f

Proof state:
case e_f
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (fun m => m i) ∘ ⇑(addRightEmbedding (Finsupp.single j 1)) = fun m => m i

Tactic:
ext

Result:
case e_f.h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
x✝ : σ →₀ ℕ
⊢ ((fun m => m i) ∘ ⇑(addRightEmbedding (Finsupp.single j 1))) x✝ = x✝ i

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ degreeOf i (f * X j) = degreeOf i f

Tactic:
simp only [degreeOf_eq_sup i, support_mul_X, Finset.sup_map]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ f.support.sup ((fun m => m i) ∘ ⇑(addRightEmbedding (Finsupp.single j 1))) = f.support.sup fun m => m i

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ f.support.sup ((fun m => m i) ∘ ⇑(addRightEmbedding (Finsupp.single j 1))) = f.support.sup fun m => m i

Tactic:
congr

Result:
case e_f
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (fun m => m i) ∘ ⇑(addRightEmbedding (Finsupp.single j 1)) = fun m => m i

Proof state:
case e_f.h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
x✝ : σ →₀ ℕ
⊢ ((fun m => m i) ∘ ⇑(addRightEmbedding (Finsupp.single j 1))) x✝ = x✝ i

Tactic:
simp only [Finsupp.single, add_right_eq_self, addRightEmbedding_apply, coe_mk,
  Pi.add_apply, comp_apply, ite_eq_right_iff, Finsupp.coe_add, Pi.single_eq_of_ne h]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ degreeOf i (f * X j) = degreeOf i f

Tactic:
classical
simp only [degreeOf_eq_sup i, support_mul_X, Finset.sup_map]
congr
ext
simp only [Finsupp.single, add_right_eq_self, addRightEmbedding_apply, coe_mk,
  Pi.add_apply, comp_apply, ite_eq_right_iff, Finsupp.coe_add, Pi.single_eq_of_ne h]

Result:
no goals